defpred S1[ set ] means ( $1 is expression of F1() implies P1[$1] );
set X = MSVars F1();
set V = (MSVars F1()) \/ (the carrier of F1() --> {0 });
set S = F1();
set C = F1();
B0: F2() is Term of F1(),((MSVars F1()) \/ (the carrier of F1() --> {0 })) by MSAFREE3:9;
B1: for s being SortSymbol of F1()
for v being Element of ((MSVars F1()) \/ (the carrier of F1() --> {0 })) . s holds S1[ root-tree [v,s]]
proof
let s be SortSymbol of F1(); :: thesis: for v being Element of ((MSVars F1()) \/ (the carrier of F1() --> {0 })) . s holds S1[ root-tree [v,s]]
let v be Element of ((MSVars F1()) \/ (the carrier of F1() --> {0 })) . s; :: thesis: S1[ root-tree [v,s]]
set t = root-tree [v,s];
assume C1: root-tree [v,s] is expression of F1() ; :: thesis: P1[ root-tree [v,s]]
( (root-tree [v,s]) . {} = [v,s] & s in the carrier of F1() ) by TREES_4:3;
then C2: ( ((root-tree [v,s]) . {} ) `2 = s & s <> the carrier of F1() ) by MCART_1:7;
per cases ( ex x being variable st root-tree [v,s] = x -term F1() or ex c being constructor OperSymbol of F1() ex p being FinSequence of QuasiTerms F1() st
( len p = len (the_arity_of c) & root-tree [v,s] = c -trm p ) or ex a being expression of F1(), an_Adj F1() st root-tree [v,s] = (non_op F1()) term a or ex a being expression of F1(), an_Adj F1() ex q being expression of F1(), a_Type F1() st root-tree [v,s] = (ast F1()) term a,q ) by C1, Th100;
suppose ex c being constructor OperSymbol of F1() ex p being FinSequence of QuasiTerms F1() st
( len p = len (the_arity_of c) & root-tree [v,s] = c -trm p ) ; :: thesis: P1[ root-tree [v,s]]
then consider c being constructor OperSymbol of F1(), p being FinSequence of QuasiTerms F1() such that
C3: ( len p = len (the_arity_of c) & root-tree [v,s] = c -trm p ) ;
root-tree [v,s] = [c,the carrier of F1()] -tree p by C3, TERM;
then (root-tree [v,s]) . {} = [c,the carrier of F1()] by TREES_4:def 4;
hence P1[ root-tree [v,s]] by C2, MCART_1:7; :: thesis: verum
end;
suppose ex a being expression of F1(), an_Adj F1() st root-tree [v,s] = (non_op F1()) term a ; :: thesis: P1[ root-tree [v,s]]
then consider a being expression of F1(), an_Adj F1() such that
C4: root-tree [v,s] = (non_op F1()) term a ;
( the_arity_of (non_op F1()) = <*(an_Adj F1())*> & <*(an_Adj F1())*> . 1 = an_Adj F1() & len <*(an_Adj F1())*> = 1 ) by CONSTRSIGN, FINSEQ_1:57;
then root-tree [v,s] = [(non_op F1()),the carrier of F1()] -tree <*a*> by C4, TERM1;
then (root-tree [v,s]) . {} = [(non_op F1()),the carrier of F1()] by TREES_4:def 4;
hence P1[ root-tree [v,s]] by C2, MCART_1:7; :: thesis: verum
end;
suppose ex a being expression of F1(), an_Adj F1() ex q being expression of F1(), a_Type F1() st root-tree [v,s] = (ast F1()) term a,q ; :: thesis: P1[ root-tree [v,s]]
then consider a being expression of F1(), an_Adj F1(), q being expression of F1(), a_Type F1() such that
C5: root-tree [v,s] = (ast F1()) term a,q ;
( the_arity_of (ast F1()) = <*(an_Adj F1()),(a_Type F1())*> & <*(an_Adj F1()),(a_Type F1())*> . 1 = an_Adj F1() & <*(an_Adj F1()),(a_Type F1())*> . 2 = a_Type F1() & len <*(an_Adj F1()),(a_Type F1())*> = 2 ) by CONSTRSIGN, FINSEQ_1:61;
then root-tree [v,s] = [(ast F1()),the carrier of F1()] -tree <*a,q*> by C5, TERM2;
then (root-tree [v,s]) . {} = [(ast F1()),the carrier of F1()] by TREES_4:def 4;
hence P1[ root-tree [v,s]] by C2, MCART_1:7; :: thesis: verum
end;
end;
end;
B2: for o being OperSymbol of F1()
for p being ArgumentSeq of Sym o,((MSVars F1()) \/ (the carrier of F1() --> {0 })) st ( for t being Term of F1(),((MSVars F1()) \/ (the carrier of F1() --> {0 })) st t in rng p holds
S1[t] ) holds
S1[[o,the carrier of F1()] -tree p]
proof
let o be OperSymbol of F1(); :: thesis: for p being ArgumentSeq of Sym o,((MSVars F1()) \/ (the carrier of F1() --> {0 })) st ( for t being Term of F1(),((MSVars F1()) \/ (the carrier of F1() --> {0 })) st t in rng p holds
S1[t] ) holds
S1[[o,the carrier of F1()] -tree p]
let p be ArgumentSeq of Sym o,((MSVars F1()) \/ (the carrier of F1() --> {0 })); :: thesis: ( ( for t being Term of F1(),((MSVars F1()) \/ (the carrier of F1() --> {0 })) st t in rng p holds
S1[t] ) implies S1[[o,the carrier of F1()] -tree p] )
assume Z0: for t being Term of F1(),((MSVars F1()) \/ (the carrier of F1() --> {0 })) st t in rng p holds
S1[t] ; :: thesis: S1[[o,the carrier of F1()] -tree p]
set t = [o,the carrier of F1()] -tree p;
assume C1: [o,the carrier of F1()] -tree p is expression of F1() ; :: thesis: P1[[o,the carrier of F1()] -tree p]
per cases ( ex x being variable st [o,the carrier of F1()] -tree p = x -term F1() or ex c being constructor OperSymbol of F1() ex p being FinSequence of QuasiTerms F1() st
( len p = len (the_arity_of c) & [o,the carrier of F1()] -tree p = c -trm p ) or ex a being expression of F1(), an_Adj F1() st [o,the carrier of F1()] -tree p = (non_op F1()) term a or ex a being expression of F1(), an_Adj F1() ex q being expression of F1(), a_Type F1() st [o,the carrier of F1()] -tree p = (ast F1()) term a,q ) by C1, Th100;
suppose ex x being variable st [o,the carrier of F1()] -tree p = x -term F1() ; :: thesis: P1[[o,the carrier of F1()] -tree p]
hence P1[[o,the carrier of F1()] -tree p] by W1; :: thesis: verum
end;
suppose ex c being constructor OperSymbol of F1() ex p being FinSequence of QuasiTerms F1() st
( len p = len (the_arity_of c) & [o,the carrier of F1()] -tree p = c -trm p ) ; :: thesis: P1[[o,the carrier of F1()] -tree p]
then consider c being constructor OperSymbol of F1(), q being FinSequence of QuasiTerms F1() such that
C3: ( len q = len (the_arity_of c) & [o,the carrier of F1()] -tree p = c -trm q ) ;
[o,the carrier of F1()] -tree p = [c,the carrier of F1()] -tree q by C3, TERM;
then C4: p = q by TREES_4:15;
now
let t be quasi-term of F1(); :: thesis: ( t in rng q implies P1[t] )
t is Term of F1(),((MSVars F1()) \/ (the carrier of F1() --> {0 })) by MSAFREE3:9;
hence ( t in rng q implies P1[t] ) by Z0, C4; :: thesis: verum
end;
hence P1[[o,the carrier of F1()] -tree p] by C3, W2; :: thesis: verum
end;
suppose ex a being expression of F1(), an_Adj F1() st [o,the carrier of F1()] -tree p = (non_op F1()) term a ; :: thesis: P1[[o,the carrier of F1()] -tree p]
then consider a being expression of F1(), an_Adj F1() such that
C4: [o,the carrier of F1()] -tree p = (non_op F1()) term a ;
( the_arity_of (non_op F1()) = <*(an_Adj F1())*> & <*(an_Adj F1())*> . 1 = an_Adj F1() & len <*(an_Adj F1())*> = 1 ) by CONSTRSIGN, FINSEQ_1:57;
then [o,the carrier of F1()] -tree p = [(non_op F1()),the carrier of F1()] -tree <*a*> by C4, TERM1;
then 00: p = <*a*> by TREES_4:15;
( rng <*a*> = {a} & a in {a} & a is Term of F1(),((MSVars F1()) \/ (the carrier of F1() --> {0 })) ) by FINSEQ_1:56, MSAFREE3:9, TARSKI:def 1;
hence P1[[o,the carrier of F1()] -tree p] by C4, W3, 00, Z0; :: thesis: verum
end;
suppose ex a being expression of F1(), an_Adj F1() ex q being expression of F1(), a_Type F1() st [o,the carrier of F1()] -tree p = (ast F1()) term a,q ; :: thesis: P1[[o,the carrier of F1()] -tree p]
then consider a being expression of F1(), an_Adj F1(), q being expression of F1(), a_Type F1() such that
C5: [o,the carrier of F1()] -tree p = (ast F1()) term a,q ;
( the_arity_of (ast F1()) = <*(an_Adj F1()),(a_Type F1())*> & <*(an_Adj F1()),(a_Type F1())*> . 1 = an_Adj F1() & <*(an_Adj F1()),(a_Type F1())*> . 2 = a_Type F1() & len <*(an_Adj F1()),(a_Type F1())*> = 2 ) by CONSTRSIGN, FINSEQ_1:61;
then [o,the carrier of F1()] -tree p = [(ast F1()),the carrier of F1()] -tree <*a,q*> by C5, TERM2;
then 00: p = <*a,q*> by TREES_4:15;
( rng <*a,q*> = {a,q} & a in {a,q} & q in {a,q} & a is Term of F1(),((MSVars F1()) \/ (the carrier of F1() --> {0 })) & q is Term of F1(),((MSVars F1()) \/ (the carrier of F1() --> {0 })) ) by FINSEQ_2:147, MSAFREE3:9, TARSKI:def 2;
then ( P1[a] & P1[q] ) by 00, Z0;
hence P1[[o,the carrier of F1()] -tree p] by C5, W4; :: thesis: verum
end;
end;
end;
for t being Term of F1(),((MSVars F1()) \/ (the carrier of F1() --> {0 })) holds S1[t] from MSATERM:sch 1(B1, B2);
 hence P1[F2()] by B0; :: thesis: verum