Grammar of Mizar

Date: February 9, 2012
Version: 7.13.01
Initial term: Article

Contents

  1. Article
  2. Environment
  3. Text Proper
  4. Expressions
  5. Non-terminals
  6. Terminals

System terms (usage):
File-Name, Identifier, Numeral, Symbol.

Article


Article = use
Environment-Declaration Text-Proper .

Environment

Environment-Declaration = use
"environ" { Directive } .
Directive = use
Vocabulary-Directive | Library-Directive | Requirement-Directive .



Vocabulary-Directive = use
"vocabularies" Vocabulary-Name { "," Vocabulary-Name } ";" .


Vocabulary-Name = use
File-Name .


Library-Directive = use
( "notations" | "constructors" | "registrations" | "definitions" | "theorems" | "schemes" ) Article-Name { "," Article-Name } ";" .


Article-Name = use
File-Name .


Requirement-Directive = use
"requirements" Requirement { "," Requirement } ";" .


Requirement = use
File-Name .

Text Proper


Text-Proper = use
Section { Section } .


Section = use
"begin" { Text-Item } .


Text-Item = use
Reservation | Definitional-Item | Registration-Item | Notation-Item | Theorem | Scheme-Item | Auxiliary-Item | Canceled-Theorem .


Reservation = use
"reserve" Reservation-Segment { "," Reservation-Segment } ";" .


Reservation-Segment = use
Reserved-Identifiers "for" Type-Expression .


Reserved-Identifiers = use
Identifier { "," Identifier } .


Definitional-Item = use
Definitional-Block ";" .


Registration-Item = use
Registration-Block ";" .


Notation-Item = use
Notation-Block ";" .


Definitional-Block = use
"definition" { ( Definition-Item | Definition | Redefinition ) } "end" .


Registration-Block = use
"registration" { ( Loci-Declaration | Cluster-Registration | Identify-Registration | Property-Registration | Reduction-Registration | Canceled-Registration ) } "end" .


Notation-Block = use
"notation" { ( Loci-Declaration | Notation-Declaration ) } "end" .


Definition-Item = use
Loci-Declaration | Permissive-Assumption | Auxiliary-Item .


Notation-Declaration = use
Attribute-Synonym | Attribute-Antonym | Functor-Synonym | Mode-Synonym | Predicate-Synonym | Predicate-Antonym .


Loci-Declaration = use
"let" Qualified-Variables [ "such" Conditions ] ";" .


Permissive-Assumption = use
Assumption .


Definition = use
Structure-Definition | Mode-Definition | Functor-Definition | Predicate-Definition | Attribute-Definition | Canceled-Definition .


Redefinition = use
"redefine" ( Mode-Definition | Functor-Definition | Predicate-Definition | Attribute-Definition ) .


Structure-Definition = use
"struct" [ "(" Ancestors ")" ] Structure-Symbol [ "over" Loci ] "(#" Fields "#)" ";" .


Ancestors = use
Structure-Type-Expression { "," Structure-Type-Expression } .


Structure-Symbol = use
Symbol .


Loci = use
Locus { "," Locus } .


Fields = use
Field-Segment { "," Field-Segment } .


Locus = use
Variable-Identifier .


Variable-Identifier = use
Identifier .


Field-Segment = use
Selector-Symbol { "," Selector-Symbol } Specification .


Selector-Symbol = use
Symbol .


Specification = use
"->" Type-Expression .


Mode-Definition = use
"mode" Mode-Pattern ( [ Specification ] [ "means" Definiens ] ";" Correctness-Conditions | "is" Type-Expression ";" ) .


Mode-Pattern = use
Mode-Symbol [ "of" Loci ] .


Mode-Symbol = use
Symbol | "set" .


Mode-Synonym = use
"synonym" Mode-Pattern "for" Mode-Pattern ";" .


Definiens = use
Simple-Definiens | Conditional-Definiens .


Simple-Definiens = use
[ ":" Label-Identifier ":" ] ( Sentence | Term-Expression ) .


Label-Identifier = use
Identifier .


Conditional-Definiens = use
[ ":" Label-Identifier ":" ] Partial-Definiens-List [ "otherwise" ( Sentence | Term-Expression ) ] .


Partial-Definiens-List = use
Partial-Definiens { "," Partial-Definiens } .


Partial-Definiens = use
( Sentence | Term-Expression ) "if" Sentence .


Functor-Definition = use
"func" Functor-Pattern [ Specification ] [ ( "means" | "equals" ) Definiens ] ";" Correctness-Conditions { Functor-Property } .


Functor-Pattern = use
[ Functor-Loci ] Functor-Symbol [ Functor-Loci ] | Left-Functor-Bracket Loci Right-Functor-Bracket .


Functor-Property = use
( "commutativity" | "idempotence" | "involutiveness" | "projectivity" ) Justification ";" .


Functor-Synonym = use
"synonym" Functor-Pattern "for" Functor-Pattern ";" .


Functor-Loci = use
Locus | "(" Loci ")" .


Functor-Symbol = use
Symbol .


Left-Functor-Bracket = use
Symbol | "{" | "[" .


Right-Functor-Bracket = use
Symbol | "}" | "]" .


Predicate-Definition = use
"pred" Predicate-Pattern [ "means" Definiens ] ";" Correctness-Conditions { Predicate-Property } .


Predicate-Pattern = use
[ Loci ] Predicate-Symbol [ Loci ] .


Predicate-Property = use
( "symmetry" | "asymmetry" | "connectedness" | "reflexivity" | "irreflexivity" ) Justification ";" .


Predicate-Synonym = use
"synonym" Predicate-Pattern "for" Predicate-Pattern ";" .


Predicate-Antonym = use
"antonym" Predicate-Pattern "for" Predicate-Pattern ";" .


Predicate-Symbol = use
Symbol | "=" .


Attribute-Definition = use
"attr" Attribute-Pattern "means" Definiens ";" Correctness-Conditions .


Attribute-Pattern = use
Locus "is" [ Attribute-Loci ] Attribute-Symbol .


Attribute-Synonym = use
"synonym" Attribute-Pattern "for" Attribute-Pattern ";" .


Attribute-Antonym = use
"antonym" Attribute-Pattern "for" Attribute-Pattern ";" .


Attribute-Symbol = use
Symbol .


Attribute-Loci = use
Loci | "(" Loci ")" .


Canceled-Definition = use
"canceled" [ Numeral ] ";" .


Canceled-Registration = use
"canceled" [ Numeral ] ";" .


Cluster-Registration = use
Existential-Registration | Conditional-Registration | Functorial-Registration .


Existential-Registration = use
"cluster" Adjective-Cluster "for" Type-Expression ";" Correctness-Conditions .


Adjective-Cluster = use
{ Adjective } .


Adjective = use
[ "non" ] [ Adjective-Arguments ] Attribute-Symbol .


Conditional-Registration = use
"cluster" Adjective-Cluster "->" Adjective-Cluster "for" Type-Expression ";" Correctness-Conditions .


Functorial-Registration = use
"cluster" Term-Expression "->" Adjective-Cluster [ "for" Type-Expression ] ";" Correctness-Conditions .


Identify-Registration = use
"identify" Functor-Pattern "with" Functor-Pattern [ "when" Locus "=" Locus { "," Locus "=" Locus } ] ";" Correctness-Conditions .


Reduction-Registration = use
"reduce" Term-Expression "->" Term-Expression ";" Correctness-Conditions .


Property-Registration = use
"sethood" "of" Type-Expression ";" Correctness-Conditions .


Correctness-Conditions = use
{ Correctness-Condition } [ "correctness" Justification ";" ] .


Correctness-Condition = use
( "existence" | "uniqueness" | "coherence" | "compatibility" | "consistency" | "reducibility" ) Justification ";" .


Theorem = use
"theorem" Compact-Statement .


Scheme-Item = use
Scheme-Block ";" .


Scheme-Block = use
"scheme" Scheme-Identifier "{" Scheme-Parameters "}" ":" Scheme-Conclusion [ "provided" Scheme-Premise { "and" Scheme-Premise } ] Proof .


Scheme-Identifier = use
Identifier .


Scheme-Parameters = use
Scheme-Segment { "," Scheme-Segment } .


Scheme-Conclusion = use
Sentence .


Scheme-Premise = use
Proposition .


Scheme-Segment = use
Predicate-Segment | Functor-Segment .


Predicate-Segment = use
Predicate-Identifier { "," Predicate-Identifier } "[" [ Type-Expression-List ] "]" .


Predicate-Identifier = use
Identifier .


Functor-Segment = use
Functor-Identifier { "," Functor-Identifier } "(" [ Type-Expression-List ] ")" Specification .


Functor-Identifier = use
Identifier .


Auxiliary-Item = use
Statement | Private-Definition .


Canceled-Theorem = use
"canceled" [ Numeral ] ";" .


Private-Definition = use
Constant-Definition | Private-Functor-Definition | Private-Predicate-Definition .


Constant-Definition = use
"set" Equating-List ";" .


Equating-List = use
Equating { "," Equating } .


Equating = use
Variable-Identifier "=" Term-Expression .


Private-Functor-Definition = use
"deffunc" Private-Functor-Pattern "=" Term-Expression .


Private-Predicate-Definition = use
"defpred" Private-Predicate-Pattern "means" Sentence .


Private-Functor-Pattern = use
Functor-Identifier "(" [ Type-Expression-List ] ")" .


Private-Predicate-Pattern = use
Predicate-Identifier "[" [ Type-Expression-List ] "]" .


Reasoning = use
{ Reasoning-Item } [ "per" "cases" Simple-Justification ";" ( Case-List | Suppose-List ) ] .


Case-List = use
Case { Case } .


Case = use
"case" ( Proposition | Conditions ) ";" Reasoning "end" ";" .


Suppose-List = use
Suppose { Suppose } .


Suppose = use
"suppose" ( Proposition | Conditions ) ";" Reasoning "end" ";" .


Reasoning-Item = use
Auxiliary-Item | Skeleton-Item .


Skeleton-Item = use
Generalization | Assumption | Conclusion | Exemplification .


Generalization = use
"let" Qualified-Variables [ "such" Conditions ] ";" .


Assumption = use
Single-Assumption | Collective-Assumption | Existential-Assumption .


Single-Assumption = use
"assume" Proposition ";" .


Collective-Assumption = use
"assume" Conditions ";" .


Existential-Assumption = use
"given" Qualified-Variables [ "such" Conditions ] ";" .


Conclusion = use
( "thus" | "hence" ) Compact-Statement | Diffuse-Conclusion .


Diffuse-Conclusion = use
"thus" Diffuse-Statement | "hereby" Reasoning "end" ";" .


Exemplification = use
"take" Example { "," Example } ";" .


Example = use
Term-Expression | Variable-Identifier "=" Term-Expression .


Statement = use
[ "then" ] Linkable-Statement | Diffuse-Statement .


Linkable-Statement = use
Compact-Statement | Choice-Statement | Type-Changing-Statement | Iterative-Equality .


Compact-Statement = use
Proposition Justification ";" .


Choice-Statement = use
"consider" Qualified-Variables "such" Conditions Simple-Justification ";" .


Type-Changing-Statement = use
"reconsider" Type-Change-List "as" Type-Expression Simple-Justification ";" .


Type-Change-List = use
( Equating | Variable-Identifier ) { "," ( Equating | Variable-Identifier ) } .


Iterative-Equality = use
[ Label-Identifier ":" ] Term-Expression "=" Term-Expression Simple-Justification ".=" Term-Expression Simple-Justification { ".=" Term-Expression Simple-Justification } ";" .


Diffuse-Statement = use
[ Label-Identifier ":" ] "now" Reasoning "end" ";" .


Justification = use
Simple-Justification | Proof .


Simple-Justification = use
Straightforward-Justification | Scheme-Justification .


Proof = use
( "proof" | "@proof" ) Reasoning "end" .


Straightforward-Justification = use
[ "by" References ] .


Scheme-Justification = use
"from" Scheme-Reference [ "(" References ")" ] .


References = use
Reference { "," Reference } .


Reference = use
Local-Reference | Library-Reference .


Scheme-Reference = use
Local-Scheme-Reference | Library-Scheme-Reference .


Local-Reference = use
Label-Identifier .


Local-Scheme-Reference = use
Scheme-Identifier .


Library-Reference = use
Article-Name ":" ( Theorem-Number | "def" Definition-Number ) { "," ( Theorem-Number | "def" Definition-Number ) } .


Library-Scheme-Reference = use
Article-Name ":" "sch" Scheme-Number .


Theorem-Number = use
Numeral .


Definition-Number = use
Numeral .


Scheme-Number = use
Numeral .


Conditions = use
"that" Proposition { "and" Proposition } .


Proposition = use
[ Label-Identifier ":" ] Sentence .


Sentence = use
Formula-Expression .

Expressions


Formula-Expression = use
"(" Formula-Expression ")" | Atomic-Formula-Expression | Quantified-Formula-Expression | Formula-Expression "&" Formula-Expression | Formula-Expression "&" ",,," "&" Formula-Expression | Formula-Expression "or" Formula-Expression | Formula-Expression "or" "..." "or" Formula-Expression | Formula-Expression "implies" Formula-Expression | Formula-Expression "iff" Formula-Expression | "not" Formula-Expression | "contradiction" | "thesis" .


Atomic-Formula-Expression = use
[ Term-Expression-List ] Predicate-Symbol [ Term-Expression-List ] | Predicate-Identifier "[" [ Term-Expression-List ] "]" | Term-Expression "is" Adjective { Adjective } | Term-Expression "is" Type-Expression .


Quantified-Formula-Expression = use
"for" Qualified-Variables [ "st" Formula-Expression ] ( "holds" Formula-Expression | Quantified-Formula-Expression ) | "ex" Qualified-Variables "st" Formula-Expression .


Qualified-Variables = use
Implicitly-Qualified-Variables | Explicitly-Qualified-Variables | Explicitly-Qualified-Variables "," Implicitly-Qualified-Variables | Indexed-Variable-Sequent .


Indexed-Variable-Sequent = use
Indexed-Variable "..." Indexed-Variable .


Indexed-Variable = use
Variable-Identifier "_" Term-Expression .


Implicitly-Qualified-Variables = use
Variables .


Explicitly-Qualified-Variables = use
Qualified-Segment { "," Qualified-Segment } .


Qualified-Segment = use
Variables Qualification .


Variables = use
Variable-Identifier { "," Variable-Identifier } .


Qualification = use
( "being" | "be" ) Type-Expression .


Type-Expression = use
"(" Type-Expression ")" | Adjective-Cluster Type-Expression | Radix-Type .


Structure-Type-Expression = use
"(" Structure-Type-Expression ")" | Adjective-Cluster Structure-Type-Expression | Structure-Symbol [ "over" Term-Expression-List ] .


Radix-Type = use
Mode-Symbol [ "of" Term-Expression-List ] | Structure-Symbol [ "over" Term-Expression-List ] .


Type-Expression-List = use
Type-Expression { "," Type-Expression } .


Term-Expression = use
"(" Term-Expression ")" | [ Arguments ] Functor-Symbol [ Arguments ] | Left-Functor-Bracket Term-Expression-List Right-Functor-Bracket | Functor-Identifier "(" [ Term-Expression-List ] ")" | Structure-Symbol "(#" Term-Expression-List "#)" | Variable-Identifier | "{" Term-Expression [ Postqualification ] ":" Sentence "}" | Numeral | Term-Expression "qua" Type-Expression | "the" Selector-Symbol "of" Term-Expression | "the" Selector-Symbol | "the" Type-Expression | Variable-Identifier "_" Type-Expression | Private-Definition-Parameter | "it" .


Arguments = use
Term-Expression | "(" Term-Expression-List ")" .


Adjective-Arguments = use
Term-Expression-List | "(" Term-Expression-List ")" .


Term-Expression-List = use
Term-Expression { "," Term-Expression } .


Postqualification = use
"where" Postqualifying-Segment { "," Postqualifying-Segment } .


Postqualifying-Segment = use
Postqualified-Variable { "," Postqualified-Variable } "is" Type-Expression .


Postqualified-Variable = use
Identifier .


Private-Definition-Parameter = use
"$1" | "$2" | "$3" | "$4" | "$5" | "$6" | "$7" | "$8" | "$9" | "$10" .

Usage of non-terminals and system-terms:
  1. Adjective in Adjective-Cluster, Atomic-Formula-Expression,
  2. Adjective-Arguments in Adjective,
  3. Adjective-Cluster in Existential-Registration, Conditional-Registration, Conditional-Registration, Functorial-Registration, Type-Expression, Structure-Type-Expression,
  4. Ancestors in Structure-Definition,
  5. Arguments in Term-Expression, Term-Expression,
  6. Article in ,
  7. Article-Name in Library-Directive, Library-Reference, Library-Scheme-Reference,
  8. Assumption in Permissive-Assumption, Skeleton-Item,
  9. Atomic-Formula-Expression in Formula-Expression,
  10. Attribute-Antonym in Notation-Declaration,
  11. Attribute-Definition in Definition, Redefinition,
  12. Attribute-Loci in Attribute-Pattern,
  13. Attribute-Pattern in Attribute-Definition, Attribute-Synonym, Attribute-Synonym, Attribute-Antonym, Attribute-Antonym,
  14. Attribute-Symbol in Attribute-Pattern, Adjective,
  15. Attribute-Synonym in Notation-Declaration,
  16. Auxiliary-Item in Text-Item, Definition-Item, Reasoning-Item,
  17. Canceled-Definition in Definition,
  18. Canceled-Registration in Registration-Block,
  19. Canceled-Theorem in Text-Item,
  20. Case in Case-List,
  21. Case-List in Reasoning,
  22. Choice-Statement in Linkable-Statement,
  23. Cluster-Registration in Registration-Block,
  24. Collective-Assumption in Assumption,
  25. Compact-Statement in Theorem, Conclusion, Linkable-Statement,
  26. Conclusion in Skeleton-Item,
  27. Conditional-Definiens in Definiens,
  28. Conditional-Registration in Cluster-Registration,
  29. Conditions in Loci-Declaration, Case, Suppose, Generalization, Collective-Assumption, Existential-Assumption, Choice-Statement,
  30. Constant-Definition in Private-Definition,
  31. Correctness-Condition in Correctness-Conditions,
  32. Correctness-Conditions in Mode-Definition, Functor-Definition, Predicate-Definition, Attribute-Definition, Existential-Registration, Conditional-Registration, Functorial-Registration, Identify-Registration, Reduction-Registration, Property-Registration,
  33. Definiens in Mode-Definition, Functor-Definition, Predicate-Definition, Attribute-Definition,
  34. Definition in Definitional-Block,
  35. Definition-Item in Definitional-Block,
  36. Definition-Number in Library-Reference,
  37. Definitional-Block in Definitional-Item,
  38. Definitional-Item in Text-Item,
  39. Diffuse-Conclusion in Conclusion,
  40. Diffuse-Statement in Diffuse-Conclusion, Statement,
  41. Directive in Environment-Declaration,
  42. Environment-Declaration in Article,
  43. Equating in Equating-List, Type-Change-List,
  44. Equating-List in Constant-Definition,
  45. Example in Exemplification,
  46. Exemplification in Skeleton-Item,
  47. Existential-Assumption in Assumption,
  48. Existential-Registration in Cluster-Registration,
  49. Explicitly-Qualified-Variables in Qualified-Variables, Qualified-Variables,
  50. Field-Segment in Fields,
  51. Fields in Structure-Definition,
  52. File-Name in Vocabulary-Name, Article-Name, Requirement,
  53. Formula-Expression in Sentence, Formula-Expression, Formula-Expression, Formula-Expression, Formula-Expression, Formula-Expression, Formula-Expression, Formula-Expression, Formula-Expression, Formula-Expression, Formula-Expression, Formula-Expression, Formula-Expression, Formula-Expression, Formula-Expression, Quantified-Formula-Expression, Quantified-Formula-Expression, Quantified-Formula-Expression,
  54. Functor-Definition in Definition, Redefinition,
  55. Functor-Identifier in Functor-Segment, Private-Functor-Pattern, Term-Expression,
  56. Functor-Loci in Functor-Pattern, Functor-Pattern,
  57. Functor-Pattern in Functor-Definition, Functor-Synonym, Functor-Synonym, Identify-Registration, Identify-Registration,
  58. Functor-Property in Functor-Definition,
  59. Functor-Segment in Scheme-Segment,
  60. Functor-Symbol in Functor-Pattern, Term-Expression,
  61. Functor-Synonym in Notation-Declaration,
  62. Functorial-Registration in Cluster-Registration,
  63. Generalization in Skeleton-Item,
  64. Identifier in Reserved-Identifiers, Variable-Identifier, Label-Identifier, Scheme-Identifier, Predicate-Identifier, Functor-Identifier, Postqualified-Variable,
  65. Identify-Registration in Registration-Block,
  66. Implicitly-Qualified-Variables in Qualified-Variables, Qualified-Variables,
  67. Indexed-Variable in Indexed-Variable-Sequent, Indexed-Variable-Sequent,
  68. Indexed-Variable-Sequent in Qualified-Variables,
  69. Iterative-Equality in Linkable-Statement,
  70. Justification in Functor-Property, Predicate-Property, Correctness-Conditions, Correctness-Condition, Compact-Statement,
  71. Label-Identifier in Simple-Definiens, Conditional-Definiens, Iterative-Equality, Diffuse-Statement, Local-Reference, Proposition,
  72. Left-Functor-Bracket in Functor-Pattern, Term-Expression,
  73. Library-Directive in Directive,
  74. Library-Reference in Reference,
  75. Library-Scheme-Reference in Scheme-Reference,
  76. Linkable-Statement in Statement,
  77. Local-Reference in Reference,
  78. Local-Scheme-Reference in Scheme-Reference,
  79. Loci in Structure-Definition, Mode-Pattern, Functor-Pattern, Functor-Loci, Predicate-Pattern, Predicate-Pattern, Attribute-Loci, Attribute-Loci,
  80. Loci-Declaration in Registration-Block, Notation-Block, Definition-Item,
  81. Locus in Loci, Functor-Loci, Attribute-Pattern, Identify-Registration, Identify-Registration,
  82. Mode-Definition in Definition, Redefinition,
  83. Mode-Pattern in Mode-Definition, Mode-Synonym, Mode-Synonym,
  84. Mode-Symbol in Mode-Pattern, Radix-Type,
  85. Mode-Synonym in Notation-Declaration,
  86. Notation-Block in Notation-Item,
  87. Notation-Declaration in Notation-Block,
  88. Notation-Item in Text-Item,
  89. Numeral in Canceled-Definition, Canceled-Registration, Canceled-Theorem, Theorem-Number, Definition-Number, Scheme-Number, Term-Expression,
  90. Partial-Definiens in Partial-Definiens-List,
  91. Partial-Definiens-List in Conditional-Definiens,
  92. Permissive-Assumption in Definition-Item,
  93. Postqualification in Term-Expression,
  94. Postqualified-Variable in Postqualifying-Segment,
  95. Postqualifying-Segment in Postqualification,
  96. Predicate-Antonym in Notation-Declaration,
  97. Predicate-Definition in Definition, Redefinition,
  98. Predicate-Identifier in Predicate-Segment, Private-Predicate-Pattern, Atomic-Formula-Expression,
  99. Predicate-Pattern in Predicate-Definition, Predicate-Synonym, Predicate-Synonym, Predicate-Antonym, Predicate-Antonym,
  100. Predicate-Property in Predicate-Definition,
  101. Predicate-Segment in Scheme-Segment,
  102. Predicate-Symbol in Predicate-Pattern, Atomic-Formula-Expression,
  103. Predicate-Synonym in Notation-Declaration,
  104. Private-Definition in Auxiliary-Item,
  105. Private-Definition-Parameter in Term-Expression,
  106. Private-Functor-Definition in Private-Definition,
  107. Private-Functor-Pattern in Private-Functor-Definition,
  108. Private-Predicate-Definition in Private-Definition,
  109. Private-Predicate-Pattern in Private-Predicate-Definition,
  110. Proof in Scheme-Block, Justification,
  111. Property-Registration in Registration-Block,
  112. Proposition in Scheme-Premise, Case, Suppose, Single-Assumption, Compact-Statement, Conditions,
  113. Qualification in Qualified-Segment,
  114. Qualified-Segment in Explicitly-Qualified-Variables,
  115. Qualified-Variables in Loci-Declaration, Generalization, Existential-Assumption, Choice-Statement, Quantified-Formula-Expression, Quantified-Formula-Expression,
  116. Quantified-Formula-Expression in Formula-Expression, Quantified-Formula-Expression,
  117. Radix-Type in Type-Expression,
  118. Reasoning in Case, Suppose, Diffuse-Conclusion, Diffuse-Statement, Proof,
  119. Reasoning-Item in Reasoning,
  120. Redefinition in Definitional-Block,
  121. Reduction-Registration in Registration-Block,
  122. Reference in References,
  123. References in Straightforward-Justification, Scheme-Justification,
  124. Registration-Block in Registration-Item,
  125. Registration-Item in Text-Item,
  126. Requirement in Requirement-Directive,
  127. Requirement-Directive in Directive,
  128. Reservation in Text-Item,
  129. Reservation-Segment in Reservation,
  130. Reserved-Identifiers in Reservation-Segment,
  131. Right-Functor-Bracket in Functor-Pattern, Term-Expression,
  132. Scheme-Block in Scheme-Item,
  133. Scheme-Conclusion in Scheme-Block,
  134. Scheme-Identifier in Scheme-Block, Local-Scheme-Reference,
  135. Scheme-Item in Text-Item,
  136. Scheme-Justification in Simple-Justification,
  137. Scheme-Number in Library-Scheme-Reference,
  138. Scheme-Parameters in Scheme-Block,
  139. Scheme-Premise in Scheme-Block,
  140. Scheme-Reference in Scheme-Justification,
  141. Scheme-Segment in Scheme-Parameters,
  142. Section in Text-Proper,
  143. Selector-Symbol in Field-Segment, Term-Expression, Term-Expression,
  144. Sentence in Simple-Definiens, Conditional-Definiens, Partial-Definiens, Partial-Definiens, Scheme-Conclusion, Private-Predicate-Definition, Proposition, Term-Expression,
  145. Simple-Definiens in Definiens,
  146. Simple-Justification in Reasoning, Choice-Statement, Type-Changing-Statement, Iterative-Equality, Iterative-Equality, Justification,
  147. Single-Assumption in Assumption,
  148. Skeleton-Item in Reasoning-Item,
  149. Specification in Field-Segment, Mode-Definition, Functor-Definition, Functor-Segment,
  150. Statement in Auxiliary-Item,
  151. Straightforward-Justification in Simple-Justification,
  152. Structure-Definition in Definition,
  153. Structure-Symbol in Structure-Definition, Structure-Type-Expression, Radix-Type, Term-Expression,
  154. Structure-Type-Expression in Ancestors, Structure-Type-Expression, Structure-Type-Expression,
  155. Suppose in Suppose-List,
  156. Suppose-List in Reasoning,
  157. Symbol in Structure-Symbol, Selector-Symbol, Mode-Symbol, Functor-Symbol, Left-Functor-Bracket, Right-Functor-Bracket, Predicate-Symbol, Attribute-Symbol,
  158. Term-Expression in Simple-Definiens, Conditional-Definiens, Partial-Definiens, Functorial-Registration, Reduction-Registration, Reduction-Registration, Equating, Private-Functor-Definition, Example, Example, Iterative-Equality, Iterative-Equality, Iterative-Equality, Atomic-Formula-Expression, Atomic-Formula-Expression, Indexed-Variable, Term-Expression, Term-Expression, Term-Expression, Term-Expression, Arguments, Term-Expression-List,
  159. Term-Expression-List in Atomic-Formula-Expression, Atomic-Formula-Expression, Atomic-Formula-Expression, Structure-Type-Expression, Radix-Type, Radix-Type, Term-Expression, Term-Expression, Term-Expression, Arguments, Adjective-Arguments, Adjective-Arguments,
  160. Text-Item in Section,
  161. Text-Proper in Article,
  162. Theorem in Text-Item,
  163. Theorem-Number in Library-Reference,
  164. Type-Change-List in Type-Changing-Statement,
  165. Type-Changing-Statement in Linkable-Statement,
  166. Type-Expression in Reservation-Segment, Specification, Mode-Definition, Existential-Registration, Conditional-Registration, Functorial-Registration, Property-Registration, Type-Changing-Statement, Atomic-Formula-Expression, Qualification, Type-Expression, Type-Expression, Type-Expression-List, Term-Expression, Term-Expression, Term-Expression, Postqualifying-Segment,
  167. Type-Expression-List in Predicate-Segment, Functor-Segment, Private-Functor-Pattern, Private-Predicate-Pattern,
  168. Variable-Identifier in Locus, Equating, Example, Type-Change-List, Indexed-Variable, Variables, Term-Expression, Term-Expression,
  169. Variables in Implicitly-Qualified-Variables, Qualified-Segment,
  170. Vocabulary-Directive in Directive,
  171. Vocabulary-Name in Vocabulary-Directive
Usage of terminals:
  1. "#)" in Structure-Definition, Term-Expression,
  2. "$1" in Private-Definition-Parameter,
  3. "$10" in Private-Definition-Parameter,
  4. "$2" in Private-Definition-Parameter,
  5. "$3" in Private-Definition-Parameter,
  6. "$4" in Private-Definition-Parameter,
  7. "$5" in Private-Definition-Parameter,
  8. "$6" in Private-Definition-Parameter,
  9. "$7" in Private-Definition-Parameter,
  10. "$8" in Private-Definition-Parameter,
  11. "$9" in Private-Definition-Parameter,
  12. "&" in Formula-Expression, Formula-Expression, Formula-Expression,
  13. "(" in Structure-Definition, Functor-Loci, Attribute-Loci, Functor-Segment, Private-Functor-Pattern, Scheme-Justification, Formula-Expression, Type-Expression, Structure-Type-Expression, Term-Expression, Term-Expression, Arguments, Adjective-Arguments,
  14. "(#" in Structure-Definition, Term-Expression,
  15. ")" in Structure-Definition, Functor-Loci, Attribute-Loci, Functor-Segment, Private-Functor-Pattern, Scheme-Justification, Formula-Expression, Type-Expression, Structure-Type-Expression, Term-Expression, Term-Expression, Arguments, Adjective-Arguments,
  16. "," in Vocabulary-Directive, Library-Directive, Requirement-Directive, Reservation, Reserved-Identifiers, Ancestors, Loci, Fields, Field-Segment, Partial-Definiens-List, Identify-Registration, Scheme-Parameters, Predicate-Segment, Functor-Segment, Equating-List, Exemplification, Type-Change-List, References, Library-Reference, Qualified-Variables, Explicitly-Qualified-Variables, Variables, Type-Expression-List, Term-Expression-List, Postqualification, Postqualifying-Segment,
  17. ",,," in Formula-Expression,
  18. "->" in Specification, Conditional-Registration, Functorial-Registration, Reduction-Registration,
  19. "..." in Formula-Expression, Indexed-Variable-Sequent,
  20. ".=" in Iterative-Equality,
  21. ":" in Simple-Definiens, Simple-Definiens, Conditional-Definiens, Conditional-Definiens, Scheme-Block, Iterative-Equality, Diffuse-Statement, Library-Reference, Library-Scheme-Reference, Proposition, Term-Expression,
  22. ";" in Vocabulary-Directive, Library-Directive, Requirement-Directive, Reservation, Definitional-Item, Registration-Item, Notation-Item, Loci-Declaration, Structure-Definition, Mode-Definition, Mode-Definition, Mode-Synonym, Functor-Definition, Functor-Property, Functor-Synonym, Predicate-Definition, Predicate-Property, Predicate-Synonym, Predicate-Antonym, Attribute-Definition, Attribute-Synonym, Attribute-Antonym, Canceled-Definition, Canceled-Registration, Existential-Registration, Conditional-Registration, Functorial-Registration, Identify-Registration, Reduction-Registration, Property-Registration, Correctness-Conditions, Correctness-Condition, Scheme-Item, Canceled-Theorem, Constant-Definition, Reasoning, Case, Case, Suppose, Suppose, Generalization, Single-Assumption, Collective-Assumption, Existential-Assumption, Diffuse-Conclusion, Exemplification, Compact-Statement, Choice-Statement, Type-Changing-Statement, Iterative-Equality, Diffuse-Statement,
  23. "=" in Predicate-Symbol, Identify-Registration, Equating, Private-Functor-Definition, Example, Iterative-Equality,
  24. "@proof" in Proof,
  25. "[" in Left-Functor-Bracket, Predicate-Segment, Private-Predicate-Pattern, Atomic-Formula-Expression,
  26. "]" in Right-Functor-Bracket, Predicate-Segment, Private-Predicate-Pattern, Atomic-Formula-Expression,
  27. "_" in Indexed-Variable, Term-Expression,
  28. "and" in Scheme-Block, Conditions,
  29. "antonym" in Predicate-Antonym, Attribute-Antonym,
  30. "as" in Type-Changing-Statement,
  31. "assume" in Single-Assumption, Collective-Assumption,
  32. "asymmetry" in Predicate-Property,
  33. "attr" in Attribute-Definition,
  34. "be" in Qualification,
  35. "begin" in Section,
  36. "being" in Qualification,
  37. "by" in Straightforward-Justification,
  38. "canceled" in Canceled-Definition, Canceled-Registration, Canceled-Theorem,
  39. "case" in Case,
  40. "cases" in Reasoning,
  41. "cluster" in Existential-Registration, Conditional-Registration, Functorial-Registration,
  42. "coherence" in Correctness-Condition,
  43. "commutativity" in Functor-Property,
  44. "compatibility" in Correctness-Condition,
  45. "connectedness" in Predicate-Property,
  46. "consider" in Choice-Statement,
  47. "consistency" in Correctness-Condition,
  48. "constructors" in Library-Directive,
  49. "contradiction" in Formula-Expression,
  50. "correctness" in Correctness-Conditions,
  51. "def" in Library-Reference,
  52. "deffunc" in Private-Functor-Definition,
  53. "definition" in Definitional-Block,
  54. "definitions" in Library-Directive,
  55. "defpred" in Private-Predicate-Definition,
  56. "end" in Definitional-Block, Registration-Block, Notation-Block, Case, Suppose, Diffuse-Conclusion, Diffuse-Statement, Proof,
  57. "environ" in Environment-Declaration,
  58. "equals" in Functor-Definition,
  59. "ex" in Quantified-Formula-Expression,
  60. "existence" in Correctness-Condition,
  61. "for" in Reservation-Segment, Mode-Synonym, Functor-Synonym, Predicate-Synonym, Predicate-Antonym, Attribute-Synonym, Attribute-Antonym, Existential-Registration, Conditional-Registration, Functorial-Registration, Quantified-Formula-Expression,
  62. "from" in Scheme-Justification,
  63. "func" in Functor-Definition,
  64. "given" in Existential-Assumption,
  65. "hence" in Conclusion,
  66. "hereby" in Diffuse-Conclusion,
  67. "holds" in Quantified-Formula-Expression,
  68. "idempotence" in Functor-Property,
  69. "identify" in Identify-Registration,
  70. "if" in Partial-Definiens,
  71. "iff" in Formula-Expression,
  72. "implies" in Formula-Expression,
  73. "involutiveness" in Functor-Property,
  74. "irreflexivity" in Predicate-Property,
  75. "is" in Mode-Definition, Attribute-Pattern, Atomic-Formula-Expression, Atomic-Formula-Expression, Postqualifying-Segment,
  76. "it" in Term-Expression,
  77. "let" in Loci-Declaration, Generalization,
  78. "means" in Mode-Definition, Functor-Definition, Predicate-Definition, Attribute-Definition, Private-Predicate-Definition,
  79. "mode" in Mode-Definition,
  80. "non" in Adjective,
  81. "not" in Formula-Expression,
  82. "notation" in Notation-Block,
  83. "notations" in Library-Directive,
  84. "now" in Diffuse-Statement,
  85. "of" in Mode-Pattern, Property-Registration, Radix-Type, Term-Expression,
  86. "or" in Formula-Expression, Formula-Expression, Formula-Expression,
  87. "otherwise" in Conditional-Definiens,
  88. "over" in Structure-Definition, Structure-Type-Expression, Radix-Type,
  89. "per" in Reasoning,
  90. "pred" in Predicate-Definition,
  91. "projectivity" in Functor-Property,
  92. "proof" in Proof,
  93. "provided" in Scheme-Block,
  94. "qua" in Term-Expression,
  95. "reconsider" in Type-Changing-Statement,
  96. "redefine" in Redefinition,
  97. "reduce" in Reduction-Registration,
  98. "reducibility" in Correctness-Condition,
  99. "reflexivity" in Predicate-Property,
  100. "registration" in Registration-Block,
  101. "registrations" in Library-Directive,
  102. "requirements" in Requirement-Directive,
  103. "reserve" in Reservation,
  104. "sch" in Library-Scheme-Reference,
  105. "scheme" in Scheme-Block,
  106. "schemes" in Library-Directive,
  107. "set" in Mode-Symbol, Constant-Definition,
  108. "sethood" in Property-Registration,
  109. "st" in Quantified-Formula-Expression, Quantified-Formula-Expression,
  110. "struct" in Structure-Definition,
  111. "such" in Loci-Declaration, Generalization, Existential-Assumption, Choice-Statement,
  112. "suppose" in Suppose,
  113. "symmetry" in Predicate-Property,
  114. "synonym" in Mode-Synonym, Functor-Synonym, Predicate-Synonym, Attribute-Synonym,
  115. "take" in Exemplification,
  116. "that" in Conditions,
  117. "the" in Term-Expression, Term-Expression, Term-Expression,
  118. "then" in Statement,
  119. "theorem" in Theorem,
  120. "theorems" in Library-Directive,
  121. "thesis" in Formula-Expression,
  122. "thus" in Conclusion, Diffuse-Conclusion,
  123. "uniqueness" in Correctness-Condition,
  124. "vocabularies" in Vocabulary-Directive,
  125. "when" in Identify-Registration,
  126. "where" in Postqualification,
  127. "with" in Identify-Registration,
  128. "{" in Left-Functor-Bracket, Scheme-Block, Term-Expression,
  129. "}" in Right-Functor-Bracket, Scheme-Block, Term-Expression
Grzegorz Bancerek, bancerek@mizar.org
Done with grammar2thtml.xsl