diff options
Diffstat (limited to 'test/golden/datatype')
| -rw-r--r-- | test/golden/datatype/encoding tasks.golden | 69 | ||||
| -rw-r--r-- | test/golden/datatype/generating tasks.golden | 8698 | ||||
| -rw-r--r-- | test/golden/datatype/glossing.golden | 656 | ||||
| -rw-r--r-- | test/golden/datatype/verification.golden | 11 |
4 files changed, 0 insertions, 9434 deletions
diff --git a/test/golden/datatype/encoding tasks.golden b/test/golden/datatype/encoding tasks.golden deleted file mode 100644 index 5be38a4..0000000 --- a/test/golden/datatype/encoding tasks.golden +++ /dev/null @@ -1,69 +0,0 @@ -fof(zf_q0,conjecture,zf_u6(zf_u3,zf_u4)). -fof(zf_h0,axiom,![V0,V1,V2,V3]:(zf_u0(V0,V1)=zf_u0(V2,V3)=>(V0=V2&V1=V3))). -fof(zf_h1,axiom,![V4,V5,V6]:zf_u5(V4)!=zf_u0(V5,V6)). -fof(zf_h2,axiom,![V7,V8]:((zf_u6(V7,zf_u4)&zf_u6(V8,zf_u4))=>zf_u6(zf_u0(V7,V8),zf_u4))). -fof(zf_h3,axiom,![V9,V10]:(zf_u5(V9)=zf_u5(V10)=>V9=V10)). -fof(zf_h4,axiom,![V11,V12]:zf_u3!=zf_u0(V11,V12)). -fof(zf_h5,axiom,![V13]:((zf_u6(zf_u3,V13)&![V14]:(zf_u6(V14,zf_u1(zf_u2,zf_u2))=>zf_u6(zf_u5(V14),V13))&![V15,V16]:((zf_u6(V15,V13)&zf_u6(V16,V13))=>zf_u6(zf_u0(V15,V16),V13)))=>![V17]:(zf_u6(V17,zf_u4)=>zf_u6(V17,V13)))). -fof(zf_h6,axiom,![V18]:(zf_u6(V18,zf_u1(zf_u2,zf_u2))=>zf_u6(zf_u5(V18),zf_u4))). -fof(zf_h7,axiom,![V19]:(zf_u6(V19,zf_u4)=>(V19=zf_u3|?[V20]:(zf_u6(V20,zf_u1(zf_u2,zf_u2))&V19=zf_u5(V20))|?[V21,V22]:(zf_u6(V21,zf_u4)&zf_u6(V22,zf_u4)&V19=zf_u0(V21,V22))))). -fof(zf_h8,axiom,![V23]:zf_u3!=zf_u5(V23)). -fof(zf_h9,axiom,zf_u6(zf_u3,zf_u4)). ------------------- -fof(zf_q0,conjecture,zf_u6(zf_u2,zf_u1(zf_u2,zf_u2))=>zf_u6(zf_u5(zf_u2),zf_u4)). -fof(zf_h0,axiom,![V0,V1,V2,V3]:(zf_u0(V0,V1)=zf_u0(V2,V3)=>(V0=V2&V1=V3))). -fof(zf_h1,axiom,![V4,V5,V6]:zf_u5(V4)!=zf_u0(V5,V6)). -fof(zf_h2,axiom,![V7,V8]:((zf_u6(V7,zf_u4)&zf_u6(V8,zf_u4))=>zf_u6(zf_u0(V7,V8),zf_u4))). -fof(zf_h3,axiom,![V9,V10]:(zf_u5(V9)=zf_u5(V10)=>V9=V10)). -fof(zf_h4,axiom,![V11,V12]:zf_u3!=zf_u0(V11,V12)). -fof(zf_h5,axiom,![V13]:((zf_u6(zf_u3,V13)&![V14]:(zf_u6(V14,zf_u1(zf_u2,zf_u2))=>zf_u6(zf_u5(V14),V13))&![V15,V16]:((zf_u6(V15,V13)&zf_u6(V16,V13))=>zf_u6(zf_u0(V15,V16),V13)))=>![V17]:(zf_u6(V17,zf_u4)=>zf_u6(V17,V13)))). -fof(zf_h6,axiom,![V18]:(zf_u6(V18,zf_u1(zf_u2,zf_u2))=>zf_u6(zf_u5(V18),zf_u4))). -fof(zf_h7,axiom,![V19]:(zf_u6(V19,zf_u4)=>(V19=zf_u3|?[V20]:(zf_u6(V20,zf_u1(zf_u2,zf_u2))&V19=zf_u5(V20))|?[V21,V22]:(zf_u6(V21,zf_u4)&zf_u6(V22,zf_u4)&V19=zf_u0(V21,V22))))). -fof(zf_h8,axiom,![V23]:zf_u3!=zf_u5(V23)). -fof(zf_h9,axiom,zf_u6(zf_u3,zf_u4)). -fof(zf_h10,axiom,zf_u6(zf_u3,zf_u4)). ------------------- -fof(zf_q0,conjecture,zf_u6(zf_u0(zf_u3,zf_u3),zf_u4)). -fof(zf_h0,axiom,![V0,V1,V2,V3]:(zf_u0(V0,V1)=zf_u0(V2,V3)=>(V0=V2&V1=V3))). -fof(zf_h1,axiom,![V4,V5,V6]:zf_u5(V4)!=zf_u0(V5,V6)). -fof(zf_h2,axiom,![V7,V8]:((zf_u6(V7,zf_u4)&zf_u6(V8,zf_u4))=>zf_u6(zf_u0(V7,V8),zf_u4))). -fof(zf_h3,axiom,![V9,V10]:(zf_u5(V9)=zf_u5(V10)=>V9=V10)). -fof(zf_h4,axiom,![V11,V12]:zf_u3!=zf_u0(V11,V12)). -fof(zf_h5,axiom,![V13]:((zf_u6(zf_u3,V13)&![V14]:(zf_u6(V14,zf_u1(zf_u2,zf_u2))=>zf_u6(zf_u5(V14),V13))&![V15,V16]:((zf_u6(V15,V13)&zf_u6(V16,V13))=>zf_u6(zf_u0(V15,V16),V13)))=>![V17]:(zf_u6(V17,zf_u4)=>zf_u6(V17,V13)))). -fof(zf_h6,axiom,![V18]:(zf_u6(V18,zf_u1(zf_u2,zf_u2))=>zf_u6(zf_u5(V18),zf_u4))). -fof(zf_h7,axiom,![V19]:(zf_u6(V19,zf_u4)=>(V19=zf_u3|?[V20]:(zf_u6(V20,zf_u1(zf_u2,zf_u2))&V19=zf_u5(V20))|?[V21,V22]:(zf_u6(V21,zf_u4)&zf_u6(V22,zf_u4)&V19=zf_u0(V21,V22))))). -fof(zf_h8,axiom,![V23]:zf_u3!=zf_u5(V23)). -fof(zf_h9,axiom,zf_u6(zf_u2,zf_u1(zf_u2,zf_u2))=>zf_u6(zf_u5(zf_u2),zf_u4)). -fof(zf_h10,axiom,zf_u6(zf_u3,zf_u4)). -fof(zf_h11,axiom,zf_u6(zf_u3,zf_u4)). ------------------- -fof(zf_q0,conjecture,zf_u3!=zf_u0(zf_u3,zf_u3)). -fof(zf_h0,axiom,![V0,V1,V2,V3]:(zf_u0(V0,V1)=zf_u0(V2,V3)=>(V0=V2&V1=V3))). -fof(zf_h1,axiom,![V4,V5,V6]:zf_u5(V4)!=zf_u0(V5,V6)). -fof(zf_h2,axiom,![V7,V8]:((zf_u6(V7,zf_u4)&zf_u6(V8,zf_u4))=>zf_u6(zf_u0(V7,V8),zf_u4))). -fof(zf_h3,axiom,![V9,V10]:(zf_u5(V9)=zf_u5(V10)=>V9=V10)). -fof(zf_h4,axiom,![V11,V12]:zf_u3!=zf_u0(V11,V12)). -fof(zf_h5,axiom,![V13]:((zf_u6(zf_u3,V13)&![V14]:(zf_u6(V14,zf_u1(zf_u2,zf_u2))=>zf_u6(zf_u5(V14),V13))&![V15,V16]:((zf_u6(V15,V13)&zf_u6(V16,V13))=>zf_u6(zf_u0(V15,V16),V13)))=>![V17]:(zf_u6(V17,zf_u4)=>zf_u6(V17,V13)))). -fof(zf_h6,axiom,![V18]:(zf_u6(V18,zf_u1(zf_u2,zf_u2))=>zf_u6(zf_u5(V18),zf_u4))). -fof(zf_h7,axiom,![V19]:(zf_u6(V19,zf_u4)=>(V19=zf_u3|?[V20]:(zf_u6(V20,zf_u1(zf_u2,zf_u2))&V19=zf_u5(V20))|?[V21,V22]:(zf_u6(V21,zf_u4)&zf_u6(V22,zf_u4)&V19=zf_u0(V21,V22))))). -fof(zf_h8,axiom,![V23]:zf_u3!=zf_u5(V23)). -fof(zf_h9,axiom,zf_u6(zf_u0(zf_u3,zf_u3),zf_u4)). -fof(zf_h10,axiom,zf_u6(zf_u2,zf_u1(zf_u2,zf_u2))=>zf_u6(zf_u5(zf_u2),zf_u4)). -fof(zf_h11,axiom,zf_u6(zf_u3,zf_u4)). -fof(zf_h12,axiom,zf_u6(zf_u3,zf_u4)). ------------------- -fof(zf_q0,conjecture,zf_u5(zf_f0)=zf_u5(zf_f1)=>zf_f0=zf_f1). -fof(zf_h0,axiom,![V0,V1,V2,V3]:(zf_u0(V0,V1)=zf_u0(V2,V3)=>(V0=V2&V1=V3))). -fof(zf_h1,axiom,![V4,V5,V6]:zf_u5(V4)!=zf_u0(V5,V6)). -fof(zf_h2,axiom,![V7,V8]:((zf_u6(V7,zf_u4)&zf_u6(V8,zf_u4))=>zf_u6(zf_u0(V7,V8),zf_u4))). -fof(zf_h3,axiom,![V9,V10]:(zf_u5(V9)=zf_u5(V10)=>V9=V10)). -fof(zf_h4,axiom,![V11,V12]:zf_u3!=zf_u0(V11,V12)). -fof(zf_h5,axiom,![V13]:((zf_u6(zf_u3,V13)&![V14]:(zf_u6(V14,zf_u1(zf_u2,zf_u2))=>zf_u6(zf_u5(V14),V13))&![V15,V16]:((zf_u6(V15,V13)&zf_u6(V16,V13))=>zf_u6(zf_u0(V15,V16),V13)))=>![V17]:(zf_u6(V17,zf_u4)=>zf_u6(V17,V13)))). -fof(zf_h6,axiom,![V18]:(zf_u6(V18,zf_u1(zf_u2,zf_u2))=>zf_u6(zf_u5(V18),zf_u4))). -fof(zf_h7,axiom,![V19]:(zf_u6(V19,zf_u4)=>(V19=zf_u3|?[V20]:(zf_u6(V20,zf_u1(zf_u2,zf_u2))&V19=zf_u5(V20))|?[V21,V22]:(zf_u6(V21,zf_u4)&zf_u6(V22,zf_u4)&V19=zf_u0(V21,V22))))). -fof(zf_h8,axiom,![V23]:zf_u3!=zf_u5(V23)). -fof(zf_h9,axiom,zf_u3!=zf_u0(zf_u3,zf_u3)). -fof(zf_h10,axiom,zf_u6(zf_u0(zf_u3,zf_u3),zf_u4)). -fof(zf_h11,axiom,zf_u6(zf_u2,zf_u1(zf_u2,zf_u2))=>zf_u6(zf_u5(zf_u2),zf_u4)). -fof(zf_h12,axiom,zf_u6(zf_u3,zf_u4)). -fof(zf_h13,axiom,zf_u6(zf_u3,zf_u4)).
\ No newline at end of file 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 diff --git a/test/golden/datatype/glossing.golden b/test/golden/datatype/glossing.golden deleted file mode 100644 index c9c52b8..0000000 --- a/test/golden/datatype/glossing.golden +++ /dev/null @@ -1,656 +0,0 @@ -[ BlockData - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 1 - , locColumn = 1 - } - ) - ( Marker "propform" ) - ( Datatype - { datatypeHead = SymbolPattern - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) [] - , datatypeClauses = DatatypeClause - { datatypeClauseConstructor = SymbolPattern - ( MixfixItem - ( TokenCons - ( Command "propbot" ) End - ) - ( Marker "propbot" ) NonAssoc - ) [] - , datatypeClausePremises = [] - } :| - [ DatatypeClause - { datatypeClauseConstructor = SymbolPattern - ( MixfixItem - ( TokenCons - ( Command "propvar" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "propvar" ) NonAssoc - ) - [ NamedVar "n" ] - , datatypeClausePremises = - [ - ( 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 - ) - ) [] - ] - ) - ] - } - , DatatypeClause - { datatypeClauseConstructor = SymbolPattern - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "propto" ) ( HoleCons End ) - ) - ) - ( Marker "propto" ) RightAssoc - ) - [ NamedVar "p" - , NamedVar "q" - ] - , datatypeClausePremises = - [ - ( NamedVar "p" - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 7 - , locColumn = 56 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ) - , - ( NamedVar "q" - , TermSymbol - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 7 - , locColumn = 78 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "propform" ) End - ) - ( Marker "propform" ) NonAssoc - ) - ) [] - ) - ] - } - ] - } - ) -, BlockLemma - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 10 - , locColumn = 1 - } - ) - ( Marker "propform_bot_test" ) - ( Lemma [] - ( 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 - ) - ) [] - ] - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 14 - , locColumn = 1 - } - ) - ( Marker "propform_var_test" ) - ( Lemma [] - ( 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 - ) - ) [] - ] - ) - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 18 - , locColumn = 1 - } - ) - ( Marker "propform_imp_test" ) - ( Lemma [] - ( 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 - ) - ) [] - ] - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 22 - , locColumn = 1 - } - ) - ( Marker "propform_distinct_test" ) - ( Lemma [] - ( 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 - ) - ) [] - ] - ] - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/datatype.tex" - , locLine = 26 - , locColumn = 1 - } - ) - ( Marker "propform_injective_test" ) - ( Lemma [] - ( 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 diff --git a/test/golden/datatype/verification.golden b/test/golden/datatype/verification.golden deleted file mode 100644 index f5e656e..0000000 --- a/test/golden/datatype/verification.golden +++ /dev/null @@ -1,11 +0,0 @@ -VerifiedWithTrustedVampire - ( VerificationReport - { verificationRoute = LegacyVerificationRoute - , verificationLegacyDeclaredAssumptionCount = 0 - , verificationTypedDeclaredAssumptionCount = 0 - , verificationTrustedVampireCount = 5 - , verificationExplicitGapLocations = [] - , verificationTrustedLegacyRuleCount = 10 - , verificationKernelProofCount = 0 - } - )
\ No newline at end of file |