Grammar of Mizar

Date: February 10, 2005
Version: 7.4.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-Block ] "end" .


Redefinition-Block = use
"redefine" { ( Definition-Item | Definition ) } .


Registration-Block = use
"registration" { ( Loci-Declaration | Cluster-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 .


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 .


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" Justification ";" ] { 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" Justification ";" ] .


Attribute-Pattern = use
Locus "is" Attribute-Symbol .


Attribute-Synonym = use
"synonym" ( Attribute-Pattern | Predicate-Pattern ) "for" Attribute-Pattern ";" .


Attribute-Antonym = use
"antonym" ( Attribute-Pattern | Predicate-Pattern ) "for" Attribute-Pattern ";" .


Attribute-Symbol = use
Symbol .


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


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


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


Adjective-Cluster = use
{ Adjective } .


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


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


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


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


Correctness-Condition = use
( "existence" | "uniqueness" | "coherence" | "compatibility" | "consistency" ) 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" { Reasoning-Item } "end" .


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-Item } "end" ";" .


Suppose-List = use
Suppose { Suppose } .


Suppose = use
"suppose" ( Proposition | Conditions ) ";" { Reasoning-Item } "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
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 "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 .


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-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 | Private-Definition-Parameter | "it" .


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