| Article = | use | |
| Environment-Declaration Text-Proper . | ||
| 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 = | 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 | Identify-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 | "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-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 [ Type-Expression ] ";" Correctness-Conditions . | ||
| Identify-Registration = | use | |
| "identify" Functor-Pattern "with" Functor-Pattern [ "when" Locus "=" Locus { "," Locus "=" Locus } ] ";" 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 . | ||
| 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 . | ||
| 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" . | ||