Table of Contents
Namespace:
Table 1. Element: Abstractness
|
Documentation |
No documentation available. |
|
Content Model |
EMPTY |
|
Source |
<element name="Abstractness" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<empty/>
</element>
|
Table 2. Element: Adjective
|
Documentation |
No documentation available. | ||||||||||||||||||||||||||||
|
Content Model |
( %Term; )* | ||||||||||||||||||||||||||||
|
Attributes |
| ||||||||||||||||||||||||||||
|
Source |
<element name="Adjective" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="nr">
<data type="integer"/>
</attribute>
<optional>
<attribute name="value">
<data type="boolean"/>
</attribute>
</optional>
<optional>
<attribute name="absnr">
<data type="integer"/>
</attribute>
<attribute name="aid">
<data type="string"/>
</attribute>
</optional>
<optional>
<attribute name="kind">
<value>V</value>
</attribute>
</optional>
<optional>
<attribute name="pid">
<data type="integer"/>
</attribute>
</optional>
<zeroOrMore>
<ref name="Term"/>
</zeroOrMore>
</element>
|
Table 3. Element: And
|
Documentation |
No documentation available. | ||||||||
|
Content Model |
( %Formula; )* | ||||||||
|
Attributes |
| ||||||||
|
Source |
<element name="And" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<optional>
<attribute name="pid">
<data type="integer"/>
</attribute>
</optional>
<zeroOrMore>
<ref name="Formula"/>
</zeroOrMore>
</element>
|
Table 4. Element: Antisymmetry
|
Documentation |
No documentation available. |
|
Content Model |
EMPTY |
|
Source |
<element name="Antisymmetry" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<empty/>
</element>
|
Table 5. Element: ArgTypes
|
Documentation |
No documentation available. |
|
Content Model |
( %Typ; )* |
|
Source |
<element name="ArgTypes" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<zeroOrMore>
<ref name="Typ"/>
</zeroOrMore>
</element>
|
Table 6. Element: Article
|
Documentation |
No documentation available. | ||||||||||||
|
Content Model |
( ( %DefinitionBlock; | %RegistrationBlock; | %NotationBlock; | %Reservation; | %SchemeBlock; | %JustifiedTheorem; | %DefTheorem; | %Definiens; | %Canceled; | %Section; | %AuxiliaryItem; ) )* | ||||||||||||
|
Attributes |
| ||||||||||||
|
Source |
<element name="Article" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="aid">
<data type="string"/>
</attribute>
<optional>
<attribute name="mizfiles">
<data type="string"/>
</attribute>
</optional>
<zeroOrMore>
<choice>
<ref name="DefinitionBlock"/>
<ref name="RegistrationBlock"/>
<ref name="NotationBlock"/>
<ref name="Reservation"/>
<ref name="SchemeBlock"/>
<ref name="JustifiedTheorem"/>
<ref name="DefTheorem"/>
<ref name="Definiens"/>
<ref name="Canceled"/>
<ref name="Section"/>
<ref name="AuxiliaryItem"/>
</choice>
</zeroOrMore>
</element>
|
Table 7. Element: ArticleID
|
Documentation |
No documentation available. | ||||||||
|
Content Model |
| ||||||||
|
Attributes |
| ||||||||
|
Source |
<element name="ArticleID" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="name">
<data type="string"/>
</attribute>
</element>
|
Table 8. Element: Associativity
|
Documentation |
No documentation available. |
|
Content Model |
EMPTY |
|
Source |
<element name="Associativity" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<empty/>
</element>
|
Table 9. Element: Assume
|
Documentation |
No documentation available. |
|
Content Model |
( %Proposition; )+ |
|
Source |
<element name="Assume" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<oneOrMore>
<ref name="Proposition"/>
</oneOrMore>
</element>
|
Table 10. Element: BlockThesis
|
Documentation |
No documentation available. |
|
Content Model | |
|
Source |
<element name="BlockThesis" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<zeroOrMore>
<ref name="Thesis"/>
</zeroOrMore>
<ref name="Formula"/>
</element>
|
Table 11. Element: By
|
Documentation |
No documentation available. | ||||||||||||||||
|
Content Model |
( %Ref; )* | ||||||||||||||||
|
Attributes |
| ||||||||||||||||
|
Source |
<element name="By" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<ref name="Position"/>
<optional>
<attribute name="linked">
<data type="boolean"/>
</attribute>
</optional>
<zeroOrMore>
<ref name="Ref"/>
</zeroOrMore>
</element>
|
Table 12. Element: ByExplanations
|
Documentation |
No documentation available. | ||||||||
|
Content Model |
( %PolyEval; )* | ||||||||
|
Attributes |
| ||||||||
|
Source |
<element name="ByExplanations" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="aid">
<data type="string"/>
</attribute>
<zeroOrMore>
<ref name="PolyEval"/>
</zeroOrMore>
</element>
|
Table 13. Element: CCluster
|
Documentation |
No documentation available. | ||||||||||||
|
Content Model |
( %ErrorCluster; | ( %ArgTypes;, %Cluster;, %Typ;, %Cluster;, %Cluster; ? ) ) | ||||||||||||
|
Attributes |
| ||||||||||||
|
Source |
<element name="CCluster" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<optional>
<attribute name="nr">
<data type="integer"/>
</attribute>
<attribute name="aid">
<data type="string"/>
</attribute>
</optional>
<choice>
<ref name="ErrorCluster"/>
<group>
<ref name="ArgTypes"/>
<ref name="Cluster"/>
<ref name="Typ"/>
<ref name="Cluster"/>
<optional>
<ref name="Cluster"/>
</optional>
</group>
</choice>
</element>
|
Table 14. Element: Canceled
|
Documentation |
No documentation available. |
|
Content Model |
EMPTY |
|
Source |
<element name="Canceled" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<empty/>
</element>
|
Table 15. Element: Case
|
Documentation |
No documentation available. |
|
Content Model |
( %Proposition; )+ |
|
Source |
<element name="Case" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<oneOrMore>
<ref name="Proposition"/>
</oneOrMore>
</element>
|
Table 16. Element: CaseBlock
|
Documentation |
No documentation available. | ||||||||||||
|
Content Model |
( ( %BlockThesis; %Case; %Thesis; %Reasoning; ) | ( %Case; %Reasoning; %BlockThesis; ) ) | ||||||||||||
|
Attributes |
| ||||||||||||
|
Source |
<element name="CaseBlock" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<ref name="Position"/>
<choice>
<group>
<ref name="BlockThesis"/>
<ref name="Case"/>
<ref name="Thesis"/>
<ref name="Reasoning"/>
</group>
<group>
<ref name="Case"/>
<ref name="Reasoning"/>
<ref name="BlockThesis"/>
</group>
</choice>
</element>
|
Table 17. Element: Choice
|
Documentation |
No documentation available. |
|
Content Model | |
|
Source |
<element name="Choice" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<ref name="Typ"/>
</element>
|
Table 18. Element: Cluster
|
Documentation |
No documentation available. |
|
Content Model |
( %Adjective; )* |
|
Source |
<element name="Cluster" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<zeroOrMore>
<ref name="Adjective"/>
</zeroOrMore>
</element>
|
Table 19. Element: Coherence
|
Documentation |
No documentation available. |
|
Content Model |
( %Formula; | ( %Proposition; %Justification; ) ) |
|
Source |
<element name="Coherence" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<choice>
<ref name="Formula"/>
<group>
<ref name="Proposition"/>
<ref name="Justification"/>
</group>
</choice>
</element>
|
Table 20. Element: Commutativity
|
Documentation |
No documentation available. |
|
Content Model |
EMPTY |
|
Source |
<element name="Commutativity" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<empty/>
</element>
|
Table 21. Element: Compatibility
|
Documentation |
No documentation available. |
|
Content Model |
( %Formula; | ( %Proposition; %Justification; ) ) |
|
Source |
<element name="Compatibility" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<choice>
<ref name="Formula"/>
<group>
<ref name="Proposition"/>
<ref name="Justification"/>
</group>
</choice>
</element>
|
Table 22. Element: ComplexNr
|
Documentation |
No documentation available. |
|
Content Model | |
|
Source |
<element name="ComplexNr" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<ref name="RationalNr"/>
<ref name="RationalNr"/>
</element>
|
Table 23. Element: Conclusion
|
Documentation |
No documentation available. |
|
Content Model | |
|
Source |
<element name="Conclusion" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<ref name="JustifiedProposition"/>
</element>
|
Table 24. Element: Connectedness
|
Documentation |
No documentation available. |
|
Content Model |
EMPTY |
|
Source |
<element name="Connectedness" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<empty/>
</element>
|
Table 25. Element: Consider
|
Documentation |
No documentation available. | ||||||||
|
Content Model |
%Proposition;, %Justification;, ( %Typ; )+ , ( %Proposition; )* | ||||||||
|
Attributes |
| ||||||||
|
Source |
<element name="Consider" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<optional>
<attribute name="nr">
<data type="integer"/>
</attribute>
</optional>
<ref name="Proposition"/>
<ref name="Justification"/>
<oneOrMore>
<ref name="Typ"/>
</oneOrMore>
<zeroOrMore>
<ref name="Proposition"/>
</zeroOrMore>
</element>
|
Table 26. Element: Consistency
|
Documentation |
No documentation available. |
|
Content Model |
( %Formula; | ( %Proposition; %Justification; ) ) |
|
Source |
<element name="Consistency" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<choice>
<ref name="Formula"/>
<group>
<ref name="Proposition"/>
<ref name="Justification"/>
</group>
</choice>
</element>
|
Table 27. Element: Const
|
Documentation |
No documentation available. | ||||||||||||
|
Content Model |
| ||||||||||||
|
Attributes |
| ||||||||||||
|
Source |
<element name="Const" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="nr">
<data type="integer"/>
</attribute>
<optional>
<attribute name="vid">
<data type="integer"/>
</attribute>
</optional>
</element>
|
Table 28. Element: ConstrCount
|
Documentation |
No documentation available. | ||||||||||||
|
Content Model |
| ||||||||||||
|
Attributes |
| ||||||||||||
|
Source |
<element name="ConstrCount" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="kind">
<choice>
<value>M</value>
<value>L</value>
<value>V</value>
<value>R</value>
<value>K</value>
<value>U</value>
<value>G</value>
</choice>
</attribute>
<attribute name="nr">
<data type="integer"/>
</attribute>
</element>
|
Table 29. Element: ConstrCounts
|
Documentation |
No documentation available. | ||||||||
|
Content Model |
( ConstrCount )* | ||||||||
|
Attributes |
| ||||||||
|
Source |
<element name="ConstrCounts" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<optional>
<attribute name="name">
<data type="string"/>
</attribute>
</optional>
<zeroOrMore>
<element name="ConstrCount">
<attribute name="kind">
<choice>
<value>M</value>
<value>L</value>
<value>V</value>
<value>R</value>
<value>K</value>
<value>U</value>
<value>G</value>
</choice>
</attribute>
<attribute name="nr">
<data type="integer"/>
</attribute>
</element>
</zeroOrMore>
</element>
|
Table 30. Element: ConstrDef
|
Documentation |
No documentation available. | ||||||||||||
|
Content Model | |||||||||||||
|
Attributes |
| ||||||||||||
|
Source |
<element name="ConstrDef" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="constrkind">
<choice>
<value>K</value>
<value>U</value>
<value>G</value>
</choice>
</attribute>
<attribute name="constrnr">
<data type="integer"/>
</attribute>
<zeroOrMore>
<ref name="Typ"/>
</zeroOrMore>
<optional>
<ref name="Term"/>
</optional>
</element>
|
Table 31. Element: Constructor
|
Documentation |
No documentation available. | ||||||||||||||||||||||||||||||||||||||||||||
|
Content Model |
%Properties; ? , %ArgTypes;, %StructLoci; ? , ( %Typ; )* , %Fields; ? | ||||||||||||||||||||||||||||||||||||||||||||
|
Attributes |
| ||||||||||||||||||||||||||||||||||||||||||||
|
Source |
<element name="Constructor" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="kind">
<choice>
<value>M</value>
<value>L</value>
<value>V</value>
<value>R</value>
<value>K</value>
<value>U</value>
<value>G</value>
</choice>
</attribute>
<attribute name="nr">
<data type="integer"/>
</attribute>
<attribute name="aid">
<data type="string"/>
</attribute>
<optional>
<attribute name="relnr">
<data type="integer"/>
</attribute>
</optional>
<optional>
<attribute name="redefnr">
<data type="integer"/>
</attribute>
<attribute name="superfluous">
<data type="integer"/>
</attribute>
<optional>
<attribute name="absredefnr">
<data type="integer"/>
</attribute>
<attribute name="redefaid">
<data type="string"/>
</attribute>
</optional>
</optional>
<optional>
<choice>
<attribute name="structmodeaggrnr">
<data type="integer"/>
</attribute>
<attribute name="aggregbase">
<data type="integer"/>
</attribute>
</choice>
</optional>
<optional>
<ref name="Properties"/>
</optional>
<ref name="ArgTypes"/>
<optional>
<ref name="StructLoci"/>
</optional>
<zeroOrMore>
<ref name="Typ"/>
</zeroOrMore>
<optional>
<ref name="Fields"/>
</optional>
</element>
|
Table 32. Element: Constructors
|
Documentation |
No documentation available. | ||||||||
|
Content Model |
( SignatureWithCounts | ( %Signature; %ConstrCounts; ) ) ? , ( %Constructor; )* | ||||||||
|
Attributes |
| ||||||||
|
Source |
<element name="Constructors" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<optional>
<attribute name="aid">
<data type="string"/>
</attribute>
</optional>
<optional>
<choice>
<element name="SignatureWithCounts">
<zeroOrMore>
<ref name="ConstrCounts"/>
</zeroOrMore>
</element>
<group>
<ref name="Signature"/>
<ref name="ConstrCounts"/>
</group>
</choice>
</optional>
<zeroOrMore>
<ref name="Constructor"/>
</zeroOrMore>
</element>
|
Table 33. Element: Correctness
|
Documentation |
No documentation available. |
|
Content Model | |
|
Source |
<element name="Correctness" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<zeroOrMore>
<ref name="CorrectnessCondition"/>
</zeroOrMore>
<ref name="Proposition"/>
<ref name="Justification"/>
</element>
|
Table 34. Element: DefFunc
|
Documentation |
No documentation available. | ||||||||||||
|
Content Model | |||||||||||||
|
Attributes |
| ||||||||||||
|
Source |
<element name="DefFunc" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<optional>
<attribute name="nr">
<data type="integer"/>
</attribute>
</optional>
<optional>
<attribute name="vid">
<data type="integer"/>
</attribute>
</optional>
<ref name="ArgTypes"/>
<ref name="Term"/>
<ref name="Typ"/>
</element>
|
Table 35. Element: DefMeaning
|
Documentation |
No documentation available. | ||||||||
|
Content Model |
( PartialDef )* , ( %Formula; | %Term; ) ? | ||||||||
|
Attributes |
| ||||||||
|
Source |
<element name="DefMeaning" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="kind">
<choice>
<value>e</value>
<value>m</value>
</choice>
</attribute>
<zeroOrMore>
<element name="PartialDef">
<choice>
<ref name="Formula"/>
<ref name="Term"/>
</choice>
<ref name="Formula"/>
</element>
</zeroOrMore>
<optional>
<choice>
<ref name="Formula"/>
<ref name="Term"/>
</choice>
</optional>
</element>
|
Table 36. Element: DefPred
|
Documentation |
No documentation available. | ||||||||||||
|
Content Model | |||||||||||||
|
Attributes |
| ||||||||||||
|
Source |
<element name="DefPred" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<optional>
<attribute name="nr">
<data type="integer"/>
</attribute>
</optional>
<optional>
<attribute name="vid">
<data type="integer"/>
</attribute>
</optional>
<ref name="ArgTypes"/>
<ref name="Formula"/>
</element>
|
Table 37. Element: DefTheorem
|
Documentation |
No documentation available. | ||||||||||||
|
Content Model | |||||||||||||
|
Attributes |
| ||||||||||||
|
Source |
<element name="DefTheorem" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<optional>
<attribute name="constrkind">
<choice>
<value>M</value>
<value>V</value>
<value>R</value>
<value>K</value>
</choice>
</attribute>
<attribute name="constrnr">
<data type="integer"/>
</attribute>
</optional>
<ref name="Proposition"/>
</element>
|
Table 38. Element: Definiens
|
Documentation |
No documentation available. | ||||||||||||||||||||||||||||||||
|
Content Model |
( %Typ; )* , Essentials, %Formula; ? %DefMeaning; | ||||||||||||||||||||||||||||||||
|
Attributes |
| ||||||||||||||||||||||||||||||||
|
Source |
<element name="Definiens" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="constrkind">
<choice>
<value>M</value>
<value>L</value>
<value>V</value>
<value>R</value>
<value>K</value>
<value>U</value>
<value>G</value>
</choice>
</attribute>
<attribute name="constrnr">
<data type="integer"/>
</attribute>
<attribute name="defnr">
<data type="integer"/>
</attribute>
<optional>
<attribute name="vid">
<data type="integer"/>
</attribute>
</optional>
<attribute name="aid">
<data type="string"/>
</attribute>
<optional>
<attribute name="nr">
<data type="integer"/>
</attribute>
</optional>
<optional>
<attribute name="relnr">
<data type="integer"/>
</attribute>
</optional>
<zeroOrMore>
<ref name="Typ"/>
</zeroOrMore>
<element name="Essentials">
<zeroOrMore>
<ref name="Int"/>
</zeroOrMore>
</element>
<optional>
<ref name="Formula"/>
</optional>
<ref name="DefMeaning"/>
</element>
|
Table 39. Element: Definientia
|
Documentation |
No documentation available. | ||||||||
|
Content Model |
%Signature; ? , ( %Definiens; )* | ||||||||
|
Attributes |
| ||||||||
|
Source |
<element name="Definientia" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<optional>
<attribute name="aid">
<data type="string"/>
</attribute>
</optional>
<optional>
<ref name="Signature"/>
</optional>
<zeroOrMore>
<ref name="Definiens"/>
</zeroOrMore>
</element>
|
Table 40. Element: Definition
|
Documentation |
No documentation available. | ||||||||||||||||||||||||||||||||
|
Content Model |
? , ( ( ( %CorrectnessCondition; )* , %Correctness; ? , ( %JustifiedProperty; )* , %Constructor; ? , %Pattern; ? ) | ( %Constructor;, %Constructor;, ( %Constructor; )+ , %Registration;, ( %CorrectnessCondition; )* , %Correctness; ? , ( %Pattern; )+ ) ) | ||||||||||||||||||||||||||||||||
|
Attributes |
| ||||||||||||||||||||||||||||||||
|
Source |
<element name="Definition" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="kind">
<choice>
<value>M</value>
<value>V</value>
<value>R</value>
<value>K</value>
<value>G</value>
</choice>
</attribute>
<optional>
<attribute name="redefinition">
<data type="boolean"/>
</attribute>
</optional>
<optional>
<attribute name="expandable">
<data type="boolean"/>
</attribute>
</optional>
<optional>
<attribute name="nr">
<data type="integer"/>
</attribute>
<ref name="Position"/>
</optional>
<optional>
<attribute name="vid">
<data type="integer"/>
</attribute>
</optional>
<choice>
<group>
<zeroOrMore>
<ref name="CorrectnessCondition"/>
</zeroOrMore>
<optional>
<ref name="Correctness"/>
</optional>
<zeroOrMore>
<ref name="JustifiedProperty"/>
</zeroOrMore>
<optional>
<ref name="Constructor"/>
</optional>
<optional>
<ref name="Pattern"/>
</optional>
</group>
<group>
<ref name="Constructor"/>
<ref name="Constructor"/>
<oneOrMore>
<ref name="Constructor"/>
</oneOrMore>
<ref name="Registration"/>
<zeroOrMore>
<ref name="CorrectnessCondition"/>
</zeroOrMore>
<optional>
<ref name="Correctness"/>
</optional>
<oneOrMore>
<ref name="Pattern"/>
</oneOrMore>
</group>
</choice>
</element>
|
Table 41. Element: DefinitionBlock
|
Documentation |
No documentation available. | ||||||||||||
|
Content Model |
( ( %Let; | %Assume; | %Given; | %AuxiliaryItem; | %Canceled; | %Definition; ) )* %EndPosition; | ||||||||||||
|
Attributes |
| ||||||||||||
|
Source |
<element name="DefinitionBlock" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<ref name="Position"/>
<zeroOrMore>
<choice>
<ref name="Let"/>
<ref name="Assume"/>
<ref name="Given"/>
<ref name="AuxiliaryItem"/>
<ref name="Canceled"/>
<ref name="Definition"/>
</choice>
</zeroOrMore>
<ref name="EndPosition"/>
</element>
|
Table 42. Element: EndPosition
|
Documentation |
No documentation available. | ||||||||||||
|
Content Model |
| ||||||||||||
|
Attributes |
| ||||||||||||
|
Source |
<element name="EndPosition" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<ref name="Position"/>
</element>
|
Table 43. Element: EqArgs
|
Documentation |
No documentation available. |
|
Content Model |
( %Pair; )* |
|
Source |
<element name="EqArgs" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<zeroOrMore>
<ref name="Pair"/>
</zeroOrMore>
</element>
|
Table 44. Element: ErrorCluster
|
Documentation |
No documentation available. |
|
Content Model |
EMPTY |
|
Source |
<element name="ErrorCluster" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<empty/>
</element>
|
Table 45. Element: ErrorFrm
|
Documentation |
No documentation available. |
|
Content Model |
EMPTY |
|
Source |
<element name="ErrorFrm" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<empty/>
</element>
|
Table 46. Element: ErrorIdentify
|
Documentation |
No documentation available. |
|
Content Model |
EMPTY |
|
Source |
<element name="ErrorIdentify" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<empty/>
</element>
|
Table 47. Element: ErrorInf
|
Documentation |
No documentation available. |
|
Content Model |
EMPTY |
|
Source |
<element name="ErrorInf" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<empty/>
</element>
|
Table 48. Element: ErrorTrm
|
Documentation |
No documentation available. |
|
Content Model |
EMPTY |
|
Source |
<element name="ErrorTrm" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<empty/>
</element>
|
Table 49. Element: Essentials
|
Documentation |
No documentation available. |
|
Content Model |
( %Int; )* |
|
Source |
<element name="Essentials" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<zeroOrMore>
<ref name="Int"/>
</zeroOrMore>
</element>
|
Table 50. Element: Existence
|
Documentation |
No documentation available. |
|
Content Model |
( %Formula; | ( %Proposition; %Justification; ) ) |
|
Source |
<element name="Existence" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<choice>
<ref name="Formula"/>
<group>
<ref name="Proposition"/>
<ref name="Justification"/>
</group>
</choice>
</element>
|
Table 51. Element: Expansion
|
Documentation |
No documentation available. |
|
Content Model | |
|
Source |
<element name="Expansion" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<ref name="Typ"/>
</element>
|
Table 52. Element: FCluster
|
Documentation |
No documentation available. | ||||||||||||
|
Content Model |
( %ErrorCluster; | ( %ArgTypes;, %Term;, %Cluster;, %Cluster; ? , %Typ; ? ) ) | ||||||||||||
|
Attributes |
| ||||||||||||
|
Source |
<element name="FCluster" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<optional>
<attribute name="nr">
<data type="integer"/>
</attribute>
<attribute name="aid">
<data type="string"/>
</attribute>
</optional>
<choice>
<ref name="ErrorCluster"/>
<group>
<ref name="ArgTypes"/>
<ref name="Term"/>
<ref name="Cluster"/>
<optional>
<ref name="Cluster"/>
</optional>
<optional>
<ref name="Typ"/>
</optional>
</group>
</choice>
</element>
|
Table 53. Element: Field
|
Documentation |
No documentation available. | ||||||||||||||||||||
|
Content Model |
| ||||||||||||||||||||
|
Attributes |
| ||||||||||||||||||||
|
Source |
<element name="Field" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="nr">
<data type="integer"/>
</attribute>
<optional>
<attribute name="kind">
<value>U</value>
</attribute>
</optional>
<optional>
<attribute name="aid">
<data type="string"/>
</attribute>
</optional>
<optional>
<attribute name="absnr">
<data type="integer"/>
</attribute>
</optional>
</element>
|
Table 54. Element: Fields
|
Documentation |
No documentation available. |
|
Content Model |
( Field )* |
|
Source |
<element name="Fields" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<zeroOrMore>
<element name="Field">
<attribute name="nr">
<data type="integer"/>
</attribute>
<optional>
<attribute name="kind">
<value>U</value>
</attribute>
</optional>
<optional>
<attribute name="aid">
<data type="string"/>
</attribute>
</optional>
<optional>
<attribute name="absnr">
<data type="integer"/>
</attribute>
</optional>
</element>
</zeroOrMore>
</element>
|
Table 55. Element: For
|
Documentation |
No documentation available. | ||||||||||||
|
Content Model | |||||||||||||
|
Attributes |
| ||||||||||||
|
Source |
<element name="For" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<optional>
<attribute name="pid">
<data type="integer"/>
</attribute>
</optional>
<optional>
<attribute name="vid">
<data type="integer"/>
</attribute>
</optional>
<ref name="Typ"/>
<ref name="Formula"/>
</element>
|
Table 56. Element: Format
|
Documentation |
No documentation available. | ||||||||||||||||||||||||||||
|
Content Model |
| ||||||||||||||||||||||||||||
|
Attributes |
| ||||||||||||||||||||||||||||
|
Source |
<element name="Format" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="kind">
<choice>
<value>G</value>
<value>K</value>
<value>J</value>
<value>L</value>
<value>M</value>
<value>O</value>
<value>R</value>
<value>U</value>
<value>V</value>
</choice>
</attribute>
<optional>
<attribute name="nr">
<data type="integer"/>
</attribute>
</optional>
<attribute name="symbolnr">
<data type="integer"/>
</attribute>
<attribute name="argnr">
<data type="integer"/>
</attribute>
<optional>
<attribute name="leftargnr">
<data type="integer"/>
</attribute>
</optional>
<optional>
<attribute name="rightsymbolnr">
<data type="integer"/>
</attribute>
</optional>
</element>
|
Table 57. Element: Formats
|
Documentation |
No documentation available. |
|
Content Model | |
|
Source |
<element name="Formats" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<zeroOrMore>
<ref name="Format"/>
</zeroOrMore>
<zeroOrMore>
<element name="Priority">
<attribute name="kind">
<choice>
<value>O</value>
<value>K</value>
<value>L</value>
</choice>
</attribute>
<attribute name="symbolnr">
<data type="integer"/>
</attribute>
<attribute name="value">
<data type="integer"/>
</attribute>
</element>
</zeroOrMore>
</element>
|
Table 58. Element: Fraenkel
|
Documentation |
No documentation available. |
|
Content Model | |
|
Source |
<element name="Fraenkel" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<zeroOrMore>
<ref name="Typ"/>
</zeroOrMore>
<ref name="Term"/>
<ref name="Formula"/>
</element>
|
Table 59. Element: FreeVar
|
Documentation |
No documentation available. | ||||||||
|
Content Model |
| ||||||||
|
Attributes |
| ||||||||
|
Source |
<element name="FreeVar" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="nr">
<data type="integer"/>
</attribute>
</element>
|
Table 60. Element: From
|
Documentation |
No documentation available. | ||||||||||||||||||||
|
Content Model |
( %Ref; )* | ||||||||||||||||||||
|
Attributes |
| ||||||||||||||||||||
|
Source |
<element name="From" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<ref name="Position"/>
<attribute name="articlenr">
<data type="integer"/>
</attribute>
<attribute name="nr">
<data type="integer"/>
</attribute>
<zeroOrMore>
<ref name="Ref"/>
</zeroOrMore>
</element>
|
Table 61. Element: FromExplanations
|
Documentation |
No documentation available. | ||||||||
|
Content Model | |||||||||
|
Attributes |
| ||||||||
|
Source |
<element name="FromExplanations" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="aid">
<data type="string"/>
</attribute>
<zeroOrMore>
<ref name="SchemeInstantiation"/>
</zeroOrMore>
</element>
|
Table 62. Element: Func
|
Documentation |
No documentation available. | ||||||||||||||||||||||||
|
Content Model |
( %Term; )* | ||||||||||||||||||||||||
|
Attributes |
| ||||||||||||||||||||||||
|
Source |
<element name="Func" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="kind">
<choice>
<value>F</value>
<value>G</value>
<value>K</value>
<value>U</value>
</choice>
</attribute>
<attribute name="nr">
<data type="integer"/>
</attribute>
<optional>
<attribute name="absnr">
<data type="integer"/>
</attribute>
<attribute name="aid">
<data type="string"/>
</attribute>
</optional>
<optional>
<attribute name="pid">
<data type="integer"/>
</attribute>
</optional>
<zeroOrMore>
<ref name="Term"/>
</zeroOrMore>
</element>
|
Table 63. Element: FuncInstance
|
Documentation |
No documentation available. | ||||||||||||||||||||||||
|
Content Model |
( ( ) | %Term; ) | ||||||||||||||||||||||||
|
Attributes |
| ||||||||||||||||||||||||
|
Source |
<element name="FuncInstance" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="instnr">
<data type="integer"/>
</attribute>
<choice>
<group>
<attribute name="kind">
<choice>
<value>F</value>
<value>H</value>
<value>G</value>
<value>K</value>
<value>U</value>
</choice>
</attribute>
<attribute name="nr">
<data type="integer"/>
</attribute>
<optional>
<attribute name="absnr">
<data type="integer"/>
</attribute>
<attribute name="aid">
<data type="string"/>
</attribute>
</optional>
</group>
<ref name="Term"/>
</choice>
</element>
|
Table 64. Element: Given
|
Documentation |
No documentation available. | ||||||||
|
Content Model |
%Proposition;, ( %Typ; )+ , ( %Proposition; )+ | ||||||||
|
Attributes |
| ||||||||
|
Source |
<element name="Given" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<optional>
<attribute name="nr">
<data type="integer"/>
</attribute>
</optional>
<ref name="Proposition"/>
<oneOrMore>
<ref name="Typ"/>
</oneOrMore>
<oneOrMore>
<ref name="Proposition"/>
</oneOrMore>
</element>
|
Table 65. Element: Idempotence
|
Documentation |
No documentation available. |
|
Content Model |
EMPTY |
|
Source |
<element name="Idempotence" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<empty/>
</element>
|
Table 66. Element: Ident
|
Documentation |
No documentation available. | ||||||||
|
Content Model |
| ||||||||
|
Attributes |
| ||||||||
|
Source |
<element name="Ident" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="vid">
<data type="integer"/>
</attribute>
</element>
|
Table 67. Element: Identify
|
Documentation |
No documentation available. | ||||||||||||||||
|
Content Model |
( %ErrorIdentify; | ( ( %Typ; )* , ( ( %Term; %Term; ) | ( %Formula; %Formula; ) ) EqArgs ) ) | ||||||||||||||||
|
Attributes |
| ||||||||||||||||
|
Source |
<element name="Identify" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="nr">
<data type="integer"/>
</attribute>
<attribute name="aid">
<data type="string"/>
</attribute>
<attribute name="constrkind">
<choice>
<value>K</value>
<value>U</value>
<value>G</value>
<value>V</value>
<value>R</value>
</choice>
</attribute>
<choice>
<ref name="ErrorIdentify"/>
<group>
<zeroOrMore>
<ref name="Typ"/>
</zeroOrMore>
<choice>
<group>
<ref name="Term"/>
<ref name="Term"/>
</group>
<group>
<ref name="Formula"/>
<ref name="Formula"/>
</group>
</choice>
<element name="EqArgs">
<zeroOrMore>
<ref name="Pair"/>
</zeroOrMore>
</element>
</group>
</choice>
</element>
|
Table 68. Element: IdentifyRegistration
|
Documentation |
No documentation available. |
|
Content Model |
%Identify;, ( %CorrectnessCondition; )* , %Correctness; ? |
|
Source |
<element name="IdentifyRegistration" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<ref name="Identify"/>
<zeroOrMore>
<ref name="CorrectnessCondition"/>
</zeroOrMore>
<optional>
<ref name="Correctness"/>
</optional>
</element>
|
Table 69. Element: IdentifyRegistrations
|
Documentation |
No documentation available. | ||||||||
|
Content Model |
%Signature; ? , ( %Identify; )* | ||||||||
|
Attributes |
| ||||||||
|
Source |
<element name="IdentifyRegistrations" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<optional>
<attribute name="aid">
<data type="string"/>
</attribute>
</optional>
<optional>
<ref name="Signature"/>
</optional>
<zeroOrMore>
<ref name="Identify"/>
</zeroOrMore>
</element>
|
Table 70. Element: IdentifyWithExp
|
Documentation |
No documentation available. | ||||||||||||||||||||
|
Content Model |
( %ErrorIdentify; | ( ( %Typ; )* ( ( %Term; %Term; ) | ( %Formula; %Formula; ) ) ) ) | ||||||||||||||||||||
|
Attributes |
| ||||||||||||||||||||
|
Source |
<element name="IdentifyWithExp" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<optional>
<attribute name="nr">
<data type="integer"/>
</attribute>
<attribute name="aid">
<data type="string"/>
</attribute>
</optional>
<choice>
<ref name="ErrorIdentify"/>
<group>
<attribute name="constrkind">
<choice>
<value>K</value>
<value>U</value>
<value>G</value>
<value>V</value>
<value>R</value>
</choice>
</attribute>
<attribute name="constrnr">
<data type="integer"/>
</attribute>
<zeroOrMore>
<ref name="Typ"/>
</zeroOrMore>
<choice>
<group>
<ref name="Term"/>
<ref name="Term"/>
</group>
<group>
<ref name="Formula"/>
<ref name="Formula"/>
</group>
</choice>
</group>
</choice>
</element>
|
Table 71. Element: InfConst
|
Documentation |
No documentation available. | ||||||||
|
Content Model |
| ||||||||
|
Attributes |
| ||||||||
|
Source |
<element name="InfConst" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="nr">
<data type="integer"/>
</attribute>
</element>
|
Table 72. Element: Int
|
Documentation |
No documentation available. | ||||||||
|
Content Model |
| ||||||||
|
Attributes |
| ||||||||
|
Source |
<element name="Int" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="x">
<data type="integer"/>
</attribute>
</element>
|
Table 73. Element: Involutiveness
|
Documentation |
No documentation available. |
|
Content Model |
EMPTY |
|
Source |
<element name="Involutiveness" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<empty/>
</element>
|
Table 74. Element: Irreflexivity
|
Documentation |
No documentation available. |
|
Content Model |
EMPTY |
|
Source |
<element name="Irreflexivity" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<empty/>
</element>
|
Table 76. Element: It
|
Documentation |
No documentation available. |
|
Content Model |
EMPTY |
|
Source |
<element name="It" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<empty/>
</element>
|
Table 77. Element: IterEquality
|
Documentation |
No documentation available. | ||||||||||||||||||||
|
Content Model |
%Term;, ( %IterStep; )+ | ||||||||||||||||||||
|
Attributes |
| ||||||||||||||||||||
|
Source |
<element name="IterEquality" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<optional>
<attribute name="nr">
<data type="integer"/>
</attribute>
</optional>
<optional>
<attribute name="vid">
<data type="integer"/>
</attribute>
</optional>
<ref name="Position"/>
<ref name="Term"/>
<oneOrMore>
<ref name="IterStep"/>
</oneOrMore>
</element>
|
Table 78. Element: IterStep
|
Documentation |
No documentation available. |
|
Content Model | |
|
Source |
<element name="IterStep" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<ref name="Term"/>
<ref name="Inference"/>
</element>
|
Table 79. Element: JustifiedProperty
|
Documentation |
No documentation available. |
|
Content Model | |
|
Source |
<element name="JustifiedProperty" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<ref name="Property"/>
<ref name="Proposition"/>
<ref name="Justification"/>
</element>
|
Table 80. Element: JustifiedTheorem
|
Documentation |
No documentation available. |
|
Content Model | |
|
Source |
<element name="JustifiedTheorem" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<ref name="Proposition"/>
<ref name="Justification"/>
</element>
|
Table 81. Element: LambdaVar
|
Documentation |
No documentation available. | ||||||||
|
Content Model |
| ||||||||
|
Attributes |
| ||||||||
|
Source |
<element name="LambdaVar" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="nr">
<data type="integer"/>
</attribute>
</element>
|
Table 82. Element: Let
|
Documentation |
No documentation available. | ||||||||
|
Content Model |
( %Typ; )+ | ||||||||
|
Attributes |
| ||||||||
|
Source |
<element name="Let" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<optional>
<attribute name="nr">
<data type="integer"/>
</attribute>
</optional>
<oneOrMore>
<ref name="Typ"/>
</oneOrMore>
</element>
|
Table 83. Element: LocusVar
|
Documentation |
No documentation available. | ||||||||
|
Content Model |
| ||||||||
|
Attributes |
| ||||||||
|
Source |
<element name="LocusVar" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="nr">
<data type="integer"/>
</attribute>
</element>
|
Table 84. Element: Monomial
|
Documentation |
No documentation available. |
|
Content Model |
%Number;, ( PoweredVar )* |
|
Source |
<element name="Monomial" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<ref name="Number"/>
<zeroOrMore>
<element name="PoweredVar">
<attribute name="nr">
<data type="integer"/>
</attribute>
<attribute name="exponent">
<data type="integer"/>
</attribute>
</element>
</zeroOrMore>
</element>
|
Table 85. Element: Not
|
Documentation |
No documentation available. | ||||||||
|
Content Model | |||||||||
|
Attributes |
| ||||||||
|
Source |
<element name="Not" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<optional>
<attribute name="pid">
<data type="integer"/>
</attribute>
</optional>
<ref name="Formula"/>
</element>
|
Table 86. Element: NotationBlock
|
Documentation |
No documentation available. | ||||||||||||
|
Content Model |
( ( %Let; | %AuxiliaryItem; | %Pattern; ) )* %EndPosition; | ||||||||||||
|
Attributes |
| ||||||||||||
|
Source |
<element name="NotationBlock" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<ref name="Position"/>
<zeroOrMore>
<choice>
<ref name="Let"/>
<ref name="AuxiliaryItem"/>
<ref name="Pattern"/>
</choice>
</zeroOrMore>
<ref name="EndPosition"/>
</element>
|
Table 87. Element: Notations
|
Documentation |
No documentation available. | ||||||||
|
Content Model |
%Signature; %Vocabularies; ? , ( %Pattern; )* | ||||||||
|
Attributes |
| ||||||||
|
Source |
<element name="Notations" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<optional>
<attribute name="aid">
<data type="string"/>
</attribute>
</optional>
<optional>
<ref name="Signature"/>
<ref name="Vocabularies"/>
</optional>
<zeroOrMore>
<ref name="Pattern"/>
</zeroOrMore>
</element>
|
Table 88. Element: Now
|
Documentation |
No documentation available. | ||||||||||||||||||||
|
Content Model | |||||||||||||||||||||
|
Attributes |
| ||||||||||||||||||||
|
Source |
<element name="Now" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<optional>
<attribute name="nr">
<data type="integer"/>
</attribute>
</optional>
<optional>
<attribute name="vid">
<data type="integer"/>
</attribute>
</optional>
<ref name="Position"/>
<ref name="Reasoning"/>
<ref name="BlockThesis"/>
</element>
|
Table 89. Element: Num
|
Documentation |
No documentation available. | ||||||||
|
Content Model |
| ||||||||
|
Attributes |
| ||||||||
|
Source |
<element name="Num" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="nr">
<data type="integer"/>
</attribute>
</element>
|
Table 90. Element: Pair
|
Documentation |
No documentation available. | ||||||||||||
|
Content Model |
| ||||||||||||
|
Attributes |
| ||||||||||||
|
Source |
<element name="Pair" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="x">
<data type="integer"/>
</attribute>
<attribute name="y">
<data type="integer"/>
</attribute>
</element>
|
Table 91. Element: PartialDef
|
Documentation |
No documentation available. |
|
Content Model | |
|
Source |
<element name="PartialDef" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<choice>
<ref name="Formula"/>
<ref name="Term"/>
</choice>
<ref name="Formula"/>
</element>
|
Table 92. Element: Pattern
|
Documentation |
No documentation available. | ||||||||||||||||||||||||||||||||||||||||
|
Content Model |
( | %Format; ) %ArgTypes;, Visible, Expansion ? | ||||||||||||||||||||||||||||||||||||||||
|
Attributes |
| ||||||||||||||||||||||||||||||||||||||||
|
Source |
<element name="Pattern" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="kind">
<choice>
<value>M</value>
<value>L</value>
<value>V</value>
<value>R</value>
<value>K</value>
<value>U</value>
<value>G</value>
<value>J</value>
</choice>
</attribute>
<optional>
<attribute name="nr">
<data type="integer"/>
</attribute>
<attribute name="aid">
<data type="string"/>
</attribute>
</optional>
<choice>
<attribute name="formatnr">
<data type="integer"/>
</attribute>
<ref name="Format"/>
</choice>
<attribute name="constrkind">
<choice>
<value>M</value>
<value>L</value>
<value>V</value>
<value>R</value>
<value>K</value>
<value>U</value>
<value>G</value>
<value>J</value>
</choice>
</attribute>
<attribute name="constrnr">
<data type="integer"/>
</attribute>
<optional>
<attribute name="antonymic">
<data type="boolean"/>
</attribute>
</optional>
<optional>
<attribute name="relnr">
<data type="integer"/>
</attribute>
</optional>
<optional>
<attribute name="redefnr">
<data type="integer"/>
</attribute>
</optional>
<ref name="ArgTypes"/>
<element name="Visible">
<zeroOrMore>
<ref name="Int"/>
</zeroOrMore>
</element>
<optional>
<element name="Expansion">
<ref name="Typ"/>
</element>
</optional>
</element>
|
Table 93. Element: PerCases
|
Documentation |
No documentation available. |
|
Content Model | |
|
Source |
<element name="PerCases" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<ref name="Proposition"/>
<ref name="Inference"/>
</element>
|
Table 94. Element: PerCasesReasoning
|
Documentation |
No documentation available. | ||||||||||||
|
Content Model |
( ( %BlockThesis; ( ( %CaseBlock; )+ | ( %SupposeBlock; )+ ) %PerCases; %Thesis; %EndPosition; ) | ( ( ( %CaseBlock; )+ | ( %SupposeBlock; )+ ) %PerCases; %EndPosition; %BlockThesis; ) ) | ||||||||||||
|
Attributes |
| ||||||||||||
|
Source |
<element name="PerCasesReasoning" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<ref name="Position"/>
<choice>
<group>
<ref name="BlockThesis"/>
<choice>
<oneOrMore>
<ref name="CaseBlock"/>
</oneOrMore>
<oneOrMore>
<ref name="SupposeBlock"/>
</oneOrMore>
</choice>
<ref name="PerCases"/>
<ref name="Thesis"/>
<ref name="EndPosition"/>
</group>
<group>
<choice>
<oneOrMore>
<ref name="CaseBlock"/>
</oneOrMore>
<oneOrMore>
<ref name="SupposeBlock"/>
</oneOrMore>
</choice>
<ref name="PerCases"/>
<ref name="EndPosition"/>
<ref name="BlockThesis"/>
</group>
</choice>
</element>
|
Table 95. Element: PolyEval
|
Documentation |
No documentation available. | ||||||||||||||||
|
Content Model | |||||||||||||||||
|
Attributes |
| ||||||||||||||||
|
Source |
<element name="PolyEval" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<ref name="Position"/>
<optional>
<attribute name="value">
<data type="boolean"/>
</attribute>
</optional>
<ref name="Requirement"/>
<oneOrMore>
<ref name="GeneralPolynomial"/>
</oneOrMore>
</element>
|
Table 96. Element: Polynomial
|
Documentation |
No documentation available. |
|
Content Model |
( %Monomial; )+ |
|
Source |
<element name="Polynomial" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<oneOrMore>
<ref name="Monomial"/>
</oneOrMore>
</element>
|
Table 97. Element: PoweredVar
|
Documentation |
No documentation available. | ||||||||||||
|
Content Model |
| ||||||||||||
|
Attributes |
| ||||||||||||
|
Source |
<element name="PoweredVar" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="nr">
<data type="integer"/>
</attribute>
<attribute name="exponent">
<data type="integer"/>
</attribute>
</element>
|
Table 98. Element: Pred
|
Documentation |
No documentation available. | ||||||||||||||||||||||||
|
Content Model |
( %Term; )* | ||||||||||||||||||||||||
|
Attributes |
| ||||||||||||||||||||||||
|
Source |
<element name="Pred" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="kind">
<choice>
<value>P</value>
<value>V</value>
<value>R</value>
</choice>
</attribute>
<attribute name="nr">
<data type="integer"/>
</attribute>
<optional>
<attribute name="absnr">
<data type="integer"/>
</attribute>
<attribute name="aid">
<data type="string"/>
</attribute>
</optional>
<optional>
<attribute name="pid">
<data type="integer"/>
</attribute>
</optional>
<zeroOrMore>
<ref name="Term"/>
</zeroOrMore>
</element>
|
Table 99. Element: PredInstance
|
Documentation |
No documentation available. | ||||||||||||||||||||||||
|
Content Model |
| ||||||||||||||||||||||||
|
Attributes |
| ||||||||||||||||||||||||
|
Source |
<element name="PredInstance" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="instnr">
<data type="integer"/>
</attribute>
<attribute name="kind">
<choice>
<value>P</value>
<value>S</value>
<value>V</value>
<value>R</value>
</choice>
</attribute>
<attribute name="nr">
<data type="integer"/>
</attribute>
<optional>
<attribute name="absnr">
<data type="integer"/>
</attribute>
<attribute name="aid">
<data type="string"/>
</attribute>
</optional>
</element>
|
Table 100. Element: Priority
|
Documentation |
No documentation available. | ||||||||||||||||
|
Content Model |
| ||||||||||||||||
|
Attributes |
| ||||||||||||||||
|
Source |
<element name="Priority" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="kind">
<choice>
<value>O</value>
<value>K</value>
<value>L</value>
</choice>
</attribute>
<attribute name="symbolnr">
<data type="integer"/>
</attribute>
<attribute name="value">
<data type="integer"/>
</attribute>
</element>
|
Table 101. Element: PrivFunc
|
Documentation |
No documentation available. | ||||||||
|
Content Model |
( %Term; )+ | ||||||||
|
Attributes |
| ||||||||
|
Source |
<element name="PrivFunc" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="nr">
<data type="integer"/>
</attribute>
<oneOrMore>
<ref name="Term"/>
</oneOrMore>
</element>
|
Table 102. Element: PrivPred
|
Documentation |
No documentation available. | ||||||||
|
Content Model | |||||||||
|
Attributes |
| ||||||||
|
Source |
<element name="PrivPred" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="nr">
<data type="integer"/>
</attribute>
<zeroOrMore>
<ref name="Term"/>
</zeroOrMore>
<ref name="Formula"/>
</element>
|
Table 103. Element: Projectivity
|
Documentation |
No documentation available. |
|
Content Model |
EMPTY |
|
Source |
<element name="Projectivity" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<empty/>
</element>
|
Table 104. Element: Proof
|
Documentation |
No documentation available. | ||||||||||||||||||||
|
Content Model | |||||||||||||||||||||
|
Attributes |
| ||||||||||||||||||||
|
Source |
<element name="Proof" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<optional>
<attribute name="nr">
<data type="integer"/>
</attribute>
</optional>
<optional>
<attribute name="vid">
<data type="integer"/>
</attribute>
</optional>
<ref name="Position"/>
<ref name="BlockThesis"/>
<ref name="Reasoning"/>
</element>
|
Table 105. Element: Properties
|
Documentation |
No documentation available. | ||||||||||||
|
Content Model |
( %Property; )+ | ||||||||||||
|
Attributes |
| ||||||||||||
|
Source |
<element name="Properties" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="propertyarg1">
<data type="integer"/>
</attribute>
<attribute name="propertyarg2">
<data type="integer"/>
</attribute>
<oneOrMore>
<ref name="Property"/>
</oneOrMore>
</element>
|
Table 106. Element: Proposition
|
Documentation |
No documentation available. | ||||||||||||||||||||
|
Content Model | |||||||||||||||||||||
|
Attributes |
| ||||||||||||||||||||
|
Source |
<element name="Proposition" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<ref name="Position"/>
<optional>
<attribute name="nr">
<data type="integer"/>
</attribute>
</optional>
<optional>
<attribute name="vid">
<data type="integer"/>
</attribute>
</optional>
<ref name="Formula"/>
</element>
|
Table 108. Element: RCluster
|
Documentation |
No documentation available. | ||||||||||||
|
Content Model |
( %ErrorCluster; | ( %ArgTypes;, %Typ;, %Cluster;, %Cluster; ? ) ) | ||||||||||||
|
Attributes |
| ||||||||||||
|
Source |
<element name="RCluster" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<optional>
<attribute name="nr">
<data type="integer"/>
</attribute>
<attribute name="aid">
<data type="string"/>
</attribute>
</optional>
<choice>
<ref name="ErrorCluster"/>
<group>
<ref name="ArgTypes"/>
<ref name="Typ"/>
<ref name="Cluster"/>
<optional>
<ref name="Cluster"/>
</optional>
</group>
</choice>
</element>
|
Table 109. Element: RationalNr
|
Documentation |
No documentation available. | ||||||||||||
|
Content Model |
| ||||||||||||
|
Attributes |
| ||||||||||||
|
Source |
<element name="RationalNr" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="numerator">
<data type="integer"/>
</attribute>
<attribute name="denominator">
<data type="integer"/>
</attribute>
</element>
|
Table 110. Element: Reconsider
|
Documentation |
No documentation available. | ||||||||
|
Content Model | |||||||||
|
Attributes |
| ||||||||
|
Source |
<element name="Reconsider" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<optional>
<attribute name="nr">
<data type="integer"/>
</attribute>
</optional>
<oneOrMore>
<ref name="Typ"/>
<ref name="Term"/>
</oneOrMore>
<ref name="Proposition"/>
<ref name="Justification"/>
</element>
|
Table 111. Element: Ref
|
Documentation |
No documentation available. | ||||||||||||||||||||||||||||
|
Content Model |
| ||||||||||||||||||||||||||||
|
Attributes |
| ||||||||||||||||||||||||||||
|
Source |
<element name="Ref" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="nr">
<data type="integer"/>
</attribute>
<optional>
<attribute name="vid">
<data type="integer"/>
</attribute>
</optional>
<optional>
<attribute name="articlenr">
<data type="integer"/>
</attribute>
<attribute name="kind">
<choice>
<value>T</value>
<value>D</value>
</choice>
</attribute>
</optional>
<ref name="Position"/>
</element>
|
Table 112. Element: Reflexivity
|
Documentation |
No documentation available. |
|
Content Model |
EMPTY |
|
Source |
<element name="Reflexivity" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<empty/>
</element>
|
Table 113. Element: Registration
|
Documentation |
No documentation available. |
|
Content Model |
( %RCluster; | %FCluster; | %CCluster; ) ( %CorrectnessCondition; )* , %Correctness; ? |
|
Source |
<element name="Registration" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<choice>
<ref name="RCluster"/>
<ref name="FCluster"/>
<ref name="CCluster"/>
</choice>
<zeroOrMore>
<ref name="CorrectnessCondition"/>
</zeroOrMore>
<optional>
<ref name="Correctness"/>
</optional>
</element>
|
Table 114. Element: RegistrationBlock
|
Documentation |
No documentation available. | ||||||||||||
|
Content Model |
( ( %Let; | %AuxiliaryItem; | %Registration; | %IdentifyRegistration; | %Canceled; ) )+ %EndPosition; | ||||||||||||
|
Attributes |
| ||||||||||||
|
Source |
<element name="RegistrationBlock" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<ref name="Position"/>
<oneOrMore>
<choice>
<ref name="Let"/>
<ref name="AuxiliaryItem"/>
<ref name="Registration"/>
<ref name="IdentifyRegistration"/>
<ref name="Canceled"/>
</choice>
</oneOrMore>
<ref name="EndPosition"/>
</element>
|
Table 115. Element: Registrations
|
Documentation |
No documentation available. | ||||||||
|
Content Model |
%Signature; ? , ( ( %RCluster; | %CCluster; | %FCluster; ) )* | ||||||||
|
Attributes |
| ||||||||
|
Source |
<element name="Registrations" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<optional>
<attribute name="aid">
<data type="string"/>
</attribute>
</optional>
<optional>
<ref name="Signature"/>
</optional>
<zeroOrMore>
<choice>
<ref name="RCluster"/>
<ref name="CCluster"/>
<ref name="FCluster"/>
</choice>
</zeroOrMore>
</element>
|
Table 116. Element: Requirement
|
Documentation |
No documentation available. | ||||||||||||||||||||||||||||
|
Content Model |
| ||||||||||||||||||||||||||||
|
Attributes |
| ||||||||||||||||||||||||||||
|
Source |
<element name="Requirement" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="constrkind">
<choice>
<value>M</value>
<value>L</value>
<value>V</value>
<value>R</value>
<value>K</value>
<value>U</value>
<value>G</value>
</choice>
</attribute>
<attribute name="constrnr">
<data type="integer"/>
</attribute>
<attribute name="nr">
<data type="integer"/>
</attribute>
<optional>
<attribute name="reqname">
<data type="string"/>
</attribute>
</optional>
<optional>
<attribute name="absnr">
<data type="integer"/>
</attribute>
<attribute name="aid">
<data type="string"/>
</attribute>
</optional>
</element>
|
Table 117. Element: Requirements
|
Documentation |
No documentation available. |
|
Content Model |
%Signature;, ( %Requirement; )* |
|
Source |
<element name="Requirements" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<ref name="Signature"/>
<zeroOrMore>
<ref name="Requirement"/>
</zeroOrMore>
</element>
|
Table 118. Element: Reservation
|
Documentation |
No documentation available. |
|
Content Model | |
|
Source |
<element name="Reservation" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<oneOrMore>
<element name="Ident">
<attribute name="vid">
<data type="integer"/>
</attribute>
</element>
</oneOrMore>
<ref name="Typ"/>
</element>
|
Table 119. Element: Scheme
|
Documentation |
No documentation available. | ||||||||||||||||
|
Content Model |
%ArgTypes;, %Formula;, ( %Formula; )* | ||||||||||||||||
|
Attributes |
| ||||||||||||||||
|
Source |
<element name="Scheme" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<optional>
<attribute name="articlenr">
<data type="integer"/>
</attribute>
<attribute name="nr">
<data type="integer"/>
</attribute>
</optional>
<optional>
<attribute name="aid">
<data type="string"/>
</attribute>
</optional>
<ref name="ArgTypes"/>
<ref name="Formula"/>
<zeroOrMore>
<ref name="Formula"/>
</zeroOrMore>
</element>
|
Table 120. Element: SchemeBlock
|
Documentation |
No documentation available. | ||||||||||||||||||||
|
Content Model |
( ( %SchemeFuncDecl; | %SchemePredDecl; ) )* , SchemePremises %Proposition; %Justification; %EndPosition; | ||||||||||||||||||||
|
Attributes |
| ||||||||||||||||||||
|
Source |
<element name="SchemeBlock" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="schemenr">
<data type="integer"/>
</attribute>
<optional>
<attribute name="vid">
<data type="integer"/>
</attribute>
</optional>
<ref name="Position"/>
<zeroOrMore>
<choice>
<ref name="SchemeFuncDecl"/>
<ref name="SchemePredDecl"/>
</choice>
</zeroOrMore>
<element name="SchemePremises">
<zeroOrMore>
<ref name="Proposition"/>
</zeroOrMore>
</element>
<ref name="Proposition"/>
<ref name="Justification"/>
<ref name="EndPosition"/>
</element>
|
Table 121. Element: SchemeFuncDecl
|
Documentation |
No documentation available. | ||||||||||||
|
Content Model | |||||||||||||
|
Attributes |
| ||||||||||||
|
Source |
<element name="SchemeFuncDecl" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="nr">
<data type="integer"/>
</attribute>
<optional>
<attribute name="vid">
<data type="integer"/>
</attribute>
</optional>
<ref name="ArgTypes"/>
<ref name="Typ"/>
</element>
|
Table 122. Element: SchemeInstantiation
|
Documentation |
No documentation available. | ||||||||||||
|
Content Model |
( FuncInstance )* , ( PredInstance )* | ||||||||||||
|
Attributes |
| ||||||||||||
|
Source |
<element name="SchemeInstantiation" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<ref name="Position"/>
<zeroOrMore>
<element name="FuncInstance">
<attribute name="instnr">
<data type="integer"/>
</attribute>
<choice>
<group>
<attribute name="kind">
<choice>
<value>F</value>
<value>H</value>
<value>G</value>
<value>K</value>
<value>U</value>
</choice>
</attribute>
<attribute name="nr">
<data type="integer"/>
</attribute>
<optional>
<attribute name="absnr">
<data type="integer"/>
</attribute>
<attribute name="aid">
<data type="string"/>
</attribute>
</optional>
</group>
<ref name="Term"/>
</choice>
</element>
</zeroOrMore>
<zeroOrMore>
<element name="PredInstance">
<attribute name="instnr">
<data type="integer"/>
</attribute>
<attribute name="kind">
<choice>
<value>P</value>
<value>S</value>
<value>V</value>
<value>R</value>
</choice>
</attribute>
<attribute name="nr">
<data type="integer"/>
</attribute>
<optional>
<attribute name="absnr">
<data type="integer"/>
</attribute>
<attribute name="aid">
<data type="string"/>
</attribute>
</optional>
</element>
</zeroOrMore>
</element>
|
Table 123. Element: SchemePredDecl
|
Documentation |
No documentation available. | ||||||||||||
|
Content Model | |||||||||||||
|
Attributes |
| ||||||||||||
|
Source |
<element name="SchemePredDecl" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="nr">
<data type="integer"/>
</attribute>
<optional>
<attribute name="vid">
<data type="integer"/>
</attribute>
</optional>
<ref name="ArgTypes"/>
</element>
|
Table 124. Element: SchemePremises
|
Documentation |
No documentation available. |
|
Content Model |
( %Proposition; )* |
|
Source |
<element name="SchemePremises" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<zeroOrMore>
<ref name="Proposition"/>
</zeroOrMore>
</element>
|
Table 125. Element: Schemes
|
Documentation |
No documentation available. | ||||||||
|
Content Model |
%Signature; ? , ( %Scheme; )* | ||||||||
|
Attributes |
| ||||||||
|
Source |
<element name="Schemes" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<optional>
<attribute name="aid">
<data type="string"/>
</attribute>
</optional>
<optional>
<ref name="Signature"/>
</optional>
<zeroOrMore>
<ref name="Scheme"/>
</zeroOrMore>
</element>
|
Table 126. Element: Section
|
Documentation |
No documentation available. |
|
Content Model |
EMPTY |
|
Source |
<element name="Section" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<empty/>
</element>
|
Table 127. Element: Set
|
Documentation |
No documentation available. | ||||||||
|
Content Model | |||||||||
|
Attributes |
| ||||||||
|
Source |
<element name="Set" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<optional>
<attribute name="nr">
<data type="integer"/>
</attribute>
</optional>
<ref name="Term"/>
<ref name="Typ"/>
</element>
|
Table 128. Element: Signature
|
Documentation |
No documentation available. |
|
Content Model |
( %ArticleID; )* |
|
Source |
<element name="Signature" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<zeroOrMore>
<ref name="ArticleID"/>
</zeroOrMore>
</element>
|
Table 129. Element: SignatureWithCounts
|
Documentation |
No documentation available. |
|
Content Model |
( %ConstrCounts; )* |
|
Source |
<element name="SignatureWithCounts" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<zeroOrMore>
<ref name="ConstrCounts"/>
</zeroOrMore>
</element>
|
Table 130. Element: SkippedProof
|
Documentation |
No documentation available. |
|
Content Model |
EMPTY |
|
Source |
<element name="SkippedProof" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<empty/>
</element>
|
Table 131. Element: StructLoci
|
Documentation |
No documentation available. |
|
Content Model |
( %Pair; )* |
|
Source |
<element name="StructLoci" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<zeroOrMore>
<ref name="Pair"/>
</zeroOrMore>
</element>
|
Table 132. Element: Suppose
|
Documentation |
No documentation available. |
|
Content Model |
( %Proposition; )+ |
|
Source |
<element name="Suppose" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<oneOrMore>
<ref name="Proposition"/>
</oneOrMore>
</element>
|
Table 133. Element: SupposeBlock
|
Documentation |
No documentation available. | ||||||||||||
|
Content Model |
( ( %BlockThesis; %Suppose; %Thesis; %Reasoning; ) | ( %Suppose; %Reasoning; %BlockThesis; ) ) | ||||||||||||
|
Attributes |
| ||||||||||||
|
Source |
<element name="SupposeBlock" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<ref name="Position"/>
<choice>
<group>
<ref name="BlockThesis"/>
<ref name="Suppose"/>
<ref name="Thesis"/>
<ref name="Reasoning"/>
</group>
<group>
<ref name="Suppose"/>
<ref name="Reasoning"/>
<ref name="BlockThesis"/>
</group>
</choice>
</element>
|
Table 134. Element: Symbol
|
Documentation |
No documentation available. | ||||||||||||||||
|
Content Model |
| ||||||||||||||||
|
Attributes |
| ||||||||||||||||
|
Source |
<element name="Symbol" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="kind">
<data type="string"/>
</attribute>
<attribute name="nr">
<data type="integer"/>
</attribute>
<attribute name="name">
<data type="integer"/>
</attribute>
</element>
|
Table 135. Element: SymbolCount
|
Documentation |
No documentation available. | ||||||||||||
|
Content Model |
| ||||||||||||
|
Attributes |
| ||||||||||||
|
Source |
<element name="SymbolCount" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="kind">
<choice>
<value>G</value>
<value>K</value>
<value>L</value>
<value>M</value>
<value>O</value>
<value>R</value>
<value>U</value>
<value>V</value>
</choice>
</attribute>
<attribute name="nr">
<data type="integer"/>
</attribute>
</element>
|
Table 136. Element: Symbols
|
Documentation |
No documentation available. |
|
Content Model |
( Symbol )* |
|
Source |
<element name="Symbols" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<zeroOrMore>
<element name="Symbol">
<attribute name="kind">
<data type="string"/>
</attribute>
<attribute name="nr">
<data type="integer"/>
</attribute>
<attribute name="name">
<data type="integer"/>
</attribute>
</element>
</zeroOrMore>
</element>
|
Table 137. Element: Symmetry
|
Documentation |
No documentation available. |
|
Content Model |
EMPTY |
|
Source |
<element name="Symmetry" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<empty/>
</element>
|
Table 138. Element: Take
|
Documentation |
No documentation available. |
|
Content Model | |
|
Source |
<element name="Take" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<ref name="Term"/>
</element>
|
Table 139. Element: TakeAsVar
|
Documentation |
No documentation available. | ||||||||
|
Content Model | |||||||||
|
Attributes |
| ||||||||
|
Source |
<element name="TakeAsVar" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<optional>
<attribute name="nr">
<data type="integer"/>
</attribute>
</optional>
<ref name="Typ"/>
<ref name="Term"/>
</element>
|
Table 140. Element: Theorem
|
Documentation |
No documentation available. | ||||||||||||||||||||||||||||
|
Content Model | |||||||||||||||||||||||||||||
|
Attributes |
| ||||||||||||||||||||||||||||
|
Source |
<element name="Theorem" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<optional>
<attribute name="articlenr">
<data type="integer"/>
</attribute>
<attribute name="nr">
<data type="integer"/>
</attribute>
</optional>
<optional>
<attribute name="constrkind">
<choice>
<value>M</value>
<value>V</value>
<value>R</value>
<value>K</value>
</choice>
</attribute>
<attribute name="constrnr">
<data type="integer"/>
</attribute>
</optional>
<optional>
<attribute name="aid">
<data type="string"/>
</attribute>
</optional>
<attribute name="kind">
<choice>
<value>T</value>
<value>D</value>
</choice>
</attribute>
<ref name="Formula"/>
</element>
|
Table 141. Element: Theorems
|
Documentation |
No documentation available. | ||||||||
|
Content Model |
%Signature; ? , ( Theorem )* | ||||||||
|
Attributes |
| ||||||||
|
Source |
<element name="Theorems" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<optional>
<attribute name="aid">
<data type="string"/>
</attribute>
</optional>
<optional>
<ref name="Signature"/>
</optional>
<zeroOrMore>
<element name="Theorem">
<optional>
<attribute name="articlenr">
<data type="integer"/>
</attribute>
<attribute name="nr">
<data type="integer"/>
</attribute>
</optional>
<optional>
<attribute name="constrkind">
<choice>
<value>M</value>
<value>V</value>
<value>R</value>
<value>K</value>
</choice>
</attribute>
<attribute name="constrnr">
<data type="integer"/>
</attribute>
</optional>
<optional>
<attribute name="aid">
<data type="string"/>
</attribute>
</optional>
<attribute name="kind">
<choice>
<value>T</value>
<value>D</value>
</choice>
</attribute>
<ref name="Formula"/>
</element>
</zeroOrMore>
</element>
|
Table 142. Element: Thesis
|
Documentation |
No documentation available. |
|
Content Model | |
|
Source |
<element name="Thesis" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<ref name="Formula"/>
<ref name="ThesisExpansions"/>
</element>
|
Table 143. Element: ThesisExpansions
|
Documentation |
No documentation available. |
|
Content Model |
( %Pair; )* |
|
Source |
<element name="ThesisExpansions" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<zeroOrMore>
<ref name="Pair"/>
</zeroOrMore>
</element>
|
Table 144. Element: Transitivity
|
Documentation |
No documentation available. |
|
Content Model |
EMPTY |
|
Source |
<element name="Transitivity" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<empty/>
</element>
|
Table 145. Element: Typ
|
Documentation |
No documentation available. | ||||||||||||||||||||||||||||
|
Content Model | |||||||||||||||||||||||||||||
|
Attributes |
| ||||||||||||||||||||||||||||
|
Source |
<element name="Typ" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="kind">
<choice>
<value>M</value>
<value>G</value>
<value>L</value>
<value>errortyp</value>
</choice>
</attribute>
<optional>
<attribute name="nr">
<data type="integer"/>
</attribute>
</optional>
<optional>
<attribute name="absnr">
<data type="integer"/>
</attribute>
<attribute name="aid">
<data type="string"/>
</attribute>
</optional>
<optional>
<attribute name="pid">
<data type="integer"/>
</attribute>
</optional>
<optional>
<attribute name="vid">
<data type="integer"/>
</attribute>
</optional>
<zeroOrMore>
<ref name="Cluster"/>
</zeroOrMore>
<zeroOrMore>
<ref name="Term"/>
</zeroOrMore>
</element>
|
Table 146. Element: UnexpectedProp
|
Documentation |
No documentation available. |
|
Content Model |
EMPTY |
|
Source |
<element name="UnexpectedProp" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<empty/>
</element>
|
Table 147. Element: Uniqueness
|
Documentation |
No documentation available. |
|
Content Model |
( %Formula; | ( %Proposition; %Justification; ) ) |
|
Source |
<element name="Uniqueness" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<choice>
<ref name="Formula"/>
<group>
<ref name="Proposition"/>
<ref name="Justification"/>
</group>
</choice>
</element>
|
Table 148. Element: UnknownCorrCond
|
Documentation |
No documentation available. |
|
Content Model |
( %Formula; | ( %Proposition; %Justification; ) ) |
|
Source |
<element name="UnknownCorrCond" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<choice>
<ref name="Formula"/>
<group>
<ref name="Proposition"/>
<ref name="Justification"/>
</group>
</choice>
</element>
|
Table 149. Element: Var
|
Documentation |
No documentation available. | ||||||||
|
Content Model |
| ||||||||
|
Attributes |
| ||||||||
|
Source |
<element name="Var" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<attribute name="nr">
<data type="integer"/>
</attribute>
</element>
|
Table 150. Element: Verum
|
Documentation |
No documentation available. |
|
Content Model |
EMPTY |
|
Source |
<element name="Verum" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<empty/>
</element>
|
Table 151. Element: Visible
|
Documentation |
No documentation available. |
|
Content Model |
( %Int; )* |
|
Source |
<element name="Visible" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<zeroOrMore>
<ref name="Int"/>
</zeroOrMore>
</element>
|
Table 152. Element: Vocabularies
|
Documentation |
No documentation available. |
|
Content Model |
( Vocabulary )* |
|
Source |
<element name="Vocabularies" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<zeroOrMore>
<element name="Vocabulary">
<ref name="ArticleID"/>
<zeroOrMore>
<element name="SymbolCount">
<attribute name="kind">
<choice>
<value>G</value>
<value>K</value>
<value>L</value>
<value>M</value>
<value>O</value>
<value>R</value>
<value>U</value>
<value>V</value>
</choice>
</attribute>
<attribute name="nr">
<data type="integer"/>
</attribute>
</element>
</zeroOrMore>
</element>
</zeroOrMore>
</element>
|
Table 153. Element: Vocabulary
|
Documentation |
No documentation available. |
|
Content Model |
%ArticleID;, ( SymbolCount )* |
|
Source |
<element name="Vocabulary" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0">
<ref name="ArticleID"/>
<zeroOrMore>
<element name="SymbolCount">
<attribute name="kind">
<choice>
<value>G</value>
<value>K</value>
<value>L</value>
<value>M</value>
<value>O</value>
<value>R</value>
<value>U</value>
<value>V</value>
</choice>
</attribute>
<attribute name="nr">
<data type="integer"/>
</attribute>
</element>
</zeroOrMore>
</element>
|
Table 154. Pattern: Adjective
|
Namespace | |
|
Documentation |
Adjective is a possibly negated (and paramaterized) attribute Optionally the article id (aid) and order in article (absnr) can be given. If available, presentational info (number of the Pattern) is given in pid. The heuristic for for displaying clusters is that attributes without pid have been added automatically by cluster mechanisms. The attribute kind (kind) 'V' can be added explicitly. |
|
Content Model |
Table 155. Pattern: And
|
Namespace | |
|
Documentation |
Conjunctive formula. If available, presentational info is given in pid. |
|
Content Model |
Table 156. Pattern: ArgTypes
|
Namespace | |
|
Documentation |
Argument types of constructors, patterns, clusters, etc. |
|
Content Model |
Table 157. Pattern: Article
|
Namespace | |
|
Documentation |
The complete article after analyzer. aid specifies its name in uppercase, and mizfiles optionally gives a location of the local MIZFILES directory used during processing the article (needed to know for browsing of locally installed html in MIZFILES/html). |
|
Content Model |
Table 158. Pattern: ArticleID
|
Namespace | |
|
Documentation |
This is now only the unique name of an article. |
|
Content Model |
Table 159. Pattern: Assume
|
Namespace | |
|
Documentation |
One assumption may consist of several propositions. |
|
Content Model |
Table 160. Pattern: AuxiliaryItem
|
Namespace | |
|
Documentation |
Auxiliary items are items which do not change thesis. |
|
Content Model |
( %JustifiedProposition; | %Consider; | %Set; | %Reconsider; | %DefFunc; | %DefPred; ) |
Table 161. Pattern: BlockThesis
|
Namespace | |
|
Documentation |
The block thesis is printed for proofs in the beginning and for diffuse reasoning in the end. For diffuse reasoning, the series of temporary subthesis corresponding to all skeleton items is printed before the main theses (in the same order as the skeleton items in the block). |
|
Content Model |
Table 163. Pattern: ByExplanations
|
Namespace | |
|
Documentation |
Reports from the Mizar checker, now only arithmetical evaluations. They are now only available when the verifier is compiled with a special directive - this should be changed to a user option eventually. |
|
Content Model |
Table 164. Pattern: CCluster
|
Namespace | |
|
Documentation |
Conditional cluster. This says that Typ with the first cluster has also the second (optionally followed by its extended version created by rounding up in current environment). Optionally the article id (aid) and order in article (nr) can be given. |
|
Content Model |
Table 165. Pattern: Canceled
|
Namespace | |
|
Documentation |
Canceled theorem ( if on top-level), definition or registration (if inside such blocks). We should add to this the number of canceled items as an attribute. |
|
Content Model |
Table 167. Pattern: CaseBlock
|
Namespace | |
|
Documentation |
Block starting with one case, the direct and diffuse version (this depends on the kind of its parent block). The block thesis is printed for proofs in the beginning and for diffuse reasoning in the end. |
|
Content Model |
Table 168. Pattern: Choice
|
Namespace | |
|
Documentation |
Choice term is defined by the type of its argument, |
|
Content Model |
Table 172. Pattern: ComplexNr
|
Namespace | |
|
Documentation |
Complex rational numbers used in Mizar |
|
Content Model |
Table 173. Pattern: Conclusion
|
Namespace | |
|
Documentation |
Justified conclusion. In text, this can appear as _hence_, _thus_ or _hereby_ (which starts diffuse conclusion). |
|
Content Model |
Table 174. Pattern: Consider
|
Namespace | |
|
Documentation |
First comes the reconstructed existential statement and its justification, then the new local constants and zero or more propositions about them. For easier presentation, nr optionally contains the number of the first local constant created here. Each type may optionally have presentational info about the variable (vid) inside. |
|
Content Model |
Table 176. Pattern: Const
|
Namespace | |
|
Documentation |
Normal local constant introduced e.g. by Let or Consider presentational info may be given in vid. |
|
Content Model |
Table 177. Pattern: ConstrCounts
|
Namespace | |
|
Documentation |
Constructor counts are used probably for renumerating. The article named can be given if not implicit. This implementation might change in some time. |
|
Content Model |
Table 178. Pattern: ConstrDef
|
Namespace | |
|
Documentation |
ConstrDef holds a term together with types of its variables and the top-level functor. Used now mainly for identify. |
|
Content Model |
Table 179. Pattern: Constructor
|
Namespace | |
|
Documentation |
Constructors are functors, predicates, attributes, etc. nr, kind and aid (article id) determine the constructor absolutely in MML, relnr optionally gives its serial number in environment for a particular article (it is not in prels). All have (possibly empty) properties, argtypes and some have one or more mother types. The optional final Fields are selectors for agrregates and structmodes. aggregbase is for aggregates (maybe OVER-arguments), structmodeaggrnr is for structmodes (nr of corresponding aggregate). absredefnr and redefaid optionally give absolute address of a redefinition. |
|
Content Model |
Table 180. Pattern: Constructors
|
Namespace | |
|
Documentation |
Constructors, either imported from other articles ( after accommodation) - the signature is implicit in that case, or exported from the current article - then the signature has to be specified. aid optionally specifies its article's name in uppercase. |
|
Content Model |
Table 181. Pattern: Correctness
|
Namespace | |
|
Documentation |
This is a way how to state all correctness conditions in one keyword. The relevant conditions are computed by the analyzer and printed here, their conjunction has to be justified. |
|
Content Model |
Table 182. Pattern: CorrectnessCondition
|
Namespace | |
|
Documentation |
The possible correctness conditions are following. They can either be only stated in the Correctness, which conjugates them and proves them all, or come separately as a proposition with a justification. |
|
Content Model |
( %UnknownCorrCond; | %Coherence; | %Compatibility; | %Consistency; | %Existence; | %Uniqueness; ) |
Table 183. Pattern: DefFunc
|
Namespace | |
|
Documentation |
Private functor. First come the types of arguments, then its definition and the result type. For easier presentation, nr optionally contains number of the private functor created here, and its identifier's number (vid). |
|
Content Model |
Table 184. Pattern: DefMeaning
|
Namespace | |
|
Documentation |
DefMeaning consists of the formulas and terms defining a constructor. It can be either defined by _equals_ (terms) or by _means_ (formulas). It may contain several partial (case) definitions - first in them comes the definition (term or formula) valid in that case and second comes the case formula. The final term or formula specifies the default case, it is mandatory if no partial definitions are given. If no default is given, the disjunction of all case formulas must be true (this have to be proved using the _consistency_ condition). |
|
Content Model |
Table 185. Pattern: DefPred
|
Namespace | |
|
Documentation |
Private predicate. First come the types of arguments, then its definition. For easier presentation, nr optionally contains number of the private predicate created here, and its identifier's number (vid). |
|
Content Model |
Table 186. Pattern: DefTheorem
|
Namespace | |
|
Documentation |
Theorems created from definitions are now printed as separate top-level items after definitional blocks, constrkind and constrnr determine the defined constructor. If they do not appear, this is a canceled (verum) deftheorem. |
|
Content Model |
Table 187. Pattern: Definiens
|
Namespace | |
|
Documentation |
Definiens of a constructor. This overlaps a bit with Constructor. defnr is the number of the corresponding definitional theorem, and vid optionally its label's identifier. First come the argument types and possibly also the result type. The optional formula is conjunction of all assumptions if any given. If this is a redefinition, essentials are indeces of arguments corresponding to the arguments of original, otherwise it is just identity. This could be now encode with just one number like the superfluous does for Constructor. Optionally the article id (aid) and order in article (nr) can be given. relnr optionally gives its serial number in environment for a particular article (it is not in prels). vid gives a number of the label identifier if present. |
|
Content Model |
Table 188. Pattern: Definientia
|
Namespace | |
|
Documentation |
Definientia, either imported from other articles ( after accommodation) - the signature is implicit in that case, or exported from the current article - then the signature has to be specified. aid optionally specifies article's name in uppercase. |
|
Content Model |
Table 189. Pattern: Definition
|
Namespace | |
|
Documentation |
Definition of a functor, predicate, mode, attribute or structure. with optional label, properties and correctness conditions. Sometimes no constructor is created (e.g. for expandable modes). The second optional form creating three or more constructors is for structure definitions, which define the aggregate functor, the structure mode, the strict attribute and zero or more selectors, and create existential registration for the strict attribute. If any definientia and definitional theorems are created, they follow immediately after the enclosing definitional block (this might be changed in the future). Number, position, and identifier number of the definiens (vid) can be optionally given. |
|
Content Model |
Table 190. Pattern: DefinitionBlock
|
Namespace | |
|
Documentation |
A block of one or more (possibly canceled) (re)definitions, possibly with assumptions. If any definientia and definitional theorems are created, they follow immediately after this block. |
|
Content Model |
Table 191. Pattern: EndPosition
|
Namespace | |
|
Documentation |
Ending position (e.g. of blocks). |
|
Content Model |
Table 192. Pattern: ErrorCluster
|
Namespace | |
|
Documentation |
This encodes error during cluster processing |
|
Content Model |
Table 193. Pattern: ErrorFrm
|
Namespace | |
|
Documentation |
Incorrect (erroneous formula) - e.g. containing undefined symbols |
|
Content Model |
Table 194. Pattern: ErrorIdentify
|
Namespace | |
|
Documentation |
This encodes error during identification processing |
|
Content Model |
Table 195. Pattern: ErrorTrm
|
Namespace | |
|
Documentation |
Incorrect (erroneous term) - e.g. containing undefined symbols |
|
Content Model |
Table 197. Pattern: FCluster
|
Namespace | |
|
Documentation |
Functor (term) cluster. This says that Term with ArgTypes has Cluster (optionally followed by its extended version created by rounding up in current environment), optionally with explicit Typ. Optionally the article id (aid) and order in article (nr) can be given. |
|
Content Model |
Table 198. Pattern: Fields
|
Namespace | |
|
Documentation |
Specify fields of aggregates and structmodes by their relative nr. Optionally the article id (aid) and order in article (absnr) can be given. The selector kind (kind) 'U' can can be added explicitly. |
|
Content Model |
Table 199. Pattern: For
|
Namespace | |
|
Documentation |
Universally quantified formula If available, presentational info is given in pid. If available, numbere of the variable identifier is given in vid. |
|
Content Model |
Table 200. Pattern: Format
|
Namespace | |
|
Documentation |
Format keeps the kind of a given symbol and arities. For bracket formats (K) this keeps both symbols. Optionally a nr (of the format) is kept, to which patterns may refer, This implementation might change in some time. |
|
Content Model |
Table 201. Pattern: Formats
|
Namespace | |
|
Documentation |
Format info contains symbol formats and priorities. Priorities are used only for functor symbols. This implementation might change in some time. |
|
Content Model |
Table 202. Pattern: Formula
|
Namespace | |
|
Documentation |
No documentation available. |
|
Content Model |
( %Not; | %And; | %For; | %Pred; | %PrivPred; | %Is; | %Verum; | %ErrorFrm; ) |
Table 203. Pattern: Fraenkel
|
Namespace | |
|
Documentation |
Fraenkel term is defined by the types of its lambda arguments, its lambda term and the separating formula. Each type may optionally have presentational info about the variable (vid) inside. |
|
Content Model |
Table 204. Pattern: FreeVar
|
Namespace | |
|
Documentation |
Free variable - used only internally in checker |
|
Content Model |
Table 205. Pattern: From
|
Namespace | |
|
Documentation |
From encodes one scheme justification, it cannot be linked. |
|
Content Model |
Table 206. Pattern: FromExplanations
|
Namespace | |
|
Documentation |
Reports from the Mizar schematizer - scheme instantioations. They are now only available when the verifier is compiled with a special directive - this should be changed to a user option eventually. |
|
Content Model |
Table 207. Pattern: Func
|
Namespace | |
|
Documentation |
Functor terms - schematic, aggregates, normal and selectors Optionally the article id (aid) and order in article (absnr) can be given. If available, presentational info (number of the Pattern) is given in pid. |
|
Content Model |
Table 208. Pattern: GeneralPolynomial
|
Namespace | |
|
Documentation |
No documentation available. |
|
Content Model |
( %Polynomial; | %Number; ) |
Table 209. Pattern: Given
|
Namespace | |
|
Documentation |
This is existential assumption, it may be used when the normal assumption starts with existential quantifier, and emulates the use of assume followed by consider. First comes the reconstructed assumed existential statement, then the newly introduced local constant(s), and finally the proposition(s) containing the new local constant(s). For easier presentation, nr optionally contains the number of the first local constant created here. Each type may optionally have presentational info about the variable (vid) inside. |
|
Content Model |
Table 210. Pattern: Identify
|
Namespace | |
|
Documentation |
Identification (unoriented, this is not used currently, see identifyWithExp instead). This says that two terms with the two constructors at the top are equal when the pairs of their arguments specified in EqArgs are equal. Optionally the article id (aid) and order in article (nr) can be given. |
|
Content Model |
Table 211. Pattern: IdentifyRegistration
|
Namespace | |
|
Documentation |
One justified identification registration. The correctness conditions could be made more specific. |
|
Content Model |
Table 212. Pattern: IdentifyRegistrations
|
Namespace | |
|
Documentation |
Identifications, either imported from other articles ( after accommodation) - the signature is implicit in that case, or exported from the current article - then the signature has to be specified. aid optionally specifies its article's name in uppercase. |
|
Content Model |
Table 213. Pattern: IdentifyWithExp
|
Namespace | |
|
Documentation |
Identification (oriented, currently used version). This says to identify anything matching the first term or formula pattern (with ConstrKind and ConstrNr as the top constructor) with the second pattern (instantiated by the matching). The type requirements for the matching (i.e. the loci) are given first. Note that this works only one way, if you want it also the other way, the symmetrical variant has to be explicitly stated as another identification. Optionally the article id (aid) and order in article (nr) can be given. |
|
Content Model |
Table 214. Pattern: InfConst
|
Namespace | |
|
Documentation |
Inference constant - used for internal term sharing |
|
Content Model |
Table 217. Pattern: Is
|
Namespace | |
|
Documentation |
Qualification formula (claims that a term has certaing type) |
|
Content Model |
Table 218. Pattern: It
|
Namespace | |
|
Documentation |
_It_ is a special term used in definitions. Probably no longer used on this level. |
|
Content Model |
Table 219. Pattern: IterEquality
|
Namespace | |
|
Documentation |
Iterative equality. The optional numbers (nr) is serial label numbering, and original label identifier (vid). |
|
Content Model |
Table 220. Pattern: IterStep
|
Namespace | |
|
Documentation |
This is one step in an iterative equation. |
|
Content Model |
Table 221. Pattern: Justification
|
Namespace | |
|
Documentation |
Direct justification. |
|
Content Model |
( %Inference; | %Proof; | %SkippedProof; ) |
Table 222. Pattern: JustifiedProperty
|
Namespace | |
|
Documentation |
A property of a constructor, the proposition expreesing it, and its justification. |
|
Content Model |
Table 223. Pattern: JustifiedProposition
|
Namespace | |
|
Documentation |
No documentation available. |
|
Content Model |
( %Now; | %IterEquality; | ( %Proposition; %Justification; ) ) |
Table 224. Pattern: JustifiedTheorem
|
Namespace | |
|
Documentation |
Theorem as a proposition with justification. |
|
Content Model |
Table 226. Pattern: Let
|
Namespace | |
|
Documentation |
Introduction of local constants, the numbering is automatic, so only types are needed. For easier presentation, nr optionally contains the number of the first local constant created here. Each type may optionally have presentational info about the variable (vid) inside. |
|
Content Model |
Table 227. Pattern: LocusVar
|
Namespace | |
|
Documentation |
Locus variable used usually for pattern matching. Their types are given elsewhere in data using them - see e.g. Constructor |
|
Content Model |
Table 228. Pattern: Monomial
|
Namespace | |
|
Documentation |
Monomial has a coefficient and a series of variables with their exponents. |
|
Content Model |
Table 229. Pattern: Not
|
Namespace | |
|
Documentation |
Negation. If available, presentational info is given in pid. |
|
Content Model |
Table 230. Pattern: NotationBlock
|
Namespace | |
|
Documentation |
Block of synonyms or antonyms. The patterns are semantically irrelevant and are not printed yet - fix this. |
|
Content Model |
Table 231. Pattern: Notations
|
Namespace | |
|
Documentation |
Notations, either imported from other articles ( after accommodation) - the signature is implicit in that case, or exported from the current article - then the signature and vocabularies have to be specified. aid optionally specifies article's name in uppercase. |
|
Content Model |
Table 232. Pattern: Now
|
Namespace | |
|
Documentation |
Diffuse statement - its thesis is reconstructed in the end. Label (nr) and its identifier (vid) of diffuse statement (if any) is label of its thesis. |
|
Content Model |
Table 234. Pattern: Number
|
Namespace | |
|
Documentation |
No documentation available. |
|
Content Model |
( %RationalNr; | %ComplexNr; ) |
Table 236. Pattern: Pattern
|
Namespace | |
|
Documentation |
Patterns map formats with argtypes to constructors. The format is either specified as a number (then it must be available in some table), or is given explicitely. Visible are indeces of visible (nonhidden) arguments. If antonymic, its constructor has to be negated. Mode patterns can have expansion instead of just a constructor - this might be done for other patterns too, or replaced by the _equals_ mechanism. The J (forgetful functor) patterns are actually an example of another expanded patterns, but the expansion is uniform for all of them, so it does not have to be given. The invalid ConstrKind J is now used for forgetful functors, this should be changed. Optionally the article id (aid) and order in article (nr) can be given. relnr optionally gives its serial number in environment for a particular article (it is not in prels). redefnr optonally gives the relative number of the original pattern to which the current is defined as synonym/antonym. |
|
Content Model |
Table 237. Pattern: PerCases
|
Namespace | |
|
Documentation |
This justifies the case split (the disjunction of all Suppose or Case items in direct subblocks) in PerCasesReasoning. The case split is only known after all subblocks are known, so this is the last item in its block, not like in the Mizar text. |
|
Content Model |
Table 238. Pattern: PerCasesReasoning
|
Namespace | |
|
Documentation |
Reasoning per cases. It only contains CaseBlock or SupposeBlock subblocks, with the exception of the mandatory last PerCases justifying the case split. Direct and diffuse versions are possible (this depends on the kind of its parent block). The block thesis is printed for proofs in the beginning and for diffuse reasoning in the end. |
|
Content Model |
Table 239. Pattern: PolyEval
|
Namespace | |
|
Documentation |
Builtin numerical evaluations of arithmetical functors and predicates. For predicates, the value can be false. Arguments are generally polynoms with complex coefficients. For functors, the last polynom is the result value. |
|
Content Model |
Table 240. Pattern: Polynomial
|
Namespace | |
|
Documentation |
Polynomial consists of several monomials. |
|
Content Model |
Table 241. Pattern: Position
|
Namespace | |||||||||||||
|
Documentation |
No documentation available. | ||||||||||||
| Attributes |
|
Table 242. Pattern: Pred
|
Namespace | |
|
Documentation |
Atomic predicate formulas - schematic, attributive and normal Optionally the article id (aid) and order in article (absnr) can be given. If available, presentational info (number of the Pattern) is given in pid. |
|
Content Model |
Table 243. Pattern: PrivFunc
|
Namespace | |
|
Documentation |
Private functor with arguments is a shorthand for another term. The first (mandatory) term is the expansion, arguments follow. |
|
Content Model |
Table 244. Pattern: PrivPred
|
Namespace | |
|
Documentation |
Private predicate with arguments is a shorthand for another formula |
|
Content Model |
Table 245. Pattern: Proof
|
Namespace | |
|
Documentation |
Direct proof of some proposition (which is the proof's thesis). Label (nr) of proof (if any) is label of its thesis, vid is then the identifier nr of this label. |
|
Content Model |
Table 246. Pattern: Properties
|
Namespace | |
|
Documentation |
Properties of constructors; if some given, the first and the second argument to which they apply must be specified. |
|
Content Model |
Table 247. Pattern: Property
|
Namespace | |
|
Documentation |
No documentation available. |
|
Content Model |
( UnexpectedProp | Symmetry | Reflexivity | Irreflexivity | Associativity | Transitivity | Commutativity | Connectedness | Antisymmetry | Idempotence | Involutiveness | Projectivity | Abstractness ) |
Table 248. Pattern: Proposition
|
Namespace | |
|
Documentation |
Proposition is a sentence with position and possible label (and its identifier). |
|
Content Model |
Table 249. Pattern: QuaTrm
|
Namespace | |
|
Documentation |
Qua terms capture the retyping term qua type construct, but they are probably no longer used on this level. |
|
Content Model |
Table 250. Pattern: RCluster
|
Namespace | |
|
Documentation |
Existential (registration) cluster. This says that exists Typ with Cluster (optionally followed by its extended version created by rounding up in current environment). Optionally the article id (aid) and order in article (nr) can be given. |
|
Content Model |
Table 252. Pattern: Reasoning
|
Namespace | |
|
Documentation |
Reasoning is a series of skeleton and auxiliary items, finished by optional per cases reasoning. |
|
Content Model |
( ( %SkeletonItem; | %AuxiliaryItem; ) )* , %PerCasesReasoning; ? %EndPosition; |
Table 253. Pattern: Reconsider
|
Namespace | |
|
Documentation |
First comes the series of target types and reconsidered terms. For all these terms a new local variable with its target type is created, and its equality to the corresponding term is remembered. Finally the proposition about the typing is given and justified. For easier presentation, nr optionally contains the number of the first local constant created here. Each type may optionally have presentational info about the variable (vid) inside. |
|
Content Model |
Table 254. Pattern: Ref
|
Namespace | |
|
Documentation |
Reference can be either private (coming from the current article) - their number is the position at the stack of accessible references (so it is not unique), or library - these additionally contain their kind (theorem or definition) and article nr. The position in the inference is kept for error messaging. For a private inference, the vid attribute optionally tells its identifier's number. |
|
Content Model |
Table 255. Pattern: Registration
|
Namespace | |
|
Documentation |
One justified cluster registration. The correctness conditions could be made more specific for each. |
|
Content Model |
Table 256. Pattern: RegistrationBlock
|
Namespace | |
|
Documentation |
Block of cluster registrations. |
|
Content Model |
Table 257. Pattern: Registrations
|
Namespace | |
|
Documentation |
Registrations, either imported from other articles ( after accommodation) - the signature is implicit in that case, or exported from the current article - then the signature has to be specified. aid optionally specifies its article's name in uppercase. |
|
Content Model |
Table 258. Pattern: Requirement
|
Namespace | |
|
Documentation |
Requirement is a constructor specially treated by the system. We give its internal number and optionally its name and the article id (aid) and order in article (absnr). |
|
Content Model |
Table 259. Pattern: Requirements
|
Namespace | |
|
Documentation |
Requirements (now only the exported form). |
|
Content Model |
Table 260. Pattern: Reservation
|
Namespace | |
|
Documentation |
Reservation of a new variable for a type. The type may optionally have presentational info about the variable (vid) inside. |
|
Content Model |
Table 261. Pattern: Scheme
|
Namespace | |
|
Documentation |
Schemes keep types of their second-order variables. First comes the scheme thesis, then the premises. The article number and order in article can be given, otherwise it belongs to the current article and order is implicit. Optional aid attribute specifies article name. |
|
Content Model |
Table 262. Pattern: SchemeBlock
|
Namespace | |
|
Documentation |
Scheme blocks are used for declaring the types of second-order variables appearing in a scheme, and for its justification. This could be a bit unified with Scheme later. schemenr is its serial nr in the article, while vid is its identifier number. |
|
Content Model |
Table 263. Pattern: SchemeFuncDecl
|
Namespace | |
|
Documentation |
Declaration of a scheme functor, possibly with its identifier number. |
|
Content Model |
Table 264. Pattern: SchemeInstantiation
|
Namespace | |
|
Documentation |
Instantions of scheme functors and predicates. and predicates. Scheme functors can be instantiated to other functors or terms (if zero arity). Scheme predicates can be instantiated to other predicates |
|
Content Model |
Table 265. Pattern: SchemePredDecl
|
Namespace | |
|
Documentation |
Declaration of a scheme predicate, possibly with its identifier number. |
|
Content Model |
Table 266. Pattern: Schemes
|
Namespace | |
|
Documentation |
Schemes, either imported from other articles ( after accommodation) - the signature is implicit in that case, or exported from the current article - then the signature has to be specified. aid optionally specifies article's name in uppercase. |
|
Content Model |
Table 268. Pattern: Set
|
Namespace | |
|
Documentation |
This is e.g.: set a = f(b); . The type of the new local constant is given. This local constant is now always expanded to its definition, and should not directly appear in any expression, but it is now needed for some implementation reasons. For easier presentation, nr optionally contains the number of the first local constant created here. The type may optionally have presentational info about the variable (vid) inside. |
|
Content Model |
Table 269. Pattern: Signature
|
Namespace | |
|
Documentation |
Signature is a list of articles from which we import constructors. |
|
Content Model |
Table 270. Pattern: SkeletonItem
|
Namespace | |
|
Documentation |
Skeleton items change the InFile.Current thesis, for Proof the changed Thesis together with used expansions is printed explicitely after them. PerCasesReasoning is not included here. |
|
Content Model |
( %Let; | %Conclusion; | %Assume; | %Given; | %Take; | %TakeAsVar; ) %Thesis; ? |
Table 271. Pattern: SkippedProof
|
Namespace | |
|
Documentation |
This means that the author has skipped the proof. Articles with such items are not yet fully completed. |
|
Content Model |
Table 272. Pattern: StructLoci
|
Namespace | |
|
Documentation |
Structural loci are not used yet (that is all I know about them). |
|
Content Model |
Table 273. Pattern: Suppose
|
Namespace | |
|
Documentation |
Supposition of one or more propositions. |
|
Content Model |
Table 274. Pattern: SupposeBlock
|
Namespace | |
|
Documentation |
Block starting with one supposition, the direct and diffuse version (this depends on the kind of its parent block). The block thesis is printed for proofs in the beginning and for diffuse reasoning in the end. |
|
Content Model |
Table 275. Pattern: Symbols
|
Namespace | |||||||||
|
Documentation |
Local dictionary for an article. The symbol kinds still use very internal notation. | ||||||||
|
Content Model | |||||||||
| Attributes |
|
Table 276. Pattern: Take
|
Namespace | |
|
Documentation |
Take without equality. This does not introduce a new local constant, just changes the thesis. |
|
Content Model |
Table 277. Pattern: TakeAsVar
|
Namespace | |
|
Documentation |
Take with equality. This introduces a new local constant, whose type is given here. For easier presentation, nr optionally contains the number of the first local constant created here. The type may optionally have presentational info about the variable (vid) inside. |
|
Content Model |
Table 278. Pattern: Term
|
Namespace | |
|
Documentation |
No documentation available. |
|
Content Model |
( %Var; | %LocusVar; | %FreeVar; | %LambdaVar; | %Const; | %InfConst; | %Num; | %Func; | %PrivFunc; | %Fraenkel; | %QuaTrm; | %It; | %Choice; | %ErrorTrm; ) |
Table 279. Pattern: Theorems
|
Namespace | |
|
Documentation |
Theorems, either imported from other articles ( after accommodation) - the signature is implicit in that case, or exported from the current article - then the signature has to be specified. They can be either ordinary or definitional. The article number and order in article can be given, otherwise it belongs to the current article and order is implicit. Optional aid attribute specifies article name. constrkind and constrnr determine for def. theorems the defined constructor. If they do not appear (and kind='D'), then this is a canceled (verum) deftheorem. |
|
Content Model |
Table 280. Pattern: Thesis
|
Namespace | |
|
Documentation |
The changed thesis is printed after skeleton items in proofs, together with the numbers of definientia used for its expansion. |
|
Content Model |
Table 281. Pattern: ThesisExpansions
|
Namespace | |
|
Documentation |
Numbers of Definiens used in expanding the thesis, together with their counts. |
|
Content Model |
Table 282. Pattern: Typ
|
Namespace | |
|
Documentation |
Parameterized type - either mode or structure The kinds "L" and "G" are equivalent, "G" is going to be replaced by more correct "L" in Mizar gradually. First goes the LowerCluster, than UpperCluster Optionally the article id (aid) and order in article (absnr) can be given. If available, presentational info (number of the Pattern) is given in pid, and presentational info about variable introduced (e.g. in Fraenkel) may be given in vid. |
|
Content Model |
Table 284. Pattern: UnknownCorrCond
|
Namespace | |
|
Documentation |
No documentation available. |
|
Content Model |
Table 285. Pattern: Var
|
Namespace | |
|
Documentation |
Normal bound variable (deBruijn index). Their types are given in quantification - see For, Fraenkel |
|
Content Model |