diff options
Diffstat (limited to 'test/golden/datatype/generating tasks.golden')
| -rw-r--r-- | test/golden/datatype/generating tasks.golden | 8698 |
1 files changed, 0 insertions, 8698 deletions
diff --git a/test/golden/datatype/generating tasks.golden b/test/golden/datatype/generating tasks.golden deleted file mode 100644 index e052235..0000000 --- a/test/golden/datatype/generating tasks.golden +++ /dev/null @@ -1,8698 +0,0 @@ -[ Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "propform_propbot_intro" TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - , Hypothesis Marker "propform_propvar_intro" Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 54 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "cons" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "cons" ) NonAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 56 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 54 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - ] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ) - ) - , Hypothesis Marker "propform_propto_intro" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 7 - , locColumn = 56 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "q" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 7 - , locColumn = 78 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermVar - ( B - ( NamedVar "q" ) - ) - ] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ) - ) - , Hypothesis Marker "propform_propbot_propvar_distinct" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "neq" ) - ( ParameterArity 0 ) - ( Marker "neq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "n_rhs" ) - ) - ] - ] - ) - ) - , Hypothesis Marker "propform_propbot_propto_distinct" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "neq" ) - ( ParameterArity 0 ) - ( Marker "neq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "p_rhs" ) - ) - , TermVar - ( B - ( NamedVar "q_rhs" ) - ) - ] - ] - ) - ) - , Hypothesis Marker "propform_propvar_propto_distinct" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "neq" ) - ( ParameterArity 0 ) - ( Marker "neq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - ] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "p_rhs" ) - ) - , TermVar - ( B - ( NamedVar "q_rhs" ) - ) - ] - ] - ) - ) - , Hypothesis Marker "propform_propvar_injective" Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - ] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "n_rhs" ) - ) - ] - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - , TermVar - ( B - ( NamedVar "n_rhs" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "propform_propto_injective" Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermVar - ( B - ( NamedVar "q" ) - ) - ] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "p_rhs" ) - ) - , TermVar - ( B - ( NamedVar "q_rhs" ) - ) - ] - ] - ) - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermVar - ( B - ( NamedVar "p_rhs" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "q" ) - ) - , TermVar - ( B - ( NamedVar "q_rhs" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "propform_cases" Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ( Connected Disjunction - ( Connected Disjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - ] - ) - ( Quantified Existentially - ( Scope - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 54 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "cons" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "cons" ) NonAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 56 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 54 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - ] - ] - ) - ) - ) - ) - ) - ( Quantified Existentially - ( Scope - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 7 - , locColumn = 56 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "q" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 7 - , locColumn = 78 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermVar - ( B - ( NamedVar "q" ) - ) - ] - ] - ) - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "propform_induct" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - , TermVar - ( B - ( NamedVar "S" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 54 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "cons" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "cons" ) NonAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 56 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 54 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - ] - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "S" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ( Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "S" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "q" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "S" ) - ) - ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermVar - ( B - ( NamedVar "q" ) - ) - ] - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "S" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ( Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "S" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - ] - , taskConjectureLabel = Marker "propform_bot_test" - , taskLocation = Location - { locFile = "test/examples/datatype.tex" - , locLine = 10 - , locColumn = 1 - } - , taskConjecture = TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 11 - , locColumn = 15 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 11 - , locColumn = 6 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 11 - , locColumn = 19 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "propform_bot_test" TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 11 - , locColumn = 15 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 11 - , locColumn = 6 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 11 - , locColumn = 19 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - , Hypothesis Marker "propform_propbot_intro" TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - , Hypothesis Marker "propform_propvar_intro" Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 54 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "cons" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "cons" ) NonAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 56 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 54 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - ] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ) - ) - , Hypothesis Marker "propform_propto_intro" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 7 - , locColumn = 56 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "q" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 7 - , locColumn = 78 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermVar - ( B - ( NamedVar "q" ) - ) - ] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ) - ) - , Hypothesis Marker "propform_propbot_propvar_distinct" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "neq" ) - ( ParameterArity 0 ) - ( Marker "neq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "n_rhs" ) - ) - ] - ] - ) - ) - , Hypothesis Marker "propform_propbot_propto_distinct" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "neq" ) - ( ParameterArity 0 ) - ( Marker "neq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "p_rhs" ) - ) - , TermVar - ( B - ( NamedVar "q_rhs" ) - ) - ] - ] - ) - ) - , Hypothesis Marker "propform_propvar_propto_distinct" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "neq" ) - ( ParameterArity 0 ) - ( Marker "neq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - ] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "p_rhs" ) - ) - , TermVar - ( B - ( NamedVar "q_rhs" ) - ) - ] - ] - ) - ) - , Hypothesis Marker "propform_propvar_injective" Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - ] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "n_rhs" ) - ) - ] - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - , TermVar - ( B - ( NamedVar "n_rhs" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "propform_propto_injective" Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermVar - ( B - ( NamedVar "q" ) - ) - ] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "p_rhs" ) - ) - , TermVar - ( B - ( NamedVar "q_rhs" ) - ) - ] - ] - ) - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermVar - ( B - ( NamedVar "p_rhs" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "q" ) - ) - , TermVar - ( B - ( NamedVar "q_rhs" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "propform_cases" Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ( Connected Disjunction - ( Connected Disjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - ] - ) - ( Quantified Existentially - ( Scope - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 54 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "cons" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "cons" ) NonAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 56 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 54 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - ] - ] - ) - ) - ) - ) - ) - ( Quantified Existentially - ( Scope - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 7 - , locColumn = 56 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "q" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 7 - , locColumn = 78 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermVar - ( B - ( NamedVar "q" ) - ) - ] - ] - ) - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "propform_induct" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - , TermVar - ( B - ( NamedVar "S" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 54 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "cons" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "cons" ) NonAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 56 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 54 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - ] - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "S" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ( Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "S" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "q" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "S" ) - ) - ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermVar - ( B - ( NamedVar "q" ) - ) - ] - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "S" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ( Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "S" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - ] - , taskConjectureLabel = Marker "propform_var_test" - , taskLocation = Location - { locFile = "test/examples/datatype.tex" - , locLine = 14 - , locColumn = 1 - } - , taskConjecture = Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 9 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 23 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "cons" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "cons" ) NonAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 25 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 23 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 65 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 45 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 54 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 69 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "propform_var_test" Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 9 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 23 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "cons" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "cons" ) NonAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 25 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 23 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 65 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 45 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 54 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 69 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - , Hypothesis Marker "propform_bot_test" TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 11 - , locColumn = 15 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 11 - , locColumn = 6 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 11 - , locColumn = 19 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - , Hypothesis Marker "propform_propbot_intro" TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - , Hypothesis Marker "propform_propvar_intro" Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 54 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "cons" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "cons" ) NonAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 56 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 54 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - ] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ) - ) - , Hypothesis Marker "propform_propto_intro" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 7 - , locColumn = 56 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "q" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 7 - , locColumn = 78 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermVar - ( B - ( NamedVar "q" ) - ) - ] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ) - ) - , Hypothesis Marker "propform_propbot_propvar_distinct" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "neq" ) - ( ParameterArity 0 ) - ( Marker "neq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "n_rhs" ) - ) - ] - ] - ) - ) - , Hypothesis Marker "propform_propbot_propto_distinct" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "neq" ) - ( ParameterArity 0 ) - ( Marker "neq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "p_rhs" ) - ) - , TermVar - ( B - ( NamedVar "q_rhs" ) - ) - ] - ] - ) - ) - , Hypothesis Marker "propform_propvar_propto_distinct" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "neq" ) - ( ParameterArity 0 ) - ( Marker "neq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - ] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "p_rhs" ) - ) - , TermVar - ( B - ( NamedVar "q_rhs" ) - ) - ] - ] - ) - ) - , Hypothesis Marker "propform_propvar_injective" Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - ] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "n_rhs" ) - ) - ] - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - , TermVar - ( B - ( NamedVar "n_rhs" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "propform_propto_injective" Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermVar - ( B - ( NamedVar "q" ) - ) - ] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "p_rhs" ) - ) - , TermVar - ( B - ( NamedVar "q_rhs" ) - ) - ] - ] - ) - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermVar - ( B - ( NamedVar "p_rhs" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "q" ) - ) - , TermVar - ( B - ( NamedVar "q_rhs" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "propform_cases" Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ( Connected Disjunction - ( Connected Disjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - ] - ) - ( Quantified Existentially - ( Scope - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 54 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "cons" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "cons" ) NonAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 56 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 54 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - ] - ] - ) - ) - ) - ) - ) - ( Quantified Existentially - ( Scope - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 7 - , locColumn = 56 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "q" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 7 - , locColumn = 78 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermVar - ( B - ( NamedVar "q" ) - ) - ] - ] - ) - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "propform_induct" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - , TermVar - ( B - ( NamedVar "S" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 54 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "cons" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "cons" ) NonAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 56 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 54 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - ] - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "S" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ( Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "S" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "q" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "S" ) - ) - ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermVar - ( B - ( NamedVar "q" ) - ) - ] - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "S" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ( Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "S" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - ] - , taskConjectureLabel = Marker "propform_imp_test" - , taskLocation = Location - { locFile = "test/examples/datatype.tex" - , locLine = 18 - , locColumn = 1 - } - , taskConjecture = TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 19 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 19 - , locColumn = 7 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 19 - , locColumn = 7 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 19 - , locColumn = 24 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - ] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 19 - , locColumn = 38 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "propform_imp_test" TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 19 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 19 - , locColumn = 7 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 19 - , locColumn = 7 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 19 - , locColumn = 24 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - ] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 19 - , locColumn = 38 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - , Hypothesis Marker "propform_var_test" Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 9 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 23 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "cons" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "cons" ) NonAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 25 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 23 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 65 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 45 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 54 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 69 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - , Hypothesis Marker "propform_bot_test" TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 11 - , locColumn = 15 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 11 - , locColumn = 6 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 11 - , locColumn = 19 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - , Hypothesis Marker "propform_propbot_intro" TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - , Hypothesis Marker "propform_propvar_intro" Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 54 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "cons" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "cons" ) NonAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 56 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 54 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - ] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ) - ) - , Hypothesis Marker "propform_propto_intro" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 7 - , locColumn = 56 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "q" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 7 - , locColumn = 78 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermVar - ( B - ( NamedVar "q" ) - ) - ] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ) - ) - , Hypothesis Marker "propform_propbot_propvar_distinct" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "neq" ) - ( ParameterArity 0 ) - ( Marker "neq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "n_rhs" ) - ) - ] - ] - ) - ) - , Hypothesis Marker "propform_propbot_propto_distinct" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "neq" ) - ( ParameterArity 0 ) - ( Marker "neq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "p_rhs" ) - ) - , TermVar - ( B - ( NamedVar "q_rhs" ) - ) - ] - ] - ) - ) - , Hypothesis Marker "propform_propvar_propto_distinct" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "neq" ) - ( ParameterArity 0 ) - ( Marker "neq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - ] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "p_rhs" ) - ) - , TermVar - ( B - ( NamedVar "q_rhs" ) - ) - ] - ] - ) - ) - , Hypothesis Marker "propform_propvar_injective" Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - ] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "n_rhs" ) - ) - ] - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - , TermVar - ( B - ( NamedVar "n_rhs" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "propform_propto_injective" Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermVar - ( B - ( NamedVar "q" ) - ) - ] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "p_rhs" ) - ) - , TermVar - ( B - ( NamedVar "q_rhs" ) - ) - ] - ] - ) - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermVar - ( B - ( NamedVar "p_rhs" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "q" ) - ) - , TermVar - ( B - ( NamedVar "q_rhs" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "propform_cases" Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ( Connected Disjunction - ( Connected Disjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - ] - ) - ( Quantified Existentially - ( Scope - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 54 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "cons" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "cons" ) NonAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 56 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 54 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - ] - ] - ) - ) - ) - ) - ) - ( Quantified Existentially - ( Scope - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 7 - , locColumn = 56 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "q" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 7 - , locColumn = 78 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermVar - ( B - ( NamedVar "q" ) - ) - ] - ] - ) - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "propform_induct" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - , TermVar - ( B - ( NamedVar "S" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 54 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "cons" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "cons" ) NonAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 56 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 54 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - ] - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "S" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ( Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "S" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "q" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "S" ) - ) - ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermVar - ( B - ( NamedVar "q" ) - ) - ] - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "S" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ( Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "S" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - ] - , taskConjectureLabel = Marker "propform_distinct_test" - , taskLocation = Location - { locFile = "test/examples/datatype.tex" - , locLine = 22 - , locColumn = 1 - } - , taskConjecture = TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 23 - , locColumn = 15 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "neq" ) - ( ParameterArity 0 ) - ( Marker "neq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 23 - , locColumn = 6 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 23 - , locColumn = 21 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 23 - , locColumn = 21 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 23 - , locColumn = 38 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - ] - ] - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "propform_distinct_test" TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 23 - , locColumn = 15 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "neq" ) - ( ParameterArity 0 ) - ( Marker "neq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 23 - , locColumn = 6 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 23 - , locColumn = 21 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 23 - , locColumn = 21 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 23 - , locColumn = 38 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - ] - ] - , Hypothesis Marker "propform_imp_test" TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 19 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 19 - , locColumn = 7 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 19 - , locColumn = 7 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 19 - , locColumn = 24 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - ] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 19 - , locColumn = 38 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - , Hypothesis Marker "propform_var_test" Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 9 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 23 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "cons" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "cons" ) NonAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 25 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 23 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 65 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 45 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 54 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 69 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - , Hypothesis Marker "propform_bot_test" TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 11 - , locColumn = 15 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 11 - , locColumn = 6 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 11 - , locColumn = 19 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - , Hypothesis Marker "propform_propbot_intro" TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - , Hypothesis Marker "propform_propvar_intro" Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 54 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "cons" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "cons" ) NonAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 56 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 54 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - ] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ) - ) - , Hypothesis Marker "propform_propto_intro" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 7 - , locColumn = 56 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "q" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 7 - , locColumn = 78 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermVar - ( B - ( NamedVar "q" ) - ) - ] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ) - ) - , Hypothesis Marker "propform_propbot_propvar_distinct" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "neq" ) - ( ParameterArity 0 ) - ( Marker "neq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "n_rhs" ) - ) - ] - ] - ) - ) - , Hypothesis Marker "propform_propbot_propto_distinct" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "neq" ) - ( ParameterArity 0 ) - ( Marker "neq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "p_rhs" ) - ) - , TermVar - ( B - ( NamedVar "q_rhs" ) - ) - ] - ] - ) - ) - , Hypothesis Marker "propform_propvar_propto_distinct" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "neq" ) - ( ParameterArity 0 ) - ( Marker "neq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - ] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "p_rhs" ) - ) - , TermVar - ( B - ( NamedVar "q_rhs" ) - ) - ] - ] - ) - ) - , Hypothesis Marker "propform_propvar_injective" Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - ] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "n_rhs" ) - ) - ] - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - , TermVar - ( B - ( NamedVar "n_rhs" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "propform_propto_injective" Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermVar - ( B - ( NamedVar "q" ) - ) - ] - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "p_rhs" ) - ) - , TermVar - ( B - ( NamedVar "q_rhs" ) - ) - ] - ] - ) - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermVar - ( B - ( NamedVar "p_rhs" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "q" ) - ) - , TermVar - ( B - ( NamedVar "q_rhs" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "propform_cases" Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ( Connected Disjunction - ( Connected Disjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - ] - ) - ( Quantified Existentially - ( Scope - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 54 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "cons" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "cons" ) NonAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 56 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 54 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - ] - ] - ) - ) - ) - ) - ) - ( Quantified Existentially - ( Scope - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 7 - , locColumn = 56 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "q" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 7 - , locColumn = 78 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermVar - ( B - ( NamedVar "q" ) - ) - ] - ] - ) - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "propform_induct" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) - ) [] - , TermVar - ( B - ( NamedVar "S" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 54 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "cons" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "cons" ) NonAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 56 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 54 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "n" ) - ) - ] - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "S" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ( Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "S" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "q" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "S" ) - ) - ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - , TermVar - ( B - ( NamedVar "q" ) - ) - ] - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "S" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ( Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "S" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - ] - , taskConjectureLabel = Marker "propform_injective_test" - , taskLocation = Location - { locFile = "test/examples/datatype.tex" - , locLine = 26 - , locColumn = 1 - } - , taskConjecture = Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 27 - , locColumn = 21 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 27 - , locColumn = 9 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( NamedVar "x" ) - ] - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 27 - , locColumn = 23 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - ) - [ TermVar - ( NamedVar "y" ) - ] - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 27 - , locColumn = 45 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - ) - } -]
\ No newline at end of file |