OWL2.Corpus.Accepted.Raw

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

module OWL2.Corpus.Accepted.Raw where

open import OWL2.Prelude
open import OWL2.Check.Result
open import OWL2.Elab
open import OWL2.Foundation.List
open import OWL2.Kernel.Semantics
open import OWL2.Raw
open import OWL2.Semantics.Complete
import OWL2.Check.Bundle as Bundle
import OWL2.Kernel as K

emptyRawDocument : RawOntology
emptyRawDocument =
  emptyRawOntology anonymousSource

emptyRawDocumentResult : ElaborationResult
emptyRawDocumentResult =
  elaborateEmptyKernelStrict emptyRawDocument

emptyRawDocumentClean : Clean emptyRawDocumentResult
emptyRawDocumentClean =
  tt

emptyRawDocumentChecked : EvidenceAvailable emptyRawDocumentResult
emptyRawDocumentChecked =
  cleanEvidence emptyRawDocumentResult emptyRawDocumentClean

emptyRawCheckedFromClean : CheckedImport
emptyRawCheckedFromClean =
  checkedFromClean emptyRawDocumentResult emptyRawDocumentClean

emptyRawSourceEvidenceFromClean :
  CheckedSourceEvidence emptyRawCheckedFromClean
emptyRawSourceEvidenceFromClean =
  sourceEvidenceFromClean emptyRawDocumentResult emptyRawDocumentClean

emptyRawDocumentSound :
  ElaboratesToCheckedImport emptyRawDocument
    (elaborationSucceeded emptyRawDocumentResult emptyRawDocumentChecked)
emptyRawDocumentSound =
  soundFromClean emptyRawDocumentResult emptyRawDocumentClean

emptyRawCompleteSourceSound :
  ElaboratesToCheckedImport emptyRawDocument emptyRawCheckedFromClean
emptyRawCompleteSourceSound =
  completeSourceSound emptyRawDocumentResult emptyRawDocumentClean

trivialKernelInterpretation : (Sig : K.Signature) → Interpretation Sig
trivialKernelInterpretation Sig .ObjectDomain =
  Unit
trivialKernelInterpretation Sig .DataDomain =
  Unit
trivialKernelInterpretation Sig .classDenotation name value =
  Unit
trivialKernelInterpretation Sig .objectPropertyDenotation name subject object =
  Unit
trivialKernelInterpretation Sig .dataPropertyDenotation name subject value =
  Unit
trivialKernelInterpretation Sig .individualDenotation name =
  tt
trivialKernelInterpretation Sig .literalDenotation literal =
  tt
trivialKernelInterpretation Sig .datatypeDenotation name value =
  Unit
trivialKernelInterpretation Sig .facetRestrictionDenotation restriction value =
  Unit

emptyRawCompleteSourceInterpretation :
  Interpretation (signature emptyRawCheckedFromClean)
emptyRawCompleteSourceInterpretation =
  trivialKernelInterpretation (signature emptyRawCheckedFromClean)

emptyRawModelOfCompleteSource :
  ModelOfCompleteSource
    emptyRawDocumentResult
    emptyRawDocumentClean
    emptyRawCompleteSourceInterpretation
emptyRawModelOfCompleteSource =
  all[]

emptyRawCompleteSourceModel :
  CompleteSourceModel emptyRawDocumentResult emptyRawDocumentClean
emptyRawCompleteSourceModel =
  completeSourceModel
    emptyRawCompleteSourceInterpretation
    emptyRawModelOfCompleteSource

emptyRawElaboratedInterpretation :
  Interpretation
    (signature
      (elaborationSucceeded emptyRawDocumentResult emptyRawDocumentChecked))
emptyRawElaboratedInterpretation =
  trivialKernelInterpretation
    (signature
      (elaborationSucceeded emptyRawDocumentResult emptyRawDocumentChecked))

emptyRawModelOfElaboratedSource :
  ModelOfElaboratedSource
    emptyRawDocumentResult
    emptyRawDocumentChecked
    (sourceSemanticSupportEvidence
      (checkedSourceEvidenceOf
        (elaborationSucceeded emptyRawDocumentResult emptyRawDocumentChecked)))
    emptyRawElaboratedInterpretation
emptyRawModelOfElaboratedSource =
  all[]

emptyRawDocumentImportsRecorded :
  requestedImports
    (sourceImportClosure
      (elaborationSucceeded emptyRawDocumentResult emptyRawDocumentChecked)) ≡
  imports emptyRawDocument
emptyRawDocumentImportsRecorded =
  sourceImportsRecorded emptyRawDocumentSound

emptyRawDeclarationTraceRawPresent :
  traceRawEvidence
    (declarationTrace (sourceDeclarationEvidence emptyRawCheckedFromClean)) ≡
  present
    (checkedSourceTableRawTrace
      emptyRawDocument
      refl
      anonymousSource
      refl)
emptyRawDeclarationTraceRawPresent =
  refl

emptyRawPropertyRoleTraceRawPresent :
  traceRawEvidence
    (propertyRoleTrace (sourcePropertyRoleEvidence emptyRawCheckedFromClean)) ≡
  present
    (checkedSourceTableRawTrace
      emptyRawDocument
      refl
      anonymousSource
      refl)
emptyRawPropertyRoleTraceRawPresent =
  refl

declaredClassIri : RawIRI
declaredClassIri =
  rawIRI "http://example.test/Class"

declaredClassAxiom : RawAnnotated RawAxiom
declaredClassAxiom =
  rawAnnotated []
    (rawDeclaration (rawEntity rawClass declaredClassIri))

declaredClassDocument : RawOntology
declaredClassDocument =
  rawOntology
    anonymousSource
    absent
    absent
    []
    []
    (declaredClassAxiom ∷ [])

declaredClassResult : ElaborationResult
declaredClassResult =
  elaborateDeclarationsKernelStrict declaredClassDocument

declaredClassClean : Clean declaredClassResult
declaredClassClean =
  tt

declaredClassEvidence : EvidenceAvailable declaredClassResult
declaredClassEvidence =
  cleanEvidence declaredClassResult declaredClassClean

declaredClassChecked : CheckedImport
declaredClassChecked =
  elaborationSucceeded declaredClassResult declaredClassEvidence

declaredClassSound :
  ElaboratesToCheckedImport declaredClassDocument declaredClassChecked
declaredClassSound =
  soundFromClean declaredClassResult declaredClassClean

declaredClassImportsRecorded :
  requestedImports (sourceImportClosure declaredClassChecked) ≡
  imports declaredClassDocument
declaredClassImportsRecorded =
  sourceImportsRecorded declaredClassSound

declaredClassEvidenceBundle :
  Bundle.EvidenceBundle CheckedImport CheckedEvidence
declaredClassEvidenceBundle =
  checkedEvidenceBundle declaredClassChecked

declaredClassSourceEvidence : CheckedSourceEvidence declaredClassChecked
declaredClassSourceEvidence =
  checkedSourceEvidenceOf declaredClassChecked

declaredClassSourcePolicyPreserved :
  Bundle.storedValue (sourcePolicyEvidence declaredClassSourceEvidence) ≡
  policyEvidence declaredClassChecked
declaredClassSourcePolicyPreserved =
  Bundle.storedValuePreserved
    (sourcePolicyEvidence declaredClassSourceEvidence)

declaredClassDeclarationClassCountRecorded :
  declarationClassCount (sourceDeclarationEvidence declaredClassChecked) ≡
  K.classCount (signature declaredClassChecked)
declaredClassDeclarationClassCountRecorded =
  declarationClassCountRecorded
    (sourceDeclarationEvidence declaredClassChecked)

declaredClassPropertyRoleObjectCountRecorded :
  roleObjectPropertyCount (sourcePropertyRoleEvidence declaredClassChecked) ≡
  K.objectPropertyCount (signature declaredClassChecked)
declaredClassPropertyRoleObjectCountRecorded =
  roleObjectPropertyCountRecorded
    (sourcePropertyRoleEvidence declaredClassChecked)

declaredClassDeclarationTraceRawPresent :
  traceRawEvidence
    (declarationTrace (sourceDeclarationEvidence declaredClassChecked)) ≡
  present
    (checkedSourceTableRawTrace
      declaredClassDocument
      refl
      anonymousSource
      refl)
declaredClassDeclarationTraceRawPresent =
  refl

declaredClassDeclarationClassIRIs :
  declarationClassIRIs (sourceDeclarationEvidence declaredClassChecked) ≡
  declaredClassIri ∷ []
declaredClassDeclarationClassIRIs =
  refl

declaredClassBundleDeclarationsPresent :
  Bundle.declarations declaredClassEvidenceBundle ≡
  present (Bundle.storedEvidenceOf (sourceDeclarationEvidence declaredClassChecked))
declaredClassBundleDeclarationsPresent =
  refl

declaredClassBundlePropertyRolesPresent :
  Bundle.propertyRoles declaredClassEvidenceBundle ≡
  present (Bundle.storedEvidenceOf (sourcePropertyRoleEvidence declaredClassChecked))
declaredClassBundlePropertyRolesPresent =
  refl

declaredClassBundlePunningPresent :
  Bundle.punning declaredClassEvidenceBundle ≡ present refl
declaredClassBundlePunningPresent =
  refl

declaredClassBundleDatatypePresent :
  Bundle.datatypeMap declaredClassEvidenceBundle ≡
  present (Bundle.storedEvidenceOf (K.datatypeSupport (ontology declaredClassChecked)))
declaredClassBundleDatatypePresent =
  refl

declaredClassBundleImportClosurePresent :
  Bundle.importClosure declaredClassEvidenceBundle ≡
  present (Bundle.storedEvidenceOf (sourceImportClosure declaredClassChecked))
declaredClassBundleImportClosurePresent =
  refl

declaredClassBundleSemanticSupportPresent :
  Bundle.semanticSupport declaredClassEvidenceBundle ≡
  present (Bundle.storedEvidenceOf (sourceSemanticSupport declaredClassChecked))
declaredClassBundleSemanticSupportPresent =
  refl

declaredClassSemanticSupportSourcePreserved :
  K.sourceAxiomsPreserved (sourceSemanticSupport declaredClassChecked) ≡ refl
declaredClassSemanticSupportSourcePreserved =
  refl

declaredClassBundleAnnotationErasurePresent :
  Bundle.annotationErased declaredClassEvidenceBundle ≡
  present (Bundle.storedEvidenceOf (K.annotationErasure (ontology declaredClassChecked)))
declaredClassBundleAnnotationErasurePresent =
  refl

declaredClassBundleRegularityPresent :
  Bundle.regularity declaredClassEvidenceBundle ≡
  present (Bundle.storedEvidenceOf (K.regularity (ontology declaredClassChecked)))
declaredClassBundleRegularityPresent =
  refl

declaredClassCount : K.classCount (signature declaredClassChecked) ≡ 1
declaredClassCount =
  refl

declaredClassAxiomCount :
  listCount (K.axioms (ontology declaredClassChecked)) ≡ 1
declaredClassAxiomCount =
  refl

superClassIri : RawIRI
superClassIri =
  rawIRI "http://example.test/SuperClass"

superClassAxiom : RawAnnotated RawAxiom
superClassAxiom =
  rawAnnotated []
    (rawDeclaration (rawEntity rawClass superClassIri))

declaredSubClassAxiom : RawAnnotated RawAxiom
declaredSubClassAxiom =
  rawAnnotated []
    (rawSubClassOf
      (rawNamedClass declaredClassIri)
      (rawNamedClass superClassIri))

declaredSubClassDocument : RawOntology
declaredSubClassDocument =
  rawOntology
    anonymousSource
    absent
    absent
    []
    []
    (declaredClassAxiom ∷
     superClassAxiom ∷
     declaredSubClassAxiom ∷ [])

declaredSubClassResult : ElaborationResult
declaredSubClassResult =
  elaborateStructuralKernelStrict declaredSubClassDocument

declaredSubClassClean : Clean declaredSubClassResult
declaredSubClassClean =
  tt

declaredSubClassEvidence : EvidenceAvailable declaredSubClassResult
declaredSubClassEvidence =
  cleanEvidence declaredSubClassResult declaredSubClassClean

declaredSubClassChecked : CheckedImport
declaredSubClassChecked =
  elaborationSucceeded declaredSubClassResult declaredSubClassEvidence

declaredSubClassClassCount :
  K.classCount (signature declaredSubClassChecked) ≡ 2
declaredSubClassClassCount =
  refl

declaredSubClassAxiomCount :
  listCount (K.axioms (ontology declaredSubClassChecked)) ≡ 3
declaredSubClassAxiomCount =
  refl

relatedToIri : RawIRI
relatedToIri =
  rawIRI "http://example.test/relatedTo"

relatedToAxiom : RawAnnotated RawAxiom
relatedToAxiom =
  rawAnnotated []
    (rawDeclaration (rawEntity rawObjectProperty relatedToIri))

someValuesSubClassAxiom : RawAnnotated RawAxiom
someValuesSubClassAxiom =
  rawAnnotated []
    (rawSubClassOf
      (rawNamedClass declaredClassIri)
      (rawObjectSomeValuesFrom
        (rawObjectProperty relatedToIri)
        (rawNamedClass superClassIri)))

someValuesDocument : RawOntology
someValuesDocument =
  rawOntology
    anonymousSource
    absent
    absent
    []
    []
    (declaredClassAxiom ∷
     superClassAxiom ∷
     relatedToAxiom ∷
     someValuesSubClassAxiom ∷ [])

someValuesResult : ElaborationResult
someValuesResult =
  elaborateStructuralKernelStrict someValuesDocument

someValuesClean : Clean someValuesResult
someValuesClean =
  tt

someValuesEvidence : EvidenceAvailable someValuesResult
someValuesEvidence =
  cleanEvidence someValuesResult someValuesClean

someValuesChecked : CheckedImport
someValuesChecked =
  elaborationSucceeded someValuesResult someValuesEvidence

someValuesSound :
  ElaboratesToCheckedImport someValuesDocument someValuesChecked
someValuesSound =
  soundFromClean someValuesResult someValuesClean

someValuesImportsRecorded :
  requestedImports (sourceImportClosure someValuesChecked) ≡
  imports someValuesDocument
someValuesImportsRecorded =
  sourceImportsRecorded someValuesSound

someValuesSemanticSupportSourcePreserved :
  K.sourceAxiomsPreserved (sourceSemanticSupport someValuesChecked) ≡ refl
someValuesSemanticSupportSourcePreserved =
  refl

someValuesClassCount : K.classCount (signature someValuesChecked) ≡ 2
someValuesClassCount =
  refl

someValuesObjectPropertyCount :
  K.objectPropertyCount (signature someValuesChecked) ≡ 1
someValuesObjectPropertyCount =
  refl

someValuesDeclarationObjectPropertyCountRecorded :
  declarationObjectPropertyCount (sourceDeclarationEvidence someValuesChecked) ≡
  K.objectPropertyCount (signature someValuesChecked)
someValuesDeclarationObjectPropertyCountRecorded =
  declarationObjectPropertyCountRecorded
    (sourceDeclarationEvidence someValuesChecked)

someValuesPropertyRoleObjectCountRecorded :
  roleObjectPropertyCount (sourcePropertyRoleEvidence someValuesChecked) ≡
  K.objectPropertyCount (signature someValuesChecked)
someValuesPropertyRoleObjectCountRecorded =
  roleObjectPropertyCountRecorded
    (sourcePropertyRoleEvidence someValuesChecked)

someValuesPropertyRoleTraceRawPresent :
  traceRawEvidence
    (propertyRoleTrace (sourcePropertyRoleEvidence someValuesChecked)) ≡
  present
    (checkedSourceTableRawTrace
      someValuesDocument
      refl
      anonymousSource
      refl)
someValuesPropertyRoleTraceRawPresent =
  refl

someValuesObjectRoleIRIs :
  roleObjectPropertyIRIs (sourcePropertyRoleEvidence someValuesChecked) ≡
  relatedToIri ∷ []
someValuesObjectRoleIRIs =
  refl

someValuesDataRoleIRIs :
  roleDataPropertyIRIs (sourcePropertyRoleEvidence someValuesChecked) ≡ []
someValuesDataRoleIRIs =
  refl

someValuesAnnotationRoleIRIs :
  roleAnnotationPropertyIRIs (sourcePropertyRoleEvidence someValuesChecked) ≡ []
someValuesAnnotationRoleIRIs =
  refl

someValuesAxiomCount :
  listCount (K.axioms (ontology someValuesChecked)) ≡ 4
someValuesAxiomCount =
  refl

booleanClassConstructorsSubClassAxiom : RawAnnotated RawAxiom
booleanClassConstructorsSubClassAxiom =
  rawAnnotated []
    (rawSubClassOf
      (rawObjectIntersectionOf (rawNamedClass declaredClassIri ∷ []))
      (rawObjectUnionOf
        (rawObjectComplementOf (rawNamedClass superClassIri) ∷ [])))

equivalentClassesAxiom : RawAnnotated RawAxiom
equivalentClassesAxiom =
  rawAnnotated []
    (rawEquivalentClasses
      (rawNamedClass declaredClassIri ∷
       rawNamedClass superClassIri ∷ []))

disjointClassesAxiom : RawAnnotated RawAxiom
disjointClassesAxiom =
  rawAnnotated []
    (rawDisjointClasses
      (rawObjectComplementOf (rawNamedClass declaredClassIri) ∷
       rawNamedClass superClassIri ∷ []))

booleanClassesDocument : RawOntology
booleanClassesDocument =
  rawOntology
    anonymousSource
    absent
    absent
    []
    []
    (declaredClassAxiom ∷
     superClassAxiom ∷
     booleanClassConstructorsSubClassAxiom ∷
     equivalentClassesAxiom ∷
     disjointClassesAxiom ∷ [])

booleanClassesResult : ElaborationResult
booleanClassesResult =
  elaborateStructuralKernelStrict booleanClassesDocument

booleanClassesClean : Clean booleanClassesResult
booleanClassesClean =
  tt

booleanClassesEvidence : EvidenceAvailable booleanClassesResult
booleanClassesEvidence =
  cleanEvidence booleanClassesResult booleanClassesClean

booleanClassesChecked : CheckedImport
booleanClassesChecked =
  elaborationSucceeded booleanClassesResult booleanClassesEvidence

booleanClassesClassCount :
  K.classCount (signature booleanClassesChecked) ≡ 2
booleanClassesClassCount =
  refl

booleanClassesAxiomCount :
  listCount (K.axioms (ontology booleanClassesChecked)) ≡ 5
booleanClassesAxiomCount =
  refl

parentRelationIri : RawIRI
parentRelationIri =
  rawIRI "http://example.test/parentRelation"

parentRelationAxiom : RawAnnotated RawAxiom
parentRelationAxiom =
  rawAnnotated []
    (rawDeclaration (rawEntity rawObjectProperty parentRelationIri))

dataValueIri : RawIRI
dataValueIri =
  rawIRI "http://example.test/dataValue"

parentDataValueIri : RawIRI
parentDataValueIri =
  rawIRI "http://example.test/parentDataValue"

dataValueAxiom : RawAnnotated RawAxiom
dataValueAxiom =
  rawAnnotated []
    (rawDeclaration (rawEntity rawDataProperty dataValueIri))

parentDataValueAxiom : RawAnnotated RawAxiom
parentDataValueAxiom =
  rawAnnotated []
    (rawDeclaration (rawEntity rawDataProperty parentDataValueIri))

subObjectPropertyAxiom : RawAnnotated RawAxiom
subObjectPropertyAxiom =
  rawAnnotated []
    (rawSubObjectPropertyOf
      (rawSubObjectProperty (rawObjectProperty relatedToIri))
      (rawObjectProperty parentRelationIri))

objectPropertyDomainAxiom : RawAnnotated RawAxiom
objectPropertyDomainAxiom =
  rawAnnotated []
    (rawObjectPropertyDomain
      (rawObjectProperty relatedToIri)
      (rawNamedClass declaredClassIri))

objectPropertyRangeAxiom : RawAnnotated RawAxiom
objectPropertyRangeAxiom =
  rawAnnotated []
    (rawObjectPropertyRange
      (rawObjectProperty relatedToIri)
      (rawNamedClass superClassIri))

subDataPropertyAxiom : RawAnnotated RawAxiom
subDataPropertyAxiom =
  rawAnnotated []
    (rawSubDataPropertyOf
      (rawDataProperty dataValueIri)
      (rawDataProperty parentDataValueIri))

dataPropertyDomainAxiom : RawAnnotated RawAxiom
dataPropertyDomainAxiom =
  rawAnnotated []
    (rawDataPropertyDomain
      (rawDataProperty dataValueIri)
      (rawNamedClass declaredClassIri))

propertyAxiomsDocument : RawOntology
propertyAxiomsDocument =
  rawOntology
    anonymousSource
    absent
    absent
    []
    []
    (declaredClassAxiom ∷
     superClassAxiom ∷
     relatedToAxiom ∷
     parentRelationAxiom ∷
     dataValueAxiom ∷
     parentDataValueAxiom ∷
     subObjectPropertyAxiom ∷
     objectPropertyDomainAxiom ∷
     objectPropertyRangeAxiom ∷
     subDataPropertyAxiom ∷
     dataPropertyDomainAxiom ∷ [])

propertyAxiomsResult : ElaborationResult
propertyAxiomsResult =
  elaborateStructuralKernelStrict propertyAxiomsDocument

propertyAxiomsClean : Clean propertyAxiomsResult
propertyAxiomsClean =
  tt

propertyAxiomsEvidence : EvidenceAvailable propertyAxiomsResult
propertyAxiomsEvidence =
  cleanEvidence propertyAxiomsResult propertyAxiomsClean

propertyAxiomsChecked : CheckedImport
propertyAxiomsChecked =
  elaborationSucceeded propertyAxiomsResult propertyAxiomsEvidence

propertyAxiomsClassCount :
  K.classCount (signature propertyAxiomsChecked) ≡ 2
propertyAxiomsClassCount =
  refl

propertyAxiomsObjectPropertyCount :
  K.objectPropertyCount (signature propertyAxiomsChecked) ≡ 2
propertyAxiomsObjectPropertyCount =
  refl

propertyAxiomsDataPropertyCount :
  K.dataPropertyCount (signature propertyAxiomsChecked) ≡ 2
propertyAxiomsDataPropertyCount =
  refl

propertyAxiomsObjectRoleIRIs :
  roleObjectPropertyIRIs
    (sourcePropertyRoleEvidence propertyAxiomsChecked) ≡
  relatedToIri ∷ parentRelationIri ∷ []
propertyAxiomsObjectRoleIRIs =
  refl

propertyAxiomsDataRoleIRIs :
  roleDataPropertyIRIs
    (sourcePropertyRoleEvidence propertyAxiomsChecked) ≡
  dataValueIri ∷ parentDataValueIri ∷ []
propertyAxiomsDataRoleIRIs =
  refl

propertyAxiomsAxiomCount :
  listCount (K.axioms (ontology propertyAxiomsChecked)) ≡ 11
propertyAxiomsAxiomCount =
  refl

equivalentObjectPropertiesAxiom : RawAnnotated RawAxiom
equivalentObjectPropertiesAxiom =
  rawAnnotated []
    (rawEquivalentObjectProperties
      (rawObjectProperty relatedToIri ∷
       rawObjectProperty parentRelationIri ∷ []))

disjointObjectPropertiesAxiom : RawAnnotated RawAxiom
disjointObjectPropertiesAxiom =
  rawAnnotated []
    (rawDisjointObjectProperties
      (rawObjectProperty relatedToIri ∷
       rawObjectProperty parentRelationIri ∷ []))

inverseObjectPropertiesAxiom : RawAnnotated RawAxiom
inverseObjectPropertiesAxiom =
  rawAnnotated []
    (rawInverseObjectProperties
      (rawObjectProperty relatedToIri)
      (rawObjectInverseOf (rawObjectProperty parentRelationIri)))

functionalObjectPropertyAxiom : RawAnnotated RawAxiom
functionalObjectPropertyAxiom =
  rawAnnotated []
    (rawFunctionalObjectProperty (rawObjectProperty relatedToIri))

inverseFunctionalObjectPropertyAxiom : RawAnnotated RawAxiom
inverseFunctionalObjectPropertyAxiom =
  rawAnnotated []
    (rawInverseFunctionalObjectProperty (rawObjectProperty relatedToIri))

reflexiveObjectPropertyAxiom : RawAnnotated RawAxiom
reflexiveObjectPropertyAxiom =
  rawAnnotated []
    (rawReflexiveObjectProperty rawTopObjectProperty)

irreflexiveObjectPropertyAxiom : RawAnnotated RawAxiom
irreflexiveObjectPropertyAxiom =
  rawAnnotated []
    (rawIrreflexiveObjectProperty (rawObjectProperty relatedToIri))

symmetricObjectPropertyAxiom : RawAnnotated RawAxiom
symmetricObjectPropertyAxiom =
  rawAnnotated []
    (rawSymmetricObjectProperty
      (rawObjectInverseOf (rawObjectProperty relatedToIri)))

asymmetricObjectPropertyAxiom : RawAnnotated RawAxiom
asymmetricObjectPropertyAxiom =
  rawAnnotated []
    (rawAsymmetricObjectProperty (rawObjectProperty relatedToIri))

transitiveRelationIri : RawIRI
transitiveRelationIri =
  rawIRI "http://example.test/transitiveRelation"

transitiveRelationAxiom : RawAnnotated RawAxiom
transitiveRelationAxiom =
  rawAnnotated []
    (rawDeclaration (rawEntity rawObjectProperty transitiveRelationIri))

transitiveObjectPropertyAxiom : RawAnnotated RawAxiom
transitiveObjectPropertyAxiom =
  rawAnnotated []
    (rawTransitiveObjectProperty (rawObjectProperty transitiveRelationIri))

objectPropertyCharacteristicsDocument : RawOntology
objectPropertyCharacteristicsDocument =
  rawOntology
    anonymousSource
    absent
    absent
    []
    []
    (relatedToAxiom ∷
     parentRelationAxiom ∷
     equivalentObjectPropertiesAxiom ∷
     disjointObjectPropertiesAxiom ∷
     inverseObjectPropertiesAxiom ∷
     functionalObjectPropertyAxiom ∷
     inverseFunctionalObjectPropertyAxiom ∷
     reflexiveObjectPropertyAxiom ∷
     irreflexiveObjectPropertyAxiom ∷
     symmetricObjectPropertyAxiom ∷
     asymmetricObjectPropertyAxiom ∷ [])

objectPropertyCharacteristicsResult : ElaborationResult
objectPropertyCharacteristicsResult =
  elaborateStructuralKernelStrict objectPropertyCharacteristicsDocument

objectPropertyCharacteristicsClean :
  Clean objectPropertyCharacteristicsResult
objectPropertyCharacteristicsClean =
  tt

objectPropertyCharacteristicsEvidence :
  EvidenceAvailable objectPropertyCharacteristicsResult
objectPropertyCharacteristicsEvidence =
  cleanEvidence
    objectPropertyCharacteristicsResult
    objectPropertyCharacteristicsClean

objectPropertyCharacteristicsChecked : CheckedImport
objectPropertyCharacteristicsChecked =
  elaborationSucceeded
    objectPropertyCharacteristicsResult
    objectPropertyCharacteristicsEvidence

objectPropertyCharacteristicsObjectPropertyCount :
  K.objectPropertyCount (signature objectPropertyCharacteristicsChecked) ≡ 2
objectPropertyCharacteristicsObjectPropertyCount =
  refl

objectPropertyCharacteristicsAxiomCount :
  listCount (K.axioms (ontology objectPropertyCharacteristicsChecked)) ≡ 11
objectPropertyCharacteristicsAxiomCount =
  refl

transitiveObjectPropertyDocument : RawOntology
transitiveObjectPropertyDocument =
  rawOntology
    anonymousSource
    absent
    absent
    []
    []
    (transitiveRelationAxiom ∷
     transitiveObjectPropertyAxiom ∷ [])

transitiveObjectPropertyResult : ElaborationResult
transitiveObjectPropertyResult =
  elaborateStructuralKernelStrict transitiveObjectPropertyDocument

transitiveObjectPropertyClean :
  Clean transitiveObjectPropertyResult
transitiveObjectPropertyClean =
  tt

transitiveObjectPropertyEvidence :
  EvidenceAvailable transitiveObjectPropertyResult
transitiveObjectPropertyEvidence =
  cleanEvidence
    transitiveObjectPropertyResult
    transitiveObjectPropertyClean

transitiveObjectPropertyChecked : CheckedImport
transitiveObjectPropertyChecked =
  elaborationSucceeded
    transitiveObjectPropertyResult
    transitiveObjectPropertyEvidence

transitiveObjectPropertyObjectPropertyCount :
  K.objectPropertyCount (signature transitiveObjectPropertyChecked) ≡ 1
transitiveObjectPropertyObjectPropertyCount =
  refl

transitiveObjectPropertyAxiomCount :
  listCount (K.axioms (ontology transitiveObjectPropertyChecked)) ≡ 2
transitiveObjectPropertyAxiomCount =
  refl

equivalentDataPropertiesAxiom : RawAnnotated RawAxiom
equivalentDataPropertiesAxiom =
  rawAnnotated []
    (rawEquivalentDataProperties
      (rawDataProperty dataValueIri ∷
       rawDataProperty parentDataValueIri ∷ []))

disjointDataPropertiesAxiom : RawAnnotated RawAxiom
disjointDataPropertiesAxiom =
  rawAnnotated []
    (rawDisjointDataProperties
      (rawDataProperty dataValueIri ∷
       rawDataProperty parentDataValueIri ∷ []))

functionalDataPropertyAxiom : RawAnnotated RawAxiom
functionalDataPropertyAxiom =
  rawAnnotated []
    (rawFunctionalDataProperty (rawDataProperty dataValueIri))

dataPropertyCharacteristicsDocument : RawOntology
dataPropertyCharacteristicsDocument =
  rawOntology
    anonymousSource
    absent
    absent
    []
    []
    (dataValueAxiom ∷
     parentDataValueAxiom ∷
     equivalentDataPropertiesAxiom ∷
     disjointDataPropertiesAxiom ∷
     functionalDataPropertyAxiom ∷ [])

dataPropertyCharacteristicsResult : ElaborationResult
dataPropertyCharacteristicsResult =
  elaborateStructuralKernelStrict dataPropertyCharacteristicsDocument

dataPropertyCharacteristicsClean : Clean dataPropertyCharacteristicsResult
dataPropertyCharacteristicsClean =
  tt

dataPropertyCharacteristicsEvidence :
  EvidenceAvailable dataPropertyCharacteristicsResult
dataPropertyCharacteristicsEvidence =
  cleanEvidence
    dataPropertyCharacteristicsResult
    dataPropertyCharacteristicsClean

dataPropertyCharacteristicsChecked : CheckedImport
dataPropertyCharacteristicsChecked =
  elaborationSucceeded
    dataPropertyCharacteristicsResult
    dataPropertyCharacteristicsEvidence

dataPropertyCharacteristicsDataPropertyCount :
  K.dataPropertyCount (signature dataPropertyCharacteristicsChecked) ≡ 2
dataPropertyCharacteristicsDataPropertyCount =
  refl

dataPropertyCharacteristicsAxiomCount :
  listCount (K.axioms (ontology dataPropertyCharacteristicsChecked)) ≡ 5
dataPropertyCharacteristicsAxiomCount =
  refl

aliceIri : RawIRI
aliceIri =
  rawIRI "http://example.test/Alice"

bobIri : RawIRI
bobIri =
  rawIRI "http://example.test/Bob"

aliceAxiom : RawAnnotated RawAxiom
aliceAxiom =
  rawAnnotated []
    (rawDeclaration (rawEntity rawIndividual aliceIri))

bobAxiom : RawAnnotated RawAxiom
bobAxiom =
  rawAnnotated []
    (rawDeclaration (rawEntity rawIndividual bobIri))

classAssertionAxiom : RawAnnotated RawAxiom
classAssertionAxiom =
  rawAnnotated []
    (rawClassAssertion
      (rawNamedClass declaredClassIri)
      (rawNamedIndividual aliceIri))

objectPropertyAssertionAxiom : RawAnnotated RawAxiom
objectPropertyAssertionAxiom =
  rawAnnotated []
    (rawObjectPropertyAssertion
      (rawObjectProperty relatedToIri)
      (rawNamedIndividual aliceIri)
      (rawNamedIndividual bobIri))

aboxDocument : RawOntology
aboxDocument =
  rawOntology
    anonymousSource
    absent
    absent
    []
    []
    (declaredClassAxiom ∷
     relatedToAxiom ∷
     aliceAxiom ∷
     bobAxiom ∷
     classAssertionAxiom ∷
     objectPropertyAssertionAxiom ∷ [])

aboxResult : ElaborationResult
aboxResult =
  elaborateStructuralKernelStrict aboxDocument

aboxClean : Clean aboxResult
aboxClean =
  tt

aboxEvidence : EvidenceAvailable aboxResult
aboxEvidence =
  cleanEvidence aboxResult aboxClean

aboxChecked : CheckedImport
aboxChecked =
  elaborationSucceeded aboxResult aboxEvidence

aboxClassCount : K.classCount (signature aboxChecked) ≡ 1
aboxClassCount =
  refl

aboxObjectPropertyCount :
  K.objectPropertyCount (signature aboxChecked) ≡ 1
aboxObjectPropertyCount =
  refl

aboxIndividualCount : K.individualCount (signature aboxChecked) ≡ 2
aboxIndividualCount =
  refl

aboxAxiomCount : listCount (K.axioms (ontology aboxChecked)) ≡ 6
aboxAxiomCount =
  refl

objectHasValueAxiom : RawAnnotated RawAxiom
objectHasValueAxiom =
  rawAnnotated []
    (rawSubClassOf
      (rawNamedClass declaredClassIri)
      (rawObjectHasValue
        (rawObjectProperty relatedToIri)
        (rawNamedIndividual aliceIri)))

objectOneOfAxiom : RawAnnotated RawAxiom
objectOneOfAxiom =
  rawAnnotated []
    (rawSubClassOf
      (rawNamedClass declaredClassIri)
      (rawObjectOneOf
        (rawNamedIndividual aliceIri ∷
         rawNamedIndividual bobIri ∷ [])))

objectValueAndNominalDocument : RawOntology
objectValueAndNominalDocument =
  rawOntology
    anonymousSource
    absent
    absent
    []
    []
    (declaredClassAxiom ∷
     relatedToAxiom ∷
     aliceAxiom ∷
     bobAxiom ∷
     objectHasValueAxiom ∷
     objectOneOfAxiom ∷ [])

objectValueAndNominalResult : ElaborationResult
objectValueAndNominalResult =
  elaborateStructuralKernelStrict objectValueAndNominalDocument

objectValueAndNominalClean : Clean objectValueAndNominalResult
objectValueAndNominalClean =
  tt

objectValueAndNominalEvidence :
  EvidenceAvailable objectValueAndNominalResult
objectValueAndNominalEvidence =
  cleanEvidence
    objectValueAndNominalResult
    objectValueAndNominalClean

objectValueAndNominalChecked : CheckedImport
objectValueAndNominalChecked =
  elaborationSucceeded
    objectValueAndNominalResult
    objectValueAndNominalEvidence

objectValueAndNominalClassCount :
  K.classCount (signature objectValueAndNominalChecked) ≡ 1
objectValueAndNominalClassCount =
  refl

objectValueAndNominalObjectPropertyCount :
  K.objectPropertyCount (signature objectValueAndNominalChecked) ≡ 1
objectValueAndNominalObjectPropertyCount =
  refl

objectValueAndNominalIndividualCount :
  K.individualCount (signature objectValueAndNominalChecked) ≡ 2
objectValueAndNominalIndividualCount =
  refl

objectValueAndNominalAxiomCount :
  listCount (K.axioms (ontology objectValueAndNominalChecked)) ≡ 6
objectValueAndNominalAxiomCount =
  refl

objectHasSelfAxiom : RawAnnotated RawAxiom
objectHasSelfAxiom =
  rawAnnotated []
    (rawSubClassOf
      (rawNamedClass declaredClassIri)
      (rawObjectHasSelf (rawObjectProperty relatedToIri)))

objectMinCardinalityAxiom : RawAnnotated RawAxiom
objectMinCardinalityAxiom =
  rawAnnotated []
    (rawSubClassOf
      (rawNamedClass declaredClassIri)
      (rawObjectMinCardinality
        1
        (rawObjectProperty relatedToIri)
        (present (rawNamedClass superClassIri))))

objectMaxCardinalityAxiom : RawAnnotated RawAxiom
objectMaxCardinalityAxiom =
  rawAnnotated []
    (rawSubClassOf
      (rawNamedClass declaredClassIri)
      (rawObjectMaxCardinality
        2
        (rawObjectProperty relatedToIri)
        absent))

objectExactCardinalityAxiom : RawAnnotated RawAxiom
objectExactCardinalityAxiom =
  rawAnnotated []
    (rawSubClassOf
      (rawNamedClass declaredClassIri)
      (rawObjectExactCardinality
        1
        (rawObjectProperty relatedToIri)
        (present rawOwlThing)))

objectSelfAndCardinalityDocument : RawOntology
objectSelfAndCardinalityDocument =
  rawOntology
    anonymousSource
    absent
    absent
    []
    []
    (declaredClassAxiom ∷
     superClassAxiom ∷
     relatedToAxiom ∷
     objectHasSelfAxiom ∷
     objectMinCardinalityAxiom ∷
     objectMaxCardinalityAxiom ∷
     objectExactCardinalityAxiom ∷ [])

objectSelfAndCardinalityResult : ElaborationResult
objectSelfAndCardinalityResult =
  elaborateStructuralKernelStrict objectSelfAndCardinalityDocument

objectSelfAndCardinalityClean : Clean objectSelfAndCardinalityResult
objectSelfAndCardinalityClean =
  tt

objectSelfAndCardinalityEvidence :
  EvidenceAvailable objectSelfAndCardinalityResult
objectSelfAndCardinalityEvidence =
  cleanEvidence
    objectSelfAndCardinalityResult
    objectSelfAndCardinalityClean

objectSelfAndCardinalityChecked : CheckedImport
objectSelfAndCardinalityChecked =
  elaborationSucceeded
    objectSelfAndCardinalityResult
    objectSelfAndCardinalityEvidence

objectSelfAndCardinalityClassCount :
  K.classCount (signature objectSelfAndCardinalityChecked) ≡ 2
objectSelfAndCardinalityClassCount =
  refl

objectSelfAndCardinalityObjectPropertyCount :
  K.objectPropertyCount (signature objectSelfAndCardinalityChecked) ≡ 1
objectSelfAndCardinalityObjectPropertyCount =
  refl

objectSelfAndCardinalityAxiomCount :
  listCount (K.axioms (ontology objectSelfAndCardinalityChecked)) ≡ 7
objectSelfAndCardinalityAxiomCount =
  refl

stringDatatypeIri : RawIRI
stringDatatypeIri =
  rawIRI "http://www.w3.org/2001/XMLSchema#string"

stringDatatypeAxiom : RawAnnotated RawAxiom
stringDatatypeAxiom =
  rawAnnotated []
    (rawDeclaration (rawEntity rawDatatype stringDatatypeIri))

typedStringLiteral : RawLiteral
typedStringLiteral =
  rawLiteral "hello" (present stringDatatypeIri) absent

dataPropertyRangeAxiom : RawAnnotated RawAxiom
dataPropertyRangeAxiom =
  rawAnnotated []
    (rawDataPropertyRange
      (rawDataProperty dataValueIri)
      (rawDatatype stringDatatypeIri))

dataPropertyAssertionAxiom : RawAnnotated RawAxiom
dataPropertyAssertionAxiom =
  rawAnnotated []
    (rawDataPropertyAssertion
      (rawDataProperty dataValueIri)
      (rawNamedIndividual aliceIri)
      typedStringLiteral)

dataAssertionDocument : RawOntology
dataAssertionDocument =
  rawOntology
    anonymousSource
    absent
    absent
    []
    []
    (dataValueAxiom ∷
     stringDatatypeAxiom ∷
     aliceAxiom ∷
     dataPropertyRangeAxiom ∷
     dataPropertyAssertionAxiom ∷ [])

dataAssertionResult : ElaborationResult
dataAssertionResult =
  elaborateStructuralKernelStrict dataAssertionDocument

dataAssertionClean : Clean dataAssertionResult
dataAssertionClean =
  tt

dataAssertionEvidence : EvidenceAvailable dataAssertionResult
dataAssertionEvidence =
  cleanEvidence dataAssertionResult dataAssertionClean

dataAssertionChecked : CheckedImport
dataAssertionChecked =
  elaborationSucceeded dataAssertionResult dataAssertionEvidence

dataAssertionDataPropertyCount :
  K.dataPropertyCount (signature dataAssertionChecked) ≡ 1
dataAssertionDataPropertyCount =
  refl

dataAssertionDatatypeCount :
  K.datatypeCount (signature dataAssertionChecked) ≡ 1
dataAssertionDatatypeCount =
  refl

dataAssertionIndividualCount :
  K.individualCount (signature dataAssertionChecked) ≡ 1
dataAssertionIndividualCount =
  refl

dataAssertionAxiomCount :
  listCount (K.axioms (ontology dataAssertionChecked)) ≡ 5
dataAssertionAxiomCount =
  refl

dataAssertionDatatypeSupportGenerated :
  K.datatypeSupport (ontology dataAssertionChecked) ≡
  K.completeOntologyDatatypeSupport (K.axioms (ontology dataAssertionChecked))
dataAssertionDatatypeSupportGenerated =
  refl

sameIndividualAxiom : RawAnnotated RawAxiom
sameIndividualAxiom =
  rawAnnotated []
    (rawSameIndividual
      (rawNamedIndividual aliceIri ∷
       rawNamedIndividual bobIri ∷ []))

differentIndividualsAxiom : RawAnnotated RawAxiom
differentIndividualsAxiom =
  rawAnnotated []
    (rawDifferentIndividuals
      (rawNamedIndividual aliceIri ∷
       rawNamedIndividual bobIri ∷ []))

negativeObjectPropertyAssertionAxiom : RawAnnotated RawAxiom
negativeObjectPropertyAssertionAxiom =
  rawAnnotated []
    (rawNegativeObjectPropertyAssertion
      (rawObjectProperty relatedToIri)
      (rawNamedIndividual aliceIri)
      (rawNamedIndividual bobIri))

negativeDataPropertyAssertionAxiom : RawAnnotated RawAxiom
negativeDataPropertyAssertionAxiom =
  rawAnnotated []
    (rawNegativeDataPropertyAssertion
      (rawDataProperty dataValueIri)
      (rawNamedIndividual aliceIri)
      typedStringLiteral)

extendedABoxDocument : RawOntology
extendedABoxDocument =
  rawOntology
    anonymousSource
    absent
    absent
    []
    []
    (relatedToAxiom ∷
     dataValueAxiom ∷
     stringDatatypeAxiom ∷
     aliceAxiom ∷
     bobAxiom ∷
     sameIndividualAxiom ∷
     differentIndividualsAxiom ∷
     negativeObjectPropertyAssertionAxiom ∷
     negativeDataPropertyAssertionAxiom ∷ [])

extendedABoxResult : ElaborationResult
extendedABoxResult =
  elaborateStructuralKernelStrict extendedABoxDocument

extendedABoxClean : Clean extendedABoxResult
extendedABoxClean =
  tt

extendedABoxEvidence : EvidenceAvailable extendedABoxResult
extendedABoxEvidence =
  cleanEvidence extendedABoxResult extendedABoxClean

extendedABoxChecked : CheckedImport
extendedABoxChecked =
  elaborationSucceeded extendedABoxResult extendedABoxEvidence

extendedABoxObjectPropertyCount :
  K.objectPropertyCount (signature extendedABoxChecked) ≡ 1
extendedABoxObjectPropertyCount =
  refl

extendedABoxDataPropertyCount :
  K.dataPropertyCount (signature extendedABoxChecked) ≡ 1
extendedABoxDataPropertyCount =
  refl

extendedABoxDatatypeCount :
  K.datatypeCount (signature extendedABoxChecked) ≡ 1
extendedABoxDatatypeCount =
  refl

extendedABoxIndividualCount :
  K.individualCount (signature extendedABoxChecked) ≡ 2
extendedABoxIndividualCount =
  refl

extendedABoxAxiomCount :
  listCount (K.axioms (ontology extendedABoxChecked)) ≡ 9
extendedABoxAxiomCount =
  refl

dataSomeValuesAxiom : RawAnnotated RawAxiom
dataSomeValuesAxiom =
  rawAnnotated []
    (rawSubClassOf
      (rawNamedClass declaredClassIri)
      (rawDataSomeValuesFrom
        (rawDataProperty dataValueIri)
        (rawDatatype stringDatatypeIri)))

dataAllValuesAxiom : RawAnnotated RawAxiom
dataAllValuesAxiom =
  rawAnnotated []
    (rawSubClassOf
      (rawNamedClass declaredClassIri)
      (rawDataAllValuesFrom
        (rawDataProperty dataValueIri)
        (rawDatatype stringDatatypeIri)))

dataHasValueAxiom : RawAnnotated RawAxiom
dataHasValueAxiom =
  rawAnnotated []
    (rawSubClassOf
      (rawNamedClass declaredClassIri)
      (rawDataHasValue
        (rawDataProperty dataValueIri)
        typedStringLiteral))

dataMinCardinalityAxiom : RawAnnotated RawAxiom
dataMinCardinalityAxiom =
  rawAnnotated []
    (rawSubClassOf
      (rawNamedClass declaredClassIri)
      (rawDataMinCardinality
        1
        (rawDataProperty dataValueIri)
        (present (rawDatatype stringDatatypeIri))))

dataMaxCardinalityAxiom : RawAnnotated RawAxiom
dataMaxCardinalityAxiom =
  rawAnnotated []
    (rawSubClassOf
      (rawNamedClass declaredClassIri)
      (rawDataMaxCardinality 2 (rawDataProperty dataValueIri) absent))

dataExactCardinalityAxiom : RawAnnotated RawAxiom
dataExactCardinalityAxiom =
  rawAnnotated []
    (rawSubClassOf
      (rawNamedClass declaredClassIri)
      (rawDataExactCardinality
        1
        (rawDataProperty dataValueIri)
        (present (rawDatatype stringDatatypeIri))))

dataRestrictionsDocument : RawOntology
dataRestrictionsDocument =
  rawOntology
    anonymousSource
    absent
    absent
    []
    []
    (declaredClassAxiom ∷
     dataValueAxiom ∷
     stringDatatypeAxiom ∷
     dataSomeValuesAxiom ∷
     dataAllValuesAxiom ∷
     dataHasValueAxiom ∷
     dataMinCardinalityAxiom ∷
     dataMaxCardinalityAxiom ∷
     dataExactCardinalityAxiom ∷ [])

dataRestrictionsResult : ElaborationResult
dataRestrictionsResult =
  elaborateStructuralKernelStrict dataRestrictionsDocument

dataRestrictionsClean : Clean dataRestrictionsResult
dataRestrictionsClean =
  tt

dataRestrictionsEvidence : EvidenceAvailable dataRestrictionsResult
dataRestrictionsEvidence =
  cleanEvidence dataRestrictionsResult dataRestrictionsClean

dataRestrictionsChecked : CheckedImport
dataRestrictionsChecked =
  elaborationSucceeded dataRestrictionsResult dataRestrictionsEvidence

dataRestrictionsClassCount :
  K.classCount (signature dataRestrictionsChecked) ≡ 1
dataRestrictionsClassCount =
  refl

dataRestrictionsDataPropertyCount :
  K.dataPropertyCount (signature dataRestrictionsChecked) ≡ 1
dataRestrictionsDataPropertyCount =
  refl

dataRestrictionsDatatypeCount :
  K.datatypeCount (signature dataRestrictionsChecked) ≡ 1
dataRestrictionsDatatypeCount =
  refl

dataRestrictionsAxiomCount :
  listCount (K.axioms (ontology dataRestrictionsChecked)) ≡ 9
dataRestrictionsAxiomCount =
  refl

dataComplementRangeAxiom : RawAnnotated RawAxiom
dataComplementRangeAxiom =
  rawAnnotated []
    (rawDataPropertyRange
      (rawDataProperty dataValueIri)
      (rawDataComplementOf (rawDatatype stringDatatypeIri)))

dataIntersectionRangeAxiom : RawAnnotated RawAxiom
dataIntersectionRangeAxiom =
  rawAnnotated []
    (rawDataPropertyRange
      (rawDataProperty dataValueIri)
      (rawDataIntersectionOf
        (rawDatatype stringDatatypeIri ∷
         rawDataTop ∷ [])))

dataUnionRangeAxiom : RawAnnotated RawAxiom
dataUnionRangeAxiom =
  rawAnnotated []
    (rawDataPropertyRange
      (rawDataProperty dataValueIri)
      (rawDataUnionOf
        (rawDataBottom ∷
         rawDatatype stringDatatypeIri ∷ [])))

dataOneOfRangeAxiom : RawAnnotated RawAxiom
dataOneOfRangeAxiom =
  rawAnnotated []
    (rawDataPropertyRange
      (rawDataProperty dataValueIri)
      (rawDataOneOf (typedStringLiteral ∷ [])))

lengthFacetIri : RawIRI
lengthFacetIri =
  rawIRI "http://www.w3.org/2001/XMLSchema#length"

facetDatatypeRestrictionRangeAxiom : RawAnnotated RawAxiom
facetDatatypeRestrictionRangeAxiom =
  rawAnnotated []
    (rawDataPropertyRange
      (rawDataProperty dataValueIri)
      (rawDatatypeRestriction
        stringDatatypeIri
        (rawFacetRestriction lengthFacetIri typedStringLiteral ∷ [])))

emptyDatatypeRestrictionRangeAxiom : RawAnnotated RawAxiom
emptyDatatypeRestrictionRangeAxiom =
  rawAnnotated []
    (rawDataPropertyRange
      (rawDataProperty dataValueIri)
      (rawDatatypeRestriction stringDatatypeIri []))

dataRangeConstructorsDocument : RawOntology
dataRangeConstructorsDocument =
  rawOntology
    anonymousSource
    absent
    absent
    []
    []
    (dataValueAxiom ∷
     stringDatatypeAxiom ∷
     dataComplementRangeAxiom ∷
     dataIntersectionRangeAxiom ∷
     dataUnionRangeAxiom ∷
     dataOneOfRangeAxiom ∷
     facetDatatypeRestrictionRangeAxiom ∷
     emptyDatatypeRestrictionRangeAxiom ∷ [])

dataRangeConstructorsResult : ElaborationResult
dataRangeConstructorsResult =
  elaborateStructuralKernelStrict dataRangeConstructorsDocument

dataRangeConstructorsClean : Clean dataRangeConstructorsResult
dataRangeConstructorsClean =
  tt

dataRangeConstructorsEvidence :
  EvidenceAvailable dataRangeConstructorsResult
dataRangeConstructorsEvidence =
  cleanEvidence
    dataRangeConstructorsResult
    dataRangeConstructorsClean

dataRangeConstructorsChecked : CheckedImport
dataRangeConstructorsChecked =
  elaborationSucceeded
    dataRangeConstructorsResult
    dataRangeConstructorsEvidence

dataRangeConstructorsDataPropertyCount :
  K.dataPropertyCount (signature dataRangeConstructorsChecked) ≡ 1
dataRangeConstructorsDataPropertyCount =
  refl

dataRangeConstructorsDatatypeCount :
  K.datatypeCount (signature dataRangeConstructorsChecked) ≡ 1
dataRangeConstructorsDatatypeCount =
  refl

dataRangeConstructorsFacetCount :
  K.facetCount (signature dataRangeConstructorsChecked) ≡ 1
dataRangeConstructorsFacetCount =
  refl

dataRangeConstructorsAxiomCount :
  listCount (K.axioms (ontology dataRangeConstructorsChecked)) ≡ 8
dataRangeConstructorsAxiomCount =
  refl

disjointUnionAxiom : RawAnnotated RawAxiom
disjointUnionAxiom =
  rawAnnotated []
    (rawDisjointUnion
      declaredClassIri
      (rawNamedClass superClassIri ∷
       rawOwlThing ∷ []))

datatypeDefinitionAxiom : RawAnnotated RawAxiom
datatypeDefinitionAxiom =
  rawAnnotated []
    (rawDatatypeDefinition stringDatatypeIri rawDataTop)

hasKeyAxiom : RawAnnotated RawAxiom
hasKeyAxiom =
  rawAnnotated []
    (rawHasKey
      (rawNamedClass declaredClassIri)
      (rawObjectProperty relatedToIri ∷ [])
      (rawDataProperty dataValueIri ∷ []))

remainingStructuralAxiomsDocument : RawOntology
remainingStructuralAxiomsDocument =
  rawOntology
    anonymousSource
    absent
    absent
    []
    []
    (declaredClassAxiom ∷
     superClassAxiom ∷
     relatedToAxiom ∷
     dataValueAxiom ∷
     stringDatatypeAxiom ∷
     disjointUnionAxiom ∷
     datatypeDefinitionAxiom ∷
     hasKeyAxiom ∷ [])

remainingStructuralAxiomsResult : ElaborationResult
remainingStructuralAxiomsResult =
  elaborateStructuralKernelStrict remainingStructuralAxiomsDocument

remainingStructuralAxiomsClean : Clean remainingStructuralAxiomsResult
remainingStructuralAxiomsClean =
  tt

remainingStructuralAxiomsEvidence :
  EvidenceAvailable remainingStructuralAxiomsResult
remainingStructuralAxiomsEvidence =
  cleanEvidence
    remainingStructuralAxiomsResult
    remainingStructuralAxiomsClean

remainingStructuralAxiomsChecked : CheckedImport
remainingStructuralAxiomsChecked =
  elaborationSucceeded
    remainingStructuralAxiomsResult
    remainingStructuralAxiomsEvidence

remainingStructuralAxiomsClassCount :
  K.classCount (signature remainingStructuralAxiomsChecked) ≡ 2
remainingStructuralAxiomsClassCount =
  refl

remainingStructuralAxiomsObjectPropertyCount :
  K.objectPropertyCount (signature remainingStructuralAxiomsChecked) ≡ 1
remainingStructuralAxiomsObjectPropertyCount =
  refl

remainingStructuralAxiomsDataPropertyCount :
  K.dataPropertyCount (signature remainingStructuralAxiomsChecked) ≡ 1
remainingStructuralAxiomsDataPropertyCount =
  refl

remainingStructuralAxiomsDatatypeCount :
  K.datatypeCount (signature remainingStructuralAxiomsChecked) ≡ 1
remainingStructuralAxiomsDatatypeCount =
  refl

remainingStructuralAxiomsAxiomCount :
  listCount (K.axioms (ontology remainingStructuralAxiomsChecked)) ≡ 8
remainingStructuralAxiomsAxiomCount =
  refl

labelAnnotationIri : RawIRI
labelAnnotationIri =
  rawIRI "http://example.test/label"

commentAnnotationIri : RawIRI
commentAnnotationIri =
  rawIRI "http://example.test/comment"

annotationSubjectIri : RawIRI
annotationSubjectIri =
  rawIRI "http://example.test/subject"

annotationValueIri : RawIRI
annotationValueIri =
  rawIRI "http://example.test/value"

axiomAnnotation : RawAnnotation
axiomAnnotation =
  rawAnnotation []
    labelAnnotationIri
    (rawAnnotationValueLiteral
      (rawLiteral "axiom metadata" (present stringDatatypeIri) absent))

ontologyNestedAnnotation : RawAnnotation
ontologyNestedAnnotation =
  rawAnnotation []
    commentAnnotationIri
    (rawAnnotationValueLiteral
      (rawLiteral "nested metadata" (present stringDatatypeIri) absent))

ontologyAnnotation : RawAnnotation
ontologyAnnotation =
  rawAnnotation
    (ontologyNestedAnnotation ∷ [])
    labelAnnotationIri
    (rawAnnotationValueLiteral
      (rawLiteral "ontology metadata" (present stringDatatypeIri) absent))

labelAnnotationAxiom : RawAnnotated RawAxiom
labelAnnotationAxiom =
  rawAnnotated (axiomAnnotation ∷ [])
    (rawDeclaration (rawEntity rawAnnotationProperty labelAnnotationIri))

commentAnnotationAxiom : RawAnnotated RawAxiom
commentAnnotationAxiom =
  rawAnnotated []
    (rawDeclaration (rawEntity rawAnnotationProperty commentAnnotationIri))

annotationSubjectClassAxiom : RawAnnotated RawAxiom
annotationSubjectClassAxiom =
  rawAnnotated []
    (rawDeclaration (rawEntity rawClass annotationSubjectIri))

annotationIRIAssertionAxiom : RawAnnotated RawAxiom
annotationIRIAssertionAxiom =
  rawAnnotated []
    (rawAnnotationAssertion
      labelAnnotationIri
      (rawAnnotationSubjectIRI annotationSubjectIri)
      (rawAnnotationValueIRI annotationValueIri))

annotationBlankAssertionAxiom : RawAnnotated RawAxiom
annotationBlankAssertionAxiom =
  rawAnnotated []
    (rawAnnotationAssertion
      labelAnnotationIri
      (rawAnnotationSubjectAnonymous "annotation-subject")
      (rawAnnotationValueAnonymous "annotation-value"))

annotationLiteralAssertionAxiom : RawAnnotated RawAxiom
annotationLiteralAssertionAxiom =
  rawAnnotated []
    (rawAnnotationAssertion
      labelAnnotationIri
      (rawAnnotationSubjectIRI annotationSubjectIri)
      (rawAnnotationValueLiteral
        (rawLiteral "visible label" (present stringDatatypeIri) absent)))

subAnnotationPropertyAxiom : RawAnnotated RawAxiom
subAnnotationPropertyAxiom =
  rawAnnotated []
    (rawSubAnnotationPropertyOf labelAnnotationIri commentAnnotationIri)

annotationPropertyDomainAxiom : RawAnnotated RawAxiom
annotationPropertyDomainAxiom =
  rawAnnotated []
    (rawAnnotationPropertyDomain labelAnnotationIri annotationSubjectIri)

annotationPropertyRangeAxiom : RawAnnotated RawAxiom
annotationPropertyRangeAxiom =
  rawAnnotated []
    (rawAnnotationPropertyRange labelAnnotationIri annotationValueIri)

annotationAxiomsDocument : RawOntology
annotationAxiomsDocument =
  rawOntology
    anonymousSource
    absent
    absent
    []
    (ontologyAnnotation ∷ [])
    (labelAnnotationAxiom ∷
     commentAnnotationAxiom ∷
     stringDatatypeAxiom ∷
     annotationSubjectClassAxiom ∷
     annotationIRIAssertionAxiom ∷
     annotationBlankAssertionAxiom ∷
     annotationLiteralAssertionAxiom ∷
     subAnnotationPropertyAxiom ∷
     annotationPropertyDomainAxiom ∷
     annotationPropertyRangeAxiom ∷ [])

annotationAxiomsResult : ElaborationResult
annotationAxiomsResult =
  elaborateStructuralKernelStrict annotationAxiomsDocument

annotationAxiomsClean : Clean annotationAxiomsResult
annotationAxiomsClean =
  tt

annotationAxiomsEvidence : EvidenceAvailable annotationAxiomsResult
annotationAxiomsEvidence =
  cleanEvidence annotationAxiomsResult annotationAxiomsClean

annotationAxiomsChecked : CheckedImport
annotationAxiomsChecked =
  elaborationSucceeded annotationAxiomsResult annotationAxiomsEvidence

firstCheckedAnnotationCount :
  {Sig : K.Signature} →
  List (K.Annotated Sig (K.Axiom Sig)) →
  ℕ
firstCheckedAnnotationCount [] =
  0
firstCheckedAnnotationCount (axiom ∷ axioms) =
  listCount (K.itemAnnotations axiom)

annotationAxiomsAnnotationPropertyCount :
  K.annotationPropertyCount (signature annotationAxiomsChecked) ≡ 2
annotationAxiomsAnnotationPropertyCount =
  refl

annotationAxiomsClassCount :
  K.classCount (signature annotationAxiomsChecked) ≡ 1
annotationAxiomsClassCount =
  refl

annotationAxiomsDatatypeCount :
  K.datatypeCount (signature annotationAxiomsChecked) ≡ 1
annotationAxiomsDatatypeCount =
  refl

annotationAxiomsIRICount :
  K.iriCount (signature annotationAxiomsChecked) ≡ 5
annotationAxiomsIRICount =
  refl

annotationAxiomsBlankNodeCount :
  K.blankNodeCount (signature annotationAxiomsChecked) ≡ 2
annotationAxiomsBlankNodeCount =
  refl

annotationAxiomsOntologyAnnotationCount :
  listCount (K.ontologyAnnotations (ontology annotationAxiomsChecked)) ≡ 1
annotationAxiomsOntologyAnnotationCount =
  refl

annotationAxiomsAnnotatedAxiomCount :
  listCount (K.annotatedAxioms (ontology annotationAxiomsChecked)) ≡ 10
annotationAxiomsAnnotatedAxiomCount =
  refl

annotationAxiomsFirstAxiomAnnotationCount :
  firstCheckedAnnotationCount
    (K.annotatedAxioms (ontology annotationAxiomsChecked)) ≡ 1
annotationAxiomsFirstAxiomAnnotationCount =
  refl

annotationAxiomsAnnotationErasure :
  K.annotatedBodies (K.annotatedAxioms (ontology annotationAxiomsChecked)) ≡
  K.axioms (ontology annotationAxiomsChecked)
annotationAxiomsAnnotationErasure =
  K.annotationErasure (ontology annotationAxiomsChecked)

annotationAxiomsAxiomCount :
  listCount (K.axioms (ontology annotationAxiomsChecked)) ≡ 10
annotationAxiomsAxiomCount =
  refl