XML Schema Documentation for Mizar

Printer-friendly Version
XML Instance Representation:
[ Expand All | Collapse All ]

Schema Component Representation:
[ Expand All | Collapse All ]

Table of Contents

top

Schema Document Properties

Target Namespace None
Element and Attribute Namespaces
  • Global element and attribute declarations belong to this schema's target namespace.
  • By default, local element declarations belong to this schema's target namespace.
  • By default, local attribute declarations have no namespace.

Declared Namespaces

Prefix Namespace
xml http://www.w3.org/XML/1998/namespace
xs http://www.w3.org/2001/XMLSchema
Schema Component Representation
top

Global Declarations

Element: Abstractness

  • This element can be used wherever the following element is referenced:
Name Abstractness
Type anyType
Nillable no
Abstract no
XML Instance Representation
<Abstractness> ... </Abstractness>
Schema Component Representation
top

Element: Adjective

Name Adjective
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Adjective
nr="xs:integer [1]"
value="xs:boolean [0..1]"
absnr="xs:integer [0..1]"
aid="xs:string [0..1]"
kind="xs:token (value comes from list: {'V'}) [0..1]"
pid="xs:integer [0..1]">
<Term> ... </Term> [0..*]
</Adjective>
Schema Component Representation
top

Element: And

  • This element can be used wherever the following element is referenced:
Name And
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<And
pid="xs:integer [0..1]">
<Formula> ... </Formula> [0..*]
</And>
Schema Component Representation
top

Element: Antisymmetry

  • This element can be used wherever the following element is referenced:
Name Antisymmetry
Type anyType
Nillable no
Abstract no
XML Instance Representation
<Antisymmetry> ... </Antisymmetry>
Schema Component Representation
top

Element: ArgTypes

Name ArgTypes
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<ArgTypes>
<Typ> ... </Typ> [0..*]
</ArgTypes>
Schema Component Representation
top

Element: Article

Name Article
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Article
aid="xs:string [1]">
Start Choice [0..*]
<DefinitionBlock> ... </DefinitionBlock> [1]
<RegistrationBlock> ... </RegistrationBlock> [1]
<NotationBlock> ... </NotationBlock> [1]
<Reservation> ... </Reservation> [1]
<SchemeBlock> ... </SchemeBlock> [1]
<JustifiedTheorem> ... </JustifiedTheorem> [1]
<DefTheorem> ... </DefTheorem> [1]
<Definiens> ... </Definiens> [1]
<Canceled> ... </Canceled> [1]
Start Choice [1]
Start Choice [1]
<Now> ... </Now> [1]
<IterEquality> ... </IterEquality> [1]
<Proposition> ... </Proposition> [1]
<Justification> ... </Justification> [1]
End Choice
<Consider> ... </Consider> [1]
<Set> ... </Set> [1]
<Reconsider> ... </Reconsider> [1]
<DefFunc> ... </DefFunc> [1]
<DefPred> ... </DefPred> [1]
End Choice
End Choice
</Article>
Schema Component Representation
top

Element: ArticleID

Name ArticleID
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<ArticleID
name="xs:string [1]"/>
Schema Component Representation
top

Element: Associativity

  • This element can be used wherever the following element is referenced:
Name Associativity
Type anyType
Nillable no
Abstract no
XML Instance Representation
<Associativity> ... </Associativity>
Schema Component Representation
top

Element: Assume

Name Assume
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Assume>
<Proposition> ... </Proposition> [1..*]
</Assume>
Schema Component Representation
top

Element: BlockThesis

Name BlockThesis
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<BlockThesis>
<Formula> ... </Formula> [1]
</BlockThesis>
Schema Component Representation
top

Element: By

  • This element can be used wherever the following element is referenced:
Name By
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<By
line="xs:integer [1]"
col="xs:integer [1]"
linked="xs:boolean [0..1]">
<Ref> ... </Ref> [0..*]
</By>
Schema Component Representation
top

Element: ByExplanations

Name ByExplanations
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<ByExplanations
aid="xs:string [1]">
<PolyEval> ... </PolyEval> [0..*]
</ByExplanations>
Schema Component Representation
top

Element: CCluster

Name CCluster
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<CCluster
nr="xs:integer [0..1]"
aid="xs:string [0..1]">
Start Choice [1]
<ErrorCluster> ... </ErrorCluster> [1]
<ArgTypes> ... </ArgTypes> [1]
<Cluster> ... </Cluster> [1]
<Typ> ... </Typ> [1]
<Cluster> ... </Cluster> [1]
End Choice
</CCluster>
Schema Component Representation
top

Element: Canceled

Name Canceled
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Canceled/>
Schema Component Representation
top

Element: Case

Name Case
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Case>
<Proposition> ... </Proposition> [1..*]
</Case>
Schema Component Representation
top

Element: CaseBlock

Name CaseBlock
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<CaseBlock
line="xs:integer [1]"
col="xs:integer [1]">
Start Choice [1]
<BlockThesis> ... </BlockThesis> [1]
<Case> ... </Case> [1]
<Thesis> ... </Thesis> [1]
Start Choice [0..*]
Start Choice [1]
<Let> ... </Let> [1]
<Conclusion> ... </Conclusion> [1]
<Assume> ... </Assume> [1]
<Given> ... </Given> [1]
<Take> ... </Take> [1]
<TakeAsVar> ... </TakeAsVar> [1]
End Choice
<Thesis> ... </Thesis> [0..1]
Start Choice [1]
Start Choice [1]
<Now> ... </Now> [1]
<IterEquality> ... </IterEquality> [1]
<Proposition> ... </Proposition> [1]
<Justification> ... </Justification> [1]
End Choice
<Consider> ... </Consider> [1]
<Set> ... </Set> [1]
<Reconsider> ... </Reconsider> [1]
<DefFunc> ... </DefFunc> [1]
<DefPred> ... </DefPred> [1]
End Choice
End Choice
<PerCasesReasoning> ... </PerCasesReasoning> [0..1]
<EndPosition> ... </EndPosition> [1]
<Case> ... </Case> [1]
Start Choice [0..*]
Start Choice [1]
<Let> ... </Let> [1]
<Conclusion> ... </Conclusion> [1]
<Assume> ... </Assume> [1]
<Given> ... </Given> [1]
<Take> ... </Take> [1]
<TakeAsVar> ... </TakeAsVar> [1]
End Choice
<Thesis> ... </Thesis> [0..1]
Start Choice [1]
Start Choice [1]
<Now> ... </Now> [1]
<IterEquality> ... </IterEquality> [1]
<Proposition> ... </Proposition> [1]
<Justification> ... </Justification> [1]
End Choice
<Consider> ... </Consider> [1]
<Set> ... </Set> [1]
<Reconsider> ... </Reconsider> [1]
<DefFunc> ... </DefFunc> [1]
<DefPred> ... </DefPred> [1]
End Choice
End Choice
<PerCasesReasoning> ... </PerCasesReasoning> [0..1]
<EndPosition> ... </EndPosition> [1]
<BlockThesis> ... </BlockThesis> [1]
End Choice
</CaseBlock>
Schema Component Representation
top

Element: Cluster

Name Cluster
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Cluster>
<Adjective> ... </Adjective> [0..*]
</Cluster>
Schema Component Representation
top

Element: Coherence

Name Coherence
Type anyType
Nillable no
Abstract no
XML Instance Representation
<Coherence> ... </Coherence>
Schema Component Representation
top

Element: Commutativity

  • This element can be used wherever the following element is referenced:
Name Commutativity
Type anyType
Nillable no
Abstract no
XML Instance Representation
<Commutativity> ... </Commutativity>
Schema Component Representation
top

Element: Compatibility

Name Compatibility
Type anyType
Nillable no
Abstract no
XML Instance Representation
<Compatibility> ... </Compatibility>
Schema Component Representation
top

Element: ComplexNr

  • This element can be used wherever the following element is referenced:
Name ComplexNr
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<ComplexNr>
<RationalNr> ... </RationalNr> [1]
<RationalNr> ... </RationalNr> [1]
</ComplexNr>
Schema Component Representation
top

Element: Conclusion

Name Conclusion
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Conclusion>
Start Choice [1]
<Now> ... </Now> [1]
<IterEquality> ... </IterEquality> [1]
<Proposition> ... </Proposition> [1]
<Justification> ... </Justification> [1]
End Choice
</Conclusion>
Schema Component Representation
top

Element: Connectedness

  • This element can be used wherever the following element is referenced:
Name Connectedness
Type anyType
Nillable no
Abstract no
XML Instance Representation
<Connectedness> ... </Connectedness>
Schema Component Representation
top

Element: Consider

Name Consider
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Consider
nr="xs:integer [0..1]">
<Proposition> ... </Proposition> [1]
<Justification> ... </Justification> [1]
<Typ> ... </Typ> [1..*]
<Proposition> ... </Proposition> [0..*]
</Consider>
Schema Component Representation
top

Element: Consistency

Name Consistency
Type anyType
Nillable no
Abstract no
XML Instance Representation
<Consistency> ... </Consistency>
Schema Component Representation
top

Element: Const

  • This element can be used wherever the following element is referenced:
Name Const
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Const
nr="xs:integer [1]"/>
Schema Component Representation
top

Element: ConstrCount

Name ConstrCount
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<ConstrCount
kind="xs:token (value comes from list: {'M'|'L'|'V'|'R'|'K'|'U'|'G'}) [1]"
nr="xs:integer [1]"/>
Schema Component Representation
top

Element: ConstrCounts

Name ConstrCounts
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<ConstrCounts
name="xs:string [0..1]">
<ConstrCount> ... </ConstrCount> [0..*]
</ConstrCounts>
Schema Component Representation
top

Element: ConstrDef

Name ConstrDef
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<ConstrDef
constrkind="xs:token (value comes from list: {'K'|'U'|'G'}) [1]"
constrnr="xs:integer [1]">
<Typ> ... </Typ> [0..*]
<Term> ... </Term> [0..1]
</ConstrDef>
Schema Component Representation
top

Element: Constructor

Name Constructor
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Constructor
kind="xs:token (value comes from list: {'M'|'L'|'V'|'R'|'K'|'U'|'G'}) [1]"
nr="xs:integer [1]"
aid="xs:string [1]"
relnr="xs:integer [0..1]"
redefnr="xs:integer [0..1]"
superfluous="xs:integer [0..1]"
absredefnr="xs:integer [0..1]"
redefaid="xs:string [0..1]"
structmodeaggrnr="xs:integer [0..1]"
aggregbase="xs:integer [0..1]">
<Properties> ... </Properties> [0..1]
<ArgTypes> ... </ArgTypes> [1]
<StructLoci> ... </StructLoci> [0..1]
<Typ> ... </Typ> [0..*]
<Fields> ... </Fields> [0..1]
</Constructor>
Schema Component Representation
top

Element: Constructors

Name Constructors
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Constructors
aid="xs:string [0..1]">
Start Choice [0..1]
<SignatureWithCounts> ... </SignatureWithCounts> [1]
<Signature> ... </Signature> [1]
<ConstrCounts> ... </ConstrCounts> [1]
End Choice
<Constructor> ... </Constructor> [0..*]
</Constructors>
Schema Component Representation
top

Element: Correctness

Name Correctness
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Correctness>
<CorrectnessCondition> ... </CorrectnessCondition> [0..*]
<Proposition> ... </Proposition> [1]
<Justification> ... </Justification> [1]
</Correctness>
Schema Component Representation
top

Element: CorrectnessCondition

Name CorrectnessCondition
Type Locally-defined complex type
Nillable no
Abstract yes
XML Instance Representation
<CorrectnessCondition>
Start Choice [1]
<Formula> ... </Formula> [1]
<Proposition> ... </Proposition> [1]
<Justification> ... </Justification> [1]
End Choice
</CorrectnessCondition>
Schema Component Representation
top

Element: DefFunc

Name DefFunc
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<DefFunc
nr="xs:integer [0..1]">
<ArgTypes> ... </ArgTypes> [1]
<Term> ... </Term> [1]
<Typ> ... </Typ> [1]
</DefFunc>
Schema Component Representation
top

Element: DefMeaning

Name DefMeaning
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<DefMeaning
kind="xs:token (value comes from list: {'e'|'m'}) [1]">
<PartialDef> ... </PartialDef> [0..*]
Start Choice [0..1]
<Formula> ... </Formula> [1]
<Term> ... </Term> [1]
End Choice
</DefMeaning>
Schema Component Representation
top

Element: DefPred

Name DefPred
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<DefPred
nr="xs:integer [0..1]">
<ArgTypes> ... </ArgTypes> [1]
<Formula> ... </Formula> [1]
</DefPred>
Schema Component Representation
top

Element: DefTheorem

Name DefTheorem
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<DefTheorem
constrkind="xs:token (value comes from list: {'M'|'V'|'R'|'K'}) [0..1]"
constrnr="xs:integer [0..1]">
<Proposition> ... </Proposition> [1]
</DefTheorem>
Schema Component Representation
top

Element: Definiens

Name Definiens
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Definiens
constrkind="xs:token (value comes from list: {'M'|'L'|'V'|'R'|'K'|'U'|'G'}) [1]"
constrnr="xs:integer [1]"
defnr="xs:integer [1]"
aid="xs:string [1]"
nr="xs:integer [0..1]"
relnr="xs:integer [0..1]">
<Typ> ... </Typ> [0..*]
<Essentials> ... </Essentials> [1]
<Formula> ... </Formula> [0..1]
<DefMeaning> ... </DefMeaning> [1]
</Definiens>
Schema Component Representation
top

Element: Definientia

Name Definientia
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Definientia
aid="xs:string [0..1]">
<Signature> ... </Signature> [0..1]
<Definiens> ... </Definiens> [0..*]
</Definientia>
Schema Component Representation
top

Element: Definition

Name Definition
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Definition
kind="xs:token (value comes from list: {'M'|'V'|'R'|'K'|'G'}) [1]"
redefinition="xs:boolean [0..1]"
expandable="xs:boolean [0..1]"
nr="xs:integer [0..1]"
line="xs:integer [0..1]"
col="xs:integer [0..1]">
Start Choice [1]
<CorrectnessCondition> ... </CorrectnessCondition> [0..*]
<Correctness> ... </Correctness> [0..1]
<JustifiedProperty> ... </JustifiedProperty> [0..*]
<Constructor> ... </Constructor> [0..1]
<Pattern> ... </Pattern> [0..1]
<Constructor> ... </Constructor> [1]
<Constructor> ... </Constructor> [1]
<Constructor> ... </Constructor> [1..*]
<Registration> ... </Registration> [1]
<CorrectnessCondition> ... </CorrectnessCondition> [0..*]
<Correctness> ... </Correctness> [0..1]
<Pattern> ... </Pattern> [1..*]
End Choice
</Definition>
Schema Component Representation
top

Element: DefinitionBlock

Name DefinitionBlock
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<DefinitionBlock
line="xs:integer [1]"
col="xs:integer [1]">
Start Choice [0..*]
<Let> ... </Let> [1]
<Assume> ... </Assume> [1]
<Given> ... </Given> [1]
Start Choice [1]
Start Choice [1]
<Now> ... </Now> [1]
<IterEquality> ... </IterEquality> [1]
<Proposition> ... </Proposition> [1]
<Justification> ... </Justification> [1]
End Choice
<Consider> ... </Consider> [1]
<Set> ... </Set> [1]
<Reconsider> ... </Reconsider> [1]
<DefFunc> ... </DefFunc> [1]
<DefPred> ... </DefPred> [1]
End Choice
<Canceled> ... </Canceled> [1]
<Definition> ... </Definition> [1]
End Choice
<EndPosition> ... </EndPosition> [1]
</DefinitionBlock>
Schema Component Representation
top

Element: EndPosition

Name EndPosition
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<EndPosition
line="xs:integer [1]"
col="xs:integer [1]"/>
Schema Component Representation
top

Element: EqArgs

Name EqArgs
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<EqArgs>
<Pair> ... </Pair> [0..*]
</EqArgs>
Schema Component Representation
top

Element: ErrorCluster

Name ErrorCluster
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<ErrorCluster/>
Schema Component Representation
top

Element: ErrorFrm

  • This element can be used wherever the following element is referenced:
Name ErrorFrm
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<ErrorFrm/>
Schema Component Representation
top

Element: ErrorIdentify

Name ErrorIdentify
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<ErrorIdentify/>
Schema Component Representation
top

Element: ErrorInf

  • This element can be used wherever the following element is referenced:
Name ErrorInf
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<ErrorInf/>
Schema Component Representation
top

Element: ErrorTrm

  • This element can be used wherever the following element is referenced:
Name ErrorTrm
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<ErrorTrm/>
Schema Component Representation
top

Element: Essentials

Name Essentials
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Essentials>
<Int> ... </Int> [0..*]
</Essentials>
Schema Component Representation
top

Element: Existence

Name Existence
Type anyType
Nillable no
Abstract no
XML Instance Representation
<Existence> ... </Existence>
Schema Component Representation
top

Element: Expansion

Name Expansion
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Expansion>
<Typ> ... </Typ> [1]
</Expansion>
Schema Component Representation
top

Element: FCluster

Name FCluster
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<FCluster
nr="xs:integer [0..1]"
aid="xs:string [0..1]">
Start Choice [1]
<ErrorCluster> ... </ErrorCluster> [1]
<ArgTypes> ... </ArgTypes> [1]
<Term> ... </Term> [1]
<Cluster> ... </Cluster> [1]
<Typ> ... </Typ> [0..1]
End Choice
</FCluster>
Schema Component Representation
top

Element: Field

Name Field
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Field
nr="xs:integer [1]"
kind="xs:token (value comes from list: {'U'}) [0..1]"
aid="xs:string [0..1]"
absnr="xs:integer [0..1]"/>
Schema Component Representation
top

Element: Fields

Name Fields
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Fields>
<Field> ... </Field> [0..*]
</Fields>
Schema Component Representation
top

Element: For

  • This element can be used wherever the following element is referenced:
Name For
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<For
pid="xs:integer [0..1]">
<Typ> ... </Typ> [1]
<Formula> ... </Formula> [1]
</For>
Schema Component Representation
top

Element: Format

Name Format
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Format
kind="xs:token (value comes from list: {'G'|'K'|'J'|'L'|'M'|'O'|'R'|'U'|'V'}) [1]"
nr="xs:integer [0..1]"
symbolnr="xs:integer [1]"
argnr="xs:integer [1]"
leftargnr="xs:integer [0..1]"
rightsymbolnr="xs:integer [0..1]"/>
Schema Component Representation
top

Element: Formats

Name Formats
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Formats>
<Format> ... </Format> [0..*]
<Priority> ... </Priority> [0..*]
</Formats>
Schema Component Representation
top

Element: Formula

Name Formula
Type anyType
Nillable no
Abstract yes
XML Instance Representation
<Formula> ... </Formula>
Schema Component Representation
top

Element: Fraenkel

  • This element can be used wherever the following element is referenced:
Name Fraenkel
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Fraenkel>
<Typ> ... </Typ> [0..*]
<Term> ... </Term> [1]
<Formula> ... </Formula> [1]
</Fraenkel>
Schema Component Representation
top

Element: FreeVar

  • This element can be used wherever the following element is referenced:
Name FreeVar
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<FreeVar
nr="xs:integer [1]"/>
Schema Component Representation
top

Element: From

  • This element can be used wherever the following element is referenced:
Name From
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<From
line="xs:integer [1]"
col="xs:integer [1]"
articlenr="xs:integer [1]"
nr="xs:integer [1]">
<Ref> ... </Ref> [0..*]
</From>
Schema Component Representation
top

Element: FromExplanations

Name FromExplanations
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<FromExplanations
aid="xs:string [1]">
<SchemeInstantiation> ... </SchemeInstantiation> [0..*]
</FromExplanations>
Schema Component Representation
top

Element: Func

  • This element can be used wherever the following element is referenced:
Name Func
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Func
kind="xs:token (value comes from list: {'F'|'G'|'K'|'U'}) [1]"
nr="xs:integer [1]"
absnr="xs:integer [0..1]"
aid="xs:string [0..1]"
pid="xs:integer [0..1]">
<Term> ... </Term> [0..*]
</Func>
Schema Component Representation
top

Element: FuncInstance

Name FuncInstance
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<FuncInstance
instnr="xs:integer [1]"
kind="xs:token (value comes from list: {'F'|'H'|'G'|'K'|'U'}) [0..1]"
nr="xs:integer [0..1]"
absnr="xs:integer [0..1]"
aid="xs:string [0..1]">
<Term> ... </Term> [0..1]
</FuncInstance>
Schema Component Representation
top

Element: GeneralPolynomial

Name GeneralPolynomial
Type anyType
Nillable no
Abstract yes
XML Instance Representation
<GeneralPolynomial> ... </GeneralPolynomial>
Schema Component Representation
top

Element: Given

Name Given
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Given
nr="xs:integer [0..1]">
<Typ> ... </Typ> [1..*]
<Proposition> ... </Proposition> [1..*]
</Given>
Schema Component Representation
top

Element: Idempotence

  • This element can be used wherever the following element is referenced:
Name Idempotence
Type anyType
Nillable no
Abstract no
XML Instance Representation
<Idempotence> ... </Idempotence>
Schema Component Representation
top

Element: Identify

Name Identify
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Identify
nr="xs:integer [0..1]"
aid="xs:string [0..1]">
Start Choice [1]
<ErrorIdentify> ... </ErrorIdentify> [1]
<ConstrDef> ... </ConstrDef> [1]
<ConstrDef> ... </ConstrDef> [1]
<EqArgs> ... </EqArgs> [1]
End Choice
</Identify>
Schema Component Representation
top

Element: IdentifyRegistration

Name IdentifyRegistration
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<IdentifyRegistration>
<Identify> ... </Identify> [1]
<CorrectnessCondition> ... </CorrectnessCondition> [0..*]
<Correctness> ... </Correctness> [0..1]
</IdentifyRegistration>
Schema Component Representation
top

Element: IdentifyRegistrations

Name IdentifyRegistrations
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<IdentifyRegistrations
aid="xs:string [0..1]">
<Signature> ... </Signature> [0..1]
<Identify> ... </Identify> [0..*]
</IdentifyRegistrations>
Schema Component Representation
top

Element: InfConst

  • This element can be used wherever the following element is referenced:
Name InfConst
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<InfConst
nr="xs:integer [1]"/>
Schema Component Representation
top

Element: Inference

  • This element can be used wherever the following element is referenced:
  • The following elements can be used wherever this element is referenced:
Name Inference
Type anyType
Nillable no
Abstract yes
XML Instance Representation
<Inference> ... </Inference>
Schema Component Representation
top

Element: Int

Name Int
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Int
x="xs:integer [1]"/>
Schema Component Representation
top

Element: Involutiveness

  • This element can be used wherever the following element is referenced:
Name Involutiveness
Type anyType
Nillable no
Abstract no
XML Instance Representation
<Involutiveness> ... </Involutiveness>
Schema Component Representation
top

Element: Irreflexivity

  • This element can be used wherever the following element is referenced:
Name Irreflexivity
Type anyType
Nillable no
Abstract no
XML Instance Representation
<Irreflexivity> ... </Irreflexivity>
Schema Component Representation
top

Element: Is

  • This element can be used wherever the following element is referenced:
Name Is
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Is>
<Term> ... </Term> [1]
<Typ> ... </Typ> [1]
</Is>
Schema Component Representation
top

Element: It

  • This element can be used wherever the following element is referenced:
Name It
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<It/>
Schema Component Representation
top

Element: IterEquality

Name IterEquality
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<IterEquality
nr="xs:integer [0..1]"
line="xs:integer [1]"
col="xs:integer [1]">
<Term> ... </Term> [1]
<IterStep> ... </IterStep> [1..*]
</IterEquality>
Schema Component Representation
top

Element: IterStep

Name IterStep
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<IterStep>
<Term> ... </Term> [1]
<Inference> ... </Inference> [1]
</IterStep>
Schema Component Representation
top

Element: Justification

Name Justification
Type anyType
Nillable no
Abstract yes
Documentation Direct justification.
XML Instance Representation
<Justification> ... </Justification>
Schema Component Representation
top

Element: JustifiedProperty

Name JustifiedProperty
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<JustifiedProperty>
<Property> ... </Property> [1]
<Proposition> ... </Proposition> [1]
<Justification> ... </Justification> [1]
</JustifiedProperty>
Schema Component Representation
top

Element: JustifiedTheorem

Name JustifiedTheorem
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<JustifiedTheorem>
<Proposition> ... </Proposition> [1]
<Justification> ... </Justification> [1]
</JustifiedTheorem>
Schema Component Representation
top

Element: LambdaVar

  • This element can be used wherever the following element is referenced:
Name LambdaVar
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<LambdaVar
nr="xs:integer [1]"/>
Schema Component Representation
top

Element: Let

Name Let
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Let
nr="xs:integer [0..1]">
<Typ> ... </Typ> [1..*]
</Let>
Schema Component Representation
top

Element: LocusVar

  • This element can be used wherever the following element is referenced:
Name LocusVar
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<LocusVar
nr="xs:integer [1]"/>
Schema Component Representation
top

Element: Monomial

Name Monomial
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Monomial>
<Number> ... </Number> [1]
<PoweredVar> ... </PoweredVar> [0..*]
</Monomial>
Schema Component Representation
top

Element: Not

  • This element can be used wherever the following element is referenced:
Name Not
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Not
pid="xs:integer [0..1]">
<Formula> ... </Formula> [1]
</Not>
Schema Component Representation
top

Element: NotationBlock

Name NotationBlock
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<NotationBlock
line="xs:integer [1]"
col="xs:integer [1]">
Start Choice [0..*]
<Let> ... </Let> [1]
Start Choice [1]
Start Choice [1]
<Now> ... </Now> [1]
<IterEquality> ... </IterEquality> [1]
<Proposition> ... </Proposition> [1]
<Justification> ... </Justification> [1]
End Choice
<Consider> ... </Consider> [1]
<Set> ... </Set> [1]
<Reconsider> ... </Reconsider> [1]
<DefFunc> ... </DefFunc> [1]
<DefPred> ... </DefPred> [1]
End Choice
<Pattern> ... </Pattern> [1]
End Choice
<EndPosition> ... </EndPosition> [1]
</NotationBlock>
Schema Component Representation
top

Element: Notations

Name Notations
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Notations
aid="xs:string [0..1]">
Start Sequence [0..1]
<Signature> ... </Signature> [1]
<Vocabularies> ... </Vocabularies> [1]
End Sequence
<Pattern> ... </Pattern> [0..*]
</Notations>
Schema Component Representation
top

Element: Now

Name Now
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Now
nr="xs:integer [0..1]"
line="xs:integer [1]"
col="xs:integer [1]">
Start Choice [0..*]
Start Choice [1]
<Let> ... </Let> [1]
<Conclusion> ... </Conclusion> [1]
<Assume> ... </Assume> [1]
<Given> ... </Given> [1]
<Take> ... </Take> [1]
<TakeAsVar> ... </TakeAsVar> [1]
End Choice
<Thesis> ... </Thesis> [0..1]
Start Choice [1]
Start Choice [1]
<Now> ... </Now> [1]
<IterEquality> ... </IterEquality> [1]
<Proposition> ... </Proposition> [1]
<Justification> ... </Justification> [1]
End Choice
<Consider> ... </Consider> [1]
<Set> ... </Set> [1]
<Reconsider> ... </Reconsider> [1]
<DefFunc> ... </DefFunc> [1]
<DefPred> ... </DefPred> [1]
End Choice
End Choice
<PerCasesReasoning> ... </PerCasesReasoning> [0..1]
<EndPosition> ... </EndPosition> [1]
<BlockThesis> ... </BlockThesis> [1]
</Now>
Schema Component Representation
top

Element: Num

  • This element can be used wherever the following element is referenced:
Name Num
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Num
nr="xs:integer [1]"/>
Schema Component Representation
top

Element: Number

  • This element can be used wherever the following element is referenced:
  • The following elements can be used wherever this element is referenced:
Name Number
Type anyType
Nillable no
Abstract yes
XML Instance Representation
<Number> ... </Number>
Schema Component Representation
top

Element: Pair

Name Pair
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Pair
x="xs:integer [1]"
y="xs:integer [1]"/>
Schema Component Representation
top

Element: PartialDef

Name PartialDef
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<PartialDef>
Start Choice [1]
<Formula> ... </Formula> [1]
<Term> ... </Term> [1]
End Choice
<Formula> ... </Formula> [1]
</PartialDef>
Schema Component Representation
top

Element: Pattern

Name Pattern
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Pattern
kind="xs:token (value comes from list: {'M'|'L'|'V'|'R'|'K'|'U'|'G'|'J'}) [1]"
nr="xs:integer [0..1]"
aid="xs:string [0..1]"
formatnr="xs:integer [0..1]"
constrkind="xs:token (value comes from list: {'M'|'L'|'V'|'R'|'K'|'U'|'G'|'J'}) [1]"
constrnr="xs:integer [1]"
antonymic="xs:boolean [0..1]"
relnr="xs:integer [0..1]"
redefnr="xs:integer [0..1]">
<Format> ... </Format> [0..1]
<ArgTypes> ... </ArgTypes> [1]
<Visible> ... </Visible> [1]
<Expansion> ... </Expansion> [0..1]
</Pattern>
Schema Component Representation
top

Element: PerCases

Name PerCases
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<PerCases>
<Proposition> ... </Proposition> [1]
<Inference> ... </Inference> [1]
</PerCases>
Schema Component Representation
top

Element: PerCasesReasoning

Name PerCasesReasoning
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<PerCasesReasoning
line="xs:integer [1]"
col="xs:integer [1]">
Start Choice [1]
<BlockThesis> ... </BlockThesis> [1]
Start Choice [1]
<CaseBlock> ... </CaseBlock> [1..*]
<SupposeBlock> ... </SupposeBlock> [1..*]
End Choice
<PerCases> ... </PerCases> [1]
<Thesis> ... </Thesis> [1]
<EndPosition> ... </EndPosition> [1]
Start Choice [1]
<CaseBlock> ... </CaseBlock> [1..*]
<SupposeBlock> ... </SupposeBlock> [1..*]
End Choice
<PerCases> ... </PerCases> [1]
<EndPosition> ... </EndPosition> [1]
<BlockThesis> ... </BlockThesis> [1]
End Choice
</PerCasesReasoning>
Schema Component Representation
top

Element: PolyEval

Name PolyEval
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<PolyEval
line="xs:integer [1]"
col="xs:integer [1]"
value="xs:boolean [0..1]">
<Requirement> ... </Requirement> [1]
<GeneralPolynomial> ... </GeneralPolynomial> [1..*]
</PolyEval>
Schema Component Representation
top

Element: Polynomial

  • This element can be used wherever the following element is referenced:
Name Polynomial
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Polynomial>
<Monomial> ... </Monomial> [1..*]
</Polynomial>
Schema Component Representation
top

Element: PoweredVar

Name PoweredVar
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<PoweredVar
nr="xs:integer [1]"
exponent="xs:integer [1]"/>
Schema Component Representation
top

Element: Pred

  • This element can be used wherever the following element is referenced:
Name Pred
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Pred
kind="xs:token (value comes from list: {'P'|'V'|'R'}) [1]"
nr="xs:integer [1]"
absnr="xs:integer [0..1]"
aid="xs:string [0..1]"
pid="xs:integer [0..1]">
<Term> ... </Term> [0..*]
</Pred>
Schema Component Representation
top

Element: PredInstance

Name PredInstance
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<PredInstance
instnr="xs:integer [1]"
kind="xs:token (value comes from list: {'P'|'S'|'V'|'R'}) [1]"
nr="xs:integer [1]"
absnr="xs:integer [0..1]"
aid="xs:string [0..1]"/>
Schema Component Representation
top

Element: Priority

Name Priority
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Priority
kind="xs:token (value comes from list: {'O'|'K'|'L'}) [1]"
symbolnr="xs:integer [1]"
value="xs:integer [1]"/>
Schema Component Representation
top

Element: PrivFunc

  • This element can be used wherever the following element is referenced:
Name PrivFunc
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<PrivFunc
nr="xs:integer [1]">
<Term> ... </Term> [1..*]
</PrivFunc>
Schema Component Representation
top

Element: PrivPred

  • This element can be used wherever the following element is referenced:
Name PrivPred
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<PrivPred
nr="xs:integer [1]">
<Term> ... </Term> [0..*]
<Formula> ... </Formula> [1]
</PrivPred>
Schema Component Representation
top

Element: Projectivity

  • This element can be used wherever the following element is referenced:
Name Projectivity
Type anyType
Nillable no
Abstract no
XML Instance Representation
<Projectivity> ... </Projectivity>
Schema Component Representation
top

Element: Proof

  • This element can be used wherever the following element is referenced:
Name Proof
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Proof
nr="xs:integer [0..1]"
line="xs:integer [1]"
col="xs:integer [1]">
<BlockThesis> ... </BlockThesis> [1]
Start Choice [0..*]
Start Choice [1]
<Let> ... </Let> [1]
<Conclusion> ... </Conclusion> [1]
<Assume> ... </Assume> [1]
<Given> ... </Given> [1]
<Take> ... </Take> [1]
<TakeAsVar> ... </TakeAsVar> [1]
End Choice
<Thesis> ... </Thesis> [0..1]
Start Choice [1]
Start Choice [1]
<Now> ... </Now> [1]
<IterEquality> ... </IterEquality> [1]
<Proposition> ... </Proposition> [1]
<Justification> ... </Justification> [1]
End Choice
<Consider> ... </Consider> [1]
<Set> ... </Set> [1]
<Reconsider> ... </Reconsider> [1]
<DefFunc> ... </DefFunc> [1]
<DefPred> ... </DefPred> [1]
End Choice
End Choice
<PerCasesReasoning> ... </PerCasesReasoning> [0..1]
<EndPosition> ... </EndPosition> [1]
</Proof>
Schema Component Representation
top

Element: Properties

Name Properties
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Properties
propertyarg1="xs:integer [1]"
propertyarg2="xs:integer [1]">
<Property> ... </Property> [1..*]
</Properties>
Schema Component Representation
top

Element: Property

Name Property
Type Locally-defined complex type
Nillable no
Abstract yes
XML Instance Representation
<Property/>
Schema Component Representation
top

Element: Proposition

Name Proposition
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Proposition
line="xs:integer [1]"
col="xs:integer [1]"
nr="xs:integer [0..1]">
<Formula> ... </Formula> [1]
</Proposition>
Schema Component Representation
top

Element: QuaTrm

  • This element can be used wherever the following element is referenced:
Name QuaTrm
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<QuaTrm>
<Term> ... </Term> [1]
<Typ> ... </Typ> [1]
</QuaTrm>
Schema Component Representation
top

Element: RCluster

Name RCluster
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<RCluster
nr="xs:integer [0..1]"
aid="xs:string [0..1]">
Start Choice [1]
<ErrorCluster> ... </ErrorCluster> [1]
<ArgTypes> ... </ArgTypes> [1]
<Typ> ... </Typ> [1]
<Cluster> ... </Cluster> [1]
End Choice
</RCluster>
Schema Component Representation
top

Element: RationalNr

  • This element can be used wherever the following element is referenced:
Name RationalNr
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<RationalNr
numerator="xs:integer [1]"
denominator="xs:integer [1]"/>
Schema Component Representation
top

Element: Reconsider

Name Reconsider
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Reconsider
nr="xs:integer [0..1]">
<Typ> ... </Typ> [1]
<Term> ... </Term> [1..*]
<Proposition> ... </Proposition> [1]
<Justification> ... </Justification> [1]
</Reconsider>
Schema Component Representation
top

Element: Ref

Name Ref
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Ref
nr="xs:integer [1]"
articlenr="xs:integer [0..1]"
kind="xs:token (value comes from list: {'T'|'D'}) [0..1]"
line="xs:integer [1]"
col="xs:integer [1]"/>
Schema Component Representation
top

Element: Reflexivity

  • This element can be used wherever the following element is referenced:
Name Reflexivity
Type anyType
Nillable no
Abstract no
XML Instance Representation
<Reflexivity> ... </Reflexivity>
Schema Component Representation
top

Element: Registration

Name Registration
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Registration>
Start Choice [1]
<RCluster> ... </RCluster> [1]
<FCluster> ... </FCluster> [1]
<CCluster> ... </CCluster> [1]
End Choice
<CorrectnessCondition> ... </CorrectnessCondition> [0..*]
<Correctness> ... </Correctness> [0..1]
</Registration>
Schema Component Representation
top

Element: RegistrationBlock

Name RegistrationBlock
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<RegistrationBlock
line="xs:integer [1]"
col="xs:integer [1]">
Start Choice [1..*]
<Let> ... </Let> [1]
Start Choice [1]
Start Choice [1]
<Now> ... </Now> [1]
<IterEquality> ... </IterEquality> [1]
<Proposition> ... </Proposition> [1]
<Justification> ... </Justification> [1]
End Choice
<Consider> ... </Consider> [1]
<Set> ... </Set> [1]
<Reconsider> ... </Reconsider> [1]
<DefFunc> ... </DefFunc> [1]
<DefPred> ... </DefPred> [1]
End Choice
<Registration> ... </Registration> [1]
<IdentifyRegistration> ... </IdentifyRegistration> [1]
<Canceled> ... </Canceled> [1]
End Choice
<EndPosition> ... </EndPosition> [1]
</RegistrationBlock>
Schema Component Representation
top

Element: Registrations

Name Registrations
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Registrations
aid="xs:string [0..1]">
<Signature> ... </Signature> [0..1]
Start Choice [0..*]
<RCluster> ... </RCluster> [1]
<CCluster> ... </CCluster> [1]
<FCluster> ... </FCluster> [1]
End Choice
</Registrations>
Schema Component Representation
top

Element: Requirement

Name Requirement
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Requirement
constrkind="xs:token (value comes from list: {'M'|'L'|'V'|'R'|'K'|'U'|'G'}) [1]"
constrnr="xs:integer [1]"
nr="xs:integer [1]"
reqname="xs:string [0..1]"
absnr="xs:integer [0..1]"
aid="xs:string [0..1]"/>
Schema Component Representation
top

Element: Requirements

Name Requirements
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Requirements>
<Signature> ... </Signature> [1]
<Requirement> ... </Requirement> [0..*]
</Requirements>
Schema Component Representation
top

Element: Reservation

Name Reservation
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Reservation>
<Typ> ... </Typ> [1]
</Reservation>
Schema Component Representation
top

Element: Scheme

Name Scheme
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Scheme
articlenr="xs:integer [0..1]"
nr="xs:integer [0..1]"
aid="xs:string [0..1]">
<ArgTypes> ... </ArgTypes> [1]
<Formula> ... </Formula> [1]
<Formula> ... </Formula> [0..*]
</Scheme>
Schema Component Representation
top

Element: SchemeBlock

Name SchemeBlock
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<SchemeBlock
schemenr="xs:integer [1]"
line="xs:integer [1]"
col="xs:integer [1]">
Start Choice [0..*]
<SchemeFuncDecl> ... </SchemeFuncDecl> [1]
<SchemePredDecl> ... </SchemePredDecl> [1]
End Choice
<SchemePremises> ... </SchemePremises> [1]
<Proposition> ... </Proposition> [1]
<Justification> ... </Justification> [1]
<EndPosition> ... </EndPosition> [1]
</SchemeBlock>
Schema Component Representation
top

Element: SchemeFuncDecl

Name SchemeFuncDecl
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<SchemeFuncDecl
nr="xs:integer [1]">
<ArgTypes> ... </ArgTypes> [1]
<Typ> ... </Typ> [1]
</SchemeFuncDecl>
Schema Component Representation
top

Element: SchemeInstantiation

Name SchemeInstantiation
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<SchemeInstantiation
line="xs:integer [1]"
col="xs:integer [1]">
<FuncInstance> ... </FuncInstance> [0..*]
<PredInstance> ... </PredInstance> [0..*]
</SchemeInstantiation>
Schema Component Representation
top

Element: SchemePredDecl

Name SchemePredDecl
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<SchemePredDecl
nr="xs:integer [1]">
<ArgTypes> ... </ArgTypes> [1]
</SchemePredDecl>
Schema Component Representation
top

Element: SchemePremises

Name SchemePremises
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<SchemePremises>
<Proposition> ... </Proposition> [0..*]
</SchemePremises>
Schema Component Representation
top

Element: Schemes

Name Schemes
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Schemes
aid="xs:string [0..1]">
<Signature> ... </Signature> [0..1]
<Scheme> ... </Scheme> [0..*]
</Schemes>
Schema Component Representation
top

Element: Set

Name Set
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Set
nr="xs:integer [0..1]">
<Term> ... </Term> [1]
<Typ> ... </Typ> [1]
</Set>
Schema Component Representation
top

Element: Signature

Name Signature
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Signature>
<ArticleID> ... </ArticleID> [0..*]
</Signature>
Schema Component Representation
top

Element: SignatureWithCounts

Name SignatureWithCounts
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<SignatureWithCounts>
<ConstrCounts> ... </ConstrCounts> [0..*]
</SignatureWithCounts>
Schema Component Representation
top

Element: SkippedProof

  • This element can be used wherever the following element is referenced:
Name SkippedProof
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<SkippedProof/>
Schema Component Representation
top

Element: StructLoci

Name StructLoci
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<StructLoci>
<Pair> ... </Pair> [0..*]
</StructLoci>
Schema Component Representation
top

Element: Suppose

Name Suppose
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Suppose>
<Proposition> ... </Proposition> [1..*]
</Suppose>
Schema Component Representation
top

Element: SupposeBlock

Name SupposeBlock
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<SupposeBlock
line="xs:integer [1]"
col="xs:integer [1]">
Start Choice [1]
<BlockThesis> ... </BlockThesis> [1]
<Suppose> ... </Suppose> [1]
<Thesis> ... </Thesis> [1]
Start Choice [0..*]
Start Choice [1]
<Let> ... </Let> [1]
<Conclusion> ... </Conclusion> [1]
<Assume> ... </Assume> [1]
<Given> ... </Given> [1]
<Take> ... </Take> [1]
<TakeAsVar> ... </TakeAsVar> [1]
End Choice
<Thesis> ... </Thesis> [0..1]
Start Choice [1]
Start Choice [1]
<Now> ... </Now> [1]
<IterEquality> ... </IterEquality> [1]
<Proposition> ... </Proposition> [1]
<Justification> ... </Justification> [1]
End Choice
<Consider> ... </Consider> [1]
<Set> ... </Set> [1]
<Reconsider> ... </Reconsider> [1]
<DefFunc> ... </DefFunc> [1]
<DefPred> ... </DefPred> [1]
End Choice
End Choice
<PerCasesReasoning> ... </PerCasesReasoning> [0..1]
<EndPosition> ... </EndPosition> [1]
<Suppose> ... </Suppose> [1]
Start Choice [0..*]
Start Choice [1]
<Let> ... </Let> [1]
<Conclusion> ... </Conclusion> [1]
<Assume> ... </Assume> [1]
<Given> ... </Given> [1]
<Take> ... </Take> [1]
<TakeAsVar> ... </TakeAsVar> [1]
End Choice
<Thesis> ... </Thesis> [0..1]
Start Choice [1]
Start Choice [1]
<Now> ... </Now> [1]
<IterEquality> ... </IterEquality> [1]
<Proposition> ... </Proposition> [1]
<Justification> ... </Justification> [1]
End Choice
<Consider> ... </Consider> [1]
<Set> ... </Set> [1]
<Reconsider> ... </Reconsider> [1]
<DefFunc> ... </DefFunc> [1]
<DefPred> ... </DefPred> [1]
End Choice
End Choice
<PerCasesReasoning> ... </PerCasesReasoning> [0..1]
<EndPosition> ... </EndPosition> [1]
<BlockThesis> ... </BlockThesis> [1]
End Choice
</SupposeBlock>
Schema Component Representation
top

Element: Symbol

Name Symbol
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Symbol
kind="xs:string [1]"
nr="xs:integer [1]"
name="xs:integer [1]"/>
Schema Component Representation
top

Element: SymbolCount

Name SymbolCount
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<SymbolCount
kind="xs:token (value comes from list: {'G'|'K'|'L'|'M'|'O'|'R'|'U'|'V'}) [1]"
nr="xs:integer [1]"/>
Schema Component Representation
top

Element: Symbols

Name Symbols
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Symbols>
<Symbol> ... </Symbol> [0..*]
</Symbols>
Schema Component Representation
top

Element: Symmetry

  • This element can be used wherever the following element is referenced:
Name Symmetry
Type anyType
Nillable no
Abstract no
XML Instance Representation
<Symmetry> ... </Symmetry>
Schema Component Representation
top

Element: Take

Name Take
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Take>
<Term> ... </Term> [1]
</Take>
Schema Component Representation
top

Element: TakeAsVar

Name TakeAsVar
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<TakeAsVar
nr="xs:integer [0..1]">
<Typ> ... </Typ> [1]
<Term> ... </Term> [1]
</TakeAsVar>
Schema Component Representation
top

Element: Term

Name Term
Type anyType
Nillable no
Abstract yes
XML Instance Representation
<Term> ... </Term>
Schema Component Representation
top

Element: Theorem

Name Theorem
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Theorem
articlenr="xs:integer [0..1]"
nr="xs:integer [0..1]"
constrkind="xs:token (value comes from list: {'M'|'V'|'R'|'K'}) [0..1]"
constrnr="xs:integer [0..1]"
aid="xs:string [0..1]"
kind="xs:token (value comes from list: {'T'|'D'}) [1]">
<Formula> ... </Formula> [1]
</Theorem>
Schema Component Representation
top

Element: Theorems

Name Theorems
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Theorems
aid="xs:string [0..1]">
<Signature> ... </Signature> [0..1]
<Theorem> ... </Theorem> [0..*]
</Theorems>
Schema Component Representation
top

Element: Thesis

Name Thesis
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Thesis>
<Formula> ... </Formula> [1]
<ThesisExpansions> ... </ThesisExpansions> [1]
</Thesis>
Schema Component Representation
top

Element: ThesisExpansions

Name ThesisExpansions
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<ThesisExpansions>
<Pair> ... </Pair> [0..*]
</ThesisExpansions>
Schema Component Representation
top

Element: Transitivity

  • This element can be used wherever the following element is referenced:
Name Transitivity
Type anyType
Nillable no
Abstract no
XML Instance Representation
<Transitivity> ... </Transitivity>
Schema Component Representation
top

Element: Typ

Name Typ
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Typ
kind="xs:token (value comes from list: {'M'|'G'|'L'|'errortyp'}) [1]"
nr="xs:integer [0..1]"
absnr="xs:integer [0..1]"
aid="xs:string [0..1]"
pid="xs:integer [0..1]">
<Cluster> ... </Cluster> [0..*]
<Term> ... </Term> [0..*]
</Typ>
Schema Component Representation
top

Element: UnexpectedProp

  • This element can be used wherever the following element is referenced:
Name UnexpectedProp
Type anyType
Nillable no
Abstract no
XML Instance Representation
<UnexpectedProp> ... </UnexpectedProp>
Schema Component Representation
top

Element: Uniqueness

Name Uniqueness
Type anyType
Nillable no
Abstract no
XML Instance Representation
<Uniqueness> ... </Uniqueness>
Schema Component Representation
top

Element: UnknownCorrCond

Name UnknownCorrCond
Type anyType
Nillable no
Abstract no
XML Instance Representation
<UnknownCorrCond> ... </UnknownCorrCond>
Schema Component Representation
top

Element: Var

  • This element can be used wherever the following element is referenced:
Name Var
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Var
nr="xs:integer [1]"/>
Schema Component Representation
top

Element: Verum

  • This element can be used wherever the following element is referenced:
Name Verum
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Verum/>
Schema Component Representation
top

Element: Visible

Name Visible
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Visible>
<Int> ... </Int> [0..*]
</Visible>
Schema Component Representation
top

Element: Vocabularies

Name Vocabularies
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Vocabularies>
<Vocabulary> ... </Vocabulary> [0..*]
</Vocabularies>
Schema Component Representation
top

Element: Vocabulary

Name Vocabulary
Type Locally-defined complex type
Nillable no
Abstract no
XML Instance Representation
<Vocabulary>
<ArticleID> ... </ArticleID> [1]
<SymbolCount> ... </SymbolCount> [0..*]
</Vocabulary>
Schema Component Representation
top

Global Definitions

Attribute Group: Position

Name Position
XML Instance Representation
line="xs:integer [1]"
col="xs:integer [1]"
Schema Component Representation
top

Attribute Group: Symbols

Name Symbols
XML Instance Representation
aid="xs:string [0..1]"
Schema Component Representation
top

Model Group: AuxiliaryItem

Name AuxiliaryItem
Documentation Auxiliary items are items which do not change thesis.
XML Instance Representation
Start Choice [1]
Start Choice [1]
<Now> ... </Now> [1]
<IterEquality> ... </IterEquality> [1]
<Proposition> ... </Proposition> [1]
<Justification> ... </Justification> [1]
End Choice
<Consider> ... </Consider> [1]
<Set> ... </Set> [1]
<Reconsider> ... </Reconsider> [1]
<DefFunc> ... </DefFunc> [1]
<DefPred> ... </DefPred> [1]
End Choice
Schema Component Representation
top

Model Group: JustifiedProposition

Name JustifiedProposition
XML Instance Representation
Start Choice [1]
<Now> ... </Now> [1]
<IterEquality> ... </IterEquality> [1]
<Proposition> ... </Proposition> [1]
<Justification> ... </Justification> [1]
End Choice
Schema Component Representation
top

Model Group: Reasoning

Name Reasoning
XML Instance Representation
Start Choice [0..*]
Start Choice [1]
<Let> ... </Let> [1]
<Conclusion> ... </Conclusion> [1]
<Assume> ... </Assume> [1]
<Given> ... </Given> [1]
<Take> ... </Take> [1]
<TakeAsVar> ... </TakeAsVar> [1]
End Choice
<Thesis> ... </Thesis> [0..1]
Start Choice [1]
Start Choice [1]
<Now> ... </Now> [1]
<IterEquality> ... </IterEquality> [1]
<Proposition> ... </Proposition> [1]
<Justification> ... </Justification> [1]
End Choice
<Consider> ... </Consider> [1]
<Set> ... </Set> [1]
<Reconsider> ... </Reconsider> [1]
<DefFunc> ... </DefFunc> [1]
<DefPred> ... </DefPred> [1]
End Choice
End Choice
<PerCasesReasoning> ... </PerCasesReasoning> [0..1]
<EndPosition> ... </EndPosition> [1]
Schema Component Representation
top

Model Group: SkeletonItem

Name SkeletonItem
XML Instance Representation
Start Choice [1]
<Let> ... </Let> [1]
<Conclusion> ... </Conclusion> [1]
<Assume> ... </Assume> [1]
<Given> ... </Given> [1]
<Take> ... </Take> [1]
<TakeAsVar> ... </TakeAsVar> [1]
End Choice
<Thesis> ... </Thesis> [0..1]
Schema Component Representation
top

Legend

Complex Type:

Schema Component Type

AusAddress

Schema Component Name
Super-types: Address < AusAddress (by extension)
Sub-types:
  • QLDAddress (by restriction)
If this schema component is a type definition, its type hierarchy is shown in a gray-bordered box.
Name AusAddress
Abstract no
The table above displays the properties of this schema component.
XML Instance Representation
<... country="Australia">
<unitNo> string </unitNo> [0..1]
<houseNo> string </houseNo> [1]
<street> string </street> [1]
Start Choice[1]
<city> string </city> [1]
<town> string </town> [1]
End Choice
<state> AusStates </state> [1]
<postcode> string <<pattern = [1-9][0-9]{3}>> </postcode> [1]?
</...>

The XML Instance Representation table above shows the schema component's content as an XML instance.

Schema Component Representation
<complexTypename="AusAddress">
<complexContent>
<extensionbase="Address">
<sequence>
<elementname="state" type="AusStates"/>
<elementname="postcode">
<simpleType>
<restrictionbase="string">
<patternvalue="[1-9][0-9]{3}"/>
</restriction>
</simpleType>
</element>
</sequence>
<attributename="country" type="string" fixed="Australia"/>
</extension>
</complexContent>
</complexType>
The Schema Component Representation table above displays the underlying XML representation of the schema component. (Annotations are not shown.)
top

Glossary

Abstract (Applies to complex type definitions and element declarations). An abstract element or complex type cannot used to validate an element instance. If there is a reference to an abstract element, only element declarations that can substitute the abstract element can be used to validate the instance. For references to abstract type definitions, only derived types can be used.

All Model Group Child elements can be provided in any order in instances. See: http://www.w3.org/TR/xmlschema-1/#element-all.

Choice Model Group Only one from the list of child elements and model groups can be provided in instances. See: http://www.w3.org/TR/xmlschema-1/#element-choice.

Collapse Whitespace Policy Replace tab, line feed, and carriage return characters with space character (Unicode character 32). Then, collapse contiguous sequences of space characters into single space character, and remove leading and trailing space characters.

Disallowed Substitutions (Applies to element declarations). If substitution is specified, then substitution group members cannot be used in place of the given element declaration to validate element instances. If derivation methods, e.g. extension, restriction, are specified, then the given element declaration will not validate element instances that have types derived from the element declaration's type using the specified derivation methods. Normally, element instances can override their declaration's type by specifying an xsi:type attribute.

Key Constraint Like Uniqueness Constraint, but additionally requires that the specified value(s) must be provided. See: http://www.w3.org/TR/xmlschema-1/#cIdentity-constraint_Definitions.

Key Reference Constraint Ensures that the specified value(s) must match value(s) from a Key Constraint or Uniqueness Constraint. See: http://www.w3.org/TR/xmlschema-1/#cIdentity-constraint_Definitions.

Model Group Groups together element content, specifying the order in which the element content can occur and the number of times the group of element content may be repeated. See: http://www.w3.org/TR/xmlschema-1/#Model_Groups.

Nillable (Applies to element declarations). If an element declaration is nillable, instances can use the xsi:nil attribute. The xsi:nil attribute is the boolean attribute, nil, from the http://www.w3.org/2001/XMLSchema-instance namespace. If an element instance has an xsi:nil attribute set to true, it can be left empty, even though its element declaration may have required content.

Notation A notation is used to identify the format of a piece of data. Values of elements and attributes that are of type, NOTATION, must come from the names of declared notations. See: http://www.w3.org/TR/xmlschema-1/#cNotation_Declarations.

Preserve Whitespace Policy Preserve whitespaces exactly as they appear in instances.

Prohibited Derivations (Applies to type definitions). Derivation methods that cannot be used to create sub-types from a given type definition.

Prohibited Substitutions (Applies to complex type definitions). Prevents sub-types that have been derived using the specified derivation methods from validating element instances in place of the given type definition.

Replace Whitespace Policy Replace tab, line feed, and carriage return characters with space character (Unicode character 32).

Sequence Model Group Child elements and model groups must be provided in the specified order in instances. See: http://www.w3.org/TR/xmlschema-1/#element-sequence.

Substitution Group Elements that are members of a substitution group can be used wherever the head element of the substitution group is referenced.

Substitution Group Exclusions (Applies to element declarations). Prohibits element declarations from nominating themselves as being able to substitute a given element declaration, if they have types that are derived from the original element's type using the specified derivation methods.

Target Namespace The target namespace identifies the namespace that components in this schema belongs to. If no target namespace is provided, then the schema components do not belong to any namespace.

Uniqueness Constraint Ensures uniqueness of an element/attribute value, or a combination of values, within a specified scope. See: http://www.w3.org/TR/xmlschema-1/#cIdentity-constraint_Definitions.

top

Generated by xs3p. Last modified: 05/03/2006 22:47:20