{-# OPTIONS --safe --cubical #-}

module OWL2.Portable.RegularityProof where

open import OWL2.Prelude
open import Cubical.Data.Nat.Base using (zero; suc)
import OWL2.Data.String as String
import OWL2.Portable.ObjectPropertyKeys as Keys
import OWL2.Portable.Regularity as PR
import OWL2.Portable.Semantics as Sem
import OWL2.Portable.Syntax as P
import OWL2.Syntax as S
import OWL2.Syntax.Regularity as Reg

private
  BoolIsTrue : Bool → Type₀
  BoolIsTrue true =
    Unit*
  BoolIsTrue false =
    ⊥

  falseNotTrue : false ≡ true → ⊥
  falseNotTrue equality =
    subst BoolIsTrue (sym equality) tt*

  absurd : ∀ {ℓ} {A : Type ℓ} → ⊥ → A
  absurd ()

portableCanonicalObjectPropertyExpression :
  (property : P.ObjectPropertyExpression) →
  PR.canonicalForSimplePropertyUse property ≡ true →
  Reg.CanonicalObjectPropertyExpression
    (Sem.translateObjectPropertyExpression property)
portableCanonicalObjectPropertyExpression (P.objectProperty p) canonical =
  Reg.canonicalObjectProperty
portableCanonicalObjectPropertyExpression P.topObjectProperty canonical =
  Reg.canonicalTopObjectProperty
portableCanonicalObjectPropertyExpression P.bottomObjectProperty canonical =
  Reg.canonicalBottomObjectProperty
portableCanonicalObjectPropertyExpression
  (P.objectInverseOf (P.objectProperty p))
  canonical =
  Reg.canonicalObjectInverseOf
portableCanonicalObjectPropertyExpression
  (P.objectInverseOf P.topObjectProperty)
  canonical =
  absurd (falseNotTrue canonical)
portableCanonicalObjectPropertyExpression
  (P.objectInverseOf P.bottomObjectProperty)
  canonical =
  absurd (falseNotTrue canonical)
portableCanonicalObjectPropertyExpression
  (P.objectInverseOf (P.objectInverseOf property))
  canonical =
  absurd (falseNotTrue canonical)

portableSimpleObjectPropertyExpression :
  (context : Reg.RegularityContext Sem.PortableSignature) →
  (property : P.ObjectPropertyExpression) →
  PR.canonicalForSimplePropertyUse property ≡ true →
  (∀ q →
    Reg.PropertyHierarchyPath
      context
      q
      (Sem.translateObjectPropertyExpression property) →
    ¬ Reg.Composite context q) →
  Reg.SimpleObjectPropertyExpression
    context
    (Sem.translateObjectPropertyExpression property)
portableSimpleObjectPropertyExpression
  context
  property
  canonical
  noCompositePredecessor =
  portableCanonicalObjectPropertyExpression property canonical ,
  noCompositePredecessor

record PortableSimpleObjectPropertyExpressionCertificate
  (context : Reg.RegularityContext Sem.PortableSignature)
  (property : P.ObjectPropertyExpression)
  : Type₀ where
  constructor portableSimpleObjectPropertyExpressionCertificate
  field
    portablePropertyCanonical :
      PR.canonicalForSimplePropertyUse property ≡ true
    portablePropertyNoCompositePredecessor :
      ∀ q →
      Reg.PropertyHierarchyPath
        context
        q
        (Sem.translateObjectPropertyExpression property) →
      ¬ Reg.Composite context q

open PortableSimpleObjectPropertyExpressionCertificate public

portableSimpleObjectPropertyExpressionCertificateToSyntax :
  ∀ {context property} →
  PortableSimpleObjectPropertyExpressionCertificate context property →
  Reg.SimpleObjectPropertyExpression
    context
    (Sem.translateObjectPropertyExpression property)
portableSimpleObjectPropertyExpressionCertificateToSyntax
  {context}
  {property}
  certificate =
  portableSimpleObjectPropertyExpression
    context
    property
    (portablePropertyCanonical certificate)
    (portablePropertyNoCompositePredecessor certificate)

record PortableSimplePropertyUseCertificate
  (context : Reg.RegularityContext Sem.PortableSignature)
  (use : PR.SimplePropertyUse)
  : Type₀ where
  constructor portableSimplePropertyUseCertificate
  field
    portableUseCanonical :
      PR.canonicalForSimplePropertyUse
        (PR.simplePropertyUseProperty use)
      ≡
      true
    portableUseNoCompositePredecessor :
      ∀ q →
      Reg.PropertyHierarchyPath
        context
        q
        (Sem.translateObjectPropertyExpression
          (PR.simplePropertyUseProperty use)) →
      ¬ Reg.Composite context q

open PortableSimplePropertyUseCertificate public

portableSimplePropertyUseCertificateToSyntax :
  ∀ {context use} →
  PortableSimplePropertyUseCertificate context use →
  Reg.SimpleObjectPropertyExpression
    context
    (Sem.translateObjectPropertyExpression
      (PR.simplePropertyUseProperty use))
portableSimplePropertyUseCertificateToSyntax {context} {use} certificate =
  portableSimpleObjectPropertyExpression
    context
    (PR.simplePropertyUseProperty use)
    (portableUseCanonical certificate)
    (portableUseNoCompositePredecessor certificate)

SimplePropertyUseNoCompositePredecessor :
  Reg.RegularityContext Sem.PortableSignature →
  PR.SimplePropertyUse →
  Type₀
SimplePropertyUseNoCompositePredecessor context use =
  ∀ q →
  Reg.PropertyHierarchyPath
    context
    q
    (Sem.translateObjectPropertyExpression
      (PR.simplePropertyUseProperty use)) →
  ¬ Reg.Composite context q

record PortableCompositeObjectPropertyEvidence
  (compositeFacts : List PR.CompositeObjectPropertyFact)
  (property : S.ObjectPropertyExpression Sem.PortableSignature)
  : Type₀ where
  constructor portableCompositeObjectPropertyEvidence
  field
    portableCompositeFact :
      PR.CompositeObjectPropertyFact
    portableCompositeFactMember :
      Reg.Member portableCompositeFact compositeFacts
    portableCompositeFactMatches :
      Sem.translateObjectPropertyExpression
        (PR.compositeObjectPropertyExpression portableCompositeFact)
      ≡
      property

open PortableCompositeObjectPropertyEvidence public

record PortablePropertyHierarchyStepEvidence
  (hierarchyFacts : List PR.PropertyHierarchyFact)
  (sub super : S.ObjectPropertyExpression Sem.PortableSignature)
  : Type₀ where
  constructor portablePropertyHierarchyStepEvidence
  field
    portableHierarchyFact :
      PR.PropertyHierarchyFact
    portableHierarchyFactMember :
      Reg.Member portableHierarchyFact hierarchyFacts
    portableHierarchySubPropertyMatches :
      Sem.translateObjectPropertyExpression
        (PR.propertyHierarchySubProperty portableHierarchyFact)
      ≡
      sub
    portableHierarchySuperPropertyMatches :
      Sem.translateObjectPropertyExpression
        (PR.propertyHierarchySuperProperty portableHierarchyFact)
      ≡
      super

open PortablePropertyHierarchyStepEvidence public

SimplePropertyUseKeyCoherent :
  PR.SimplePropertyUse → Type₀
SimplePropertyUseKeyCoherent use =
  PR.simplePropertyUseKey use
  ≡
  PR.objectPropertyBaseKey (PR.simplePropertyUseProperty use)

CompositeObjectPropertyFactKeyCoherent :
  PR.CompositeObjectPropertyFact → Type₀
CompositeObjectPropertyFactKeyCoherent fact =
  PR.compositeObjectPropertyKey fact
  ≡
  PR.objectPropertyBaseKey (PR.compositeObjectPropertyExpression fact)

CompositeObjectPropertyFactKeyCoherentResolver :
  List PR.CompositeObjectPropertyFact → Type₀
CompositeObjectPropertyFactKeyCoherentResolver facts =
  (fact : PR.CompositeObjectPropertyFact) →
  Reg.Member fact facts →
  CompositeObjectPropertyFactKeyCoherent fact

PropertyHierarchyFactKeyCoherent :
  PR.PropertyHierarchyFact → Type₀
PropertyHierarchyFactKeyCoherent fact =
  ( PR.propertyHierarchySubPropertyKey fact
    ≡
    PR.objectPropertyBaseKey (PR.propertyHierarchySubProperty fact)
  )
  ×
  ( PR.propertyHierarchySuperPropertyKey fact
    ≡
    PR.objectPropertyBaseKey (PR.propertyHierarchySuperProperty fact)
  )

PropertyHierarchyFactKeyCoherentResolver :
  List PR.PropertyHierarchyFact → Type₀
PropertyHierarchyFactKeyCoherentResolver facts =
  (fact : PR.PropertyHierarchyFact) →
  Reg.Member fact facts →
  PropertyHierarchyFactKeyCoherent fact

simplePropertyUseKeyCoherentFor :
  (source : P.Annotated P.Axiom) →
  (kind : PR.SimplePropertyUseKind) →
  (property : P.ObjectPropertyExpression) →
  SimplePropertyUseKeyCoherent
    (PR.simplePropertyUse
      source
      kind
      property
      (PR.objectPropertyBaseKey property))
simplePropertyUseKeyCoherentFor source kind property =
  refl

compositeObjectPropertyFactKeyCoherentFor :
  (property : P.ObjectPropertyExpression) →
  (kind : PR.CompositeObjectPropertyKind) →
  (source : Optional (P.Annotated P.Axiom)) →
  CompositeObjectPropertyFactKeyCoherent
    (PR.compositeObjectPropertyFact
      (PR.objectPropertyBaseKey property)
      property
      kind
      source)
compositeObjectPropertyFactKeyCoherentFor property kind source =
  refl

propertyHierarchyFactKeyCoherentFor :
  (source : P.Annotated P.Axiom) →
  (kind : PR.PropertyHierarchyFactKind) →
  (sub super : P.ObjectPropertyExpression) →
  PropertyHierarchyFactKeyCoherent
    (PR.propertyHierarchyFactFor source kind sub super)
propertyHierarchyFactKeyCoherentFor source kind sub super =
  refl , refl

memberAppendElim :
  ∀ {ℓA ℓR} {A : Type ℓA} {x : A} →
  (left right : List A) →
  {R : Type ℓR} →
  Reg.Member x (left ++ right) →
  (Reg.Member x left → R) →
  (Reg.Member x right → R) →
  R
memberAppendElim [] right member leftCase rightCase =
  rightCase member
memberAppendElim (head ∷ left) right Reg.here leftCase rightCase =
  leftCase Reg.here
memberAppendElim (head ∷ left) right (Reg.there member) leftCase rightCase =
  memberAppendElim
    left
    right
    member
    (λ leftMember → leftCase (Reg.there leftMember))
    rightCase

compositeFactsForAnnotatedAxiomKeyCoherent :
  (source : P.Annotated P.Axiom) →
  (fact : PR.CompositeObjectPropertyFact) →
  Reg.Member fact (PR.compositeFactsForAnnotatedAxiom source) →
  CompositeObjectPropertyFactKeyCoherent fact
compositeFactsForAnnotatedAxiomKeyCoherent source fact member
  with P.body source | member
... | P.subObjectPropertyOf (P.subObjectProperty property) super | ()
... | P.subObjectPropertyOf (P.subObjectPropertyChain chain) super | Reg.here =
  compositeObjectPropertyFactKeyCoherentFor
    super
    PR.propertyChainSuperPropertyComposite
    (present source)
... | P.subObjectPropertyOf (P.subObjectPropertyChain chain) super | Reg.there ()
... | P.transitiveObjectProperty property | Reg.here =
  compositeObjectPropertyFactKeyCoherentFor
    property
    PR.transitiveObjectPropertyComposite
    (present source)
... | P.transitiveObjectProperty property | Reg.there ()
... | P.declaration entity | ()
... | P.subClassOf left right | ()
... | P.equivalentClasses classes | ()
... | P.disjointClasses classes | ()
... | P.disjointUnion class classes | ()
... | P.objectPropertyDomain property class | ()
... | P.objectPropertyRange property class | ()
... | P.functionalObjectProperty property | ()
... | P.inverseFunctionalObjectProperty property | ()
... | P.reflexiveObjectProperty property | ()
... | P.irreflexiveObjectProperty property | ()
... | P.symmetricObjectProperty property | ()
... | P.asymmetricObjectProperty property | ()
... | P.subDataPropertyOf left right | ()
... | P.equivalentDataProperties properties | ()
... | P.disjointDataProperties properties | ()
... | P.dataPropertyDomain property class | ()
... | P.dataPropertyRange property range | ()
... | P.functionalDataProperty property | ()
... | P.datatypeDefinition datatype range | ()
... | P.hasKey class key | ()
... | P.sameIndividual individuals | ()
... | P.differentIndividuals individuals | ()
... | P.classAssertion class individual | ()
... | P.objectPropertyAssertion property subject object | ()
... | P.negativeObjectPropertyAssertion property subject object | ()
... | P.dataPropertyAssertion property subject literal | ()
... | P.negativeDataPropertyAssertion property subject literal | ()
... | P.annotationAssertion property subject value | ()
... | P.subAnnotationPropertyOf sub super | ()
... | P.annotationPropertyDomain property targetIRI | ()
... | P.annotationPropertyRange property targetIRI | ()

compositeFactsForAnnotatedAxiomsKeyCoherent :
  (axioms : List (P.Annotated P.Axiom)) →
  CompositeObjectPropertyFactKeyCoherentResolver
    (PR.compositeFactsForAnnotatedAxioms axioms)
compositeFactsForAnnotatedAxiomsKeyCoherent [] fact ()
compositeFactsForAnnotatedAxiomsKeyCoherent (ax ∷ axioms) fact member =
  memberAppendElim
    (PR.compositeFactsForAnnotatedAxiom ax)
    (PR.compositeFactsForAnnotatedAxioms axioms)
    member
    (compositeFactsForAnnotatedAxiomKeyCoherent ax fact)
    (compositeFactsForAnnotatedAxiomsKeyCoherent axioms fact)

ontologyCompositeObjectPropertyFactsKeyCoherent :
  (ont : P.Ontology) →
  CompositeObjectPropertyFactKeyCoherentResolver
    (PR.ontologyCompositeObjectPropertyFacts ont)
ontologyCompositeObjectPropertyFactsKeyCoherent ont fact Reg.here =
  compositeObjectPropertyFactKeyCoherentFor
    P.topObjectProperty
    PR.topObjectPropertyComposite
    absent
ontologyCompositeObjectPropertyFactsKeyCoherent ont fact (Reg.there Reg.here) =
  compositeObjectPropertyFactKeyCoherentFor
    P.bottomObjectProperty
    PR.bottomObjectPropertyComposite
    absent
ontologyCompositeObjectPropertyFactsKeyCoherent
  ont
  fact
  (Reg.there (Reg.there member)) =
  compositeFactsForAnnotatedAxiomsKeyCoherent
    (P.axioms ont)
    fact
    member

ontologyDocumentCompositeObjectPropertyFactsKeyCoherent :
  (document : P.OntologyDocument) →
  CompositeObjectPropertyFactKeyCoherentResolver
    (PR.ontologyDocumentCompositeObjectPropertyFacts document)
ontologyDocumentCompositeObjectPropertyFactsKeyCoherent document =
  ontologyCompositeObjectPropertyFactsKeyCoherent (P.documentOntology document)

propertyHierarchyFactsFromPropertyToPropertiesKeyCoherent :
  (source : P.Annotated P.Axiom) →
  (kind : PR.PropertyHierarchyFactKind) →
  (property : P.ObjectPropertyExpression) →
  (targets : List P.ObjectPropertyExpression) →
  (fact : PR.PropertyHierarchyFact) →
  Reg.Member
    fact
    (PR.propertyHierarchyFactsFromPropertyToProperties
      source
      kind
      property
      targets) →
  PropertyHierarchyFactKeyCoherent fact
propertyHierarchyFactsFromPropertyToPropertiesKeyCoherent
  source
  kind
  property
  []
  fact
  ()
propertyHierarchyFactsFromPropertyToPropertiesKeyCoherent
  source
  kind
  property
  (target ∷ targets)
  fact
  Reg.here =
  propertyHierarchyFactKeyCoherentFor source kind property target
propertyHierarchyFactsFromPropertyToPropertiesKeyCoherent
  source
  kind
  property
  (target ∷ targets)
  fact
  (Reg.there member) =
  propertyHierarchyFactsFromPropertyToPropertiesKeyCoherent
    source
    kind
    property
    targets
    fact
    member

propertyHierarchyFactsForEquivalentPropertyListFromKeyCoherent :
  (source : P.Annotated P.Axiom) →
  (allProperties properties : List P.ObjectPropertyExpression) →
  (fact : PR.PropertyHierarchyFact) →
  Reg.Member
    fact
    (PR.propertyHierarchyFactsForEquivalentPropertyListFrom
      source
      allProperties
      properties) →
  PropertyHierarchyFactKeyCoherent fact
propertyHierarchyFactsForEquivalentPropertyListFromKeyCoherent
  source
  allProperties
  []
  fact
  ()
propertyHierarchyFactsForEquivalentPropertyListFromKeyCoherent
  source
  allProperties
  (property ∷ properties)
  fact
  member =
  memberAppendElim
    (PR.propertyHierarchyFactsFromPropertyToProperties
      source
      PR.equivalentObjectPropertiesHierarchy
      property
      allProperties)
    (PR.propertyHierarchyFactsForEquivalentPropertyListFrom
      source
      allProperties
      properties)
    member
    (propertyHierarchyFactsFromPropertyToPropertiesKeyCoherent
      source
      PR.equivalentObjectPropertiesHierarchy
      property
      allProperties
      fact)
    (propertyHierarchyFactsForEquivalentPropertyListFromKeyCoherent
      source
      allProperties
      properties
      fact)

propertyHierarchyFactsForEquivalentPropertiesKeyCoherent :
  (source : P.Annotated P.Axiom) →
  (properties : P.TwoOrMore P.ObjectPropertyExpression) →
  (fact : PR.PropertyHierarchyFact) →
  Reg.Member
    fact
    (PR.propertyHierarchyFactsForEquivalentProperties source properties) →
  PropertyHierarchyFactKeyCoherent fact
propertyHierarchyFactsForEquivalentPropertiesKeyCoherent
  source
  properties
  fact
  member =
  propertyHierarchyFactsForEquivalentPropertyListFromKeyCoherent
    source
    (Sem.twoOrMoreToList properties)
    (Sem.twoOrMoreToList properties)
    fact
    member

propertyHierarchyFactsForAnnotatedAxiomKeyCoherent :
  (source : P.Annotated P.Axiom) →
  (fact : PR.PropertyHierarchyFact) →
  Reg.Member fact (PR.propertyHierarchyFactsForAnnotatedAxiom source) →
  PropertyHierarchyFactKeyCoherent fact
propertyHierarchyFactsForAnnotatedAxiomKeyCoherent source fact member
  with P.body source | member
... | P.subObjectPropertyOf (P.subObjectProperty sub) super | Reg.here =
  propertyHierarchyFactKeyCoherentFor
    source
    PR.subObjectPropertyHierarchy
    sub
    super
... | P.subObjectPropertyOf (P.subObjectProperty sub) super | Reg.there ()
... | P.subObjectPropertyOf (P.subObjectPropertyChain chain) super | ()
... | P.equivalentObjectProperties properties | member =
  propertyHierarchyFactsForEquivalentPropertiesKeyCoherent
    source
    properties
    fact
    member
... | P.inverseObjectProperties left right | Reg.here =
  propertyHierarchyFactKeyCoherentFor
    source
    PR.inverseObjectPropertiesHierarchy
    left
    (P.objectInverseOf right)
... | P.inverseObjectProperties left right | Reg.there Reg.here =
  propertyHierarchyFactKeyCoherentFor
    source
    PR.inverseObjectPropertiesHierarchy
    (P.objectInverseOf right)
    left
... | P.inverseObjectProperties left right | Reg.there (Reg.there ())
... | P.declaration entity | ()
... | P.subClassOf left right | ()
... | P.equivalentClasses classes | ()
... | P.disjointClasses classes | ()
... | P.disjointUnion class classes | ()
... | P.objectPropertyDomain property class | ()
... | P.objectPropertyRange property class | ()
... | P.functionalObjectProperty property | ()
... | P.inverseFunctionalObjectProperty property | ()
... | P.reflexiveObjectProperty property | ()
... | P.irreflexiveObjectProperty property | ()
... | P.symmetricObjectProperty property | ()
... | P.asymmetricObjectProperty property | ()
... | P.transitiveObjectProperty property | ()
... | P.subDataPropertyOf left right | ()
... | P.equivalentDataProperties properties | ()
... | P.disjointDataProperties properties | ()
... | P.dataPropertyDomain property class | ()
... | P.dataPropertyRange property range | ()
... | P.functionalDataProperty property | ()
... | P.datatypeDefinition datatype range | ()
... | P.hasKey class key | ()
... | P.sameIndividual individuals | ()
... | P.differentIndividuals individuals | ()
... | P.classAssertion class individual | ()
... | P.objectPropertyAssertion property subject object | ()
... | P.negativeObjectPropertyAssertion property subject object | ()
... | P.dataPropertyAssertion property subject literal | ()
... | P.negativeDataPropertyAssertion property subject literal | ()
... | P.annotationAssertion property subject value | ()
... | P.subAnnotationPropertyOf sub super | ()
... | P.annotationPropertyDomain property targetIRI | ()
... | P.annotationPropertyRange property targetIRI | ()

propertyHierarchyFactsForAnnotatedAxiomsKeyCoherent :
  (axioms : List (P.Annotated P.Axiom)) →
  PropertyHierarchyFactKeyCoherentResolver
    (PR.propertyHierarchyFactsForAnnotatedAxioms axioms)
propertyHierarchyFactsForAnnotatedAxiomsKeyCoherent [] fact ()
propertyHierarchyFactsForAnnotatedAxiomsKeyCoherent (ax ∷ axioms) fact member =
  memberAppendElim
    (PR.propertyHierarchyFactsForAnnotatedAxiom ax)
    (PR.propertyHierarchyFactsForAnnotatedAxioms axioms)
    member
    (propertyHierarchyFactsForAnnotatedAxiomKeyCoherent ax fact)
    (propertyHierarchyFactsForAnnotatedAxiomsKeyCoherent axioms fact)

ontologyPropertyHierarchyFactsKeyCoherent :
  (ont : P.Ontology) →
  PropertyHierarchyFactKeyCoherentResolver
    (PR.ontologyPropertyHierarchyFacts ont)
ontologyPropertyHierarchyFactsKeyCoherent ont =
  propertyHierarchyFactsForAnnotatedAxiomsKeyCoherent (P.axioms ont)

ontologyDocumentPropertyHierarchyFactsKeyCoherent :
  (document : P.OntologyDocument) →
  PropertyHierarchyFactKeyCoherentResolver
    (PR.ontologyDocumentPropertyHierarchyFacts document)
ontologyDocumentPropertyHierarchyFactsKeyCoherent document =
  ontologyPropertyHierarchyFactsKeyCoherent (P.documentOntology document)

portableCompositeEvidenceSyntaxKey :
  ∀ {compositeFacts property} →
  (evidence :
    PortableCompositeObjectPropertyEvidence compositeFacts property) →
  CompositeObjectPropertyFactKeyCoherent
    (portableCompositeFact evidence) →
  Keys.syntaxObjectPropertyBaseKey property
  ≡
  PR.compositeObjectPropertyKey (portableCompositeFact evidence)
portableCompositeEvidenceSyntaxKey evidence coherent =
  cong
    Keys.syntaxObjectPropertyBaseKey
    (sym (portableCompositeFactMatches evidence))
  ∙
  Keys.syntaxObjectPropertyBaseKeyTranslate
    (PR.compositeObjectPropertyExpression
      (portableCompositeFact evidence))
  ∙
  sym coherent

simplePropertyUseSyntaxKey :
  (use : PR.SimplePropertyUse) →
  SimplePropertyUseKeyCoherent use →
  Keys.syntaxObjectPropertyBaseKey
    (Sem.translateObjectPropertyExpression
      (PR.simplePropertyUseProperty use))
  ≡
  PR.simplePropertyUseKey use
simplePropertyUseSyntaxKey use coherent =
  Keys.syntaxObjectPropertyBaseKeyTranslate
    (PR.simplePropertyUseProperty use)
  ∙
  sym coherent

portableHierarchyStepEvidenceSubSyntaxKey :
  ∀ {hierarchyFacts sub super} →
  (evidence :
    PortablePropertyHierarchyStepEvidence hierarchyFacts sub super) →
  PropertyHierarchyFactKeyCoherent
    (portableHierarchyFact evidence) →
  Keys.syntaxObjectPropertyBaseKey sub
  ≡
  PR.propertyHierarchySubPropertyKey (portableHierarchyFact evidence)
portableHierarchyStepEvidenceSubSyntaxKey evidence coherent =
  cong
    Keys.syntaxObjectPropertyBaseKey
    (sym (portableHierarchySubPropertyMatches evidence))
  ∙
  Keys.syntaxObjectPropertyBaseKeyTranslate
    (PR.propertyHierarchySubProperty
      (portableHierarchyFact evidence))
  ∙
  sym (fst coherent)

portableHierarchyStepEvidenceSuperSyntaxKey :
  ∀ {hierarchyFacts sub super} →
  (evidence :
    PortablePropertyHierarchyStepEvidence hierarchyFacts sub super) →
  PropertyHierarchyFactKeyCoherent
    (portableHierarchyFact evidence) →
  Keys.syntaxObjectPropertyBaseKey super
  ≡
  PR.propertyHierarchySuperPropertyKey (portableHierarchyFact evidence)
portableHierarchyStepEvidenceSuperSyntaxKey evidence coherent =
  cong
    Keys.syntaxObjectPropertyBaseKey
    (sym (portableHierarchySuperPropertyMatches evidence))
  ∙
  Keys.syntaxObjectPropertyBaseKeyTranslate
    (PR.propertyHierarchySuperProperty
      (portableHierarchyFact evidence))
  ∙
  sym (snd coherent)

data PropertyKeyPath
  (facts : List PR.PropertyHierarchyFact)
  : String → String → Type₀ where
  propertyKeyPathRefl :
    ∀ {key} →
    PropertyKeyPath facts key key
  propertyKeyPathStep :
    ∀ {start target} →
    (fact : PR.PropertyHierarchyFact) →
    Reg.Member fact facts →
    String.stringEquality
      start
      (PR.propertyHierarchySubPropertyKey fact)
    ≡
    true →
    PropertyKeyPath
      facts
      (PR.propertyHierarchySuperPropertyKey fact)
      target →
    PropertyKeyPath facts start target

propertyKeyPathLength :
  ∀ {facts start target} →
  PropertyKeyPath facts start target →
  ℕ
propertyKeyPathLength propertyKeyPathRefl =
  zero
propertyKeyPathLength (propertyKeyPathStep fact member keyEqual path) =
  suc (propertyKeyPathLength path)

propertyKeyReachableWithinEqual :
  (fuel : ℕ) →
  (facts : List PR.PropertyHierarchyFact) →
  (key : String) →
  PR.propertyKeyReachableWithin fuel facts key key ≡ true
propertyKeyReachableWithinEqual zero facts key =
  String.stringEqualityTrueFromEqual key key refl
propertyKeyReachableWithinEqual (suc fuel) facts key
  with String.stringEquality key key
     | String.stringEqualityTrueFromEqual key key refl
... | true | keyEqual =
  refl
... | false | keyEqual =
  absurd (falseNotTrue keyEqual)

propertyKeyReachableThroughFactsFromPathStep :
  (fuel : ℕ) →
  (allFacts facts : List PR.PropertyHierarchyFact) →
  (start target : String) →
  (fact : PR.PropertyHierarchyFact) →
  Reg.Member fact facts →
  String.stringEquality
    start
    (PR.propertyHierarchySubPropertyKey fact)
  ≡
  true →
  PR.propertyKeyReachableWithin
    fuel
    allFacts
    (PR.propertyHierarchySuperPropertyKey fact)
    target
  ≡
  true →
  PR.propertyKeyReachableThroughFacts
    fuel
    allFacts
    start
    target
    facts
  ≡
  true
propertyKeyReachableThroughFactsFromPathStep
  fuel
  allFacts
  []
  start
  target
  fact
  ()
  keyEqual
  reachable
propertyKeyReachableThroughFactsFromPathStep
  fuel
  allFacts
  (fact ∷ facts)
  start
  target
  fact
  Reg.here
  keyEqual
  reachable
  with String.stringEquality
        start
        (PR.propertyHierarchySubPropertyKey fact)
... | true
  with PR.propertyKeyReachableWithin
        fuel
        allFacts
        (PR.propertyHierarchySuperPropertyKey fact)
        target
...   | true =
  refl
...   | false =
  absurd (falseNotTrue reachable)
propertyKeyReachableThroughFactsFromPathStep
  fuel
  allFacts
  (fact ∷ facts)
  start
  target
  fact
  Reg.here
  keyEqual
  reachable
  | false =
  absurd (falseNotTrue keyEqual)
propertyKeyReachableThroughFactsFromPathStep
  fuel
  allFacts
  (headFact ∷ facts)
  start
  target
  fact
  (Reg.there member)
  keyEqual
  reachable
  with String.stringEquality
        start
        (PR.propertyHierarchySubPropertyKey headFact)
... | true
  with PR.propertyKeyReachableWithin
        fuel
        allFacts
        (PR.propertyHierarchySuperPropertyKey headFact)
        target
...   | true =
  refl
...   | false =
  propertyKeyReachableThroughFactsFromPathStep
    fuel
    allFacts
    facts
    start
    target
    fact
    member
    keyEqual
    reachable
propertyKeyReachableThroughFactsFromPathStep
  fuel
  allFacts
  (headFact ∷ facts)
  start
  target
  fact
  (Reg.there member)
  keyEqual
  reachable
  | false =
  propertyKeyReachableThroughFactsFromPathStep
    fuel
    allFacts
    facts
    start
    target
    fact
    member
    keyEqual
    reachable

propertyKeyReachableWithinFromKeyPath :
  ∀ {facts start target} →
  (path : PropertyKeyPath facts start target) →
  PR.propertyKeyReachableWithin
    (propertyKeyPathLength path)
    facts
    start
    target
  ≡
  true
propertyKeyReachableWithinFromKeyPath propertyKeyPathRefl =
  String.stringEqualityTrueFromEqual _ _ refl
propertyKeyReachableWithinFromKeyPath
  (propertyKeyPathStep {start = start} {target = target}
    fact
    member
    keyEqual
    path)
  with String.stringEquality start target
... | true =
  refl
... | false =
  propertyKeyReachableThroughFactsFromPathStep
    (propertyKeyPathLength path)
    _
    _
    start
    target
    fact
    member
    keyEqual
    (propertyKeyReachableWithinFromKeyPath path)

propertyKeyPathFromHierarchyFact :
  (facts : List PR.PropertyHierarchyFact) →
  (fact : PR.PropertyHierarchyFact) →
  Reg.Member fact facts →
  PropertyKeyPath
    facts
    (PR.propertyHierarchySubPropertyKey fact)
    (PR.propertyHierarchySuperPropertyKey fact)
propertyKeyPathFromHierarchyFact facts fact member =
  propertyKeyPathStep
    fact
    member
    (String.stringEqualityTrueFromEqual
      (PR.propertyHierarchySubPropertyKey fact)
      (PR.propertyHierarchySubPropertyKey fact)
      refl)
    propertyKeyPathRefl

propertyKeyPathFromHierarchyStepEvidence :
  ∀ {hierarchyFacts sub super} →
  (evidence :
    PortablePropertyHierarchyStepEvidence hierarchyFacts sub super) →
  PropertyKeyPath
    hierarchyFacts
    (PR.propertyHierarchySubPropertyKey (portableHierarchyFact evidence))
    (PR.propertyHierarchySuperPropertyKey (portableHierarchyFact evidence))
propertyKeyPathFromHierarchyStepEvidence evidence =
  propertyKeyPathFromHierarchyFact
    _
    (portableHierarchyFact evidence)
    (portableHierarchyFactMember evidence)

propertyKeyReachableThroughFactsHasMember :
  (fuel : ℕ) →
  (allFacts facts : List PR.PropertyHierarchyFact) →
  (fact : PR.PropertyHierarchyFact) →
  Reg.Member fact facts →
  PR.propertyKeyReachableThroughFacts
    fuel
    allFacts
    (PR.propertyHierarchySubPropertyKey fact)
    (PR.propertyHierarchySuperPropertyKey fact)
    facts
  ≡
  true
propertyKeyReachableThroughFactsHasMember fuel allFacts [] fact ()
propertyKeyReachableThroughFactsHasMember
  fuel
  allFacts
  (fact ∷ facts)
  fact
  Reg.here
  with String.stringEquality
        (PR.propertyHierarchySubPropertyKey fact)
        (PR.propertyHierarchySubPropertyKey fact)
     | String.stringEqualityTrueFromEqual
        (PR.propertyHierarchySubPropertyKey fact)
        (PR.propertyHierarchySubPropertyKey fact)
        refl
... | true | subEqual
  with PR.propertyKeyReachableWithin
        fuel
        allFacts
        (PR.propertyHierarchySuperPropertyKey fact)
        (PR.propertyHierarchySuperPropertyKey fact)
     | propertyKeyReachableWithinEqual
        fuel
        allFacts
        (PR.propertyHierarchySuperPropertyKey fact)
...   | true | superReachable =
  refl
...   | false | superReachable =
  absurd (falseNotTrue superReachable)
propertyKeyReachableThroughFactsHasMember
  fuel
  allFacts
  (fact ∷ facts)
  fact
  Reg.here
  | false | subEqual =
  absurd (falseNotTrue subEqual)
propertyKeyReachableThroughFactsHasMember
  fuel
  allFacts
  (headFact ∷ facts)
  fact
  (Reg.there member)
  with String.stringEquality
        (PR.propertyHierarchySubPropertyKey fact)
        (PR.propertyHierarchySubPropertyKey headFact)
... | true
  with PR.propertyKeyReachableWithin
        fuel
        allFacts
        (PR.propertyHierarchySuperPropertyKey headFact)
        (PR.propertyHierarchySuperPropertyKey fact)
...   | true =
  refl
...   | false =
  propertyKeyReachableThroughFactsHasMember
    fuel
    allFacts
    facts
    fact
    member
propertyKeyReachableThroughFactsHasMember
  fuel
  allFacts
  (headFact ∷ facts)
  fact
  (Reg.there member)
  | false =
  propertyKeyReachableThroughFactsHasMember
    fuel
    allFacts
    facts
    fact
    member

propertyKeyReachableFromHierarchyFact :
  (facts : List PR.PropertyHierarchyFact) →
  (fact : PR.PropertyHierarchyFact) →
  Reg.Member fact facts →
  PR.propertyKeyReachable
    facts
    (PR.propertyHierarchySubPropertyKey fact)
    (PR.propertyHierarchySuperPropertyKey fact)
  ≡
  true
propertyKeyReachableFromHierarchyFact [] fact ()
propertyKeyReachableFromHierarchyFact (headFact ∷ facts) fact member
  with String.stringEquality
        (PR.propertyHierarchySubPropertyKey fact)
        (PR.propertyHierarchySuperPropertyKey fact)
... | true =
  refl
... | false =
  propertyKeyReachableThroughFactsHasMember
    _
    (headFact ∷ facts)
    (headFact ∷ facts)
    fact
    member

propertyKeyReachableFromHierarchyStepEvidence :
  ∀ {hierarchyFacts sub super} →
  (evidence :
    PortablePropertyHierarchyStepEvidence hierarchyFacts sub super) →
  PR.propertyKeyReachable
    hierarchyFacts
    (PR.propertyHierarchySubPropertyKey (portableHierarchyFact evidence))
    (PR.propertyHierarchySuperPropertyKey (portableHierarchyFact evidence))
  ≡
  true
propertyKeyReachableFromHierarchyStepEvidence evidence =
  propertyKeyReachableFromHierarchyFact
    _
    (portableHierarchyFact evidence)
    (portableHierarchyFactMember evidence)

portableFactRegularityContext :
  List PR.CompositeObjectPropertyFact →
  List PR.PropertyHierarchyFact →
  Reg.RegularityContext Sem.PortableSignature
portableFactRegularityContext compositeFacts hierarchyFacts .Reg.Composite =
  PortableCompositeObjectPropertyEvidence compositeFacts
portableFactRegularityContext compositeFacts hierarchyFacts .Reg.HierarchyStep =
  PortablePropertyHierarchyStepEvidence hierarchyFacts

generatedRegularityContext :
  P.OntologyDocument →
  Reg.RegularityContext Sem.PortableSignature
generatedRegularityContext document =
  portableFactRegularityContext
    (PR.regularityReportCompositeObjectPropertyFacts
      (PR.reportRegularity document))
    (PR.regularityReportPropertyHierarchyFacts
      (PR.reportRegularity document))

portableCompositeObjectPropertyEvidenceForMember :
  ∀ {compositeFacts fact} →
  Reg.Member fact compositeFacts →
  PortableCompositeObjectPropertyEvidence
    compositeFacts
    (Sem.translateObjectPropertyExpression
      (PR.compositeObjectPropertyExpression fact))
portableCompositeObjectPropertyEvidenceForMember {fact = fact} member =
  portableCompositeObjectPropertyEvidence fact member refl

portablePropertyHierarchyStepEvidenceForMember :
  ∀ {hierarchyFacts fact} →
  Reg.Member fact hierarchyFacts →
  PortablePropertyHierarchyStepEvidence
    hierarchyFacts
    (Sem.translateObjectPropertyExpression
      (PR.propertyHierarchySubProperty fact))
    (Sem.translateObjectPropertyExpression
      (PR.propertyHierarchySuperProperty fact))
portablePropertyHierarchyStepEvidenceForMember {fact = fact} member =
  portablePropertyHierarchyStepEvidence fact member refl refl

propertyKeyPathFromHierarchyPath :
  ∀ {compositeFacts hierarchyFacts start target} →
  PropertyHierarchyFactKeyCoherentResolver hierarchyFacts →
  Reg.PropertyHierarchyPath
    (portableFactRegularityContext compositeFacts hierarchyFacts)
    start
    target →
  PropertyKeyPath
    hierarchyFacts
    (Keys.syntaxObjectPropertyBaseKey start)
    (Keys.syntaxObjectPropertyBaseKey target)
propertyKeyPathFromHierarchyPath coherent Reg.hierarchyRefl =
  propertyKeyPathRefl
propertyKeyPathFromHierarchyPath
  {hierarchyFacts = hierarchyFacts}
  {target = target}
  coherent
  (Reg.hierarchyTrans step path) =
  propertyKeyPathStep
    (portableHierarchyFact step)
    (portableHierarchyFactMember step)
    (String.stringEqualityTrueFromEqual
      _
      _
      (portableHierarchyStepEvidenceSubSyntaxKey
        step
        (coherent
          (portableHierarchyFact step)
          (portableHierarchyFactMember step))))
    (subst
      (λ key →
        PropertyKeyPath
          hierarchyFacts
          key
          (Keys.syntaxObjectPropertyBaseKey target))
      (portableHierarchyStepEvidenceSuperSyntaxKey
        step
        (coherent
          (portableHierarchyFact step)
          (portableHierarchyFactMember step)))
      (propertyKeyPathFromHierarchyPath coherent path))

propertyKeyReachableWithinFromHierarchyPath :
  ∀ {compositeFacts hierarchyFacts start target} →
  (coherent : PropertyHierarchyFactKeyCoherentResolver hierarchyFacts) →
  (path :
    Reg.PropertyHierarchyPath
      (portableFactRegularityContext compositeFacts hierarchyFacts)
      start
      target) →
  PR.propertyKeyReachableWithin
    (propertyKeyPathLength
      (propertyKeyPathFromHierarchyPath coherent path))
    hierarchyFacts
    (Keys.syntaxObjectPropertyBaseKey start)
    (Keys.syntaxObjectPropertyBaseKey target)
  ≡
  true
propertyKeyReachableWithinFromHierarchyPath coherent path =
  propertyKeyReachableWithinFromKeyPath
    (propertyKeyPathFromHierarchyPath coherent path)

propertyKeyReachableWithinWitnessFromHierarchyPath :
  ∀ {compositeFacts hierarchyFacts start target} →
  (coherent : PropertyHierarchyFactKeyCoherentResolver hierarchyFacts) →
  Reg.PropertyHierarchyPath
    (portableFactRegularityContext compositeFacts hierarchyFacts)
    start
    target →
  Σ ℕ
    (λ fuel →
      PR.propertyKeyReachableWithin
        fuel
        hierarchyFacts
        (Keys.syntaxObjectPropertyBaseKey start)
        (Keys.syntaxObjectPropertyBaseKey target)
      ≡
      true)
propertyKeyReachableWithinWitnessFromHierarchyPath coherent path =
  propertyKeyPathLength (propertyKeyPathFromHierarchyPath coherent path) ,
  propertyKeyReachableWithinFromHierarchyPath coherent path

portablePropertyHierarchyPathFromStepEvidence :
  ∀ {compositeFacts hierarchyFacts sub super} →
  PortablePropertyHierarchyStepEvidence hierarchyFacts sub super →
  Reg.PropertyHierarchyPath
    (portableFactRegularityContext compositeFacts hierarchyFacts)
    sub
    super
portablePropertyHierarchyPathFromStepEvidence step =
  Reg.hierarchyTrans step Reg.hierarchyRefl

simplePropertyUseCanonicalFromNoViolations :
  (compositeFacts : List PR.CompositeObjectPropertyFact) →
  (hierarchyFacts : List PR.PropertyHierarchyFact) →
  (use : PR.SimplePropertyUse) →
  PR.NoSimplePropertyViolations
    (PR.simplePropertyViolationsForUse compositeFacts hierarchyFacts use) →
  PR.canonicalForSimplePropertyUse
    (PR.simplePropertyUseProperty use)
  ≡
  true
simplePropertyUseCanonicalFromNoViolations
  compositeFacts
  hierarchyFacts
  use
  clean
  with PR.canonicalForSimplePropertyUse (PR.simplePropertyUseProperty use)
... | true =
  refl
... | false =
  absurd clean

portableSimplePropertyUseCertificateFromNoViolations :
  (context : Reg.RegularityContext Sem.PortableSignature) →
  (compositeFacts : List PR.CompositeObjectPropertyFact) →
  (hierarchyFacts : List PR.PropertyHierarchyFact) →
  (use : PR.SimplePropertyUse) →
  PR.NoSimplePropertyViolations
    (PR.simplePropertyViolationsForUse compositeFacts hierarchyFacts use) →
  SimplePropertyUseNoCompositePredecessor context use →
  PortableSimplePropertyUseCertificate context use
portableSimplePropertyUseCertificateFromNoViolations
  context
  compositeFacts
  hierarchyFacts
  use
  clean
  noCompositePredecessor =
  portableSimplePropertyUseCertificate
    (simplePropertyUseCanonicalFromNoViolations
      compositeFacts
      hierarchyFacts
      use
      clean)
    noCompositePredecessor

portableFactSimplePropertyUseCertificateFromNoViolations :
  (compositeFacts : List PR.CompositeObjectPropertyFact) →
  (hierarchyFacts : List PR.PropertyHierarchyFact) →
  (use : PR.SimplePropertyUse) →
  PR.NoSimplePropertyViolations
    (PR.simplePropertyViolationsForUse compositeFacts hierarchyFacts use) →
  SimplePropertyUseNoCompositePredecessor
    (portableFactRegularityContext compositeFacts hierarchyFacts)
    use →
  PortableSimplePropertyUseCertificate
    (portableFactRegularityContext compositeFacts hierarchyFacts)
    use
portableFactSimplePropertyUseCertificateFromNoViolations
  compositeFacts
  hierarchyFacts
  use
  clean
  noCompositePredecessor =
  portableSimplePropertyUseCertificateFromNoViolations
    (portableFactRegularityContext compositeFacts hierarchyFacts)
    compositeFacts
    hierarchyFacts
    use
    clean
    noCompositePredecessor

noSimplePropertyViolationsAppendLeft :
  (left right : List PR.SimplePropertyViolation) →
  PR.NoSimplePropertyViolations (left ++ right) →
  PR.NoSimplePropertyViolations left
noSimplePropertyViolationsAppendLeft [] right clean =
  tt*
noSimplePropertyViolationsAppendLeft (violation ∷ left) right clean =
  clean

noSimplePropertyViolationsAppendRight :
  (left right : List PR.SimplePropertyViolation) →
  PR.NoSimplePropertyViolations (left ++ right) →
  PR.NoSimplePropertyViolations right
noSimplePropertyViolationsAppendRight [] right clean =
  clean
noSimplePropertyViolationsAppendRight (violation ∷ left) right clean =
  absurd clean

simplePropertyUseNoViolationsFromUses :
  (compositeFacts : List PR.CompositeObjectPropertyFact) →
  (hierarchyFacts : List PR.PropertyHierarchyFact) →
  (uses : List PR.SimplePropertyUse) →
  (use : PR.SimplePropertyUse) →
  Reg.Member use uses →
  PR.NoSimplePropertyViolations
    (PR.simplePropertyViolationsForUses
      compositeFacts
      hierarchyFacts
      uses) →
  PR.NoSimplePropertyViolations
    (PR.simplePropertyViolationsForUse
      compositeFacts
      hierarchyFacts
      use)
simplePropertyUseNoViolationsFromUses
  compositeFacts
  hierarchyFacts
  (use ∷ uses)
  use
  Reg.here
  clean =
  noSimplePropertyViolationsAppendLeft
    (PR.simplePropertyViolationsForUse compositeFacts hierarchyFacts use)
    (PR.simplePropertyViolationsForUses compositeFacts hierarchyFacts uses)
    clean
simplePropertyUseNoViolationsFromUses
  compositeFacts
  hierarchyFacts
  (headUse ∷ uses)
  use
  (Reg.there member)
  clean =
  simplePropertyUseNoViolationsFromUses
    compositeFacts
    hierarchyFacts
    uses
    use
    member
    (noSimplePropertyViolationsAppendRight
      (PR.simplePropertyViolationsForUse
        compositeFacts
        hierarchyFacts
        headUse)
      (PR.simplePropertyViolationsForUses
        compositeFacts
        hierarchyFacts
        uses)
      clean)

compositeViolationsForUseHasDirectKey :
  (hierarchyFacts : List PR.PropertyHierarchyFact) →
  (use : PR.SimplePropertyUse) →
  (facts : List PR.CompositeObjectPropertyFact) →
  (fact : PR.CompositeObjectPropertyFact) →
  Reg.Member fact facts →
  String.stringEquality
    (PR.simplePropertyUseKey use)
    (PR.compositeObjectPropertyKey fact)
  ≡
  true →
  PR.NoSimplePropertyViolations
    (PR.compositeViolationsForUse hierarchyFacts use facts) →
  ⊥
compositeViolationsForUseHasDirectKey hierarchyFacts use [] fact () keyEqual clean
compositeViolationsForUseHasDirectKey
  hierarchyFacts
  use
  (fact ∷ facts)
  fact
  Reg.here
  keyEqual
  clean
  with String.stringEquality
        (PR.simplePropertyUseKey use)
        (PR.compositeObjectPropertyKey fact)
... | true =
  clean
... | false =
  absurd (falseNotTrue keyEqual)
compositeViolationsForUseHasDirectKey
  hierarchyFacts
  use
  (headFact ∷ facts)
  fact
  (Reg.there member)
  keyEqual
  clean
  with String.stringEquality
        (PR.simplePropertyUseKey use)
        (PR.compositeObjectPropertyKey headFact)
... | true =
  clean
... | false
  with PR.propertyKeyReachable
        hierarchyFacts
        (PR.compositeObjectPropertyKey headFact)
        (PR.simplePropertyUseKey use)
...   | true =
  clean
...   | false =
  compositeViolationsForUseHasDirectKey
    hierarchyFacts
    use
    facts
    fact
    member
    keyEqual
    clean

compositeViolationsForUseHasReachableKey :
  (hierarchyFacts : List PR.PropertyHierarchyFact) →
  (use : PR.SimplePropertyUse) →
  (facts : List PR.CompositeObjectPropertyFact) →
  (fact : PR.CompositeObjectPropertyFact) →
  Reg.Member fact facts →
  PR.propertyKeyReachable
    hierarchyFacts
    (PR.compositeObjectPropertyKey fact)
    (PR.simplePropertyUseKey use)
  ≡
  true →
  PR.NoSimplePropertyViolations
    (PR.compositeViolationsForUse hierarchyFacts use facts) →
  ⊥
compositeViolationsForUseHasReachableKey hierarchyFacts use [] fact () reachable clean
compositeViolationsForUseHasReachableKey
  hierarchyFacts
  use
  (fact ∷ facts)
  fact
  Reg.here
  reachable
  clean
  with String.stringEquality
        (PR.simplePropertyUseKey use)
        (PR.compositeObjectPropertyKey fact)
... | true =
  clean
... | false
  with PR.propertyKeyReachable
        hierarchyFacts
        (PR.compositeObjectPropertyKey fact)
        (PR.simplePropertyUseKey use)
...   | true =
  clean
...   | false =
  absurd (falseNotTrue reachable)
compositeViolationsForUseHasReachableKey
  hierarchyFacts
  use
  (headFact ∷ facts)
  fact
  (Reg.there member)
  reachable
  clean
  with String.stringEquality
        (PR.simplePropertyUseKey use)
        (PR.compositeObjectPropertyKey headFact)
... | true =
  clean
... | false
  with PR.propertyKeyReachable
        hierarchyFacts
        (PR.compositeObjectPropertyKey headFact)
        (PR.simplePropertyUseKey use)
...   | true =
  clean
...   | false =
  compositeViolationsForUseHasReachableKey
    hierarchyFacts
    use
    facts
    fact
    member
    reachable
    clean

simplePropertyViolationsForUseHasDirectCompositeKey :
  (compositeFacts : List PR.CompositeObjectPropertyFact) →
  (hierarchyFacts : List PR.PropertyHierarchyFact) →
  (use : PR.SimplePropertyUse) →
  (fact : PR.CompositeObjectPropertyFact) →
  Reg.Member fact compositeFacts →
  String.stringEquality
    (PR.simplePropertyUseKey use)
    (PR.compositeObjectPropertyKey fact)
  ≡
  true →
  PR.NoSimplePropertyViolations
    (PR.simplePropertyViolationsForUse
      compositeFacts
      hierarchyFacts
      use) →
  ⊥
simplePropertyViolationsForUseHasDirectCompositeKey
  compositeFacts
  hierarchyFacts
  use
  fact
  factMember
  keyEqual
  clean =
  compositeViolationsForUseHasDirectKey
    hierarchyFacts
    use
    compositeFacts
    fact
    factMember
    keyEqual
    (noSimplePropertyViolationsAppendRight
      (PR.nonCanonicalViolationForUse use)
      (PR.compositeViolationsForUse hierarchyFacts use compositeFacts)
      clean)

simplePropertyViolationsForUseHasReachableCompositeKey :
  (compositeFacts : List PR.CompositeObjectPropertyFact) →
  (hierarchyFacts : List PR.PropertyHierarchyFact) →
  (use : PR.SimplePropertyUse) →
  (fact : PR.CompositeObjectPropertyFact) →
  Reg.Member fact compositeFacts →
  PR.propertyKeyReachable
    hierarchyFacts
    (PR.compositeObjectPropertyKey fact)
    (PR.simplePropertyUseKey use)
  ≡
  true →
  PR.NoSimplePropertyViolations
    (PR.simplePropertyViolationsForUse
      compositeFacts
      hierarchyFacts
      use) →
  ⊥
simplePropertyViolationsForUseHasReachableCompositeKey
  compositeFacts
  hierarchyFacts
  use
  fact
  factMember
  reachable
  clean =
  compositeViolationsForUseHasReachableKey
    hierarchyFacts
    use
    compositeFacts
    fact
    factMember
    reachable
    (noSimplePropertyViolationsAppendRight
      (PR.nonCanonicalViolationForUse use)
      (PR.compositeViolationsForUse hierarchyFacts use compositeFacts)
      clean)

simplePropertyUseNoViolationsFromGeneratedReport :
  (document : P.OntologyDocument) →
  PR.NoReportSimplePropertyViolations (PR.reportRegularity document) →
  (use : PR.SimplePropertyUse) →
  Reg.Member
    use
    (PR.regularityReportSimplePropertyUses (PR.reportRegularity document)) →
  PR.NoSimplePropertyViolations
    (PR.simplePropertyViolationsForUse
      (PR.regularityReportCompositeObjectPropertyFacts
        (PR.reportRegularity document))
      (PR.regularityReportPropertyHierarchyFacts
        (PR.reportRegularity document))
      use)
simplePropertyUseNoViolationsFromGeneratedReport
  document
  clean
  use
  member =
  simplePropertyUseNoViolationsFromUses
    (PR.regularityReportCompositeObjectPropertyFacts
      (PR.reportRegularity document))
    (PR.regularityReportPropertyHierarchyFacts
      (PR.reportRegularity document))
    (PR.regularityReportSimplePropertyUses
      (PR.reportRegularity document))
    use
    member
    clean

RegularityReportSimplePropertyViolationsComputed :
  PR.RegularityReport → Type₀
RegularityReportSimplePropertyViolationsComputed report =
  PR.regularityReportSimplePropertyViolations report
  ≡
  PR.simplePropertyViolationsForUses
    (PR.regularityReportCompositeObjectPropertyFacts report)
    (PR.regularityReportPropertyHierarchyFacts report)
    (PR.regularityReportSimplePropertyUses report)

simplePropertyUseNoViolationsFromReport :
  (report : PR.RegularityReport) →
  RegularityReportSimplePropertyViolationsComputed report →
  PR.NoReportSimplePropertyViolations report →
  (use : PR.SimplePropertyUse) →
  Reg.Member use (PR.regularityReportSimplePropertyUses report) →
  PR.NoSimplePropertyViolations
    (PR.simplePropertyViolationsForUse
      (PR.regularityReportCompositeObjectPropertyFacts report)
      (PR.regularityReportPropertyHierarchyFacts report)
      use)
simplePropertyUseNoViolationsFromReport
  report
  violationsComputed
  clean
  use
  member =
  simplePropertyUseNoViolationsFromUses
    (PR.regularityReportCompositeObjectPropertyFacts report)
    (PR.regularityReportPropertyHierarchyFacts report)
    (PR.regularityReportSimplePropertyUses report)
    use
    member
    (subst
      PR.NoSimplePropertyViolations
      violationsComputed
      clean)

regularityReportRejectsDirectCompositeKey :
  (report : PR.RegularityReport) →
  RegularityReportSimplePropertyViolationsComputed report →
  PR.NoReportSimplePropertyViolations report →
  (use : PR.SimplePropertyUse) →
  Reg.Member use (PR.regularityReportSimplePropertyUses report) →
  (fact : PR.CompositeObjectPropertyFact) →
  Reg.Member fact (PR.regularityReportCompositeObjectPropertyFacts report) →
  String.stringEquality
    (PR.simplePropertyUseKey use)
    (PR.compositeObjectPropertyKey fact)
  ≡
  true →
  ⊥
regularityReportRejectsDirectCompositeKey
  report
  violationsComputed
  clean
  use
  useMember
  fact
  factMember
  keyEqual =
  simplePropertyViolationsForUseHasDirectCompositeKey
    (PR.regularityReportCompositeObjectPropertyFacts report)
    (PR.regularityReportPropertyHierarchyFacts report)
    use
    fact
    factMember
    keyEqual
    (simplePropertyUseNoViolationsFromReport
      report
      violationsComputed
      clean
      use
      useMember)

regularityReportRejectsReachableCompositeKey :
  (report : PR.RegularityReport) →
  RegularityReportSimplePropertyViolationsComputed report →
  PR.NoReportSimplePropertyViolations report →
  (use : PR.SimplePropertyUse) →
  Reg.Member use (PR.regularityReportSimplePropertyUses report) →
  (fact : PR.CompositeObjectPropertyFact) →
  Reg.Member fact (PR.regularityReportCompositeObjectPropertyFacts report) →
  PR.propertyKeyReachable
    (PR.regularityReportPropertyHierarchyFacts report)
    (PR.compositeObjectPropertyKey fact)
    (PR.simplePropertyUseKey use)
  ≡
  true →
  ⊥
regularityReportRejectsReachableCompositeKey
  report
  violationsComputed
  clean
  use
  useMember
  fact
  factMember
  reachable =
  simplePropertyViolationsForUseHasReachableCompositeKey
    (PR.regularityReportCompositeObjectPropertyFacts report)
    (PR.regularityReportPropertyHierarchyFacts report)
    use
    fact
    factMember
    reachable
    (simplePropertyUseNoViolationsFromReport
      report
      violationsComputed
      clean
      use
      useMember)

generatedRegularityReportSimplePropertyViolationsComputed :
  (document : P.OntologyDocument) →
  RegularityReportSimplePropertyViolationsComputed
    (PR.reportRegularity document)
generatedRegularityReportSimplePropertyViolationsComputed document =
  refl

generatedReportRejectsDirectCompositeKey :
  (document : P.OntologyDocument) →
  PR.NoReportSimplePropertyViolations (PR.reportRegularity document) →
  (use : PR.SimplePropertyUse) →
  Reg.Member
    use
    (PR.regularityReportSimplePropertyUses (PR.reportRegularity document)) →
  (fact : PR.CompositeObjectPropertyFact) →
  Reg.Member
    fact
    (PR.regularityReportCompositeObjectPropertyFacts
      (PR.reportRegularity document)) →
  String.stringEquality
    (PR.simplePropertyUseKey use)
    (PR.compositeObjectPropertyKey fact)
  ≡
  true →
  ⊥
generatedReportRejectsDirectCompositeKey
  document
  clean
  use
  useMember
  fact
  factMember
  keyEqual =
  regularityReportRejectsDirectCompositeKey
    (PR.reportRegularity document)
    (generatedRegularityReportSimplePropertyViolationsComputed document)
    clean
    use
    useMember
    fact
    factMember
    keyEqual

generatedReportRejectsReachableCompositeKey :
  (document : P.OntologyDocument) →
  PR.NoReportSimplePropertyViolations (PR.reportRegularity document) →
  (use : PR.SimplePropertyUse) →
  Reg.Member
    use
    (PR.regularityReportSimplePropertyUses (PR.reportRegularity document)) →
  (fact : PR.CompositeObjectPropertyFact) →
  Reg.Member
    fact
    (PR.regularityReportCompositeObjectPropertyFacts
      (PR.reportRegularity document)) →
  PR.propertyKeyReachable
    (PR.regularityReportPropertyHierarchyFacts (PR.reportRegularity document))
    (PR.compositeObjectPropertyKey fact)
    (PR.simplePropertyUseKey use)
  ≡
  true →
  ⊥
generatedReportRejectsReachableCompositeKey
  document
  clean
  use
  useMember
  fact
  factMember
  reachable =
  regularityReportRejectsReachableCompositeKey
    (PR.reportRegularity document)
    (generatedRegularityReportSimplePropertyViolationsComputed document)
    clean
    use
    useMember
    fact
    factMember
    reachable

portableFactSimplePropertyUseCertificateFromReport :
  (report : PR.RegularityReport) →
  RegularityReportSimplePropertyViolationsComputed report →
  PR.NoReportSimplePropertyViolations report →
  (use : PR.SimplePropertyUse) →
  Reg.Member use (PR.regularityReportSimplePropertyUses report) →
  SimplePropertyUseNoCompositePredecessor
    (portableFactRegularityContext
      (PR.regularityReportCompositeObjectPropertyFacts report)
      (PR.regularityReportPropertyHierarchyFacts report))
    use →
  PortableSimplePropertyUseCertificate
    (portableFactRegularityContext
      (PR.regularityReportCompositeObjectPropertyFacts report)
      (PR.regularityReportPropertyHierarchyFacts report))
    use
portableFactSimplePropertyUseCertificateFromReport
  report
  violationsComputed
  clean
  use
  member
  noCompositePredecessor =
  portableFactSimplePropertyUseCertificateFromNoViolations
    (PR.regularityReportCompositeObjectPropertyFacts report)
    (PR.regularityReportPropertyHierarchyFacts report)
    use
    (simplePropertyUseNoViolationsFromReport
      report
      violationsComputed
      clean
      use
      member)
    noCompositePredecessor

portableFactSimplePropertyUseCertificateFromGeneratedReport :
  (document : P.OntologyDocument) →
  PR.NoReportSimplePropertyViolations (PR.reportRegularity document) →
  (use : PR.SimplePropertyUse) →
  Reg.Member
    use
    (PR.regularityReportSimplePropertyUses (PR.reportRegularity document)) →
  SimplePropertyUseNoCompositePredecessor
    (generatedRegularityContext document)
    use →
  PortableSimplePropertyUseCertificate
    (generatedRegularityContext document)
    use
portableFactSimplePropertyUseCertificateFromGeneratedReport
  document
  clean
  use
  member
  noCompositePredecessor =
  portableFactSimplePropertyUseCertificateFromReport
    (PR.reportRegularity document)
    (generatedRegularityReportSimplePropertyViolationsComputed document)
    clean
    use
    member
    noCompositePredecessor

TranslatedClassExpressionUsesOnlySimpleObjectProperties :
  Reg.RegularityContext Sem.PortableSignature →
  Optional (S.ClassExpression Sem.PortableSignature) →
  Type₀
TranslatedClassExpressionUsesOnlySimpleObjectProperties context absent =
  Unit*
TranslatedClassExpressionUsesOnlySimpleObjectProperties context (present class) =
  Reg.ClassExpressionUsesOnlySimpleObjectProperties context class

TranslatedClassExpressionsUseOnlySimpleObjectProperties :
  Reg.RegularityContext Sem.PortableSignature →
  Optional (List (S.ClassExpression Sem.PortableSignature)) →
  Type₀
TranslatedClassExpressionsUseOnlySimpleObjectProperties context absent =
  Unit*
TranslatedClassExpressionsUseOnlySimpleObjectProperties context (present classes) =
  Reg.ClassExpressionsUseOnlySimpleObjectProperties context classes

TranslatedOptionalClassExpressionUsesOnlySimpleObjectProperties :
  Reg.RegularityContext Sem.PortableSignature →
  Optional (Optional (S.ClassExpression Sem.PortableSignature)) →
  Type₀
TranslatedOptionalClassExpressionUsesOnlySimpleObjectProperties context absent =
  Unit*
TranslatedOptionalClassExpressionUsesOnlySimpleObjectProperties
  context
  (present absent) =
  Unit*
TranslatedOptionalClassExpressionUsesOnlySimpleObjectProperties
  context
  (present (present class)) =
  Reg.ClassExpressionUsesOnlySimpleObjectProperties context class

translatedOptionalClassExpressionUsesOnlySimpleObjectPropertiesToRegular :
  (context : Reg.RegularityContext Sem.PortableSignature) →
  (translated : Optional (S.ClassExpression Sem.PortableSignature)) →
  TranslatedOptionalClassExpressionUsesOnlySimpleObjectProperties
    context
    (present translated) →
  Reg.OptionalClassExpressionUsesOnlySimpleObjectProperties
    context
    translated
translatedOptionalClassExpressionUsesOnlySimpleObjectPropertiesToRegular
  context
  absent
  proof =
  proof
translatedOptionalClassExpressionUsesOnlySimpleObjectPropertiesToRegular
  context
  (present class)
  proof =
  proof

mutual
  PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate :
    Reg.RegularityContext Sem.PortableSignature →
    P.ClassExpression →
    Type₀
  PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate
    context
    (P.namedClass c) =
    Unit*
  PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate
    context
    P.owlThing =
    Unit*
  PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate
    context
    P.owlNothing =
    Unit*
  PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate
    context
    (P.objectIntersectionOf classes) =
    PortableClassExpressionsTwoOrMoreUseOnlySimpleObjectPropertiesCertificate
      context
      classes
  PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate
    context
    (P.objectUnionOf classes) =
    PortableClassExpressionsTwoOrMoreUseOnlySimpleObjectPropertiesCertificate
      context
      classes
  PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate
    context
    (P.objectComplementOf class) =
    PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate
      context
      class
  PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate
    context
    (P.objectOneOf individuals) =
    Unit*
  PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate
    context
    (P.objectSomeValuesFrom property class) =
    PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate
      context
      class
  PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate
    context
    (P.objectAllValuesFrom property class) =
    PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate
      context
      class
  PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate
    context
    (P.objectHasValue property individual) =
    Unit*
  PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate
    context
    (P.objectHasSelf property) =
    PortableSimpleObjectPropertyExpressionCertificate context property
  PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate
    context
    (P.objectMinCardinality n property qualifier) =
    PortableSimpleObjectPropertyExpressionCertificate context property
    ×
    PortableOptionalClassExpressionUsesOnlySimpleObjectPropertiesCertificate
      context
      qualifier
  PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate
    context
    (P.objectMaxCardinality n property qualifier) =
    PortableSimpleObjectPropertyExpressionCertificate context property
    ×
    PortableOptionalClassExpressionUsesOnlySimpleObjectPropertiesCertificate
      context
      qualifier
  PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate
    context
    (P.objectExactCardinality n property qualifier) =
    PortableSimpleObjectPropertyExpressionCertificate context property
    ×
    PortableOptionalClassExpressionUsesOnlySimpleObjectPropertiesCertificate
      context
      qualifier
  PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate
    context
    (P.dataSomeValuesFrom property range) =
    Unit*
  PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate
    context
    (P.dataAllValuesFrom property range) =
    Unit*
  PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate
    context
    (P.dataHasValue property literal) =
    Unit*
  PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate
    context
    (P.dataMinCardinality n property qualifier) =
    Unit*
  PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate
    context
    (P.dataMaxCardinality n property qualifier) =
    Unit*
  PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate
    context
    (P.dataExactCardinality n property qualifier) =
    Unit*

  PortableClassExpressionsUseOnlySimpleObjectPropertiesCertificate :
    Reg.RegularityContext Sem.PortableSignature →
    List P.ClassExpression →
    Type₀
  PortableClassExpressionsUseOnlySimpleObjectPropertiesCertificate context [] =
    Unit*
  PortableClassExpressionsUseOnlySimpleObjectPropertiesCertificate
    context
    (class ∷ classes) =
    PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate
      context
      class
    ×
    PortableClassExpressionsUseOnlySimpleObjectPropertiesCertificate
      context
      classes

  PortableClassExpressionsTwoOrMoreUseOnlySimpleObjectPropertiesCertificate :
    Reg.RegularityContext Sem.PortableSignature →
    P.TwoOrMore P.ClassExpression →
    Type₀
  PortableClassExpressionsTwoOrMoreUseOnlySimpleObjectPropertiesCertificate
    context
    classes =
    PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate
      context
      (P.first classes)
    ×
    PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate
      context
      (P.second classes)
    ×
    PortableClassExpressionsUseOnlySimpleObjectPropertiesCertificate
      context
      (P.rest classes)

  PortableOptionalClassExpressionUsesOnlySimpleObjectPropertiesCertificate :
    Reg.RegularityContext Sem.PortableSignature →
    Optional P.ClassExpression →
    Type₀
  PortableOptionalClassExpressionUsesOnlySimpleObjectPropertiesCertificate
    context
    absent =
    Unit*
  PortableOptionalClassExpressionUsesOnlySimpleObjectPropertiesCertificate
    context
    (present class) =
    PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate
      context
      class

  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax :
    ∀ {context class} →
    PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate
      context
      class →
    TranslatedClassExpressionUsesOnlySimpleObjectProperties
      context
      (Sem.translateClassExpression class)
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
    {class = P.namedClass c}
    certificate =
    tt*
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
    {class = P.owlThing}
    certificate =
    tt*
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
    {class = P.owlNothing}
    certificate =
    tt*
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
    {context = context}
    {class = P.objectIntersectionOf classes}
    (firstCertificate , secondCertificate , restCertificate)
    with Sem.translateClassExpression (P.first classes)
       | Sem.translateClassExpression (P.second classes)
       | Sem.translateClassExpressionList (P.rest classes)
       | portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
           {context = context}
           {class = P.first classes}
           firstCertificate
       | portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
           {context = context}
           {class = P.second classes}
           secondCertificate
       | portableClassExpressionsUseOnlySimpleObjectPropertiesCertificateToSyntax
           {context = context}
           {classes = P.rest classes}
           restCertificate
  ... | present translatedFirst | present translatedSecond | present translatedRest
      | translatedFirstCertificate
      | translatedSecondCertificate
      | translatedRestCertificate =
    translatedFirstCertificate ,
    translatedSecondCertificate ,
    translatedRestCertificate
  ... | absent | translatedSecond | translatedRest
      | translatedFirstCertificate
      | translatedSecondCertificate
      | translatedRestCertificate =
    tt*
  ... | present translatedFirst | absent | translatedRest
      | translatedFirstCertificate
      | translatedSecondCertificate
      | translatedRestCertificate =
    tt*
  ... | present translatedFirst | present translatedSecond | absent
      | translatedFirstCertificate
      | translatedSecondCertificate
      | translatedRestCertificate =
    tt*
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
    {context = context}
    {class = P.objectUnionOf classes}
    (firstCertificate , secondCertificate , restCertificate)
    with Sem.translateClassExpression (P.first classes)
       | Sem.translateClassExpression (P.second classes)
       | Sem.translateClassExpressionList (P.rest classes)
       | portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
           {context = context}
           {class = P.first classes}
           firstCertificate
       | portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
           {context = context}
           {class = P.second classes}
           secondCertificate
       | portableClassExpressionsUseOnlySimpleObjectPropertiesCertificateToSyntax
           {context = context}
           {classes = P.rest classes}
           restCertificate
  ... | present translatedFirst | present translatedSecond | present translatedRest
      | translatedFirstCertificate
      | translatedSecondCertificate
      | translatedRestCertificate =
    translatedFirstCertificate ,
    translatedSecondCertificate ,
    translatedRestCertificate
  ... | absent | translatedSecond | translatedRest
      | translatedFirstCertificate
      | translatedSecondCertificate
      | translatedRestCertificate =
    tt*
  ... | present translatedFirst | absent | translatedRest
      | translatedFirstCertificate
      | translatedSecondCertificate
      | translatedRestCertificate =
    tt*
  ... | present translatedFirst | present translatedSecond | absent
      | translatedFirstCertificate
      | translatedSecondCertificate
      | translatedRestCertificate =
    tt*
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
    {context = context}
    {class = P.objectComplementOf class}
    certificate
    with Sem.translateClassExpression class
       | portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
           {context = context}
           {class = class}
           certificate
  ... | present translated | translatedCertificate =
    translatedCertificate
  ... | absent | translatedCertificate =
    tt*
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
    {class = P.objectOneOf individuals}
    certificate =
    tt*
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
    {context = context}
    {class = P.objectSomeValuesFrom property class}
    certificate
    with Sem.translateClassExpression class
       | portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
           {context = context}
           {class = class}
           certificate
  ... | present translated | translatedCertificate =
    translatedCertificate
  ... | absent | translatedCertificate =
    tt*
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
    {context = context}
    {class = P.objectAllValuesFrom property class}
    certificate
    with Sem.translateClassExpression class
       | portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
           {context = context}
           {class = class}
           certificate
  ... | present translated | translatedCertificate =
    translatedCertificate
  ... | absent | translatedCertificate =
    tt*
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
    {class = P.objectHasValue property individual}
    certificate =
    tt*
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
    {class = P.objectHasSelf property}
    certificate =
    portableSimpleObjectPropertyExpressionCertificateToSyntax certificate
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
    {context = context}
    {class = P.objectMinCardinality n property qualifier}
    (propertyCertificate , qualifierCertificate)
    with Sem.translateOptionalClassExpression qualifier
       | portableOptionalClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
           {context = context}
           {class = qualifier}
           qualifierCertificate
  ... | present translated | translatedQualifierCertificate =
    portableSimpleObjectPropertyExpressionCertificateToSyntax
      propertyCertificate
    ,
    translatedOptionalClassExpressionUsesOnlySimpleObjectPropertiesToRegular
      context
      translated
      translatedQualifierCertificate
  ... | absent | translatedQualifierCertificate =
    tt*
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
    {context = context}
    {class = P.objectMaxCardinality n property qualifier}
    (propertyCertificate , qualifierCertificate)
    with Sem.translateOptionalClassExpression qualifier
       | portableOptionalClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
           {context = context}
           {class = qualifier}
           qualifierCertificate
  ... | present translated | translatedQualifierCertificate =
    portableSimpleObjectPropertyExpressionCertificateToSyntax
      propertyCertificate
    ,
    translatedOptionalClassExpressionUsesOnlySimpleObjectPropertiesToRegular
      context
      translated
      translatedQualifierCertificate
  ... | absent | translatedQualifierCertificate =
    tt*
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
    {context = context}
    {class = P.objectExactCardinality n property qualifier}
    (propertyCertificate , qualifierCertificate)
    with Sem.translateOptionalClassExpression qualifier
       | portableOptionalClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
           {context = context}
           {class = qualifier}
           qualifierCertificate
  ... | present translated | translatedQualifierCertificate =
    portableSimpleObjectPropertyExpressionCertificateToSyntax
      propertyCertificate
    ,
    translatedOptionalClassExpressionUsesOnlySimpleObjectPropertiesToRegular
      context
      translated
      translatedQualifierCertificate
  ... | absent | translatedQualifierCertificate =
    tt*
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
    {class = P.dataSomeValuesFrom property range}
    certificate
    with Sem.translateDataRange range
  ... | present translated =
    tt*
  ... | absent =
    tt*
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
    {class = P.dataAllValuesFrom property range}
    certificate
    with Sem.translateDataRange range
  ... | present translated =
    tt*
  ... | absent =
    tt*
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
    {class = P.dataHasValue property literal}
    certificate =
    tt*
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
    {class = P.dataMinCardinality n property qualifier}
    certificate
    with Sem.translateOptionalDataRange qualifier
  ... | present translated =
    tt*
  ... | absent =
    tt*
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
    {class = P.dataMaxCardinality n property qualifier}
    certificate
    with Sem.translateOptionalDataRange qualifier
  ... | present translated =
    tt*
  ... | absent =
    tt*
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
    {class = P.dataExactCardinality n property qualifier}
    certificate
    with Sem.translateOptionalDataRange qualifier
  ... | present translated =
    tt*
  ... | absent =
    tt*

  portableClassExpressionsUseOnlySimpleObjectPropertiesCertificateToSyntax :
    ∀ {context classes} →
    PortableClassExpressionsUseOnlySimpleObjectPropertiesCertificate
      context
      classes →
    TranslatedClassExpressionsUseOnlySimpleObjectProperties
      context
      (Sem.translateClassExpressionList classes)
  portableClassExpressionsUseOnlySimpleObjectPropertiesCertificateToSyntax
    {classes = []}
    certificate =
    tt*
  portableClassExpressionsUseOnlySimpleObjectPropertiesCertificateToSyntax
    {context = context}
    {classes = class ∷ classes}
    (classCertificate , classesCertificate)
    with Sem.translateClassExpression class
       | Sem.translateClassExpressionList classes
       | portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
           {context = context}
           {class = class}
           classCertificate
       | portableClassExpressionsUseOnlySimpleObjectPropertiesCertificateToSyntax
           {context = context}
           {classes = classes}
           classesCertificate
  ... | present translatedClass | present translatedClasses
      | translatedClassCertificate | translatedClassesCertificate =
    translatedClassCertificate , translatedClassesCertificate
  ... | absent | translatedClasses
      | translatedClassCertificate | translatedClassesCertificate =
    tt*
  ... | present translatedClass | absent
      | translatedClassCertificate | translatedClassesCertificate =
    tt*

  portableClassExpressionsTwoOrMoreUseOnlySimpleObjectPropertiesCertificateToSyntax :
    ∀ {context classes} →
    PortableClassExpressionsTwoOrMoreUseOnlySimpleObjectPropertiesCertificate
      context
      classes →
    TranslatedClassExpressionsUseOnlySimpleObjectProperties
      context
      (Sem.translateClassExpressionTwoOrMore classes)
  portableClassExpressionsTwoOrMoreUseOnlySimpleObjectPropertiesCertificateToSyntax
    {context = context}
    {classes = classes}
    (firstCertificate , secondCertificate , restCertificate)
    with Sem.translateClassExpression (P.first classes)
       | Sem.translateClassExpression (P.second classes)
       | Sem.translateClassExpressionList (P.rest classes)
       | portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
           {context = context}
           {class = P.first classes}
           firstCertificate
       | portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
           {context = context}
           {class = P.second classes}
           secondCertificate
       | portableClassExpressionsUseOnlySimpleObjectPropertiesCertificateToSyntax
           {context = context}
           {classes = P.rest classes}
           restCertificate
  ... | present translatedFirst | present translatedSecond | present translatedRest
      | translatedFirstCertificate
      | translatedSecondCertificate
      | translatedRestCertificate =
    translatedFirstCertificate ,
    translatedSecondCertificate ,
    translatedRestCertificate
  ... | absent | translatedSecond | translatedRest
      | translatedFirstCertificate
      | translatedSecondCertificate
      | translatedRestCertificate =
    tt*
  ... | present translatedFirst | absent | translatedRest
      | translatedFirstCertificate
      | translatedSecondCertificate
      | translatedRestCertificate =
    tt*
  ... | present translatedFirst | present translatedSecond | absent
      | translatedFirstCertificate
      | translatedSecondCertificate
      | translatedRestCertificate =
    tt*

  portableOptionalClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax :
    ∀ {context class} →
    PortableOptionalClassExpressionUsesOnlySimpleObjectPropertiesCertificate
      context
      class →
    TranslatedOptionalClassExpressionUsesOnlySimpleObjectProperties
      context
      (Sem.translateOptionalClassExpression class)
  portableOptionalClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
    {class = absent}
    certificate =
    tt*
  portableOptionalClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
    {context = context}
    {class = present class}
    certificate
    with Sem.translateClassExpression class
       | portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
           {context = context}
           {class = class}
           certificate
  ... | present translated | translatedCertificate =
    translatedCertificate
  ... | absent | translatedCertificate =
    tt*

PortableObjectPropertyExpressionsSimpleCertificate :
  Reg.RegularityContext Sem.PortableSignature →
  List P.ObjectPropertyExpression →
  Type₀
PortableObjectPropertyExpressionsSimpleCertificate context [] =
  Unit*
PortableObjectPropertyExpressionsSimpleCertificate context (property ∷ properties) =
  PortableSimpleObjectPropertyExpressionCertificate context property
  ×
  PortableObjectPropertyExpressionsSimpleCertificate context properties

PortableObjectPropertyExpressionsTwoOrMoreSimpleCertificate :
  Reg.RegularityContext Sem.PortableSignature →
  P.TwoOrMore P.ObjectPropertyExpression →
  Type₀
PortableObjectPropertyExpressionsTwoOrMoreSimpleCertificate
  context
  properties =
  PortableSimpleObjectPropertyExpressionCertificate
    context
    (P.first properties)
  ×
  PortableSimpleObjectPropertyExpressionCertificate
    context
    (P.second properties)
  ×
  PortableObjectPropertyExpressionsSimpleCertificate
    context
    (P.rest properties)

portableObjectPropertyExpressionsSimpleCertificateToSyntax :
  ∀ {context properties} →
  PortableObjectPropertyExpressionsSimpleCertificate context properties →
  Reg.ObjectPropertyExpressionsSimple
    context
    (Sem.translateObjectPropertyExpressionList properties)
portableObjectPropertyExpressionsSimpleCertificateToSyntax {properties = []} proof =
  tt*
portableObjectPropertyExpressionsSimpleCertificateToSyntax
  {properties = property ∷ properties}
  (propertyProof , propertiesProof) =
  portableSimpleObjectPropertyExpressionCertificateToSyntax propertyProof ,
  portableObjectPropertyExpressionsSimpleCertificateToSyntax propertiesProof

portableObjectPropertyExpressionsTwoOrMoreSimpleCertificateToSyntax :
  ∀ {context properties} →
  PortableObjectPropertyExpressionsTwoOrMoreSimpleCertificate
    context
    properties →
  Reg.ObjectPropertyExpressionsSimple
    context
    (Sem.translateObjectPropertyExpressionList
      (Sem.twoOrMoreToList properties))
portableObjectPropertyExpressionsTwoOrMoreSimpleCertificateToSyntax
  {properties = properties}
  (firstProof , secondProof , restProof) =
  portableSimpleObjectPropertyExpressionCertificateToSyntax firstProof ,
  portableSimpleObjectPropertyExpressionCertificateToSyntax secondProof ,
  portableObjectPropertyExpressionsSimpleCertificateToSyntax restProof

TranslatedAxiomsUseOnlySimpleObjectProperties :
  Reg.RegularityContext Sem.PortableSignature →
  Optional (List (S.Axiom Sem.PortableSignature)) →
  Type₀
TranslatedAxiomsUseOnlySimpleObjectProperties context absent =
  Unit*
TranslatedAxiomsUseOnlySimpleObjectProperties context (present axioms) =
  Reg.AxiomsUseOnlySimpleObjectProperties context axioms

PortableAxiomUsesOnlySimpleObjectPropertiesCertificate :
  Reg.RegularityContext Sem.PortableSignature →
  P.Axiom →
  Type₀
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.declaration e) =
  Unit*
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.subClassOf c d) =
  PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate context c
  ×
  PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate context d
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.equivalentClasses classes) =
  PortableClassExpressionsUseOnlySimpleObjectPropertiesCertificate
    context
    (Sem.twoOrMoreToList classes)
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.disjointClasses classes) =
  PortableClassExpressionsUseOnlySimpleObjectPropertiesCertificate
    context
    (Sem.twoOrMoreToList classes)
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.disjointUnion c classes) =
  PortableClassExpressionsUseOnlySimpleObjectPropertiesCertificate
    context
    (Sem.twoOrMoreToList classes)
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.subObjectPropertyOf sub super) =
  Unit*
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.equivalentObjectProperties properties) =
  Unit*
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.disjointObjectProperties properties) =
  PortableObjectPropertyExpressionsTwoOrMoreSimpleCertificate
    context
    properties
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.inverseObjectProperties p q) =
  Unit*
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.objectPropertyDomain p class) =
  PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate
    context
    class
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.objectPropertyRange p class) =
  PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate
    context
    class
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.functionalObjectProperty property) =
  PortableSimpleObjectPropertyExpressionCertificate context property
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.inverseFunctionalObjectProperty property) =
  PortableSimpleObjectPropertyExpressionCertificate context property
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.reflexiveObjectProperty property) =
  Unit*
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.irreflexiveObjectProperty property) =
  PortableSimpleObjectPropertyExpressionCertificate context property
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.symmetricObjectProperty property) =
  Unit*
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.asymmetricObjectProperty property) =
  PortableSimpleObjectPropertyExpressionCertificate context property
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.transitiveObjectProperty property) =
  Unit*
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.subDataPropertyOf sub super) =
  Unit*
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.equivalentDataProperties properties) =
  Unit*
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.disjointDataProperties properties) =
  Unit*
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.dataPropertyDomain p class) =
  PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate
    context
    class
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.dataPropertyRange p range) =
  Unit*
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.functionalDataProperty property) =
  Unit*
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.datatypeDefinition datatype range) =
  Unit*
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.hasKey class key) =
  PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate
    context
    class
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.sameIndividual individuals) =
  Unit*
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.differentIndividuals individuals) =
  Unit*
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.classAssertion class individual) =
  PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate
    context
    class
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.objectPropertyAssertion property source target) =
  Unit*
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.negativeObjectPropertyAssertion property source target) =
  Unit*
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.dataPropertyAssertion property source literal) =
  Unit*
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.negativeDataPropertyAssertion property source literal) =
  Unit*
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.annotationAssertion property subject value) =
  Unit*
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.subAnnotationPropertyOf sub super) =
  Unit*
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.annotationPropertyDomain property targetIRI) =
  Unit*
PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.annotationPropertyRange property targetIRI) =
  Unit*

memberAppendLeft :
  ∀ {ℓ} {A : Type ℓ} {x : A} →
  (left right : List A) →
  Reg.Member x left →
  Reg.Member x (left ++ right)
memberAppendLeft [] right ()
memberAppendLeft (x ∷ left) right Reg.here =
  Reg.here
memberAppendLeft (y ∷ left) right (Reg.there member) =
  Reg.there (memberAppendLeft left right member)

memberAppendRight :
  ∀ {ℓ} {A : Type ℓ} {x : A} →
  (left right : List A) →
  Reg.Member x right →
  Reg.Member x (left ++ right)
memberAppendRight [] right member =
  member
memberAppendRight (y ∷ left) right member =
  Reg.there (memberAppendRight left right member)

SimplePropertyUseCertificateResolver :
  Reg.RegularityContext Sem.PortableSignature →
  List PR.SimplePropertyUse →
  Type₀
SimplePropertyUseCertificateResolver context uses =
  (use : PR.SimplePropertyUse) →
  Reg.Member use uses →
  PortableSimplePropertyUseCertificate context use

SimplePropertyUseNoCompositePredecessorResolver :
  Reg.RegularityContext Sem.PortableSignature →
  List PR.SimplePropertyUse →
  Type₀
SimplePropertyUseNoCompositePredecessorResolver context uses =
  (use : PR.SimplePropertyUse) →
  Reg.Member use uses →
  SimplePropertyUseNoCompositePredecessor context use

simplePropertyUseResolverAppendLeft :
  ∀ {context} →
  (left right : List PR.SimplePropertyUse) →
  SimplePropertyUseCertificateResolver context (left ++ right) →
  SimplePropertyUseCertificateResolver context left
simplePropertyUseResolverAppendLeft left right resolver use member =
  resolver use (memberAppendLeft left right member)

simplePropertyUseResolverAppendRight :
  ∀ {context} →
  (left right : List PR.SimplePropertyUse) →
  SimplePropertyUseCertificateResolver context (left ++ right) →
  SimplePropertyUseCertificateResolver context right
simplePropertyUseResolverAppendRight left right resolver use member =
  resolver use (memberAppendRight left right member)

simplePropertyUseNoCompositeResolverAppendLeft :
  ∀ {context} →
  (left right : List PR.SimplePropertyUse) →
  SimplePropertyUseNoCompositePredecessorResolver context (left ++ right) →
  SimplePropertyUseNoCompositePredecessorResolver context left
simplePropertyUseNoCompositeResolverAppendLeft left right resolver use member =
  resolver use (memberAppendLeft left right member)

simplePropertyUseNoCompositeResolverAppendRight :
  ∀ {context} →
  (left right : List PR.SimplePropertyUse) →
  SimplePropertyUseNoCompositePredecessorResolver context (left ++ right) →
  SimplePropertyUseNoCompositePredecessorResolver context right
simplePropertyUseNoCompositeResolverAppendRight left right resolver use member =
  resolver use (memberAppendRight left right member)

portableFactSimplePropertyUseCertificateResolverFromReport :
  (report : PR.RegularityReport) →
  RegularityReportSimplePropertyViolationsComputed report →
  PR.NoReportSimplePropertyViolations report →
  SimplePropertyUseNoCompositePredecessorResolver
    (portableFactRegularityContext
      (PR.regularityReportCompositeObjectPropertyFacts report)
      (PR.regularityReportPropertyHierarchyFacts report))
    (PR.regularityReportSimplePropertyUses report) →
  SimplePropertyUseCertificateResolver
    (portableFactRegularityContext
      (PR.regularityReportCompositeObjectPropertyFacts report)
      (PR.regularityReportPropertyHierarchyFacts report))
    (PR.regularityReportSimplePropertyUses report)
portableFactSimplePropertyUseCertificateResolverFromReport
  report
  violationsComputed
  clean
  noCompositeResolver
  use
  member =
  portableFactSimplePropertyUseCertificateFromReport
    report
    violationsComputed
    clean
    use
    member
    (noCompositeResolver use member)

portableFactSimplePropertyUseCertificateResolverFromGeneratedReport :
  (document : P.OntologyDocument) →
  PR.NoReportSimplePropertyViolations (PR.reportRegularity document) →
  SimplePropertyUseNoCompositePredecessorResolver
    (generatedRegularityContext document)
    (PR.regularityReportSimplePropertyUses (PR.reportRegularity document)) →
  SimplePropertyUseCertificateResolver
    (generatedRegularityContext document)
    (PR.regularityReportSimplePropertyUses (PR.reportRegularity document))
portableFactSimplePropertyUseCertificateResolverFromGeneratedReport
  document
  clean
  noCompositeResolver =
  portableFactSimplePropertyUseCertificateResolverFromReport
    (PR.reportRegularity document)
    (generatedRegularityReportSimplePropertyViolationsComputed document)
    clean
    noCompositeResolver

portableSimpleObjectPropertyExpressionCertificateFromUse :
  ∀ {context source kind property} →
  PortableSimplePropertyUseCertificate
    context
    (PR.simplePropertyUse
      source
      kind
      property
      (PR.objectPropertyBaseKey property)) →
  PortableSimpleObjectPropertyExpressionCertificate context property
portableSimpleObjectPropertyExpressionCertificateFromUse certificate =
  portableSimpleObjectPropertyExpressionCertificate
    (portableUseCanonical certificate)
    (portableUseNoCompositePredecessor certificate)

portableSimpleObjectPropertyExpressionCertificateFromResolver :
  ∀ {context uses source kind property} →
  SimplePropertyUseCertificateResolver context uses →
  Reg.Member
    (PR.simplePropertyUse
      source
      kind
      property
      (PR.objectPropertyBaseKey property))
    uses →
  PortableSimpleObjectPropertyExpressionCertificate context property
portableSimpleObjectPropertyExpressionCertificateFromResolver
  resolver
  member =
  portableSimpleObjectPropertyExpressionCertificateFromUse
    (resolver _ member)

mutual
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses :
    (context : Reg.RegularityContext Sem.PortableSignature) →
    (source : P.Annotated P.Axiom) →
    (class : P.ClassExpression) →
    SimplePropertyUseCertificateResolver
      context
      (PR.simplePropertyUsesForClassExpression source class) →
    PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate
      context
      class
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
    context source (P.namedClass c) resolver =
    tt*
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
    context source P.owlThing resolver =
    tt*
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
    context source P.owlNothing resolver =
    tt*
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
    context source (P.objectIntersectionOf classes) resolver =
    portableClassExpressionsTwoOrMoreUseOnlySimpleObjectPropertiesCertificateFromUses
      context
      source
      classes
      resolver
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
    context source (P.objectUnionOf classes) resolver =
    portableClassExpressionsTwoOrMoreUseOnlySimpleObjectPropertiesCertificateFromUses
      context
      source
      classes
      resolver
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
    context source (P.objectComplementOf class) resolver =
    portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
      context
      source
      class
      resolver
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
    context source (P.objectOneOf individuals) resolver =
    tt*
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
    context source (P.objectSomeValuesFrom property class) resolver =
    portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
      context
      source
      class
      resolver
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
    context source (P.objectAllValuesFrom property class) resolver =
    portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
      context
      source
      class
      resolver
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
    context source (P.objectHasValue property individual) resolver =
    tt*
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
    context source (P.objectHasSelf property) resolver =
    portableSimpleObjectPropertyExpressionCertificateFromResolver
      resolver
      Reg.here
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
    context source (P.objectMinCardinality n property qualifier) resolver =
    portableSimpleObjectPropertyExpressionCertificateFromResolver
      resolver
      Reg.here
    ,
    portableOptionalClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
      context
      source
      qualifier
      (simplePropertyUseResolverAppendRight
        (PR.simplePropertyUseAt
          source
          (PR.objectMinCardinalityUse n)
          property)
        (PR.simplePropertyUsesForOptionalClassExpression source qualifier)
        resolver)
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
    context source (P.objectMaxCardinality n property qualifier) resolver =
    portableSimpleObjectPropertyExpressionCertificateFromResolver
      resolver
      Reg.here
    ,
    portableOptionalClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
      context
      source
      qualifier
      (simplePropertyUseResolverAppendRight
        (PR.simplePropertyUseAt
          source
          (PR.objectMaxCardinalityUse n)
          property)
        (PR.simplePropertyUsesForOptionalClassExpression source qualifier)
        resolver)
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
    context source (P.objectExactCardinality n property qualifier) resolver =
    portableSimpleObjectPropertyExpressionCertificateFromResolver
      resolver
      Reg.here
    ,
    portableOptionalClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
      context
      source
      qualifier
      (simplePropertyUseResolverAppendRight
        (PR.simplePropertyUseAt
          source
          (PR.objectExactCardinalityUse n)
          property)
        (PR.simplePropertyUsesForOptionalClassExpression source qualifier)
        resolver)
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
    context source (P.dataSomeValuesFrom property range) resolver =
    tt*
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
    context source (P.dataAllValuesFrom property range) resolver =
    tt*
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
    context source (P.dataHasValue property literal) resolver =
    tt*
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
    context source (P.dataMinCardinality n property qualifier) resolver =
    tt*
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
    context source (P.dataMaxCardinality n property qualifier) resolver =
    tt*
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
    context source (P.dataExactCardinality n property qualifier) resolver =
    tt*

  portableClassExpressionsUseOnlySimpleObjectPropertiesCertificateFromUses :
    (context : Reg.RegularityContext Sem.PortableSignature) →
    (source : P.Annotated P.Axiom) →
    (classes : List P.ClassExpression) →
    SimplePropertyUseCertificateResolver
      context
      (PR.simplePropertyUsesForClassExpressions source classes) →
    PortableClassExpressionsUseOnlySimpleObjectPropertiesCertificate
      context
      classes
  portableClassExpressionsUseOnlySimpleObjectPropertiesCertificateFromUses
    context source [] resolver =
    tt*
  portableClassExpressionsUseOnlySimpleObjectPropertiesCertificateFromUses
    context source (class ∷ classes) resolver =
    portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
      context
      source
      class
      (simplePropertyUseResolverAppendLeft
        (PR.simplePropertyUsesForClassExpression source class)
        (PR.simplePropertyUsesForClassExpressions source classes)
        resolver)
    ,
    portableClassExpressionsUseOnlySimpleObjectPropertiesCertificateFromUses
      context
      source
      classes
      (simplePropertyUseResolverAppendRight
        (PR.simplePropertyUsesForClassExpression source class)
        (PR.simplePropertyUsesForClassExpressions source classes)
        resolver)

  portableClassExpressionsTwoOrMoreUseOnlySimpleObjectPropertiesCertificateFromUses :
    (context : Reg.RegularityContext Sem.PortableSignature) →
    (source : P.Annotated P.Axiom) →
    (classes : P.TwoOrMore P.ClassExpression) →
    SimplePropertyUseCertificateResolver
      context
      (PR.simplePropertyUsesForClassExpressionsTwoOrMore source classes) →
    PortableClassExpressionsTwoOrMoreUseOnlySimpleObjectPropertiesCertificate
      context
      classes
  portableClassExpressionsTwoOrMoreUseOnlySimpleObjectPropertiesCertificateFromUses
    context
    source
    classes
    resolver =
    portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
      context
      source
      (P.first classes)
      (simplePropertyUseResolverAppendLeft
        firstUses
        tailUses
        resolver)
    ,
    portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
      context
      source
      (P.second classes)
      (simplePropertyUseResolverAppendLeft
        secondUses
        restUses
        tailResolver)
    ,
    portableClassExpressionsUseOnlySimpleObjectPropertiesCertificateFromUses
      context
      source
      (P.rest classes)
      (simplePropertyUseResolverAppendRight
        secondUses
        restUses
        tailResolver)
    where
    firstUses : List PR.SimplePropertyUse
    firstUses =
      PR.simplePropertyUsesForClassExpression source (P.first classes)

    secondUses : List PR.SimplePropertyUse
    secondUses =
      PR.simplePropertyUsesForClassExpression source (P.second classes)

    restUses : List PR.SimplePropertyUse
    restUses =
      PR.simplePropertyUsesForClassExpressions source (P.rest classes)

    tailUses : List PR.SimplePropertyUse
    tailUses =
      secondUses ++ restUses

    tailResolver :
      SimplePropertyUseCertificateResolver context tailUses
    tailResolver =
      simplePropertyUseResolverAppendRight
        firstUses
        tailUses
        resolver

  portableOptionalClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses :
    (context : Reg.RegularityContext Sem.PortableSignature) →
    (source : P.Annotated P.Axiom) →
    (class : Optional P.ClassExpression) →
    SimplePropertyUseCertificateResolver
      context
      (PR.simplePropertyUsesForOptionalClassExpression source class) →
    PortableOptionalClassExpressionUsesOnlySimpleObjectPropertiesCertificate
      context
      class
  portableOptionalClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
    context source absent resolver =
    tt*
  portableOptionalClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
    context source (present class) resolver =
    portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
      context
      source
      class
      resolver

portableObjectPropertyExpressionsSimpleCertificateFromUses :
  (context : Reg.RegularityContext Sem.PortableSignature) →
  (source : P.Annotated P.Axiom) →
  (kind : PR.SimplePropertyUseKind) →
  (properties : List P.ObjectPropertyExpression) →
  SimplePropertyUseCertificateResolver
    context
    (PR.simplePropertyUsesForProperties source kind properties) →
  PortableObjectPropertyExpressionsSimpleCertificate context properties
portableObjectPropertyExpressionsSimpleCertificateFromUses
  context source kind [] resolver =
  tt*
portableObjectPropertyExpressionsSimpleCertificateFromUses
  context source kind (property ∷ properties) resolver =
  portableSimpleObjectPropertyExpressionCertificateFromResolver
    resolver
    Reg.here
  ,
  portableObjectPropertyExpressionsSimpleCertificateFromUses
    context
    source
    kind
    properties
    (simplePropertyUseResolverAppendRight
      (PR.simplePropertyUseAt source kind property)
      (PR.simplePropertyUsesForProperties source kind properties)
      resolver)

portableObjectPropertyExpressionsTwoOrMoreSimpleCertificateFromUses :
  (context : Reg.RegularityContext Sem.PortableSignature) →
  (source : P.Annotated P.Axiom) →
  (kind : PR.SimplePropertyUseKind) →
  (properties : P.TwoOrMore P.ObjectPropertyExpression) →
  SimplePropertyUseCertificateResolver
    context
    (PR.simplePropertyUsesForPropertiesTwoOrMore source kind properties) →
  PortableObjectPropertyExpressionsTwoOrMoreSimpleCertificate
    context
    properties
portableObjectPropertyExpressionsTwoOrMoreSimpleCertificateFromUses
  context
  source
  kind
  properties
  resolver =
  portableSimpleObjectPropertyExpressionCertificateFromResolver
    resolver
    Reg.here
  ,
  portableSimpleObjectPropertyExpressionCertificateFromResolver
    tailResolver
    Reg.here
  ,
  portableObjectPropertyExpressionsSimpleCertificateFromUses
    context
    source
    kind
    (P.rest properties)
    (simplePropertyUseResolverAppendRight
      secondUses
      restUses
      tailResolver)
  where
  firstUses : List PR.SimplePropertyUse
  firstUses =
    PR.simplePropertyUseAt source kind (P.first properties)

  secondUses : List PR.SimplePropertyUse
  secondUses =
    PR.simplePropertyUseAt source kind (P.second properties)

  restUses : List PR.SimplePropertyUse
  restUses =
    PR.simplePropertyUsesForProperties source kind (P.rest properties)

  tailUses : List PR.SimplePropertyUse
  tailUses =
    secondUses ++ restUses

  tailResolver :
    SimplePropertyUseCertificateResolver context tailUses
  tailResolver =
    simplePropertyUseResolverAppendRight firstUses tailUses resolver

portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses :
  (context : Reg.RegularityContext Sem.PortableSignature) →
  (source : P.Annotated P.Axiom) →
  (axiom : P.Axiom) →
  SimplePropertyUseCertificateResolver
    context
    (PR.simplePropertyUsesForAxiom source axiom) →
  PortableAxiomUsesOnlySimpleObjectPropertiesCertificate context axiom
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.declaration entity) resolver =
  tt*
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.subClassOf left right) resolver =
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
    context
    source
    left
    (simplePropertyUseResolverAppendLeft
      (PR.simplePropertyUsesForClassExpression source left)
      (PR.simplePropertyUsesForClassExpression source right)
      resolver)
  ,
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
    context
    source
    right
    (simplePropertyUseResolverAppendRight
      (PR.simplePropertyUsesForClassExpression source left)
      (PR.simplePropertyUsesForClassExpression source right)
      resolver)
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.equivalentClasses classes) resolver =
  portableClassExpressionsUseOnlySimpleObjectPropertiesCertificateFromUses
    context
    source
    (Sem.twoOrMoreToList classes)
    resolver
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.disjointClasses classes) resolver =
  portableClassExpressionsUseOnlySimpleObjectPropertiesCertificateFromUses
    context
    source
    (Sem.twoOrMoreToList classes)
    resolver
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.disjointUnion class classes) resolver =
  portableClassExpressionsUseOnlySimpleObjectPropertiesCertificateFromUses
    context
    source
    (Sem.twoOrMoreToList classes)
    resolver
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.subObjectPropertyOf sub super) resolver =
  tt*
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.equivalentObjectProperties properties) resolver =
  tt*
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.disjointObjectProperties properties) resolver =
  portableObjectPropertyExpressionsTwoOrMoreSimpleCertificateFromUses
    context
    source
    PR.disjointObjectPropertiesUse
    properties
    resolver
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.inverseObjectProperties left right) resolver =
  tt*
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.objectPropertyDomain property class) resolver =
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
    context
    source
    class
    resolver
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.objectPropertyRange property class) resolver =
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
    context
    source
    class
    resolver
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.functionalObjectProperty property) resolver =
  portableSimpleObjectPropertyExpressionCertificateFromResolver
    resolver
    Reg.here
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.inverseFunctionalObjectProperty property) resolver =
  portableSimpleObjectPropertyExpressionCertificateFromResolver
    resolver
    Reg.here
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.reflexiveObjectProperty property) resolver =
  tt*
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.irreflexiveObjectProperty property) resolver =
  portableSimpleObjectPropertyExpressionCertificateFromResolver
    resolver
    Reg.here
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.symmetricObjectProperty property) resolver =
  tt*
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.asymmetricObjectProperty property) resolver =
  portableSimpleObjectPropertyExpressionCertificateFromResolver
    resolver
    Reg.here
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.transitiveObjectProperty property) resolver =
  tt*
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.subDataPropertyOf sub super) resolver =
  tt*
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.equivalentDataProperties properties) resolver =
  tt*
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.disjointDataProperties properties) resolver =
  tt*
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.dataPropertyDomain property class) resolver =
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
    context
    source
    class
    resolver
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.dataPropertyRange property range) resolver =
  tt*
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.functionalDataProperty property) resolver =
  tt*
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.datatypeDefinition datatype range) resolver =
  tt*
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.hasKey class key) resolver =
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
    context
    source
    class
    resolver
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.sameIndividual individuals) resolver =
  tt*
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.differentIndividuals individuals) resolver =
  tt*
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.classAssertion class individual) resolver =
  portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateFromUses
    context
    source
    class
    resolver
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.objectPropertyAssertion property subject object) resolver =
  tt*
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.negativeObjectPropertyAssertion property subject object) resolver =
  tt*
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.dataPropertyAssertion property subject value) resolver =
  tt*
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.negativeDataPropertyAssertion property subject value) resolver =
  tt*
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.annotationAssertion property subject value) resolver =
  tt*
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.subAnnotationPropertyOf left right) resolver =
  tt*
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.annotationPropertyDomain property domain) resolver =
  tt*
portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context source (P.annotationPropertyRange property range) resolver =
  tt*

translatedPortableAxiomUsesOnlySimpleObjectProperties :
  (context : Reg.RegularityContext Sem.PortableSignature) →
  (axiom : P.Axiom) →
  PortableAxiomUsesOnlySimpleObjectPropertiesCertificate context axiom →
  TranslatedAxiomsUseOnlySimpleObjectProperties
    context
    (Sem.translateAxiom axiom)
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.declaration e)
  certificate =
  tt* ,
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.subClassOf c d)
  (cCertificate , dCertificate)
  with Sem.translateClassExpression c
     | Sem.translateClassExpression d
     | portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
         {context = context}
         {class = c}
         cCertificate
     | portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
         {context = context}
         {class = d}
         dCertificate
... | present c′ | present d′ | cProof | dProof =
  (cProof , dProof) ,
  tt*
... | absent | d′ | cProof | dProof =
  tt*
... | present c′ | absent | cProof | dProof =
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.equivalentClasses classes)
  certificate
  with Sem.translateClassExpressionList (Sem.twoOrMoreToList classes)
     | portableClassExpressionsUseOnlySimpleObjectPropertiesCertificateToSyntax
         {context = context}
         {classes = Sem.twoOrMoreToList classes}
         certificate
... | present classes′ | proof =
  proof ,
  tt*
... | absent | proof =
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.disjointClasses classes)
  certificate
  with Sem.translateClassExpressionList (Sem.twoOrMoreToList classes)
     | portableClassExpressionsUseOnlySimpleObjectPropertiesCertificateToSyntax
         {context = context}
         {classes = Sem.twoOrMoreToList classes}
         certificate
... | present classes′ | proof =
  proof ,
  tt*
... | absent | proof =
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.disjointUnion c classes)
  certificate
  with Sem.translateClassExpressionList (Sem.twoOrMoreToList classes)
     | portableClassExpressionsUseOnlySimpleObjectPropertiesCertificateToSyntax
         {context = context}
         {classes = Sem.twoOrMoreToList classes}
         certificate
... | present classes′ | proof =
  (tt* , (proof , tt*)) ,
  (proof , tt*)
... | absent | proof =
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.subObjectPropertyOf sub super)
  certificate =
  tt* ,
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.equivalentObjectProperties properties)
  certificate =
  tt* ,
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.disjointObjectProperties properties)
  certificate =
  portableObjectPropertyExpressionsTwoOrMoreSimpleCertificateToSyntax
    certificate
  ,
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.inverseObjectProperties p q)
  certificate =
  tt* ,
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.objectPropertyDomain p class)
  certificate
  with Sem.translateClassExpression class
     | portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
         {context = context}
         {class = class}
         certificate
... | present class′ | proof =
  proof ,
  tt*
... | absent | proof =
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.objectPropertyRange p class)
  certificate
  with Sem.translateClassExpression class
     | portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
         {context = context}
         {class = class}
         certificate
... | present class′ | proof =
  proof ,
  tt*
... | absent | proof =
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.functionalObjectProperty property)
  certificate =
  portableSimpleObjectPropertyExpressionCertificateToSyntax certificate ,
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.inverseFunctionalObjectProperty property)
  certificate =
  portableSimpleObjectPropertyExpressionCertificateToSyntax certificate ,
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.reflexiveObjectProperty property)
  certificate =
  tt* ,
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.irreflexiveObjectProperty property)
  certificate =
  portableSimpleObjectPropertyExpressionCertificateToSyntax certificate ,
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.symmetricObjectProperty property)
  certificate =
  tt* ,
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.asymmetricObjectProperty property)
  certificate =
  portableSimpleObjectPropertyExpressionCertificateToSyntax certificate ,
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.transitiveObjectProperty property)
  certificate =
  tt* ,
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.subDataPropertyOf sub super)
  certificate =
  tt* ,
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.equivalentDataProperties properties)
  certificate =
  tt* ,
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.disjointDataProperties properties)
  certificate =
  tt* ,
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.dataPropertyDomain p class)
  certificate
  with Sem.translateClassExpression class
     | portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
         {context = context}
         {class = class}
         certificate
... | present class′ | proof =
  proof ,
  tt*
... | absent | proof =
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.dataPropertyRange p range)
  certificate
  with Sem.translateDataRange range
... | present range′ =
  tt* ,
  tt*
... | absent =
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.functionalDataProperty property)
  certificate =
  tt* ,
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.datatypeDefinition datatype range)
  certificate
  with Sem.translateDataRange range
... | present range′ =
  tt* ,
  tt*
... | absent =
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.hasKey class key)
  certificate
  with Sem.translateClassExpression class
     | portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
         {context = context}
         {class = class}
         certificate
... | present class′ | proof =
  proof ,
  tt*
... | absent | proof =
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.sameIndividual individuals)
  certificate =
  tt* ,
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.differentIndividuals individuals)
  certificate =
  tt* ,
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.classAssertion class individual)
  certificate
  with Sem.translateClassExpression class
     | portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
         {context = context}
         {class = class}
         certificate
... | present class′ | proof =
  proof ,
  tt*
... | absent | proof =
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.objectPropertyAssertion property source target)
  certificate =
  tt* ,
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.negativeObjectPropertyAssertion property source target)
  certificate =
  tt* ,
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.dataPropertyAssertion property source literal)
  certificate =
  tt* ,
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.negativeDataPropertyAssertion property source literal)
  certificate =
  tt* ,
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.annotationAssertion property subject value)
  certificate =
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.subAnnotationPropertyOf sub super)
  certificate =
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.annotationPropertyDomain property targetIRI)
  certificate =
  tt*
translatedPortableAxiomUsesOnlySimpleObjectProperties
  context
  (P.annotationPropertyRange property targetIRI)
  certificate =
  tt*

AnnotatedAxiomUsesOnlySimpleObjectProperties :
  Reg.RegularityContext Sem.PortableSignature →
  P.Annotated P.Axiom →
  Type₀
AnnotatedAxiomUsesOnlySimpleObjectProperties context ax =
  Reg.AxiomsUseOnlySimpleObjectProperties
    context
    (Sem.semanticAxioms (Sem.translateAnnotatedAxiom ax))

AnnotatedAxiomUsesOnlySimpleObjectPropertiesCertificate :
  Reg.RegularityContext Sem.PortableSignature →
  P.Annotated P.Axiom →
  Type₀
AnnotatedAxiomUsesOnlySimpleObjectPropertiesCertificate context ax =
  PortableAxiomUsesOnlySimpleObjectPropertiesCertificate
    context
    (P.body ax)

AnnotatedAxiomsUseOnlySimpleObjectProperties :
  Reg.RegularityContext Sem.PortableSignature →
  List (P.Annotated P.Axiom) →
  Type₀
AnnotatedAxiomsUseOnlySimpleObjectProperties context [] =
  Unit*
AnnotatedAxiomsUseOnlySimpleObjectProperties context (ax ∷ axioms) =
  AnnotatedAxiomUsesOnlySimpleObjectProperties context ax
  ×
  AnnotatedAxiomsUseOnlySimpleObjectProperties context axioms

AnnotatedAxiomsUseOnlySimpleObjectPropertiesCertificate :
  Reg.RegularityContext Sem.PortableSignature →
  List (P.Annotated P.Axiom) →
  Type₀
AnnotatedAxiomsUseOnlySimpleObjectPropertiesCertificate context [] =
  Unit*
AnnotatedAxiomsUseOnlySimpleObjectPropertiesCertificate
  context
  (ax ∷ axioms) =
  AnnotatedAxiomUsesOnlySimpleObjectPropertiesCertificate context ax
  ×
  AnnotatedAxiomsUseOnlySimpleObjectPropertiesCertificate context axioms

translatedAnnotatedAxiomUsesOnlySimpleObjectProperties :
  (context : Reg.RegularityContext Sem.PortableSignature) →
  (ax : P.Annotated P.Axiom) →
  AnnotatedAxiomUsesOnlySimpleObjectProperties context ax →
  Reg.AxiomsUseOnlySimpleObjectProperties
    context
    (Sem.semanticAxioms (Sem.translateAnnotatedAxiom ax))
translatedAnnotatedAxiomUsesOnlySimpleObjectProperties context ax proof =
  proof

translatedAnnotatedAxiomUsesOnlySimpleObjectPropertiesCertificate :
  (context : Reg.RegularityContext Sem.PortableSignature) →
  (ax : P.Annotated P.Axiom) →
  AnnotatedAxiomUsesOnlySimpleObjectPropertiesCertificate context ax →
  AnnotatedAxiomUsesOnlySimpleObjectProperties context ax
translatedAnnotatedAxiomUsesOnlySimpleObjectPropertiesCertificate
  context
  (P.annotated annotations body)
  certificate
  with Sem.translateAxiom body
     | translatedPortableAxiomUsesOnlySimpleObjectProperties
         context
         body
         certificate
... | present axioms | proof =
  proof
... | absent | proof =
  proof

translatedAnnotatedAxiomsUseOnlySimpleObjectProperties :
  (context : Reg.RegularityContext Sem.PortableSignature) →
  (axioms : List (P.Annotated P.Axiom)) →
  AnnotatedAxiomsUseOnlySimpleObjectProperties context axioms →
  Reg.AxiomsUseOnlySimpleObjectProperties
    context
    (Sem.semanticAxioms (Sem.translateAnnotatedAxioms axioms))
translatedAnnotatedAxiomsUseOnlySimpleObjectProperties context [] proof =
  tt*
translatedAnnotatedAxiomsUseOnlySimpleObjectProperties
  context
  (ax ∷ axioms)
  (axProof , axiomsProof) =
  Reg.axiomsUseOnlySimpleObjectPropertiesAppend
    {context = context}
    {left = Sem.semanticAxioms (Sem.translateAnnotatedAxiom ax)}
    {right = Sem.semanticAxioms (Sem.translateAnnotatedAxioms axioms)}
    axProof
    (translatedAnnotatedAxiomsUseOnlySimpleObjectProperties
      context
      axioms
      axiomsProof)

translatedAnnotatedAxiomsUseOnlySimpleObjectPropertiesCertificate :
  (context : Reg.RegularityContext Sem.PortableSignature) →
  (axioms : List (P.Annotated P.Axiom)) →
  AnnotatedAxiomsUseOnlySimpleObjectPropertiesCertificate context axioms →
  Reg.AxiomsUseOnlySimpleObjectProperties
    context
    (Sem.semanticAxioms (Sem.translateAnnotatedAxioms axioms))
translatedAnnotatedAxiomsUseOnlySimpleObjectPropertiesCertificate
  context
  []
  proof =
  tt*
translatedAnnotatedAxiomsUseOnlySimpleObjectPropertiesCertificate
  context
  (ax ∷ axioms)
  (axProof , axiomsProof) =
  Reg.axiomsUseOnlySimpleObjectPropertiesAppend
    {context = context}
    {left = Sem.semanticAxioms (Sem.translateAnnotatedAxiom ax)}
    {right = Sem.semanticAxioms (Sem.translateAnnotatedAxioms axioms)}
    (translatedAnnotatedAxiomUsesOnlySimpleObjectPropertiesCertificate
      context
      ax
      axProof)
    (translatedAnnotatedAxiomsUseOnlySimpleObjectPropertiesCertificate
      context
      axioms
      axiomsProof)

OntologyUsesOnlySimpleObjectPropertiesCertificate :
  Reg.RegularityContext Sem.PortableSignature →
  P.Ontology →
  Type₀
OntologyUsesOnlySimpleObjectPropertiesCertificate context ont =
  AnnotatedAxiomsUseOnlySimpleObjectPropertiesCertificate
    context
    (P.axioms ont)

OntologyDocumentUsesOnlySimpleObjectPropertiesCertificate :
  Reg.RegularityContext Sem.PortableSignature →
  P.OntologyDocument →
  Type₀
OntologyDocumentUsesOnlySimpleObjectPropertiesCertificate context document =
  OntologyUsesOnlySimpleObjectPropertiesCertificate
    context
    (P.documentOntology document)

ontologyUsesOnlySimpleObjectPropertiesCertificateToTranslatedAxioms :
  (context : Reg.RegularityContext Sem.PortableSignature) →
  (ont : P.Ontology) →
  OntologyUsesOnlySimpleObjectPropertiesCertificate context ont →
  Reg.AxiomsUseOnlySimpleObjectProperties
    context
    (Sem.semanticAxioms (Sem.translateAnnotatedAxioms (P.axioms ont)))
ontologyUsesOnlySimpleObjectPropertiesCertificateToTranslatedAxioms
  context
  ont
  certificate =
  translatedAnnotatedAxiomsUseOnlySimpleObjectPropertiesCertificate
    context
    (P.axioms ont)
    certificate

ontologyDocumentUsesOnlySimpleObjectPropertiesCertificateToTranslatedAxioms :
  (context : Reg.RegularityContext Sem.PortableSignature) →
  (document : P.OntologyDocument) →
  OntologyDocumentUsesOnlySimpleObjectPropertiesCertificate context document →
  Reg.AxiomsUseOnlySimpleObjectProperties
    context
    (Sem.semanticAxioms
      (Sem.translateAnnotatedAxioms
        (P.axioms (P.documentOntology document))))
ontologyDocumentUsesOnlySimpleObjectPropertiesCertificateToTranslatedAxioms
  context
  document
  certificate =
  ontologyUsesOnlySimpleObjectPropertiesCertificateToTranslatedAxioms
    context
    (P.documentOntology document)
    certificate

annotatedAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses :
  (context : Reg.RegularityContext Sem.PortableSignature) →
  (ax : P.Annotated P.Axiom) →
  SimplePropertyUseCertificateResolver
    context
    (PR.simplePropertyUsesForAnnotatedAxiom ax) →
  AnnotatedAxiomUsesOnlySimpleObjectPropertiesCertificate context ax
annotatedAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
  context
  ax
  resolver =
  portableAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
    context
    ax
    (P.body ax)
    resolver

annotatedAxiomsUseOnlySimpleObjectPropertiesCertificateFromUses :
  (context : Reg.RegularityContext Sem.PortableSignature) →
  (axioms : List (P.Annotated P.Axiom)) →
  SimplePropertyUseCertificateResolver
    context
    (PR.simplePropertyUsesForAnnotatedAxioms axioms) →
  AnnotatedAxiomsUseOnlySimpleObjectPropertiesCertificate context axioms
annotatedAxiomsUseOnlySimpleObjectPropertiesCertificateFromUses
  context
  []
  resolver =
  tt*
annotatedAxiomsUseOnlySimpleObjectPropertiesCertificateFromUses
  context
  (ax ∷ axioms)
  resolver =
  annotatedAxiomUsesOnlySimpleObjectPropertiesCertificateFromUses
    context
    ax
    (simplePropertyUseResolverAppendLeft
      (PR.simplePropertyUsesForAnnotatedAxiom ax)
      (PR.simplePropertyUsesForAnnotatedAxioms axioms)
      resolver)
  ,
  annotatedAxiomsUseOnlySimpleObjectPropertiesCertificateFromUses
    context
    axioms
    (simplePropertyUseResolverAppendRight
      (PR.simplePropertyUsesForAnnotatedAxiom ax)
      (PR.simplePropertyUsesForAnnotatedAxioms axioms)
      resolver)

ontologyUsesOnlySimpleObjectPropertiesCertificateFromUseResolver :
  (context : Reg.RegularityContext Sem.PortableSignature) →
  (ont : P.Ontology) →
  SimplePropertyUseCertificateResolver
    context
    (PR.ontologySimplePropertyUses ont) →
  OntologyUsesOnlySimpleObjectPropertiesCertificate context ont
ontologyUsesOnlySimpleObjectPropertiesCertificateFromUseResolver
  context
  ont
  resolver =
  annotatedAxiomsUseOnlySimpleObjectPropertiesCertificateFromUses
    context
    (P.axioms ont)
    resolver

ontologyDocumentUsesOnlySimpleObjectPropertiesCertificateFromUseResolver :
  (context : Reg.RegularityContext Sem.PortableSignature) →
  (document : P.OntologyDocument) →
  SimplePropertyUseCertificateResolver
    context
    (PR.ontologyDocumentSimplePropertyUses document) →
  OntologyDocumentUsesOnlySimpleObjectPropertiesCertificate context document
ontologyDocumentUsesOnlySimpleObjectPropertiesCertificateFromUseResolver
  context
  document
  resolver =
  ontologyUsesOnlySimpleObjectPropertiesCertificateFromUseResolver
    context
    (P.documentOntology document)
    resolver

ontologyDocumentUsesOnlySimpleObjectPropertiesCertificateFromGeneratedUseResolver :
  (document : P.OntologyDocument) →
  SimplePropertyUseCertificateResolver
    (generatedRegularityContext document)
    (PR.regularityReportSimplePropertyUses (PR.reportRegularity document)) →
  OntologyDocumentUsesOnlySimpleObjectPropertiesCertificate
    (generatedRegularityContext document)
    document
ontologyDocumentUsesOnlySimpleObjectPropertiesCertificateFromGeneratedUseResolver
  document
  resolver =
  ontologyDocumentUsesOnlySimpleObjectPropertiesCertificateFromUseResolver
    (generatedRegularityContext document)
    document
    resolver

ontologyDocumentUsesOnlySimpleObjectPropertiesFromGeneratedUseResolver :
  (document : P.OntologyDocument) →
  SimplePropertyUseCertificateResolver
    (generatedRegularityContext document)
    (PR.regularityReportSimplePropertyUses (PR.reportRegularity document)) →
  Reg.AxiomsUseOnlySimpleObjectProperties
    (generatedRegularityContext document)
    (Sem.semanticAxioms
      (Sem.translateAnnotatedAxioms
        (P.axioms (P.documentOntology document))))
ontologyDocumentUsesOnlySimpleObjectPropertiesFromGeneratedUseResolver
  document
  resolver =
  ontologyDocumentUsesOnlySimpleObjectPropertiesCertificateToTranslatedAxioms
    (generatedRegularityContext document)
    document
    (ontologyDocumentUsesOnlySimpleObjectPropertiesCertificateFromGeneratedUseResolver
      document
      resolver)

ontologyDocumentUsesOnlySimpleObjectPropertiesCertificateFromGeneratedCleanReportAndNoCompositeResolver :
  (document : P.OntologyDocument) →
  PR.NoReportSimplePropertyViolations (PR.reportRegularity document) →
  SimplePropertyUseNoCompositePredecessorResolver
    (generatedRegularityContext document)
    (PR.regularityReportSimplePropertyUses (PR.reportRegularity document)) →
  OntologyDocumentUsesOnlySimpleObjectPropertiesCertificate
    (generatedRegularityContext document)
    document
ontologyDocumentUsesOnlySimpleObjectPropertiesCertificateFromGeneratedCleanReportAndNoCompositeResolver
  document
  clean
  noCompositeResolver =
  ontologyDocumentUsesOnlySimpleObjectPropertiesCertificateFromGeneratedUseResolver
    document
    (portableFactSimplePropertyUseCertificateResolverFromGeneratedReport
      document
      clean
      noCompositeResolver)

ontologyDocumentUsesOnlySimpleObjectPropertiesFromGeneratedCleanReportAndNoCompositeResolver :
  (document : P.OntologyDocument) →
  PR.NoReportSimplePropertyViolations (PR.reportRegularity document) →
  SimplePropertyUseNoCompositePredecessorResolver
    (generatedRegularityContext document)
    (PR.regularityReportSimplePropertyUses (PR.reportRegularity document)) →
  Reg.AxiomsUseOnlySimpleObjectProperties
    (generatedRegularityContext document)
    (Sem.semanticAxioms
      (Sem.translateAnnotatedAxioms
        (P.axioms (P.documentOntology document))))
ontologyDocumentUsesOnlySimpleObjectPropertiesFromGeneratedCleanReportAndNoCompositeResolver
  document
  clean
  noCompositeResolver =
  ontologyDocumentUsesOnlySimpleObjectPropertiesCertificateToTranslatedAxioms
    (generatedRegularityContext document)
    document
    (ontologyDocumentUsesOnlySimpleObjectPropertiesCertificateFromGeneratedCleanReportAndNoCompositeResolver
      document
      clean
      noCompositeResolver)

portableAxiomsUseOnlySimpleObjectPropertiesAppend :
  ∀ {context}
    {left right : List (S.Axiom Sem.PortableSignature)} →
  Reg.AxiomsUseOnlySimpleObjectProperties context left →
  Reg.AxiomsUseOnlySimpleObjectProperties context right →
  Reg.AxiomsUseOnlySimpleObjectProperties context (left ++ right)
portableAxiomsUseOnlySimpleObjectPropertiesAppend =
  Reg.axiomsUseOnlySimpleObjectPropertiesAppend