let C be initialized ConstructorSignature; :: thesis: for c being constructor OperSymbol of C
for p being DTree-yielding FinSequence holds
( [c, the carrier of C] -tree p is expression of C iff ( len p = len (the_arity_of c) & p in (QuasiTerms C) * ) )
let c be constructor OperSymbol of C; :: thesis: for p being DTree-yielding FinSequence holds
( [c, the carrier of C] -tree p is expression of C iff ( len p = len (the_arity_of c) & p in (QuasiTerms C) * ) )
set o = c;
A1: c <> * by Def11;
A2: c <> non_op by Def11;
let p be DTree-yielding FinSequence; :: thesis: ( [c, the carrier of C] -tree p is expression of C iff ( len p = len (the_arity_of c) & p in (QuasiTerms C) * ) )
set V = (MSVars C) (\/) ( the carrier of C --> {0});
A3: the Sorts of (Free (C,(MSVars C))) = C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0}))) by MSAFREE3:24;
hereby :: thesis: ( len p = len (the_arity_of c) & p in (QuasiTerms C) * implies [c, the carrier of C] -tree p is expression of C )
assume A4: [c, the carrier of C] -tree p is expression of C ; :: thesis: ( len p = len (the_arity_of c) & p in (QuasiTerms C) * )
then A5: [c, the carrier of C] -tree p is Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) by MSAFREE3:8;
then A6: p is ArgumentSeq of Sym (c,((MSVars C) (\/) ( the carrier of C --> {0}))) by MSATERM:1;
hence len p = len (the_arity_of c) by MSATERM:22; :: thesis: p in (QuasiTerms C) *
reconsider q = p as ArgumentSeq of Sym (c,((MSVars C) (\/) ( the carrier of C --> {0}))) by A5, MSATERM:1;
A7: the_sort_of ((Sym (c,((MSVars C) (\/) ( the carrier of C --> {0})))) -tree q) = the_result_sort_of c by MSATERM:20;
A8: variables_in ((Sym (c,((MSVars C) (\/) ( the carrier of C --> {0})))) -tree q) c= MSVars C by A4, MSAFREE3:27;
(C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0})))) . (the_result_sort_of c) = { t where t is Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) : ( the_sort_of t = the_result_sort_of c & variables_in t c= MSVars C ) } by MSAFREE3:def 5;
then (Sym (c,((MSVars C) (\/) ( the carrier of C --> {0})))) -tree p in (C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0})))) . (the_result_sort_of c) by A7, A8;
then A9: rng p c= Union (C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0})))) by A6, MSAFREE3:19;
rng p c= QuasiTerms C
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng p or a in QuasiTerms C )
assume A10: a in rng p ; :: thesis: a in QuasiTerms C
then reconsider ta = a as expression of C by A9, MSAFREE3:24;
consider i being object such that
A11: i in dom p and
A12: a = p . i by A10, FUNCT_1:def 3;
reconsider i = i as Nat by A11;
reconsider t = p . i as Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) by A6, A11, MSATERM:22;
A13: the Arity of C . c in {a_Term} * by A1, A2, Def9;
A14: dom p = dom (the_arity_of c) by A6, MSATERM:22;
A15: the_arity_of c is FinSequence of {a_Term} by A13, FINSEQ_1:def 11;
A16: (the_arity_of c) . i in rng (the_arity_of c) by A11, A14, FUNCT_1:def 3;
rng (the_arity_of c) c= {(a_Term C)} by A15, FINSEQ_1:def 4;
then (the_arity_of c) . i = a_Term C by A16, TARSKI:def 1;
then A17: the_sort_of t = a_Term C by A6, A11, MSATERM:23;
t = ta by A12;
then variables_in t c= MSVars C by MSAFREE3:27;
then t in { T where T is Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) : ( the_sort_of T = a_Term C & variables_in T c= MSVars C ) } by A17;
then t in (C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0})))) . (a_Term C) by MSAFREE3:def 5;
hence a in QuasiTerms C by A12, MSAFREE3:23; :: thesis: verum
end;
then p is FinSequence of QuasiTerms C by FINSEQ_1:def 4;
hence p in (QuasiTerms C) * by FINSEQ_1:def 11; :: thesis: verum
end;
assume A18: len p = len (the_arity_of c) ; :: thesis: ( not p in (QuasiTerms C) * or [c, the carrier of C] -tree p is expression of C )
assume A19: p in (QuasiTerms C) * ; :: thesis: [c, the carrier of C] -tree p is expression of C
Free (C,(MSVars C)) = (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) | (C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0})))) by MSAFREE3:25;
then the Sorts of (Free (C,(MSVars C))) is ManySortedSubset of the Sorts of (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) by MSUALG_2:def 9;
then the Sorts of (Free (C,(MSVars C))) c= the Sorts of (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) by PBOOLE:def 18;
then A20: QuasiTerms C c= the Sorts of (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) . (a_Term C) ;
A21: p is FinSequence of QuasiTerms C by A19, FINSEQ_1:def 11;
then A22: rng p c= QuasiTerms C by FINSEQ_1:def 4;
now :: thesis: for i being Nat st i in dom p holds
ex T being Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) st
( T = p . i & the_sort_of T = (the_arity_of c) . i )
let i be Nat; :: thesis: ( i in dom p implies ex T being Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) st
( T = p . i & the_sort_of T = (the_arity_of c) . i ) )
assume A23: i in dom p ; :: thesis: ex T being Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) st
( T = p . i & the_sort_of T = (the_arity_of c) . i )
then p . i in rng p by FUNCT_1:def 3;
then A24: p . i in QuasiTerms C by A22;
then reconsider t = p . i as expression of C ;
A25: the Arity of C . c in {a_Term} * by A1, A2, Def9;
A26: dom p = dom (the_arity_of c) by A18, FINSEQ_3:29;
A27: the_arity_of c is FinSequence of {a_Term} by A25, FINSEQ_1:def 11;
A28: (the_arity_of c) . i in rng (the_arity_of c) by A23, A26, FUNCT_1:def 3;
rng (the_arity_of c) c= {(a_Term C)} by A27, FINSEQ_1:def 4;
then A29: (the_arity_of c) . i = a_Term C by A28, TARSKI:def 1;
reconsider T = t as Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) by MSAFREE3:8;
take T = T; :: thesis: ( T = p . i & the_sort_of T = (the_arity_of c) . i )
thus T = p . i ; :: thesis: the_sort_of T = (the_arity_of c) . i
T in the Sorts of (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) . (a_Term C) by A20, A24;
then T in FreeSort (((MSVars C) (\/) ( the carrier of C --> {0})),(a_Term C)) by MSAFREE:def 11;
hence the_sort_of T = (the_arity_of c) . i by A29, MSATERM:def 5; :: thesis: verum
end;
then A30: p is ArgumentSeq of Sym (c,((MSVars C) (\/) ( the carrier of C --> {0}))) by A18, MSATERM:24;
A31: dom the Sorts of (Free (C,(MSVars C))) = the carrier of C by PARTFUN1:def 2;
rng p c= Union (C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0})))) by A3, A21, FINSEQ_1:def 4;
then (Sym (c,((MSVars C) (\/) ( the carrier of C --> {0})))) -tree p in (C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0})))) . (the_result_sort_of c) by A30, MSAFREE3:19;
hence [c, the carrier of C] -tree p is expression of C by A3, A31, CARD_5:2; :: thesis: verum