let C be initialized ConstructorSignature; :: thesis: for o being OperSymbol of C st len (the_arity_of o) = 2 holds
for a, b being expression of C st ex s1, s2 being SortSymbol of C st
( s1 = (the_arity_of o) . 1 & s2 = (the_arity_of o) . 2 & a is expression of C,s1 & b is expression of C,s2 ) holds
[o, the carrier of C] -tree <*a,b*> is expression of C, the_result_sort_of o
let o be OperSymbol of C; :: thesis: ( len (the_arity_of o) = 2 implies for a, b being expression of C st ex s1, s2 being SortSymbol of C st
( s1 = (the_arity_of o) . 1 & s2 = (the_arity_of o) . 2 & a is expression of C,s1 & b is expression of C,s2 ) holds
[o, the carrier of C] -tree <*a,b*> is expression of C, the_result_sort_of o )
assume A1: len (the_arity_of o) = 2 ; :: thesis: for a, b being expression of C st ex s1, s2 being SortSymbol of C st
( s1 = (the_arity_of o) . 1 & s2 = (the_arity_of o) . 2 & a is expression of C,s1 & b is expression of C,s2 ) holds
[o, the carrier of C] -tree <*a,b*> is expression of C, the_result_sort_of o
set X = MSVars C;
set Y = (MSVars C) (\/) ( the carrier of C --> {0});
let a, b be expression of C; :: thesis: ( ex s1, s2 being SortSymbol of C st
( s1 = (the_arity_of o) . 1 & s2 = (the_arity_of o) . 2 & a is expression of C,s1 & b is expression of C,s2 ) implies [o, the carrier of C] -tree <*a,b*> is expression of C, the_result_sort_of o )
given s1, s2 being SortSymbol of C such that A2: s1 = (the_arity_of o) . 1 and
A3: s2 = (the_arity_of o) . 2 and
A4: a is expression of C,s1 and
A5: b is expression of C,s2 ; :: thesis: [o, the carrier of C] -tree <*a,b*> is expression of C, the_result_sort_of o
reconsider ta = a, tb = b as Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) by MSAFREE3:8;
A6: dom <*ta,tb*> = Seg 2 by FINSEQ_1:89;
A7: dom <*s1,s2*> = Seg 2 by FINSEQ_1:89;
A8: the_arity_of o = <*s1,s2*> by A1, A2, A3, FINSEQ_1:44;
A9: the Sorts of (Free (C,(MSVars C))) = C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0}))) by MSAFREE3:24;
now :: thesis: for i being Nat st i in dom <*ta,tb*> holds
for t being Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) st t = <*ta,tb*> . i holds
the_sort_of t = (the_arity_of o) . i
let i be Nat; :: thesis: ( i in dom <*ta,tb*> implies for t being Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) st t = <*ta,tb*> . i holds
the_sort_of t = (the_arity_of o) . i )
assume i in dom <*ta,tb*> ; :: thesis: for t being Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) st t = <*ta,tb*> . i holds
the_sort_of t = (the_arity_of o) . i
then A10: ( i = 1 or i = 2 ) by A6, FINSEQ_1:2, TARSKI:def 2;
let t be Term of C,((MSVars C) (\/) ( the carrier of C --> {0})); :: thesis: ( t = <*ta,tb*> . i implies the_sort_of t = (the_arity_of o) . i )
assume A11: t = <*ta,tb*> . i ; :: thesis: the_sort_of t = (the_arity_of o) . i
A12: the Sorts of (Free (C,(MSVars C))) c= the Sorts of (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) by A9, PBOOLE:def 18;
A13: ( ( i = 1 & t = a ) or ( i = 2 & t = b ) ) by A10, A11, FINSEQ_1:44;
A14: the Sorts of (Free (C,(MSVars C))) . s1 c= the Sorts of (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) . s1 by A12;
A15: the Sorts of (Free (C,(MSVars C))) . s2 c= the Sorts of (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) . s2 by A12;
( ( i = 1 & t in the Sorts of (Free (C,(MSVars C))) . s1 ) or ( i = 2 & t in the Sorts of (Free (C,(MSVars C))) . s2 ) ) by A4, A5, A13, Th41;
hence the_sort_of t = (the_arity_of o) . i by A2, A3, A14, A15, MSAFREE3:7; :: thesis: verum
end;
then reconsider p = <*ta,tb*> as ArgumentSeq of Sym (o,((MSVars C) (\/) ( the carrier of C --> {0}))) by A6, A7, A8, MSATERM:25;
A16: variables_in ((Sym (o,((MSVars C) (\/) ( the carrier of C --> {0})))) -tree p) c= MSVars C
proof
let s be object ; :: according to PBOOLE:def 2 :: thesis: ( not s in the carrier of C or (variables_in ((Sym (o,((MSVars C) (\/) ( the carrier of C --> {0})))) -tree p)) . s c= (MSVars C) . s )
assume s in the carrier of C ; :: thesis: (variables_in ((Sym (o,((MSVars C) (\/) ( the carrier of C --> {0})))) -tree p)) . s c= (MSVars C) . s
then reconsider s9 = s as SortSymbol of C ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (variables_in ((Sym (o,((MSVars C) (\/) ( the carrier of C --> {0})))) -tree p)) . s or x in (MSVars C) . s )
assume x in (variables_in ((Sym (o,((MSVars C) (\/) ( the carrier of C --> {0})))) -tree p)) . s ; :: thesis: x in (MSVars C) . s
then consider t being DecoratedTree such that
A17: t in rng p and
A18: x in (C variables_in t) . s9 by MSAFREE3:11;
A19: C variables_in a c= MSVars C by MSAFREE3:27;
A20: C variables_in b c= MSVars C by MSAFREE3:27;
A21: rng p = {a,b} by FINSEQ_2:127;
A22: (C variables_in a) . s9 c= (MSVars C) . s9 by A19;
A23: (C variables_in b) . s9 c= (MSVars C) . s9 by A20;
( t = a or t = b ) by A17, A21, TARSKI:def 2;
hence x in (MSVars C) . s by A18, A22, A23; :: thesis: verum
end;
set s9 = the_result_sort_of o;
A24: the_sort_of ((Sym (o,((MSVars C) (\/) ( the carrier of C --> {0})))) -tree p) = the_result_sort_of o by MSATERM:20;
the Sorts of (Free (C,(MSVars C))) . (the_result_sort_of o) = { t where t is Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) : ( the_sort_of t = the_result_sort_of o & variables_in t c= MSVars C ) } by A9, MSAFREE3:def 5;
then [o, the carrier of C] -tree <*a,b*> in the Sorts of (Free (C,(MSVars C))) . (the_result_sort_of o) by A16, A24;
hence [o, the carrier of C] -tree <*a,b*> is expression of C, the_result_sort_of o by Th41; :: thesis: verum