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

module OWL2.Portable.RegularityRankProof where

open import Cubical.Data.Nat.Base using (zero; suc)
import Cubical.Data.Nat.Order as NatOrder
open import OWL2.Prelude
import OWL2.Portable.Equality as Equality
import OWL2.Portable.ObjectPropertyKeys as Keys
import OWL2.Portable.RegularityRank as Rank
import OWL2.Portable.Semantics as Sem
import OWL2.Portable.Syntax as P
import OWL2.Syntax as S
import OWL2.Syntax.Regularity as Reg

open import OWL2.Portable.ObjectPropertyKeys public
  using
    ( syntaxObjectPropertyBaseKey
    ; syntaxObjectPropertyBaseKeyInverse
    ; syntaxObjectPropertyBaseKeyTranslate
    )

rankForSyntaxObjectPropertyExpression :
  List Rank.PropertyRank →
  S.ObjectPropertyExpression Sem.PortableSignature →
  Optional ℕ
rankForSyntaxObjectPropertyExpression ranks property =
  Rank.rankForKey (Keys.syntaxObjectPropertyBaseKey property) ranks

rankForSyntaxObjectPropertyExpressionInverse :
  (ranks : List Rank.PropertyRank) →
  (property : S.ObjectPropertyExpression Sem.PortableSignature) →
  rankForSyntaxObjectPropertyExpression
    ranks
    (Reg.inverseObjectPropertyExpression property)
  ≡
  rankForSyntaxObjectPropertyExpression ranks property
rankForSyntaxObjectPropertyExpressionInverse ranks property =
  cong
    (λ key → Rank.rankForKey key ranks)
    (Keys.syntaxObjectPropertyBaseKeyInverse property)

optionalNatValueOr : ℕ → Optional ℕ → ℕ
optionalNatValueOr fallback absent =
  fallback
optionalNatValueOr fallback (present n) =
  n

presentNatInjective :
  ∀ {m n} → present m ≡ present n → m ≡ n
presentNatInjective {m = m} equality =
  cong (optionalNatValueOr m) equality

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

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

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

record RankedObjectPropertyLess
  (ranks : List Rank.PropertyRank)
  (lower upper : S.ObjectPropertyExpression Sem.PortableSignature)
  : Type₀ where
  constructor rankedObjectPropertyLess
  field
    lowerRank :
      ℕ
    upperRank :
      ℕ
    lowerRankLookup :
      rankForSyntaxObjectPropertyExpression ranks lower ≡ present lowerRank
    upperRankLookup :
      rankForSyntaxObjectPropertyExpression ranks upper ≡ present upperRank
    lowerRankBelowUpperRank :
      NatOrder._<_ lowerRank upperRank

open RankedObjectPropertyLess public

rankedObjectPropertyLessIrrefl :
  (ranks : List Rank.PropertyRank) →
  (property : S.ObjectPropertyExpression Sem.PortableSignature) →
  ¬ RankedObjectPropertyLess ranks property property
rankedObjectPropertyLessIrrefl ranks property less =
  NatOrder.¬m<m
    (subst
      (λ rank → NatOrder._<_ (lowerRank less) rank)
      (sym sameRank)
      (lowerRankBelowUpperRank less))
  where
  sameRank : lowerRank less ≡ upperRank less
  sameRank =
    presentNatInjective
      (sym (lowerRankLookup less) ∙ upperRankLookup less)

rankedObjectPropertyLessTrans :
  (ranks : List Rank.PropertyRank) →
  ∀ {lower middle upper} →
  RankedObjectPropertyLess ranks lower middle →
  RankedObjectPropertyLess ranks middle upper →
  RankedObjectPropertyLess ranks lower upper
rankedObjectPropertyLessTrans ranks lower<middle middle<upper =
  rankedObjectPropertyLess
    (lowerRank lower<middle)
    (upperRank middle<upper)
    (lowerRankLookup lower<middle)
    (upperRankLookup middle<upper)
    (NatOrder.<-trans
      (lowerRankBelowUpperRank lower<middle)
      middleRankBelowUpperRank)
  where
  sameMiddleRank :
    upperRank lower<middle ≡ lowerRank middle<upper
  sameMiddleRank =
    presentNatInjective
      (sym (upperRankLookup lower<middle)
       ∙ lowerRankLookup middle<upper)

  middleRankBelowUpperRank :
    NatOrder._<_ (upperRank lower<middle) (upperRank middle<upper)
  middleRankBelowUpperRank =
    subst
      (λ rank → NatOrder._<_ rank (upperRank middle<upper))
      (sym sameMiddleRank)
      (lowerRankBelowUpperRank middle<upper)

rankedObjectPropertyLessInversePreserves :
  (ranks : List Rank.PropertyRank) →
  ∀ {lower upper} →
  RankedObjectPropertyLess ranks lower upper →
  RankedObjectPropertyLess
    ranks
    (Reg.inverseObjectPropertyExpression lower)
    (Reg.inverseObjectPropertyExpression upper)
rankedObjectPropertyLessInversePreserves ranks {lower} {upper} less =
  rankedObjectPropertyLess
    (lowerRank less)
    (upperRank less)
    (rankForSyntaxObjectPropertyExpressionInverse ranks lower
     ∙ lowerRankLookup less)
    (rankForSyntaxObjectPropertyExpressionInverse ranks upper
     ∙ upperRankLookup less)
    (lowerRankBelowUpperRank less)

natLessThanTrueToLess :
  (m n : ℕ) →
  Rank.natLessThan m n ≡ true →
  NatOrder._<_ m n
natLessThanTrueToLess zero zero truth =
  absurd (falseNotTrue truth)
natLessThanTrueToLess zero (suc n) truth =
  NatOrder.suc-≤-suc NatOrder.zero-≤
natLessThanTrueToLess (suc m) zero truth =
  absurd (falseNotTrue truth)
natLessThanTrueToLess (suc m) (suc n) truth =
  NatOrder.suc-≤-suc (natLessThanTrueToLess m n truth)

rankedObjectPropertyLessCertificate :
  (ranks : List Rank.PropertyRank) →
  (lower upper : P.ObjectPropertyExpression) →
  Optional
    (RankedObjectPropertyLess
      ranks
      (Sem.translateObjectPropertyExpression lower)
      (Sem.translateObjectPropertyExpression upper))
rankedObjectPropertyLessCertificate ranks lower upper
  with rankForSyntaxObjectPropertyExpression
        ranks
        (Sem.translateObjectPropertyExpression lower)
        UsingEq
     | rankForSyntaxObjectPropertyExpression
        ranks
        (Sem.translateObjectPropertyExpression upper)
        UsingEq
... | present lowerRank , lowerLookup | present upperRank , upperLookup
  with Rank.natLessThan lowerRank upperRank UsingEq
... | true , below =
  present
    (rankedObjectPropertyLess
      lowerRank
      upperRank
      lowerLookup
      upperLookup
      (natLessThanTrueToLess lowerRank upperRank below))
... | false , below =
  absent
rankedObjectPropertyLessCertificate ranks lower upper
  | absent , lowerLookup
  | upperRank , upperLookup =
  absent
rankedObjectPropertyLessCertificate ranks lower upper
  | present lowerRank , lowerLookup
  | absent , upperLookup =
  absent

PortableObjectPropertyExpressionsLessThan :
  List Rank.PropertyRank →
  List P.ObjectPropertyExpression →
  P.ObjectPropertyExpression →
  Type₀
PortableObjectPropertyExpressionsLessThan ranks [] super =
  Unit*
PortableObjectPropertyExpressionsLessThan ranks (p ∷ ps) super =
  RankedObjectPropertyLess
    ranks
    (Sem.translateObjectPropertyExpression p)
    (Sem.translateObjectPropertyExpression super)
  ×
  PortableObjectPropertyExpressionsLessThan ranks ps super

portableObjectPropertyExpressionsLessThan :
  ∀ {ranks properties super} →
  PortableObjectPropertyExpressionsLessThan ranks properties super →
  Reg.ObjectPropertyExpressionsLessThan
    (RankedObjectPropertyLess ranks)
    (Sem.translateObjectPropertyExpressionList properties)
    (Sem.translateObjectPropertyExpression super)
portableObjectPropertyExpressionsLessThan {properties = []} proof =
  tt*
portableObjectPropertyExpressionsLessThan {properties = p ∷ ps} (p<super , ps<super) =
  p<super ,
  portableObjectPropertyExpressionsLessThan ps<super

portableObjectPropertyExpressionsLessThanCertificate :
  (ranks : List Rank.PropertyRank) →
  (properties : List P.ObjectPropertyExpression) →
  (super : P.ObjectPropertyExpression) →
  Optional (PortableObjectPropertyExpressionsLessThan ranks properties super)
portableObjectPropertyExpressionsLessThanCertificate ranks [] super =
  present tt*
portableObjectPropertyExpressionsLessThanCertificate ranks (p ∷ ps) super
  with rankedObjectPropertyLessCertificate ranks p super
     | portableObjectPropertyExpressionsLessThanCertificate ranks ps super
... | present p<super | present ps<super =
  present (p<super , ps<super)
... | absent | _ =
  absent
... | _ | absent =
  absent

data PortableRightRecursivePropertyChainByRank
  (ranks : List Rank.PropertyRank)
  : P.ObjectPropertyExpression →
    P.ObjectPropertyExpression →
    List P.ObjectPropertyExpression →
    P.ObjectPropertyExpression →
    Type₀ where
  portableRightRecursiveTwo :
    ∀ {p super} →
    RankedObjectPropertyLess
      ranks
      (Sem.translateObjectPropertyExpression p)
      (Sem.translateObjectPropertyExpression super) →
    PortableRightRecursivePropertyChainByRank ranks p super [] super
  portableRightRecursiveMore :
    ∀ {p q r ps super} →
    RankedObjectPropertyLess
      ranks
      (Sem.translateObjectPropertyExpression p)
      (Sem.translateObjectPropertyExpression super) →
    PortableRightRecursivePropertyChainByRank ranks q r ps super →
    PortableRightRecursivePropertyChainByRank ranks p q (r ∷ ps) super

portableRightRecursivePropertyChainByRank :
  ∀ {ranks p q ps super} →
  PortableRightRecursivePropertyChainByRank ranks p q ps super →
  Reg.RightRecursivePropertyChain
    (RankedObjectPropertyLess ranks)
    (Sem.translateObjectPropertyExpression p)
    (Sem.translateObjectPropertyExpression q)
    (Sem.translateObjectPropertyExpressionList ps)
    (Sem.translateObjectPropertyExpression super)
portableRightRecursivePropertyChainByRank
  (portableRightRecursiveTwo p<super) =
  Reg.rightRecursiveTwo p<super
portableRightRecursivePropertyChainByRank
  (portableRightRecursiveMore p<super rest) =
  Reg.rightRecursiveMore
    p<super
    (portableRightRecursivePropertyChainByRank rest)

data PortableRegularPropertyChainByRank
  (ranks : List Rank.PropertyRank)
  : P.ObjectPropertyChain →
    P.ObjectPropertyExpression →
    Type₀ where
  portableRegularPropertyChainToTop :
    ∀ {p q ps} →
    PortableRegularPropertyChainByRank
      ranks
      (P.objectPropertyChain (P.twoOrMore p q ps))
      P.topObjectProperty
  portableRegularTransitivePropertyChain :
    ∀ {p} →
    PortableRegularPropertyChainByRank
      ranks
      (P.objectPropertyChain (P.twoOrMore p p []))
      p
  portableRegularStrictPropertyChain :
    ∀ {p q ps super} →
    RankedObjectPropertyLess
      ranks
      (Sem.translateObjectPropertyExpression p)
      (Sem.translateObjectPropertyExpression super) →
    RankedObjectPropertyLess
      ranks
      (Sem.translateObjectPropertyExpression q)
      (Sem.translateObjectPropertyExpression super) →
    PortableObjectPropertyExpressionsLessThan ranks ps super →
    PortableRegularPropertyChainByRank
      ranks
      (P.objectPropertyChain (P.twoOrMore p q ps))
      super
  portableRegularLeftRecursivePropertyChain :
    ∀ {super q ps} →
    RankedObjectPropertyLess
      ranks
      (Sem.translateObjectPropertyExpression q)
      (Sem.translateObjectPropertyExpression super) →
    PortableObjectPropertyExpressionsLessThan ranks ps super →
    PortableRegularPropertyChainByRank
      ranks
      (P.objectPropertyChain (P.twoOrMore super q ps))
      super
  portableRegularRightRecursivePropertyChain :
    ∀ {p q ps super} →
    PortableRightRecursivePropertyChainByRank ranks p q ps super →
    PortableRegularPropertyChainByRank
      ranks
      (P.objectPropertyChain (P.twoOrMore p q ps))
      super

data ExactTransitiveSelfPropertyChain :
  P.ObjectPropertyChain →
  P.ObjectPropertyExpression →
  Type₀ where
  exactTransitiveSelf :
    ∀ {p} →
    ExactTransitiveSelfPropertyChain
      (P.objectPropertyChain (P.twoOrMore p p []))
      p

exactTransitiveSelfPropertyChainByRank :
  ∀ {ranks chain super} →
  ExactTransitiveSelfPropertyChain chain super →
  PortableRegularPropertyChainByRank ranks chain super
exactTransitiveSelfPropertyChainByRank exactTransitiveSelf =
  portableRegularTransitivePropertyChain

portableRegularTransitivePropertyChainByEquality :
  ∀ {ranks p q super} →
  p ≡ q →
  p ≡ super →
  PortableRegularPropertyChainByRank
    ranks
    (P.objectPropertyChain (P.twoOrMore p q []))
    super
portableRegularTransitivePropertyChainByEquality
  {ranks = ranks}
  {p = p}
  {q = q}
  {super = super}
  p≡q
  p≡super =
  subst
    (λ super′ →
      PortableRegularPropertyChainByRank
        ranks
        (P.objectPropertyChain (P.twoOrMore p q []))
        super′)
    p≡super
    (subst
      (λ q′ →
        PortableRegularPropertyChainByRank
          ranks
          (P.objectPropertyChain (P.twoOrMore p q′ []))
          p)
      p≡q
      portableRegularTransitivePropertyChain)

ExactTransitiveSelfChainEvidence :
  P.ObjectPropertyChain →
  P.ObjectPropertyExpression →
  Type₀
ExactTransitiveSelfChainEvidence
  (P.objectPropertyChain (P.twoOrMore p q ps))
  super =
  (p ≡ q)
  ×
  (p ≡ super)
  ×
  (ps ≡ [])

portableObjectPropertyExpressionEquality :
  (left right : P.ObjectPropertyExpression) →
  Optional (left ≡ right)
portableObjectPropertyExpressionEquality =
  Equality.objectPropertyExpressionEquality

boolAndTrueLeft :
  (left right : Bool) →
  Rank.boolAnd left right ≡ true →
  left ≡ true
boolAndTrueLeft true true truth =
  refl
boolAndTrueLeft true false truth =
  refl
boolAndTrueLeft false true truth =
  absurd (falseNotTrue truth)
boolAndTrueLeft false false truth =
  absurd (falseNotTrue truth)

boolAndTrueRight :
  (left right : Bool) →
  Rank.boolAnd left right ≡ true →
  right ≡ true
boolAndTrueRight true true truth =
  refl
boolAndTrueRight true false truth =
  absurd (falseNotTrue truth)
boolAndTrueRight false true truth =
  refl
boolAndTrueRight false false truth =
  absurd (falseNotTrue truth)

sameObjectPropertyExpressionTrueToEquality :
  (left right : P.ObjectPropertyExpression) →
  Rank.sameObjectPropertyExpression left right ≡ true →
  left ≡ right
sameObjectPropertyExpressionTrueToEquality left right truth
  with portableObjectPropertyExpressionEquality left right
... | present equalProperty =
  equalProperty
... | absent =
  absurd (falseNotTrue truth)

chainIsTransitiveSelfShapeReflectsExactEvidence :
  (chain : P.ObjectPropertyChain) →
  (super : P.ObjectPropertyExpression) →
  Rank.chainIsTransitiveSelfShape chain super ≡ true →
  ExactTransitiveSelfChainEvidence chain super
chainIsTransitiveSelfShapeReflectsExactEvidence
  (P.objectPropertyChain (P.twoOrMore p q []))
  super
  truth =
  p≡q ,
  p≡super ,
  refl
  where
  firstMatchesSuper :
    Rank.sameObjectPropertyExpression p super ≡ true
  firstMatchesSuper =
    boolAndTrueLeft
      (Rank.sameObjectPropertyExpression p super)
      (Rank.sameObjectPropertyExpression q super)
      truth

  secondMatchesSuper :
    Rank.sameObjectPropertyExpression q super ≡ true
  secondMatchesSuper =
    boolAndTrueRight
      (Rank.sameObjectPropertyExpression p super)
      (Rank.sameObjectPropertyExpression q super)
      truth

  p≡super : p ≡ super
  p≡super =
    sameObjectPropertyExpressionTrueToEquality p super firstMatchesSuper

  q≡super : q ≡ super
  q≡super =
    sameObjectPropertyExpressionTrueToEquality q super secondMatchesSuper

  p≡q : p ≡ q
  p≡q =
    p≡super ∙ sym q≡super
chainIsTransitiveSelfShapeReflectsExactEvidence
  (P.objectPropertyChain (P.twoOrMore p q (r ∷ ps)))
  super
  truth =
  absurd (falseNotTrue truth)

exactTransitiveSelfChainEvidence :
  (chain : P.ObjectPropertyChain) →
  (super : P.ObjectPropertyExpression) →
  Optional (ExactTransitiveSelfChainEvidence chain super)
exactTransitiveSelfChainEvidence
  (P.objectPropertyChain (P.twoOrMore p q []))
  super
  with portableObjectPropertyExpressionEquality p q
     | portableObjectPropertyExpressionEquality p super
... | present p≡q | present p≡super =
  present (p≡q , p≡super , refl)
... | absent | _ =
  absent
... | _ | absent =
  absent
exactTransitiveSelfChainEvidence
  (P.objectPropertyChain (P.twoOrMore p q (r ∷ ps)))
  super =
  absent

portableRegularTransitivePropertyChainByExactEvidence :
  ∀ {ranks chain super} →
  ExactTransitiveSelfChainEvidence chain super →
  PortableRegularPropertyChainByRank ranks chain super
portableRegularTransitivePropertyChainByExactEvidence
  {ranks = ranks}
  {chain = P.objectPropertyChain (P.twoOrMore p q ps)}
  {super = super}
  (p≡q , p≡super , ps≡[]) =
  subst
    (λ ps′ →
      PortableRegularPropertyChainByRank
        ranks
        (P.objectPropertyChain (P.twoOrMore p q ps′))
        super)
    (sym ps≡[])
    (portableRegularTransitivePropertyChainByEquality
      p≡q
      p≡super)

objectPropertyChainProperties :
  P.ObjectPropertyChain → P.TwoOrMore P.ObjectPropertyExpression
objectPropertyChainProperties (P.objectPropertyChain properties) =
  properties

portableRegularPropertyChainByRank :
  ∀ {ranks chain super} →
  PortableRegularPropertyChainByRank ranks chain super →
  Reg.RegularPropertyChain
    (RankedObjectPropertyLess ranks)
    (Sem.translateObjectPropertyExpression
      (P.first (objectPropertyChainProperties chain)))
    (Sem.translateObjectPropertyExpression
      (P.second (objectPropertyChainProperties chain)))
    (Sem.translateObjectPropertyExpressionList
      (P.rest (objectPropertyChainProperties chain)))
    (Sem.translateObjectPropertyExpression super)
portableRegularPropertyChainByRank
  portableRegularPropertyChainToTop =
  Reg.regularPropertyChainToTop
portableRegularPropertyChainByRank
  portableRegularTransitivePropertyChain =
  Reg.regularTransitivePropertyChain
portableRegularPropertyChainByRank
  (portableRegularStrictPropertyChain p<super q<super ps<super) =
  Reg.regularStrictPropertyChain
    p<super
    q<super
    (portableObjectPropertyExpressionsLessThan ps<super)
portableRegularPropertyChainByRank
  (portableRegularLeftRecursivePropertyChain q<super ps<super) =
  Reg.regularLeftRecursivePropertyChain
    q<super
    (portableObjectPropertyExpressionsLessThan ps<super)
portableRegularPropertyChainByRank
  (portableRegularRightRecursivePropertyChain recursive) =
  Reg.regularRightRecursivePropertyChain
    (portableRightRecursivePropertyChainByRank recursive)

portableRegularPropertyChainAxiomByRank :
  ∀ {ranks chain super} →
  PortableRegularPropertyChainByRank ranks chain super →
  Reg.AxiomPropertyChainRegular
    (RankedObjectPropertyLess ranks)
    (S.subObjectPropertyOf
      (Sem.translateObjectPropertyChain chain)
      (Sem.translateObjectPropertyExpression super))
portableRegularPropertyChainAxiomByRank
  {chain = P.objectPropertyChain (P.twoOrMore p q ps)}
  proof =
  portableRegularPropertyChainByRank proof

portableStrictRankedPropertyChainCertificate :
  (ranks : List Rank.PropertyRank) →
  (chain : P.ObjectPropertyChain) →
  (super : P.ObjectPropertyExpression) →
  Optional (PortableRegularPropertyChainByRank ranks chain super)
portableStrictRankedPropertyChainCertificate
  ranks
  (P.objectPropertyChain (P.twoOrMore p q ps))
  super
  with rankedObjectPropertyLessCertificate ranks p super
     | rankedObjectPropertyLessCertificate ranks q super
     | portableObjectPropertyExpressionsLessThanCertificate ranks ps super
... | present p<super | present q<super | present ps<super =
  present
    (portableRegularStrictPropertyChain
      p<super
      q<super
      ps<super)
... | absent | _ | _ =
  absent
... | _ | absent | _ =
  absent
... | _ | _ | absent =
  absent

portableExactTransitiveSelfPropertyChainCertificate :
  (ranks : List Rank.PropertyRank) →
  (chain : P.ObjectPropertyChain) →
  (super : P.ObjectPropertyExpression) →
  Optional (PortableRegularPropertyChainByRank ranks chain super)
portableExactTransitiveSelfPropertyChainCertificate ranks chain super
  with exactTransitiveSelfChainEvidence chain super
... | present evidence =
  present (portableRegularTransitivePropertyChainByExactEvidence evidence)
... | absent =
  absent

portableRankedPropertyChainCertificate :
  (ranks : List Rank.PropertyRank) →
  (chain : P.ObjectPropertyChain) →
  (super : P.ObjectPropertyExpression) →
  Optional (PortableRegularPropertyChainByRank ranks chain super)
portableRankedPropertyChainCertificate
  ranks
  (P.objectPropertyChain (P.twoOrMore p q ps))
  P.topObjectProperty =
  present portableRegularPropertyChainToTop
portableRankedPropertyChainCertificate ranks chain super
  with portableExactTransitiveSelfPropertyChainCertificate ranks chain super
... | present certificate =
  present certificate
... | absent =
  portableStrictRankedPropertyChainCertificate ranks chain super

portableRankedOrExactSelfPropertyChainCertificate :
  (ranks : List Rank.PropertyRank) →
  (chain : P.ObjectPropertyChain) →
  (super : P.ObjectPropertyExpression) →
  Optional (PortableRegularPropertyChainByRank ranks chain super)
portableRankedOrExactSelfPropertyChainCertificate =
  portableRankedPropertyChainCertificate

StrictPropertyChainAxiomFactCertificate :
  List Rank.PropertyRank → Rank.PropertyChainAxiomFact → Type₀
StrictPropertyChainAxiomFactCertificate ranks fact =
  PortableRegularPropertyChainByRank
    ranks
    (Rank.propertyChainAxiomChain fact)
    (Rank.propertyChainAxiomSuperProperty fact)

strictPropertyChainAxiomFactCertificate :
  (ranks : List Rank.PropertyRank) →
  (fact : Rank.PropertyChainAxiomFact) →
  Optional (StrictPropertyChainAxiomFactCertificate ranks fact)
strictPropertyChainAxiomFactCertificate ranks fact =
  portableStrictRankedPropertyChainCertificate
    ranks
    (Rank.propertyChainAxiomChain fact)
    (Rank.propertyChainAxiomSuperProperty fact)

StrictPropertyChainAxiomFactsCertified :
  List Rank.PropertyRank → List Rank.PropertyChainAxiomFact → Type₀
StrictPropertyChainAxiomFactsCertified ranks [] =
  Unit*
StrictPropertyChainAxiomFactsCertified ranks (fact ∷ facts) =
  StrictPropertyChainAxiomFactCertificate ranks fact
  ×
  StrictPropertyChainAxiomFactsCertified ranks facts

strictPropertyChainAxiomFactsCertificates :
  (ranks : List Rank.PropertyRank) →
  (facts : List Rank.PropertyChainAxiomFact) →
  Optional (StrictPropertyChainAxiomFactsCertified ranks facts)
strictPropertyChainAxiomFactsCertificates ranks [] =
  present tt*
strictPropertyChainAxiomFactsCertificates ranks (fact ∷ facts)
  with strictPropertyChainAxiomFactCertificate ranks fact
     | strictPropertyChainAxiomFactsCertificates ranks facts
... | present factCertificate | present factsCertificates =
  present (factCertificate , factsCertificates)
... | absent | _ =
  absent
... | _ | absent =
  absent

StrictOntologyPropertyChainAxiomFactsCertified :
  List Rank.PropertyRank → P.Ontology → Type₀
StrictOntologyPropertyChainAxiomFactsCertified ranks ont =
  StrictPropertyChainAxiomFactsCertified
    ranks
    (Rank.ontologyPropertyChainAxiomFacts ont)

strictOntologyPropertyChainAxiomFactsCertificates :
  (ranks : List Rank.PropertyRank) →
  (ont : P.Ontology) →
  Optional
    (StrictOntologyPropertyChainAxiomFactsCertified
      ranks
      ont)
strictOntologyPropertyChainAxiomFactsCertificates ranks ont =
  strictPropertyChainAxiomFactsCertificates
    ranks
    (Rank.ontologyPropertyChainAxiomFacts ont)

StrictOntologyDocumentPropertyChainAxiomFactsCertified :
  List Rank.PropertyRank → P.OntologyDocument → Type₀
StrictOntologyDocumentPropertyChainAxiomFactsCertified ranks document =
  StrictOntologyPropertyChainAxiomFactsCertified
    ranks
    (P.documentOntology document)

strictOntologyDocumentPropertyChainAxiomFactsCertificates :
  (ranks : List Rank.PropertyRank) →
  (document : P.OntologyDocument) →
  Optional
    (StrictOntologyDocumentPropertyChainAxiomFactsCertified
      ranks
      document)
strictOntologyDocumentPropertyChainAxiomFactsCertificates ranks document =
  strictOntologyPropertyChainAxiomFactsCertificates
    ranks
    (P.documentOntology document)

PropertyChainAxiomFactCertificateByRank :
  List Rank.PropertyRank → Rank.PropertyChainAxiomFact → Type₀
PropertyChainAxiomFactCertificateByRank ranks fact =
  PortableRegularPropertyChainByRank
    ranks
    (Rank.propertyChainAxiomChain fact)
    (Rank.propertyChainAxiomSuperProperty fact)

PropertyChainAxiomFactExactTransitiveSelfCertificate :
  Rank.PropertyChainAxiomFact → Type₀
PropertyChainAxiomFactExactTransitiveSelfCertificate fact =
  ExactTransitiveSelfChainEvidence
    (Rank.propertyChainAxiomChain fact)
    (Rank.propertyChainAxiomSuperProperty fact)

propertyChainAxiomFactCertificateByExactTransitiveSelf :
  ∀ {ranks fact} →
  PropertyChainAxiomFactExactTransitiveSelfCertificate fact →
  PropertyChainAxiomFactCertificateByRank ranks fact
propertyChainAxiomFactCertificateByExactTransitiveSelf evidence =
  portableRegularTransitivePropertyChainByExactEvidence evidence

propertyChainAxiomFactCertificateByRank :
  (ranks : List Rank.PropertyRank) →
  (fact : Rank.PropertyChainAxiomFact) →
  Optional (PropertyChainAxiomFactCertificateByRank ranks fact)
propertyChainAxiomFactCertificateByRank ranks fact =
  portableRankedPropertyChainCertificate
    ranks
    (Rank.propertyChainAxiomChain fact)
    (Rank.propertyChainAxiomSuperProperty fact)

PropertyChainAxiomFactsCertifiedByRank :
  List Rank.PropertyRank → List Rank.PropertyChainAxiomFact → Type₀
PropertyChainAxiomFactsCertifiedByRank ranks [] =
  Unit*
PropertyChainAxiomFactsCertifiedByRank ranks (fact ∷ facts) =
  PropertyChainAxiomFactCertificateByRank ranks fact
  ×
  PropertyChainAxiomFactsCertifiedByRank ranks facts

propertyChainAxiomFactsCertificatesByRank :
  (ranks : List Rank.PropertyRank) →
  (facts : List Rank.PropertyChainAxiomFact) →
  Optional (PropertyChainAxiomFactsCertifiedByRank ranks facts)
propertyChainAxiomFactsCertificatesByRank ranks [] =
  present tt*
propertyChainAxiomFactsCertificatesByRank ranks (fact ∷ facts)
  with propertyChainAxiomFactCertificateByRank ranks fact
     | propertyChainAxiomFactsCertificatesByRank ranks facts
... | present factCertificate | present factsCertificates =
  present (factCertificate , factsCertificates)
... | absent | _ =
  absent
... | _ | absent =
  absent

OntologyPropertyChainAxiomFactsCertifiedByRank :
  List Rank.PropertyRank → P.Ontology → Type₀
OntologyPropertyChainAxiomFactsCertifiedByRank ranks ont =
  PropertyChainAxiomFactsCertifiedByRank
    ranks
    (Rank.ontologyPropertyChainAxiomFacts ont)

ontologyPropertyChainAxiomFactsCertificatesByRank :
  (ranks : List Rank.PropertyRank) →
  (ont : P.Ontology) →
  Optional
    (OntologyPropertyChainAxiomFactsCertifiedByRank
      ranks
      ont)
ontologyPropertyChainAxiomFactsCertificatesByRank ranks ont =
  propertyChainAxiomFactsCertificatesByRank
    ranks
    (Rank.ontologyPropertyChainAxiomFacts ont)

OntologyDocumentPropertyChainAxiomFactsCertifiedByRank :
  List Rank.PropertyRank → P.OntologyDocument → Type₀
OntologyDocumentPropertyChainAxiomFactsCertifiedByRank ranks document =
  OntologyPropertyChainAxiomFactsCertifiedByRank
    ranks
    (P.documentOntology document)

ontologyDocumentPropertyChainAxiomFactsCertificatesByRank :
  (ranks : List Rank.PropertyRank) →
  (document : P.OntologyDocument) →
  Optional
    (OntologyDocumentPropertyChainAxiomFactsCertifiedByRank
      ranks
      document)
ontologyDocumentPropertyChainAxiomFactsCertificatesByRank ranks document =
  ontologyPropertyChainAxiomFactsCertificatesByRank
    ranks
    (P.documentOntology document)

rankedAxiomsPropertyChainsRegularAppend :
  (ranks : List Rank.PropertyRank) →
  ∀ {left right} →
  Reg.AxiomsPropertyChainsRegular
    (RankedObjectPropertyLess ranks)
    left →
  Reg.AxiomsPropertyChainsRegular
    (RankedObjectPropertyLess ranks)
    right →
  Reg.AxiomsPropertyChainsRegular
    (RankedObjectPropertyLess ranks)
    (left ++ right)
rankedAxiomsPropertyChainsRegularAppend ranks =
  Reg.axiomsPropertyChainsRegularAppend

rankedAxiomTranslationsPropertyChainsRegularAppend :
  (ranks : List Rank.PropertyRank) →
  ∀ {left right : Sem.AxiomTranslation} →
  Reg.AxiomsPropertyChainsRegular
    (RankedObjectPropertyLess ranks)
    (Sem.semanticAxioms left) →
  Reg.AxiomsPropertyChainsRegular
    (RankedObjectPropertyLess ranks)
    (Sem.semanticAxioms right) →
  Reg.AxiomsPropertyChainsRegular
    (RankedObjectPropertyLess ranks)
    (Sem.semanticAxioms (Sem.appendAxiomTranslation left right))
rankedAxiomTranslationsPropertyChainsRegularAppend ranks =
  Reg.axiomsPropertyChainsRegularAppend

AnnotatedAxiomPropertyChainsRegularByRank :
  List Rank.PropertyRank → P.Annotated P.Axiom → Type₀
AnnotatedAxiomPropertyChainsRegularByRank ranks ax =
  Reg.AxiomsPropertyChainsRegular
    (RankedObjectPropertyLess ranks)
    (Sem.semanticAxioms (Sem.translateAnnotatedAxiom ax))

AnnotatedAxiomsPropertyChainsRegularByRank :
  List Rank.PropertyRank → List (P.Annotated P.Axiom) → Type₀
AnnotatedAxiomsPropertyChainsRegularByRank ranks [] =
  Unit*
AnnotatedAxiomsPropertyChainsRegularByRank ranks (ax ∷ axioms) =
  AnnotatedAxiomPropertyChainsRegularByRank ranks ax
  ×
  AnnotatedAxiomsPropertyChainsRegularByRank ranks axioms

translatedAnnotatedAxiomPropertyChainsRegularByRank :
  (ranks : List Rank.PropertyRank) →
  (ax : P.Annotated P.Axiom) →
  AnnotatedAxiomPropertyChainsRegularByRank ranks ax →
  Reg.AxiomsPropertyChainsRegular
    (RankedObjectPropertyLess ranks)
    (Sem.semanticAxioms (Sem.translateAnnotatedAxiom ax))
translatedAnnotatedAxiomPropertyChainsRegularByRank ranks ax proof =
  proof

translatedAnnotatedAxiomsPropertyChainsRegularByRank :
  (ranks : List Rank.PropertyRank) →
  (axioms : List (P.Annotated P.Axiom)) →
  AnnotatedAxiomsPropertyChainsRegularByRank ranks axioms →
  Reg.AxiomsPropertyChainsRegular
    (RankedObjectPropertyLess ranks)
    (Sem.semanticAxioms (Sem.translateAnnotatedAxioms axioms))
translatedAnnotatedAxiomsPropertyChainsRegularByRank ranks [] proof =
  tt*
translatedAnnotatedAxiomsPropertyChainsRegularByRank
  ranks
  (ax ∷ axioms)
  (axProof , axiomsProof) =
  rankedAxiomTranslationsPropertyChainsRegularAppend
    ranks
    {left = Sem.translateAnnotatedAxiom ax}
    {right = Sem.translateAnnotatedAxioms axioms}
    axProof
    (translatedAnnotatedAxiomsPropertyChainsRegularByRank
      ranks
      axioms
      axiomsProof)

propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms :
  (ranks : List Rank.PropertyRank) →
  (axioms : List (P.Annotated P.Axiom)) →
  PropertyChainAxiomFactsCertifiedByRank
    ranks
    (Rank.propertyChainAxiomFacts axioms) →
  AnnotatedAxiomsPropertyChainsRegularByRank ranks axioms
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks [] proof =
  tt*
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated annotations (P.declaration entity) ∷ axioms)
  proof =
  (tt* , tt*) ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
    ranks
    axioms
    proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated annotations (P.subClassOf c d) ∷ axioms)
  proof
  with Sem.translateClassExpression c | Sem.translateClassExpression d
... | present c′ | present d′ =
  (tt* , tt*) ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
... | absent | d′ =
  tt* ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
... | present c′ | absent =
  tt* ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated annotations (P.equivalentClasses classes) ∷ axioms)
  proof
  with Sem.translateClassExpressionList (Sem.twoOrMoreToList classes)
... | present classes′ =
  (tt* , tt*) ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
... | absent =
  tt* ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated annotations (P.disjointClasses classes) ∷ axioms)
  proof
  with Sem.translateClassExpressionList (Sem.twoOrMoreToList classes)
... | present classes′ =
  (tt* , tt*) ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
... | absent =
  tt* ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated annotations (P.disjointUnion c classes) ∷ axioms)
  proof
  with Sem.translateClassExpressionList (Sem.twoOrMoreToList classes)
... | present classes′ =
  (tt* , (tt* , tt*)) ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
... | absent =
  tt* ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated
    annotations
    (P.subObjectPropertyOf (P.subObjectProperty property) super)
    ∷ axioms)
  proof =
  (tt* , tt*) ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
    ranks
    axioms
    proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated
    annotations
    (P.subObjectPropertyOf (P.subObjectPropertyChain chain) super)
    ∷ axioms)
  (chainProof , axiomsProof) =
  (portableRegularPropertyChainAxiomByRank chainProof , tt*) ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
    ranks
    axioms
    axiomsProof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated annotations (P.equivalentObjectProperties properties) ∷ axioms)
  proof =
  (tt* , tt*) ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated annotations (P.disjointObjectProperties properties) ∷ axioms)
  proof =
  (tt* , tt*) ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated annotations (P.inverseObjectProperties p q) ∷ axioms)
  proof =
  (tt* , tt*) ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated annotations (P.objectPropertyDomain p class) ∷ axioms)
  proof
  with Sem.translateClassExpression class
... | present class′ =
  (tt* , tt*) ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
... | absent =
  tt* ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated annotations (P.objectPropertyRange p class) ∷ axioms)
  proof
  with Sem.translateClassExpression class
... | present class′ =
  (tt* , tt*) ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
... | absent =
  tt* ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated annotations (P.functionalObjectProperty property) ∷ axioms)
  proof =
  (tt* , tt*) ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated
    annotations
    (P.inverseFunctionalObjectProperty property)
    ∷ axioms)
  proof =
  (tt* , tt*) ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated annotations (P.reflexiveObjectProperty property) ∷ axioms)
  proof =
  (tt* , tt*) ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated annotations (P.irreflexiveObjectProperty property) ∷ axioms)
  proof =
  (tt* , tt*) ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated annotations (P.symmetricObjectProperty property) ∷ axioms)
  proof =
  (tt* , tt*) ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated annotations (P.asymmetricObjectProperty property) ∷ axioms)
  proof =
  (tt* , tt*) ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated annotations (P.transitiveObjectProperty property) ∷ axioms)
  proof =
  (tt* , tt*) ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated annotations (P.subDataPropertyOf sub super) ∷ axioms)
  proof =
  (tt* , tt*) ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated annotations (P.equivalentDataProperties properties) ∷ axioms)
  proof =
  (tt* , tt*) ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated annotations (P.disjointDataProperties properties) ∷ axioms)
  proof =
  (tt* , tt*) ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated annotations (P.dataPropertyDomain p class) ∷ axioms)
  proof
  with Sem.translateClassExpression class
... | present class′ =
  (tt* , tt*) ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
... | absent =
  tt* ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated annotations (P.dataPropertyRange p range) ∷ axioms)
  proof
  with Sem.translateDataRange range
... | present range′ =
  (tt* , tt*) ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
... | absent =
  tt* ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated annotations (P.functionalDataProperty property) ∷ axioms)
  proof =
  (tt* , tt*) ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated annotations (P.datatypeDefinition datatype range) ∷ axioms)
  proof
  with Sem.translateDataRange range
... | present range′ =
  (tt* , tt*) ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
... | absent =
  tt* ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated annotations (P.hasKey class key) ∷ axioms)
  proof
  with Sem.translateClassExpression class
... | present class′ =
  (tt* , tt*) ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
... | absent =
  tt* ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated annotations (P.sameIndividual individuals) ∷ axioms)
  proof =
  (tt* , tt*) ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated annotations (P.differentIndividuals individuals) ∷ axioms)
  proof =
  (tt* , tt*) ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated annotations (P.classAssertion class individual) ∷ axioms)
  proof
  with Sem.translateClassExpression class
... | present class′ =
  (tt* , tt*) ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
... | absent =
  tt* ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated
    annotations
    (P.objectPropertyAssertion property source target)
    ∷ axioms)
  proof =
  (tt* , tt*) ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated
    annotations
    (P.negativeObjectPropertyAssertion property source target)
    ∷ axioms)
  proof =
  (tt* , tt*) ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated
    annotations
    (P.dataPropertyAssertion property source literal)
    ∷ axioms)
  proof =
  (tt* , tt*) ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated
    annotations
    (P.negativeDataPropertyAssertion property source literal)
    ∷ axioms)
  proof =
  (tt* , tt*) ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated annotations (P.annotationAssertion property subject value) ∷ axioms)
  proof =
  tt* ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated annotations (P.subAnnotationPropertyOf sub super) ∷ axioms)
  proof =
  tt* ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated annotations (P.annotationPropertyDomain property targetIRI) ∷ axioms)
  proof =
  tt* ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof
propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  (P.annotated annotations (P.annotationPropertyRange property targetIRI) ∷ axioms)
  proof =
  tt* ,
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms ranks axioms proof

ontologyPropertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms :
  (ranks : List Rank.PropertyRank) →
  (ont : P.Ontology) →
  OntologyPropertyChainAxiomFactsCertifiedByRank ranks ont →
  AnnotatedAxiomsPropertyChainsRegularByRank
    ranks
    (P.axioms ont)
ontologyPropertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  ont
  proof =
  propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
    ranks
    (P.axioms ont)
    proof

ontologyDocumentPropertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms :
  (ranks : List Rank.PropertyRank) →
  (document : P.OntologyDocument) →
  OntologyDocumentPropertyChainAxiomFactsCertifiedByRank ranks document →
  AnnotatedAxiomsPropertyChainsRegularByRank
    ranks
    (P.axioms (P.documentOntology document))
ontologyDocumentPropertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
  ranks
  document
  proof =
  ontologyPropertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
    ranks
    (P.documentOntology document)
    proof

ontologyPropertyChainAxiomFactsCertifiedByRankToTranslatedAxioms :
  (ranks : List Rank.PropertyRank) →
  (ont : P.Ontology) →
  OntologyPropertyChainAxiomFactsCertifiedByRank ranks ont →
  Reg.AxiomsPropertyChainsRegular
    (RankedObjectPropertyLess ranks)
    (Sem.semanticAxioms (Sem.translateAnnotatedAxioms (P.axioms ont)))
ontologyPropertyChainAxiomFactsCertifiedByRankToTranslatedAxioms
  ranks
  ont
  proof =
  translatedAnnotatedAxiomsPropertyChainsRegularByRank
    ranks
    (P.axioms ont)
    (ontologyPropertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
      ranks
      ont
      proof)

ontologyDocumentPropertyChainAxiomFactsCertifiedByRankToTranslatedAxioms :
  (ranks : List Rank.PropertyRank) →
  (document : P.OntologyDocument) →
  OntologyDocumentPropertyChainAxiomFactsCertifiedByRank ranks document →
  Reg.AxiomsPropertyChainsRegular
    (RankedObjectPropertyLess ranks)
    (Sem.semanticAxioms
      (Sem.translateAnnotatedAxioms
        (P.axioms (P.documentOntology document))))
ontologyDocumentPropertyChainAxiomFactsCertifiedByRankToTranslatedAxioms
  ranks
  document
  proof =
  ontologyPropertyChainAxiomFactsCertifiedByRankToTranslatedAxioms
    ranks
    (P.documentOntology document)
    proof

rankedStrictChainOrder :
  (ranks : List Rank.PropertyRank) →
  (axioms : List (S.Axiom Sem.PortableSignature)) →
  Reg.AxiomsPropertyChainsRegular
    (RankedObjectPropertyLess ranks)
    axioms →
  Reg.StrictChainOrder Sem.PortableSignature axioms
rankedStrictChainOrder ranks axioms chainRegularity .Reg.StrictChainOrder._<_ =
  RankedObjectPropertyLess ranks
rankedStrictChainOrder ranks axioms chainRegularity .Reg.StrictChainOrder.irrefl =
  rankedObjectPropertyLessIrrefl ranks
rankedStrictChainOrder ranks axioms chainRegularity .Reg.StrictChainOrder.trans =
  rankedObjectPropertyLessTrans ranks
rankedStrictChainOrder ranks axioms chainRegularity .Reg.StrictChainOrder.inversePreserves =
  rankedObjectPropertyLessInversePreserves ranks
rankedStrictChainOrder ranks axioms chainRegularity .Reg.StrictChainOrder.chainsRegular =
  chainRegularity

rankedOntologyStrictChainOrder :
  (ranks : List Rank.PropertyRank) →
  (ont : S.Ontology Sem.PortableSignature) →
  Reg.AxiomsPropertyChainsRegular
    (RankedObjectPropertyLess ranks)
    (S.axioms ont) →
  Reg.StrictChainOrder Sem.PortableSignature (S.axioms ont)
rankedOntologyStrictChainOrder ranks ont =
  rankedStrictChainOrder ranks (S.axioms ont)

rankedOntologyDocumentStrictChainOrder :
  (ranks : List Rank.PropertyRank) →
  (document : P.OntologyDocument) →
  Reg.AxiomsPropertyChainsRegular
    (RankedObjectPropertyLess ranks)
    (S.axioms
      (Sem.semanticOntology (Sem.partialTranslateOntologyDocument document))) →
  Reg.StrictChainOrder
    Sem.PortableSignature
    (S.axioms
      (Sem.semanticOntology (Sem.partialTranslateOntologyDocument document)))
rankedOntologyDocumentStrictChainOrder ranks document =
  rankedStrictChainOrder
    ranks
    (S.axioms
      (Sem.semanticOntology (Sem.partialTranslateOntologyDocument document)))

ontologyDocumentStrictChainOrderByRank :
  (ranks : List Rank.PropertyRank) →
  (document : P.OntologyDocument) →
  OntologyDocumentPropertyChainAxiomFactsCertifiedByRank ranks document →
  Reg.StrictChainOrder
    Sem.PortableSignature
    (S.axioms
      (Sem.semanticOntology (Sem.partialTranslateOntologyDocument document)))
ontologyDocumentStrictChainOrderByRank ranks document proof =
  rankedOntologyDocumentStrictChainOrder
    ranks
    document
    (ontologyDocumentPropertyChainAxiomFactsCertifiedByRankToTranslatedAxioms
      ranks
      document
      proof)

ontologyDocumentStrictChainOrderCertificateByRank :
  (ranks : List Rank.PropertyRank) →
  (document : P.OntologyDocument) →
  Optional
    (Reg.StrictChainOrder
      Sem.PortableSignature
      (S.axioms
        (Sem.semanticOntology (Sem.partialTranslateOntologyDocument document))))
ontologyDocumentStrictChainOrderCertificateByRank ranks document
  with ontologyDocumentPropertyChainAxiomFactsCertificatesByRank ranks document
... | present proof =
  present (ontologyDocumentStrictChainOrderByRank ranks document proof)
... | absent =
  absent