let S be non empty non void ManySortedSign ; :: thesis:
let X be non-empty ManySortedSet of the carrier of S; :: thesis:
let v be SortSymbol of S; :: thesis:
let n be Nat; :: thesis:
assume A1: 1 <= n ; :: thesis:
set G = InducedGraph S;
FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) by MSAFREE:def 14;
then A2: the Sorts of (FreeMSA X) . v = FreeSort (X,v) by MSAFREE:def 11;
A3: FreeSort (X,v) c= S -Terms X by MSATERM:12;
thus ( ex t being Element of the Sorts of (FreeMSA X) . v st depth t = n implies ex c being directed Chain of InducedGraph S st
( len c = n & (vertex-seq c) . ((len c) + 1) = v ) ) :: thesis:

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
set D = the carrier' of (InducedGraph S) * ;
given t being Element of the Sorts of (FreeMSA X) . v such that A4: depth t = n ; :: thesis:
t in FreeSort (X,v) by A2;
then reconsider t9 = t as Term of S,X by A3;
consider dt being finite DecoratedTree, tr being finite Tree such that
A5: ( dt = t & tr = dom dt ) and
A6: depth t = height tr by MSAFREE2:def 14;
not t is root by A1, A4, A5, A6, TREES_1:42, TREES_9:def 1;
then consider o being OperSymbol of S such that
A7: t9 . {} = [o, the carrier of S] by MSSCYC_1:20;
consider a being ArgumentSeq of Sym (o,X) such that
A8: t = [o, the carrier of S] -tree a by A7, MSATERM:10;
set args = the_arity_of o;
A9: dom a = dom (the_arity_of o) by MSATERM:22;
consider p being FinSequence of NAT such that
A10: p in tr and
A11: len p = height tr by TREES_1:def 12;
consider i being Nat, T being DecoratedTree, q being Node of T such that
A12: i < len a and
T = a . (i + 1) and
A13: p = <*i*> ^ q by A1, A4, A5, A6, A10, A11, A8, CARD_1:27, TREES_4:11;
defpred S₁[ Nat, set , set ] means ex t1, t2 being Term of S,X st
( t1 = t | (p | $1) & t2 = t | (p | ($1 + 1)) & ex o being OperSymbol of S ex rs1 being SortSymbol of S ex Ck being Element of the carrier' of (InducedGraph S) * st
( Ck = $2 & $3 = <*[o,rs1]*> ^ Ck & [o, the carrier of S] = t1 . {} & rs1 = the_sort_of t2 & [o,rs1] in the carrier' of (InducedGraph S) ) );
( 1 <= i + 1 & i + 1 <= len a ) by A12, NAT_1:11, NAT_1:13;
then A14: i + 1 in dom (the_arity_of o) by A9, FINSEQ_3:25;
then reconsider rs1 = (the_arity_of o) . (i + 1) as SortSymbol of S by DTCONSTR:2;
set e1 = [o,rs1];
A15: the Arity of S . o = the_arity_of o by MSUALG_1:def 1;
then A16: [o,rs1] in InducedEdges S by A14, Def1;
then reconsider E9 = the carrier' of (InducedGraph S) as non empty set ;
reconsider e19 = [o,rs1] as Element of E9 by A14, A15, Def1;
reconsider C19 = <*e19*> as Element of the carrier' of (InducedGraph S) * by FINSEQ_1:def 11;
A17: for k being Nat st 1 <= k & k < n1 holds
for x being Element of the carrier' of (InducedGraph S) * ex y being Element of the carrier' of (InducedGraph S) * st S₁[k,x,y]

let k be Nat; :: thesis:
set pk9 = p /^ k;
k <= k + 1 by NAT_1:13;
then A18: Seg k c= Seg (k + 1) by FINSEQ_1:5;
k in NAT by ORDINAL1:def 12;
then reconsider pk = p | k, pk1 = p | (k + 1) as Node of t by A5, A10, MSSCYC_1:19;
assume that
1 <= k and
A19: k < n1 ; :: thesis:
A20: len (p /^ k) = n - k by A4, A6, A11, A19, RFINSEQ:def 1;
then A21: len (p /^ k) <> 0 by A19;
then A22: 1 in dom (p /^ k) by CARD_1:27, FINSEQ_5:6;
reconsider t1 = t9 | pk, t2 = t9 | pk1 as Term of S,X by MSATERM:29;
p = pk ^ (p /^ k) by RFINSEQ:8;
then A23: p /^ k in tr | pk by A5, A10, TREES_1:def 6;
then A24: p /^ k in dom t1 by A5, TREES_2:def 10;
A25: k + 1 <= n by A19, NAT_1:13;
then A26: 1 <= n - k by XREAL_1:19;

now :: thesis:

assume t1 is root ; :: thesis:
then dom t1 = elementary_tree 0 by TREES_9:def 1;
hence contradiction by A20, A26, A24, TREES_1:42, TREES_1:def 12; :: thesis:

end;

then consider o being OperSymbol of S such that
A27: t1 . {} = [o, the carrier of S] by MSSCYC_1:20;
consider a being ArgumentSeq of Sym (o,X) such that
A28: t1 = [o, the carrier of S] -tree a by A27, MSATERM:10;
A29: (p /^ k) | 1 = <*((p /^ k) . 1)*> by A21, CARD_1:27, FINSEQ_5:20;
consider i being Nat, T being DecoratedTree, q being Node of T such that
A30: i < len a and
T = a . (i + 1) and
A31: p /^ k = <*i*> ^ q by A21, A24, A28, CARD_1:27, TREES_4:11;
reconsider pk9 = p /^ k as Node of t1 by A5, A23, TREES_2:def 10;
reconsider p1 = pk9 | (0 + 1) as Node of t1 by MSSCYC_1:19;
reconsider t29 = t1 | p1 as Term of S,X ;
A32: (p | (k + 1)) | k = (p | (k + 1)) | (Seg k) by FINSEQ_1:def 16
.= (p | (Seg (k + 1))) | (Seg k) by FINSEQ_1:def 16
.= p | (Seg k) by A18, FUNCT_1:51
.= pk by FINSEQ_1:def 16 ;
set args = the_arity_of o;
let x be Element of the carrier' of (InducedGraph S) * ; :: thesis:
A33: dom a = dom (the_arity_of o) by MSATERM:22;
A34: 1 <= k + 1 by NAT_1:11;
then A35: k + 1 in dom p by A4, A6, A11, A25, FINSEQ_3:25;
A36: len pk1 = k + 1 by A4, A6, A11, A25, FINSEQ_1:59;
then A37: k + 1 in dom pk1 by A34, FINSEQ_3:25;
p1 = <*(p . (k + 1))*> by A4, A6, A11, A19, A22, A29, RFINSEQ:def 1
.= <*(p /. (k + 1))*> by A35, PARTFUN1:def 6
.= <*((p | (k + 1)) /. (k + 1))*> by A37, FINSEQ_4:70
.= <*(pk1 . (k + 1))*> by A37, PARTFUN1:def 6 ;
then pk1 = pk ^ p1 by A36, A32, RFINSEQ:7;
then A38: t29 = t2 by TREES_9:3;
( 1 <= i + 1 & i + 1 <= len a ) by A30, NAT_1:11, NAT_1:13;
then A39: i + 1 in dom (the_arity_of o) by A33, FINSEQ_3:25;
then reconsider rs1 = (the_arity_of o) . (i + 1) as SortSymbol of S by DTCONSTR:2;
set e1 = [o,rs1];
A40: the Arity of S . o = the_arity_of o by MSUALG_1:def 1;
then [o,rs1] in InducedEdges S by A39, Def1;
then reconsider E9 = the carrier' of (InducedGraph S) as non empty set ;
reconsider e19 = [o,rs1] as Element of E9 by A39, A40, Def1;
reconsider x9 = x as FinSequence of E9 by FINSEQ_1:def 11;
reconsider y = <*e19*> ^ x9 as Element of the carrier' of (InducedGraph S) * by FINSEQ_1:def 11;
take y ; :: thesis:
take t1 ; :: thesis:
take t2 ; :: thesis:
thus ( t1 = t | (p | k) & t2 = t | (p | (k + 1)) ) ; :: thesis:
take o ; :: thesis:
take rs1 ; :: thesis:
take x ; :: thesis:
thus ( x = x & y = <*[o,rs1]*> ^ x ) ; :: thesis:
thus [o, the carrier of S] = t1 . {} by A27; :: thesis:
pk9 | 1 = <*i*> by A31, A29, FINSEQ_1:41;
then t29 = a . (i + 1) by A28, A30, TREES_4:def 4;
hence rs1 = the_sort_of t2 by A33, A39, A38, MSATERM:23; :: thesis:
thus [o,rs1] in the carrier' of (InducedGraph S) by A39, A40, Def1; :: thesis:

end;

consider C being FinSequence of the carrier' of (InducedGraph S) * such that
A41: ( len C = n1 & ( C . 1 = C19 or n1 = 0 ) & ( for k being Nat st 1 <= k & k < n1 holds
S₁[k,C . k,C . (k + 1)] ) ) from RECDEF_1:sch 4(A17);
defpred S₂[ Nat] means ( 1 <= $1 & $1 <= n implies ex Ck being directed Chain of InducedGraph S ex t1 being Term of S,X st
( Ck = C . $1 & len Ck = $1 & t1 = t | (p | $1) & (vertex-seq Ck) . ((len Ck) + 1) = v & (vertex-seq Ck) . 1 = the_sort_of t1 ) );
A42: for i being Nat st S₂[i] holds
S₂[i + 1]

proof

let k be Nat; :: thesis:
assume A43: ( 1 <= k & k <= n implies ex Ck being directed Chain of InducedGraph S ex t1 being Term of S,X st
( Ck = C . k & len Ck = k & t1 = t | (p | k) & (vertex-seq Ck) . ((len Ck) + 1) = v & (vertex-seq Ck) . 1 = the_sort_of t1 ) ) ; :: thesis:
A44: k <= k + 1 by NAT_1:11;
assume that
1 <= k + 1 and
A45: k + 1 <= n ; :: thesis:
A46: k < n by A45, NAT_1:13;

per cases ;

suppose A47: k = 0 ; :: thesis:

reconsider C1 = <*[o,rs1]*> as directed Chain of InducedGraph S by A16, MSSCYC_1:5;
reconsider p1 = p | (0 + 1) as Node of t by A5, A10, MSSCYC_1:19;
reconsider t2 = t9 | p1 as Term of S,X by MSATERM:29;
take C1 ; :: thesis:
take t2 ; :: thesis:
thus C1 = C . (k + 1) by A1, A41, A47; :: thesis:
thus len C1 = k + 1 by A47, FINSEQ_1:39; :: thesis:
thus t2 = t | (p | (k + 1)) by A47; :: thesis:
reconsider p9 = p as PartFunc of NAT,NAT ;
A48: vertex-seq C1 = <*( the Source of (InducedGraph S) . [o,rs1]),( the Target of (InducedGraph S) . [o,rs1])*> by A16, MSSCYC_1:7;
(vertex-seq C1) . ((len C1) + 1) = (vertex-seq C1) . (1 + 1) by FINSEQ_1:39
.= the Target of (InducedGraph S) . [o,rs1] by A48
.= the ResultSort of S . ([o,rs1] `1) by A16, Def3
.= the ResultSort of S . o
.= the_result_sort_of o by MSUALG_1:def 2
.= the_sort_of t9 by A7, MSATERM:17
.= v by A2, MSATERM:def 5 ;
hence (vertex-seq C1) . ((len C1) + 1) = v ; :: thesis:
p | 1 = <*(p9 . 1)*> by A1, A4, A6, A11, CARD_1:27, FINSEQ_5:20
.= <*(p . 1)*>
.= <*i*> by A13, FINSEQ_1:41 ;
then A50: t2 = a . (i + 1) by A8, A12, TREES_4:def 4;
(vertex-seq C1) . 1 = the Source of (InducedGraph S) . [o,rs1] by A48
.= [o,rs1] `2 by A16, Def2
.= rs1
.= the_sort_of t2 by A9, A14, A50, MSATERM:23 ;
hence (vertex-seq C1) . 1 = the_sort_of t2 ; :: thesis:

end;

suppose A51: k <> 0 ; :: thesis:

consider t1, t2 being Term of S,X such that
A52: t1 = t | (p | k) and
A53: t2 = t | (p | (k + 1)) and
A54: ex o being OperSymbol of S ex rs1 being SortSymbol of S ex Ck being Element of the carrier' of (InducedGraph S) * st
( Ck = C . k & C . (k + 1) = <*[o,rs1]*> ^ Ck & [o, the carrier of S] = t1 . {} & rs1 = the_sort_of t2 & [o,rs1] in the carrier' of (InducedGraph S) ) by A41, A46, A51, NAT_1:14;
consider o being OperSymbol of S, rs1 being SortSymbol of S, Ck9 being Element of the carrier' of (InducedGraph S) * such that
A55: ( Ck9 = C . k & C . (k + 1) = <*[o,rs1]*> ^ Ck9 ) and
A56: [o, the carrier of S] = t1 . {} and
A57: rs1 = the_sort_of t2 and
A58: [o,rs1] in the carrier' of (InducedGraph S) by A54;
A59: not InducedGraph S is void by A58;
reconsider C1 = <*[o,rs1]*> as directed Chain of InducedGraph S by A58, MSSCYC_1:5;
set e1 = [o,rs1];
A60: vertex-seq C1 = <*( the Source of (InducedGraph S) . [o,rs1]),( the Target of (InducedGraph S) . [o,rs1])*> by A58, MSSCYC_1:7;
consider Ck being directed Chain of InducedGraph S, t19 being Term of S,X such that
A61: Ck = C . k and
A62: len Ck = k and
A63: t19 = t | (p | k) and
A64: (vertex-seq Ck) . ((len Ck) + 1) = v and
A65: (vertex-seq Ck) . 1 = the_sort_of t19 by A43, A45, A44, A51, NAT_1:14, XXREAL_0:2;
(vertex-seq C1) . ((len C1) + 1) = (vertex-seq C1) . (1 + 1) by FINSEQ_1:39
.= the Target of (InducedGraph S) . [o,rs1] by A60
.= the ResultSort of S . ([o,rs1] `1) by A58, Def3
.= the ResultSort of S . o
.= the_result_sort_of o by MSUALG_1:def 2
.= the_sort_of t1 by A56, MSATERM:17 ;
then reconsider d = C1 ^ Ck as directed Chain of InducedGraph S by A51, A62, A63, A65, A52, A59, CARD_1:27, MSSCYC_1:15;
take d ; :: thesis:
take t2 ; :: thesis:
thus d = C . (k + 1) by A61, A55; :: thesis:
thus len d = (len C1) + k by A62, FINSEQ_1:22
.= k + 1 by FINSEQ_1:39 ; :: thesis:
thus t2 = t | (p | (k + 1)) by A53; :: thesis:
thus (vertex-seq d) . ((len d) + 1) = v by A51, A62, A64, A59, CARD_1:27, MSSCYC_1:16; :: thesis:
(vertex-seq C1) . 1 = the Source of (InducedGraph S) . [o,rs1] by A60
.= [o,rs1] `2 by A58, Def2
.= the_sort_of t2 by A57 ;
hence (vertex-seq d) . 1 = the_sort_of t2 by A51, A62, A59, CARD_1:27, MSSCYC_1:16; :: thesis:

end;

A66: S₂[ 0 ] ;
for k being Nat holds S₂[k] from NAT_1:sch 2(A66, A42);
then ex c being directed Chain of InducedGraph S ex t1 being Term of S,X st
( c = C . n & len c = n & t1 = t | (p | n) & (vertex-seq c) . ((len c) + 1) = v & (vertex-seq c) . 1 = the_sort_of t1 ) by A1;
hence ex c being directed Chain of InducedGraph S st
( len c = n & (vertex-seq c) . ((len c) + 1) = v ) ; :: thesis:

end;

given c being directed Chain of InducedGraph S such that A67: len c = n and
A68: (vertex-seq c) . ((len c) + 1) = v ; :: thesis:
set EG = the carrier' of (InducedGraph S);
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
deffunc H₁( object ) -> set = X . $1;
set TG = the Target of (InducedGraph S);
set SG = the Source of (InducedGraph S);
set D = S -Terms X;
set cS = the carrier of S;
A69: for e being object st e in the carrier of S holds
H₁(e) <> {} ;
consider cX being ManySortedSet of the carrier of S such that
A70: for e being object st e in the carrier of S holds
cX . e in H₁(e) from PBOOLE:sch 1(A69);
defpred S₁[ Nat, set , set ] means ex o being OperSymbol of S ex rs1 being SortSymbol of S ex Ck, Ck1 being Term of S,X ex a being ArgumentSeq of Sym (o,X) st
( Ck = $2 & $3 = Ck1 & c . ($1 + 1) = [o,rs1] & Ck1 = [o, the carrier of S] -tree a & ( for i being Nat st i in dom a holds
ex t being Term of S,X st
( t = a . i & the_sort_of t = (the_arity_of o) . i & ( the_sort_of t = rs1 & the_sort_of Ck = rs1 implies t = Ck ) & ( ( the_sort_of t <> rs1 or the_sort_of Ck <> rs1 ) implies t = root-tree [(cX . (the_sort_of t)),(the_sort_of t)] ) ) ) );
A71: c is FinSequence of the carrier' of (InducedGraph S) by MSSCYC_1:def 1;
A72: 1 in dom c by A1, A67, FINSEQ_3:25;
then reconsider EG = the carrier' of (InducedGraph S) as non empty set by A71;
c . 1 in InducedEdges S by A71, A72, DTCONSTR:2;
then consider o, rs1 being set such that
A73: c . 1 = [o,rs1] and
A74: o in the carrier' of S and
A75: rs1 in the carrier of S and
A76: ex n being Nat ex args being Element of the carrier of S * st
( the Arity of S . o = args & n in dom args & args . n = rs1 ) by Def1;
reconsider rs1 = rs1 as SortSymbol of S by A75;
reconsider o = o as OperSymbol of S by A74;
deffunc H₂( Nat) -> set = root-tree [(cX . ((the_arity_of o) . $1)),((the_arity_of o) . $1)];
consider a being FinSequence such that
A77: ( len a = len (the_arity_of o) & ( for k being Nat st k in dom a holds
a . k = H₂(k) ) ) from FINSEQ_1:sch 2();
A78: dom a = Seg (len a) by FINSEQ_1:def 3;
A79: for i being Nat st i in dom a holds
ex t being Term of S,X st
( t = a . i & the_sort_of t = (the_arity_of o) . i )

proof

let i be Nat; :: thesis:
assume A80: i in dom a ; :: thesis:
set s = (the_arity_of o) . i;
dom (the_arity_of o) = Seg (len (the_arity_of o)) by FINSEQ_1:def 3;
then reconsider s = (the_arity_of o) . i as SortSymbol of S by A77, A78, A80, DTCONSTR:2;
set x = cX . ((the_arity_of o) . i);
reconsider x = cX . ((the_arity_of o) . i) as Element of X . s by A70;
reconsider t = root-tree [x,s] as Term of S,X by MSATERM:4;
take t ; :: thesis:
thus t = a . i by A77, A80; :: thesis:
thus the_sort_of t = (the_arity_of o) . i by MSATERM:14; :: thesis:

end;

A81: dom a = Seg (len (the_arity_of o)) by A77, FINSEQ_1:def 3;
reconsider a = a as ArgumentSeq of Sym (o,X) by A77, A79, MSATERM:24;
set C1 = [o, the carrier of S] -tree a;
reconsider C1 = [o, the carrier of S] -tree a as Term of S,X by MSATERM:1;
A82: for k being Nat st 1 <= k & k < n1 holds
for x being Element of S -Terms X ex y being Element of S -Terms X st S₁[k,x,y]

proof

let k be Nat; :: thesis:
assume that
1 <= k and
A83: k < n1 ; :: thesis:
A84: 1 <= k + 1 by NAT_1:11;
k + 1 <= n by A83, NAT_1:13;
then k + 1 in dom c by A67, A84, FINSEQ_3:25;
then reconsider ck1 = c . (k + 1) as Element of EG by A71, DTCONSTR:2;
let x be Element of S -Terms X; :: thesis:
consider o, rs1 being set such that
A85: ck1 = [o,rs1] and
A86: o in the carrier' of S and
A87: rs1 in the carrier of S and
ex n being Nat ex args being Element of the carrier of S * st
( the Arity of S . o = args & n in dom args & args . n = rs1 ) by Def1;
reconsider rs1 = rs1 as SortSymbol of S by A87;
reconsider o = o as OperSymbol of S by A86;
set DA = dom (the_arity_of o);
set ar = the_arity_of o;
defpred S₂[ object , object ] means ( ( (the_arity_of o) . $1 = rs1 & the_sort_of x = rs1 implies $2 = x ) & ( ( (the_arity_of o) . $1 <> rs1 or the_sort_of x <> rs1 ) implies $2 = root-tree [(cX . ((the_arity_of o) . $1)),((the_arity_of o) . $1)] ) );
A88: for e being object st e in dom (the_arity_of o) holds
ex u being object st
( u in S -Terms X & S₂[e,u] )

proof

let e be object ; :: thesis:
assume A89: e in dom (the_arity_of o) ; :: thesis:

per cases ) . e = rs1 & the_sort_of x = rs1 ) or (the_arity_of o) . e <> rs1 or the_sort_of x <> rs1 ) ;

suppose A90: ( (the_arity_of o) . e = rs1 & the_sort_of x = rs1 ) ; :: thesis:

take x ; :: thesis:
thus ( x in S -Terms X & S₂[e,x] ) by A90; :: thesis:

end;

suppose A91: ( (the_arity_of o) . e <> rs1 or the_sort_of x <> rs1 ) ; :: thesis:

reconsider s = (the_arity_of o) . e as SortSymbol of S by A89, DTCONSTR:2;
reconsider x = cX . ((the_arity_of o) . e) as Element of X . s by A70;
reconsider t = root-tree [x,s] as Term of S,X by MSATERM:4;
take t ; :: thesis:
thus ( t in S -Terms X & S₂[e,t] ) by A91; :: thesis:

end;

consider a being Function of (dom (the_arity_of o)),(S -Terms X) such that
A92: for e being object st e in dom (the_arity_of o) holds
S₂[e,a . e] from FUNCT_2:sch 1(A88);
dom (the_arity_of o) = Seg (len (the_arity_of o)) by FINSEQ_1:def 3;
then reconsider a = a as FinSequence of S -Terms X by FINSEQ_2:25;
A93: dom a = dom (the_arity_of o) by FUNCT_2:def 1;

now :: thesis:

let i be Nat; :: thesis:
assume A94: i in dom a ; :: thesis:
then reconsider t = a . i as Term of S,X by DTCONSTR:2;
take t = t; :: thesis:
thus t = a . i ; :: thesis:

per cases ) . i = rs1 & the_sort_of x = rs1 ) or (the_arity_of o) . i <> rs1 or the_sort_of x <> rs1 ) ;

suppose ( (the_arity_of o) . i = rs1 & the_sort_of x = rs1 ) ; :: thesis:

hence the_sort_of t = (the_arity_of o) . i by A92, A93, A94; :: thesis:

end;

suppose A95: ( (the_arity_of o) . i <> rs1 or the_sort_of x <> rs1 ) ; :: thesis:

reconsider s = (the_arity_of o) . i as SortSymbol of S by A93, A94, DTCONSTR:2;
A96: cX . ((the_arity_of o) . i) is Element of X . s by A70;
t = root-tree [(cX . ((the_arity_of o) . i)),((the_arity_of o) . i)] by A92, A93, A94, A95;
hence the_sort_of t = (the_arity_of o) . i by A96, MSATERM:14; :: thesis:

end;

then reconsider a = a as ArgumentSeq of Sym (o,X) by A93, MSATERM:24;
reconsider y = [o, the carrier of S] -tree a as Term of S,X by MSATERM:1;
take y ; :: thesis:
take o ; :: thesis:
take rs1 ; :: thesis:
take x ; :: thesis:
take y ; :: thesis:
take a ; :: thesis:
thus ( x = x & y = y ) ; :: thesis:
thus c . (k + 1) = [o,rs1] by A85; :: thesis:
thus y = [o, the carrier of S] -tree a ; :: thesis:
let i be Nat; :: thesis:
assume A97: i in dom a ; :: thesis:
then reconsider t = a . i as Term of S,X by DTCONSTR:2;
take t ; :: thesis:
thus t = a . i ; :: thesis:
thus the_sort_of t = (the_arity_of o) . i by A97, MSATERM:23; :: thesis:
hence ( ( the_sort_of t = rs1 & the_sort_of x = rs1 implies t = x ) & ( ( the_sort_of t <> rs1 or the_sort_of x <> rs1 ) implies t = root-tree [(cX . (the_sort_of t)),(the_sort_of t)] ) ) by A92, A93, A97; :: thesis:

end;

consider C being FinSequence of S -Terms X such that
A98: ( len C = n1 & ( C . 1 = C1 or n1 = 0 ) & ( for k being Nat st 1 <= k & k < n1 holds
S₁[k,C . k,C . (k + 1)] ) ) from RECDEF_1:sch 4(A82);
defpred S₂[ Nat] means ( 1 <= $1 & $1 <= n implies ex C0 being Term of S,X ex o being OperSymbol of S st
( C0 = C . $1 & o = (c . $1) `1 & the_sort_of C0 = the_result_sort_of o & height (dom C0) = $1 ) );
A99: not InducedGraph S is void by A72;
A100: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis:
assume A101: ( 1 <= k & k <= n implies ex Ck being Term of S,X ex o being OperSymbol of S st
( Ck = C . k & o = (c . k) `1 & the_sort_of Ck = the_result_sort_of o & height (dom Ck) = k ) ) ; :: thesis:
assume that
A102: 1 <= k + 1 and
A103: k + 1 <= n ; :: thesis:
A104: k < n by A103, NAT_1:13;
A105: k <= k + 1 by NAT_1:11;
then A106: k <= n by A103, XXREAL_0:2;

per cases ;

suppose A107: k = 0 ; :: thesis:

take C1 ; :: thesis:
take o ; :: thesis:
thus C1 = C . (k + 1) by A1, A98, A107; :: thesis:
thus o = (c . (k + 1)) `1 by A73, A107; :: thesis:
reconsider w = doms a as FinTree-yielding FinSequence ;
A108: dom (doms a) = dom a by TREES_3:37;
C1 . {} = [o, the carrier of S] by TREES_4:def 4;
hence the_sort_of C1 = the_result_sort_of o by MSATERM:17; :: thesis:
consider i being Nat, args being Element of the carrier of S * such that
A109: the Arity of S . o = args and
A110: i in dom args and
args . i = rs1 by A76;
A111: dom args = Seg (len args) by FINSEQ_1:def 3;
A112: args = the_arity_of o by A109, MSUALG_1:def 1;
then reconsider t = a . i as Term of S,X by A77, A78, A110, A111, MSATERM:22;
(doms a) . i = dom t by A77, A78, A110, A112, A111, FUNCT_6:22;
then A113: ( dom C1 = tree (doms a) & dom t in rng w ) by A77, A78, A108, A110, A112, A111, FUNCT_1:def 3, TREES_4:10;
reconsider dt = dom t as finite Tree ;
A114: a . i = root-tree [(cX . ((the_arity_of o) . i)),((the_arity_of o) . i)] by A77, A81, A110, A112, A111;

A115: now :: thesis:

let t9 be finite Tree; :: thesis:
assume t9 in rng w ; :: thesis:
then consider j being Nat such that
A116: j in dom w and
A117: w . j = t9 by FINSEQ_2:10;
reconsider t99 = a . j as Term of S,X by A108, A116, MSATERM:22;
a . j = root-tree [(cX . ((the_arity_of o) . j)),((the_arity_of o) . j)] by A77, A108, A116;
then A118: dom t99 = elementary_tree 0 by TREES_4:3;
w . j = dom t99 by A108, A116, FUNCT_6:22;
hence height t9 <= height dt by A114, A117, A118, TREES_4:3; :: thesis:

end;

dom t = elementary_tree 0 by A114, TREES_4:3;
hence height (dom C1) = k + 1 by A107, A113, A115, TREES_1:42, TREES_3:79; :: thesis:

end;

suppose A119: k <> 0 ; :: thesis:

then A120: 1 <= k by NAT_1:14;
then k in dom c by A67, A106, FINSEQ_3:25;
then reconsider ck = c . k as Element of EG by A71, DTCONSTR:2;
consider Ck being Term of S,X, o being OperSymbol of S such that
A121: Ck = C . k and
A122: ( o = (c . k) `1 & the_sort_of Ck = the_result_sort_of o ) and
A123: height (dom Ck) = k by A101, A103, A105, A119, NAT_1:14, XXREAL_0:2;
reconsider kk = k as Element of NAT by ORDINAL1:def 12;
consider o1 being OperSymbol of S, rs1 being SortSymbol of S, Ck9, Ck1 being Term of S,X, a being ArgumentSeq of Sym (o1,X) such that
A124: Ck9 = C . k and
A125: C . (kk + 1) = Ck1 and
A126: c . (k + 1) = [o1,rs1] and
A127: Ck1 = [o1, the carrier of S] -tree a and
A128: for i being Nat st i in dom a holds
ex t being Term of S,X st
( t = a . i & the_sort_of t = (the_arity_of o1) . i & ( the_sort_of t = rs1 & the_sort_of Ck9 = rs1 implies t = Ck9 ) & ( ( the_sort_of t <> rs1 or the_sort_of Ck9 <> rs1 ) implies t = root-tree [(cX . (the_sort_of t)),(the_sort_of t)] ) ) by A98, A104, A119, NAT_1:14;
set ck1 = c . (kk + 1);
A129: k + 1 in dom c by A67, A102, A103, FINSEQ_3:25;
then c . (kk + 1) in EG by A71, DTCONSTR:2;
then consider o9, rs19 being set such that
A130: c . (kk + 1) = [o9,rs19] and
A131: o9 in the carrier' of S and
rs19 in the carrier of S and
A132: ex n being Nat ex args being Element of the carrier of S * st
( the Arity of S . o9 = args & n in dom args & args . n = rs19 ) by Def1;
A133: o1 = o9 by A126, A130, XTUPLE_0:1;
take Ck1 ; :: thesis:
take o1 ; :: thesis:
thus Ck1 = C . (k + 1) by A125; :: thesis:
thus o1 = (c . (k + 1)) `1 by A126; :: thesis:
Ck1 . {} = [o1, the carrier of S] by A127, TREES_4:def 4;
hence the_sort_of Ck1 = the_result_sort_of o1 by MSATERM:17; :: thesis:
A134: dom Ck1 = tree (doms a) by A127, TREES_4:10;
reconsider ck1 = c . (kk + 1) as Element of EG by A71, A129, DTCONSTR:2;
reconsider w = doms a as FinTree-yielding FinSequence ;
A135: ( len a = len (the_arity_of o1) & dom a = Seg (len a) ) by FINSEQ_1:def 3, MSATERM:22;
rs1 = rs19 by A126, A130, XTUPLE_0:1;
then consider i being Nat, args being Element of the carrier of S * such that
A136: the Arity of S . o9 = args and
A137: i in dom args and
A138: args . i = rs1 by A132;
reconsider o9 = o9 as OperSymbol of S by A131;
A139: dom args = Seg (len args) by FINSEQ_1:def 3;
A140: args = the_arity_of o9 by A136, MSUALG_1:def 1;
then consider t being Term of S,X such that
A141: t = a . i and
A142: ( the_sort_of t = (the_arity_of o1) . i & ( the_sort_of t = rs1 & the_sort_of Ck9 = rs1 implies t = Ck9 ) ) and
( ( the_sort_of t <> rs1 or the_sort_of Ck9 <> rs1 ) implies t = root-tree [(cX . (the_sort_of t)),(the_sort_of t)] ) by A128, A135, A133, A137, A139;
reconsider dt = dom t as finite Tree ;
A143: dom (doms a) = dom a by TREES_3:37;

A144: now :: thesis:

let t9 be finite Tree; :: thesis:
assume t9 in rng w ; :: thesis:
then consider j being Nat such that
A145: j in dom w and
A146: w . j = t9 by FINSEQ_2:10;
consider t99 being Term of S,X such that
A147: t99 = a . j and
the_sort_of t99 = (the_arity_of o1) . j and
A148: ( the_sort_of t99 = rs1 & the_sort_of Ck9 = rs1 implies t99 = Ck9 ) and
A149: ( ( the_sort_of t99 <> rs1 or the_sort_of Ck9 <> rs1 ) implies t99 = root-tree [(cX . (the_sort_of t99)),(the_sort_of t99)] ) by A128, A143, A145;
A150: w . j = dom t99 by A143, A145, A147, FUNCT_6:22;

per cases ;

suppose ( the_sort_of t99 = rs1 & the_sort_of Ck9 = rs1 ) ; :: thesis:

hence height t9 <= height dt by A143, A133, A136, A138, A142, A145, A146, A147, A148, FUNCT_6:22, MSUALG_1:def 1; :: thesis:

end;

suppose ( the_sort_of t99 <> rs1 or the_sort_of Ck9 <> rs1 ) ; :: thesis:

hence height t9 <= height dt by A146, A149, A150, TREES_1:42, TREES_4:3; :: thesis:

end;

(doms a) . i = dom t by A135, A133, A137, A140, A139, A141, FUNCT_6:22;
then A151: dom t in rng w by A143, A135, A133, A137, A140, A139, FUNCT_1:def 3;
the_sort_of Ck = the ResultSort of S . (ck `1) by A122, MSUALG_1:def 2
.= the Target of (InducedGraph S) . ck by Def3
.= (vertex-seq c) . (kk + 1) by A67, A99, A106, A120, CARD_1:27, MSSCYC_1:11
.= the Source of (InducedGraph S) . ck1 by A67, A99, A102, A103, CARD_1:27, MSSCYC_1:11
.= ck1 `2 by Def2
.= rs1 by A126 ;
hence height (dom Ck1) = k + 1 by A121, A123, A124, A134, A133, A136, A138, A142, A151, A144, MSUALG_1:def 1, TREES_3:79; :: thesis:

end;

set cn = c . (len c);
n in dom c by A1, A67, CARD_1:27, FINSEQ_5:6;
then A152: c . (len c) in InducedEdges S by A67, A71, DTCONSTR:2;
A153: S₂[ 0 ] ;
for k being Nat holds S₂[k] from NAT_1:sch 2(A153, A100);
then consider Cn being Term of S,X, o being OperSymbol of S such that
Cn = C . n and
A154: o = (c . n) `1 and
A155: the_sort_of Cn = the_result_sort_of o and
A156: height (dom Cn) = n by A1;
not InducedGraph S is void by A72;
then (vertex-seq c) . ((len c) + 1) = the Target of (InducedGraph S) . (c . (len c)) by A1, A67, CARD_1:27, MSSCYC_1:14
.= the ResultSort of S . ((c . (len c)) `1) by A152, Def3
.= the_result_sort_of o by A67, A154, MSUALG_1:def 2 ;
then reconsider Cn = Cn as Element of the Sorts of (FreeMSA X) . v by A2, A68, A155, MSATERM:def 5;
take Cn ; :: thesis:
thus depth Cn = n by A156, MSAFREE2:def 14; :: thesis: