Table of Contents
Namespace:
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 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; | %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="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 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 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: 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 18. 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: 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 24. 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 25. 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 26. 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 27. 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 28. 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 29. 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 30. 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 31. 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 32. 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 33. 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 34. 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 35. 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 36. 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 37. 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 38. 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 39. 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 40. 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 41. 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 42. 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 48. 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 49. 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: 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 52. 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 53. 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 54. 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 55. 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 56. 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 57. 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 58. 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 59. 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 60. 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 61. 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 62. 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 63. 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: Identify
Documentation |
No documentation available. | ||||||||||||
Content Model |
( %ErrorIdentify; | ( %ConstrDef;, %ConstrDef;, EqArgs ) ) | ||||||||||||
Attributes |
| ||||||||||||
Source |
<element name="Identify" 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> <ref name="ConstrDef"/> <ref name="ConstrDef"/> <element name="EqArgs"> <zeroOrMore> <ref name="Pair"/> </zeroOrMore> </element> </group> </choice> </element> |
Table 66. Element: IdentifyRegistration
Documentation |
No documentation available. |
Content Model |
%IdentifyWithExp;, ( %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="IdentifyWithExp"/> <zeroOrMore> <ref name="CorrectnessCondition"/> </zeroOrMore> <optional> <ref name="Correctness"/> </optional> </element> |
Table 67. Element: IdentifyRegistrations
Documentation |
No documentation available. | ||||||||
Content Model |
%Signature; ? , ( %IdentifyWithExp; )* | ||||||||
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="IdentifyWithExp"/> </zeroOrMore> </element> |
Table 68. 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 69. 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 70. 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 75. 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 77. 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 78. 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 79. 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 80. 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 81. 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 82. 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 83. 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 84. 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 85. 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 86. 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 87. 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 88. 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 89. 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 90. 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 92. 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 93. 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 94. 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 95. 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 96. 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 97. 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 98. 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 99. 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 100. 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 102. 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 103. 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 104. 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 106. 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 107. 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 108. 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 109. 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 111. 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 112. 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 113. 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 114. 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 115. 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 117. 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 118. 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 119. 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 120. 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 121. 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 122. 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 123. 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 124. 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 125. 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 126. 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 128. 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 129. 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 130. 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 131. 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 132. 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 133. 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 136. 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 137. 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 138. 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 140. 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 142. 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 144. 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 145. 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 146. 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 148. 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 149. 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 150. 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 151. 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 154. 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 157. Pattern: AuxiliaryItem
Namespace | |
Documentation |
Auxiliary items are items which do not change thesis. |
Content Model |
( %JustifiedProposition; | %Consider; | %Set; | %Reconsider; | %DefFunc; | %DefPred; ) |
Table 158. 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 161. 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 170. 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 175. 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 176. 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 178. 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 180. 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 183. 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 184. 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 185. 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 193. 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: Formula
Namespace | |
Documentation |
No documentation available. |
Content Model |
( %Not; | %And; | %For; | %Pred; | %PrivPred; | %Is; | %Verum; | %ErrorFrm; ) |
Table 204. Pattern: GeneralPolynomial
Namespace | |
Documentation |
No documentation available. |
Content Model |
( %Polynomial; | %Number; ) |
Table 205. 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 206. 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 208. 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 209. 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 217. Pattern: Justification
Namespace | |
Documentation |
Direct justification. |
Content Model |
( %Inference; | %Proof; | %SkippedProof; ) |
Table 219. Pattern: JustifiedProposition
Namespace | |
Documentation |
No documentation available. |
Content Model |
( %Now; | %IterEquality; | ( %Proposition; %Justification; ) ) |
Table 222. 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: 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 230. Pattern: Number
Namespace | |
Documentation |
No documentation available. |
Content Model |
( %RationalNr; | %ComplexNr; ) |
Table 232. 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 233. 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 234. 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 243. Pattern: Property
Namespace | |
Documentation |
No documentation available. |
Content Model |
( UnexpectedProp | Symmetry | Reflexivity | Irreflexivity | Associativity | Transitivity | Commutativity | Connectedness | Antisymmetry | Idempotence | Involutiveness | Projectivity | Abstractness ) |
Table 246. 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 248. 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 249. 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 250. 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 253. 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 257. 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 258. 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 262. 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 263. 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 265. 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 272. 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 273. Pattern: Term
Namespace | |
Documentation |
No documentation available. |
Content Model |
( %Var; | %LocusVar; | %FreeVar; | %LambdaVar; | %Const; | %InfConst; | %Num; | %Func; | %PrivFunc; | %Fraenkel; | %QuaTrm; | %It; | %ErrorTrm; ) |
Table 274. 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 277. 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 |