diff options
Diffstat (limited to 'test/golden/geometry/glossing.golden')
| -rw-r--r-- | test/golden/geometry/glossing.golden | 2775 |
1 files changed, 0 insertions, 2775 deletions
diff --git a/test/golden/geometry/glossing.golden b/test/golden/geometry/glossing.golden deleted file mode 100644 index 3d097de..0000000 --- a/test/golden/geometry/glossing.golden +++ /dev/null @@ -1,2775 +0,0 @@ -[ BlockDefn - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 1 - , locColumn = 1 - } - ) - ( Marker "collinear" ) - ( DefnPredicate [] - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "collinear" ) - ( TokenCons - ( Word "with" ) - ( HoleCons - ( TokenCons - ( Word "and" ) ( HoleCons End ) - ) - ) - ) - ) - ( Marker "collinear" ) - ) - ) - ( NamedVar "a" :| - [ NamedVar "b" - , NamedVar "c" - ] - ) - ( Connected Disjunction - ( Connected Disjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 2 - , locColumn = 44 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "b" ) - , TermVar - ( NamedVar "c" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 2 - , locColumn = 64 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( NamedVar "b" ) - , TermVar - ( NamedVar "c" ) - , TermVar - ( NamedVar "a" ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 2 - , locColumn = 84 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( NamedVar "c" ) - , TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "b" ) - ] - ) - ) - ) -, BlockAxiom - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 5 - , locColumn = 1 - } - ) - ( Marker "cong_refl_swap" ) - ( Axiom - [ Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 6 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "a" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 6 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "b" ) - ] - ) - ] - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 7 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "b" ) - , TermVar - ( NamedVar "b" ) - , TermVar - ( NamedVar "a" ) - ] - ) - ) -, BlockAxiom - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 10 - , locColumn = 1 - } - ) - ( Marker "cong_pseudotransitive" ) - ( Axiom - [ Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 11 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "a" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 11 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "b" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 11 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "c" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 11 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "d" ) - ] - ) - ] - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 12 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( NamedVar "c" ) - , TermVar - ( NamedVar "d" ) - , TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "b" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 12 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( NamedVar "c" ) - , TermVar - ( NamedVar "d" ) - , TermVar - ( NamedVar "e" ) - , TermVar - ( NamedVar "f" ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 12 - , locColumn = 58 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "b" ) - , TermVar - ( NamedVar "e" ) - , TermVar - ( NamedVar "f" ) - ] - ) - ) - ) -, BlockAxiom - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 15 - , locColumn = 1 - } - ) - ( Marker "cong_id" ) - ( Axiom - [ Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 16 - , locColumn = 22 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "a" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 16 - , locColumn = 22 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "b" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 16 - , locColumn = 22 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "c" ) - ] - ) - ] - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 17 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "b" ) - , TermVar - ( NamedVar "c" ) - , TermVar - ( NamedVar "c" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 17 - , locColumn = 36 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "b" ) - ] - ) - ) - ) -, BlockAxiom - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 21 - , locColumn = 1 - } - ) - ( Marker "segment_construction" ) - ( Axiom [] - ( Quantified Existentially - ( Scope - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 22 - , locColumn = 20 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 22 - , locColumn = 41 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( NamedVar "a" ) - ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "b" ) - ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 22 - , locColumn = 62 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( F - ( TermVar - ( NamedVar "b" ) - ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "d" ) - ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "e" ) - ) - ) - ] - ) - ) - ) - ) - ) - ) -, BlockDefn - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 26 - , locColumn = 1 - } - ) - ( Marker "ofs" ) - ( DefnPredicate - [ Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "y" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "z" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "r" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "u" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "v" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "w" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "p" ) - ] - ) - ] - ( PredicateSymbol "OFS" ) - ( NamedVar "x" :| - [ NamedVar "y" - , NamedVar "z" - , NamedVar "r" - , NamedVar "u" - , NamedVar "v" - , NamedVar "w" - , NamedVar "p" - ] - ) - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 29 - , locColumn = 6 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - , TermVar - ( NamedVar "z" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 30 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( NamedVar "u" ) - , TermVar - ( NamedVar "v" ) - , TermVar - ( NamedVar "w" ) - ] - ) - ) - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 32 - , locColumn = 6 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - , TermVar - ( NamedVar "u" ) - , TermVar - ( NamedVar "v" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 33 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( NamedVar "y" ) - , TermVar - ( NamedVar "z" ) - , TermVar - ( NamedVar "v" ) - , TermVar - ( NamedVar "w" ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 34 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "r" ) - , TermVar - ( NamedVar "u" ) - , TermVar - ( NamedVar "p" ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 35 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( NamedVar "y" ) - , TermVar - ( NamedVar "r" ) - , TermVar - ( NamedVar "v" ) - , TermVar - ( NamedVar "p" ) - ] - ) - ) - ) - ) -, BlockAxiom - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 39 - , locColumn = 1 - } - ) - ( Marker "five_segment" ) - ( Axiom - [ Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "a" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "b" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "c" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "d" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "a_" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "b_" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "c_" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "d_" ) - ] - ) - ] - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 41 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "OFS" ) - ) - [ TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "b" ) - , TermVar - ( NamedVar "c" ) - , TermVar - ( NamedVar "d" ) - , TermVar - ( NamedVar "a_" ) - , TermVar - ( NamedVar "b_" ) - , TermVar - ( NamedVar "c_" ) - , TermVar - ( NamedVar "d_" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 42 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "neq" ) - ( ParameterArity 0 ) - ( Marker "neq" ) - ) - ) - ) - [ TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "b" ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 42 - , locColumn = 22 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( NamedVar "c" ) - , TermVar - ( NamedVar "d" ) - , TermVar - ( NamedVar "c_" ) - , TermVar - ( NamedVar "d_" ) - ] - ) - ) - ) -, BlockAxiom - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 46 - , locColumn = 1 - } - ) - ( Marker "betw_id" ) - ( Axiom - [ Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 47 - , locColumn = 18 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "a" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 47 - , locColumn = 18 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "b" ) - ] - ) - ] - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 48 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "b" ) - , TermVar - ( NamedVar "a" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 48 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "b" ) - ] - ) - ) - ) -, BlockAxiom - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 52 - , locColumn = 1 - } - ) - ( Marker "innerpasch" ) - ( Axiom - [ Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "y" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "z" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "u" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "v" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "w" ) - ] - ) - ] - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 54 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "u" ) - , TermVar - ( NamedVar "z" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 54 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( NamedVar "y" ) - , TermVar - ( NamedVar "v" ) - , TermVar - ( NamedVar "z" ) - ] - ) - ) - ( Quantified Existentially - ( Scope - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 54 - , locColumn = 66 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "w" ) - ) - ] - ) - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 55 - , locColumn = 16 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( NamedVar "u" ) - ) - ) - , TermVar - ( B - ( NamedVar "w" ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "y" ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 55 - , locColumn = 37 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( NamedVar "v" ) - ) - ) - , TermVar - ( B - ( NamedVar "w" ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "x" ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - ) -, BlockAxiom - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 66 - , locColumn = 1 - } - ) - ( Marker "upperdim" ) - ( Axiom - [ Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 67 - , locColumn = 24 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 67 - , locColumn = 24 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "y" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 67 - , locColumn = 24 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "z" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 67 - , locColumn = 24 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "u" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 67 - , locColumn = 24 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "v" ) - ] - ) - ] - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 68 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "u" ) - , TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "v" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 68 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( NamedVar "y" ) - , TermVar - ( NamedVar "u" ) - , TermVar - ( NamedVar "y" ) - , TermVar - ( NamedVar "v" ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 69 - , locColumn = 10 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( NamedVar "z" ) - , TermVar - ( NamedVar "u" ) - , TermVar - ( NamedVar "z" ) - , TermVar - ( NamedVar "v" ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 69 - , locColumn = 36 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "neq" ) - ( ParameterArity 0 ) - ( Marker "neq" ) - ) - ) - ) - [ TermVar - ( NamedVar "u" ) - , TermVar - ( NamedVar "v" ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 70 - , locColumn = 17 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "collinear" ) - ( TokenCons - ( Word "with" ) - ( HoleCons - ( TokenCons - ( Word "and" ) ( HoleCons End ) - ) - ) - ) - ) - ( Marker "collinear" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - , TermVar - ( NamedVar "z" ) - ] - ) - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 82 - , locColumn = 1 - } - ) - ( Marker "cong_refl" ) - ( Lemma - [ Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 83 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "a" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 83 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "b" ) - ] - ) - ] - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 84 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "b" ) - , TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "b" ) - ] - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 88 - , locColumn = 1 - } - ) - ( Marker "cong_sym" ) - ( Lemma - [ Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 89 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "a" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 89 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "b" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 89 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "c" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 89 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "d" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 90 - , locColumn = 14 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "b" ) - , TermVar - ( NamedVar "c" ) - , TermVar - ( NamedVar "d" ) - ] - ) - ] - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 91 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( NamedVar "c" ) - , TermVar - ( NamedVar "d" ) - , TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "b" ) - ] - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 95 - , locColumn = 1 - } - ) - ( Marker "cong_transitive" ) - ( Lemma - [ Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 96 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "a" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 96 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "b" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 96 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "c" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 96 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "d" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 96 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "e" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 96 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "f" ) - ] - ) - ] - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 97 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "b" ) - , TermVar - ( NamedVar "c" ) - , TermVar - ( NamedVar "d" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 97 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( NamedVar "c" ) - , TermVar - ( NamedVar "d" ) - , TermVar - ( NamedVar "e" ) - , TermVar - ( NamedVar "f" ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 98 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "b" ) - , TermVar - ( NamedVar "e" ) - , TermVar - ( NamedVar "f" ) - ] - ) - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 102 - , locColumn = 1 - } - ) - ( Marker "cong_shuffle_left" ) - ( Lemma - [ Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 103 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "a" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 103 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "b" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 103 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "c" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 103 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "d" ) - ] - ) - ] - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 104 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "b" ) - , TermVar - ( NamedVar "c" ) - , TermVar - ( NamedVar "d" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 105 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( NamedVar "b" ) - , TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "c" ) - , TermVar - ( NamedVar "d" ) - ] - ) - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 109 - , locColumn = 1 - } - ) - ( Marker "cong_shuffle_right" ) - ( Lemma - [ Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 110 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "a" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 110 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "b" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 110 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "c" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 110 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "d" ) - ] - ) - ] - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 111 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "b" ) - , TermVar - ( NamedVar "c" ) - , TermVar - ( NamedVar "d" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 112 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( NamedVar "b" ) - , TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "d" ) - , TermVar - ( NamedVar "c" ) - ] - ) - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 116 - , locColumn = 1 - } - ) - ( Marker "cong_zero" ) - ( Lemma - [ Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 117 - , locColumn = 18 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "a" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 117 - , locColumn = 18 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "b" ) - ] - ) - ] - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 118 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "b" ) - , TermVar - ( NamedVar "b" ) - ] - ) - ) -]
\ No newline at end of file |