let S be non empty non void ManySortedSign ; :: thesis: for X being V2() ManySortedSet of the carrier of S

for v being SortSymbol of S

for n being Nat st 1 <= n holds

( ex t being Element of the Sorts of (FreeMSA X) . v st depth t = n iff ex c being directed Chain of InducedGraph S st

( len c = n & (vertex-seq c) . ((len c) + 1) = v ) )

let X be V2() ManySortedSet of the carrier of S; :: thesis: for v being SortSymbol of S

for n being Nat st 1 <= n holds

( ex t being Element of the Sorts of (FreeMSA X) . v st depth t = n iff ex c being directed Chain of InducedGraph S st

( len c = n & (vertex-seq c) . ((len c) + 1) = v ) )

let v be SortSymbol of S; :: thesis: for n being Nat st 1 <= n holds

( ex t being Element of the Sorts of (FreeMSA X) . v st depth t = n iff ex c being directed Chain of InducedGraph S st

( len c = n & (vertex-seq c) . ((len c) + 1) = v ) )

let n be Nat; :: thesis: ( 1 <= n implies ( ex t being Element of the Sorts of (FreeMSA X) . v st depth t = n iff ex c being directed Chain of InducedGraph S st

( len c = n & (vertex-seq c) . ((len c) + 1) = v ) ) )

assume A1: 1 <= n ; :: thesis: ( ex t being Element of the Sorts of (FreeMSA X) . v st depth t = n iff ex c being directed Chain of InducedGraph S st

( len c = n & (vertex-seq c) . ((len c) + 1) = v ) )

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: ( ex c being directed Chain of InducedGraph S st

( len c = n & (vertex-seq c) . ((len c) + 1) = v ) implies ex t being Element of the Sorts of (FreeMSA X) . v st depth t = n )

A68: (vertex-seq c) . ((len c) + 1) = v ; :: thesis: ex t being Element of the Sorts of (FreeMSA X) . v st depth t = n

set EG = the carrier' of (InducedGraph S);

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

deffunc H_{1}( 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_{1}(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_{1}(e)
from PBOOLE:sch 1(A69);

defpred S_{1}[ 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_{2}( 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_{2}(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 )

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_{1}[k,x,y]

A98: ( len C = n1 & ( C . 1 = C1 or n1 = 0 ) & ( for k being Nat st 1 <= k & k < n1 holds

S_{1}[k,C . k,C . (k + 1)] ) )
from RECDEF_1:sch 4(A82);

defpred S_{2}[ 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_{2}[k] holds

S_{2}[k + 1]

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_{2}[ 0 ]
;

for k being Nat holds S_{2}[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: depth Cn = n

thus depth Cn = n by A156, MSAFREE2:def 14; :: thesis: verum

for v being SortSymbol of S

for n being Nat st 1 <= n holds

( ex t being Element of the Sorts of (FreeMSA X) . v st depth t = n iff ex c being directed Chain of InducedGraph S st

( len c = n & (vertex-seq c) . ((len c) + 1) = v ) )

let X be V2() ManySortedSet of the carrier of S; :: thesis: for v being SortSymbol of S

for n being Nat st 1 <= n holds

( ex t being Element of the Sorts of (FreeMSA X) . v st depth t = n iff ex c being directed Chain of InducedGraph S st

( len c = n & (vertex-seq c) . ((len c) + 1) = v ) )

let v be SortSymbol of S; :: thesis: for n being Nat st 1 <= n holds

( ex t being Element of the Sorts of (FreeMSA X) . v st depth t = n iff ex c being directed Chain of InducedGraph S st

( len c = n & (vertex-seq c) . ((len c) + 1) = v ) )

let n be Nat; :: thesis: ( 1 <= n implies ( ex t being Element of the Sorts of (FreeMSA X) . v st depth t = n iff ex c being directed Chain of InducedGraph S st

( len c = n & (vertex-seq c) . ((len c) + 1) = v ) ) )

assume A1: 1 <= n ; :: thesis: ( ex t being Element of the Sorts of (FreeMSA X) . v st depth t = n iff ex c being directed Chain of InducedGraph S st

( len c = n & (vertex-seq c) . ((len c) + 1) = v ) )

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: ( ex c being directed Chain of InducedGraph S st

( len c = n & (vertex-seq c) . ((len c) + 1) = v ) implies ex t being Element of the Sorts of (FreeMSA X) . v st depth t = n )

proof

given c being directed Chain of InducedGraph S such that A67:
len c = n
and
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: ex c being directed Chain of InducedGraph S st

( len c = n & (vertex-seq c) . ((len c) + 1) = v )

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_{1}[ 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_{1}[k,x,y]

A41: ( len C = n1 & ( C . 1 = C19 or n1 = 0 ) & ( for k being Nat st 1 <= k & k < n1 holds

S_{1}[k,C . k,C . (k + 1)] ) )
from RECDEF_1:sch 4(A17);

defpred S_{2}[ 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_{2}[i] holds

S_{2}[i + 1]
_{2}[ 0 ]
;

for k being Nat holds S_{2}[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: verum

end;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: ex c being directed Chain of InducedGraph S st

( len c = n & (vertex-seq c) . ((len c) + 1) = v )

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

( 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

proof

consider C being FinSequence of the carrier' of (InducedGraph S) * such that
let k be Nat; :: thesis: ( 1 <= k & k < n1 implies for x being Element of the carrier' of (InducedGraph S) * ex y being Element of the carrier' of (InducedGraph S) * st S_{1}[k,x,y] )

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: for x being Element of the carrier' of (InducedGraph S) * ex y being Element of the carrier' of (InducedGraph S) * st S_{1}[k,x,y]

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;

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 15

.= (p | (Seg (k + 1))) | (Seg k) by FINSEQ_1:def 15

.= p | (Seg k) by A18, FUNCT_1:51

.= pk by FINSEQ_1:def 15 ;

set args = the_arity_of o;

let x be Element of the carrier' of (InducedGraph S) * ; :: thesis: ex y being Element of the carrier' of (InducedGraph S) * st S_{1}[k,x,y]

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: S_{1}[k,x,y]

take t1 ; :: thesis: ex t2 being Term of S,X st

( t1 = t | (p | k) & t2 = t | (p | (k + 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 = x & y = <*[o,rs1]*> ^ Ck & [o, the carrier of S] = t1 . {} & rs1 = the_sort_of t2 & [o,rs1] in the carrier' of (InducedGraph S) ) )

take t2 ; :: thesis: ( t1 = t | (p | k) & t2 = t | (p | (k + 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 = x & y = <*[o,rs1]*> ^ Ck & [o, the carrier of S] = t1 . {} & rs1 = the_sort_of t2 & [o,rs1] in the carrier' of (InducedGraph S) ) )

thus ( t1 = t | (p | k) & t2 = t | (p | (k + 1)) ) ; :: thesis: ex o being OperSymbol of S ex rs1 being SortSymbol of S ex Ck being Element of the carrier' of (InducedGraph S) * st

( Ck = x & y = <*[o,rs1]*> ^ Ck & [o, the carrier of S] = t1 . {} & rs1 = the_sort_of t2 & [o,rs1] in the carrier' of (InducedGraph S) )

take o ; :: thesis: ex rs1 being SortSymbol of S ex Ck being Element of the carrier' of (InducedGraph S) * st

( Ck = x & y = <*[o,rs1]*> ^ Ck & [o, the carrier of S] = t1 . {} & rs1 = the_sort_of t2 & [o,rs1] in the carrier' of (InducedGraph S) )

take rs1 ; :: thesis: ex Ck being Element of the carrier' of (InducedGraph S) * st

( Ck = x & y = <*[o,rs1]*> ^ Ck & [o, the carrier of S] = t1 . {} & rs1 = the_sort_of t2 & [o,rs1] in the carrier' of (InducedGraph S) )

take x ; :: thesis: ( x = x & y = <*[o,rs1]*> ^ x & [o, the carrier of S] = t1 . {} & rs1 = the_sort_of t2 & [o,rs1] in the carrier' of (InducedGraph S) )

thus ( x = x & y = <*[o,rs1]*> ^ x ) ; :: thesis: ( [o, the carrier of S] = t1 . {} & rs1 = the_sort_of t2 & [o,rs1] in the carrier' of (InducedGraph S) )

thus [o, the carrier of S] = t1 . {} by A27; :: thesis: ( rs1 = the_sort_of t2 & [o,rs1] in the carrier' of (InducedGraph S) )

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: [o,rs1] in the carrier' of (InducedGraph S)

thus [o,rs1] in the carrier' of (InducedGraph S) by A39, A40, Def1; :: thesis: verum

end;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: for x being Element of the carrier' of (InducedGraph S) * ex y being Element of the carrier' of (InducedGraph S) * st S

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: not t1 is root

then consider o being OperSymbol of S such that assume
t1 is root
; :: thesis: contradiction

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: verum

end;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: verum

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 15

.= (p | (Seg (k + 1))) | (Seg k) by FINSEQ_1:def 15

.= p | (Seg k) by A18, FUNCT_1:51

.= pk by FINSEQ_1:def 15 ;

set args = the_arity_of o;

let x be Element of the carrier' of (InducedGraph S) * ; :: thesis: ex y being Element of the carrier' of (InducedGraph S) * st S

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: S

take t1 ; :: thesis: ex t2 being Term of S,X st

( t1 = t | (p | k) & t2 = t | (p | (k + 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 = x & y = <*[o,rs1]*> ^ Ck & [o, the carrier of S] = t1 . {} & rs1 = the_sort_of t2 & [o,rs1] in the carrier' of (InducedGraph S) ) )

take t2 ; :: thesis: ( t1 = t | (p | k) & t2 = t | (p | (k + 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 = x & y = <*[o,rs1]*> ^ Ck & [o, the carrier of S] = t1 . {} & rs1 = the_sort_of t2 & [o,rs1] in the carrier' of (InducedGraph S) ) )

thus ( t1 = t | (p | k) & t2 = t | (p | (k + 1)) ) ; :: thesis: ex o being OperSymbol of S ex rs1 being SortSymbol of S ex Ck being Element of the carrier' of (InducedGraph S) * st

( Ck = x & y = <*[o,rs1]*> ^ Ck & [o, the carrier of S] = t1 . {} & rs1 = the_sort_of t2 & [o,rs1] in the carrier' of (InducedGraph S) )

take o ; :: thesis: ex rs1 being SortSymbol of S ex Ck being Element of the carrier' of (InducedGraph S) * st

( Ck = x & y = <*[o,rs1]*> ^ Ck & [o, the carrier of S] = t1 . {} & rs1 = the_sort_of t2 & [o,rs1] in the carrier' of (InducedGraph S) )

take rs1 ; :: thesis: ex Ck being Element of the carrier' of (InducedGraph S) * st

( Ck = x & y = <*[o,rs1]*> ^ Ck & [o, the carrier of S] = t1 . {} & rs1 = the_sort_of t2 & [o,rs1] in the carrier' of (InducedGraph S) )

take x ; :: thesis: ( x = x & y = <*[o,rs1]*> ^ x & [o, the carrier of S] = t1 . {} & rs1 = the_sort_of t2 & [o,rs1] in the carrier' of (InducedGraph S) )

thus ( x = x & y = <*[o,rs1]*> ^ x ) ; :: thesis: ( [o, the carrier of S] = t1 . {} & rs1 = the_sort_of t2 & [o,rs1] in the carrier' of (InducedGraph S) )

thus [o, the carrier of S] = t1 . {} by A27; :: thesis: ( rs1 = the_sort_of t2 & [o,rs1] in the carrier' of (InducedGraph S) )

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: [o,rs1] in the carrier' of (InducedGraph S)

thus [o,rs1] in the carrier' of (InducedGraph S) by A39, A40, Def1; :: thesis: verum

A41: ( len C = n1 & ( C . 1 = C19 or n1 = 0 ) & ( for k being Nat st 1 <= k & k < n1 holds

S

defpred S

( 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

S

proof

A66:
S
let k be Nat; :: thesis: ( S_{2}[k] implies S_{2}[k + 1] )

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: S_{2}[k + 1]

A44: k <= k + 1 by NAT_1:11;

assume that

1 <= k + 1 and

A45: k + 1 <= n ; :: thesis: ex Ck being directed Chain of InducedGraph S ex t1 being Term of S,X st

( Ck = C . (k + 1) & len Ck = k + 1 & t1 = t | (p | (k + 1)) & (vertex-seq Ck) . ((len Ck) + 1) = v & (vertex-seq Ck) . 1 = the_sort_of t1 )

A46: k < n by A45, NAT_1:13;

end;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: S

A44: k <= k + 1 by NAT_1:11;

assume that

1 <= k + 1 and

A45: k + 1 <= n ; :: thesis: ex Ck being directed Chain of InducedGraph S ex t1 being Term of S,X st

( Ck = C . (k + 1) & len Ck = k + 1 & t1 = t | (p | (k + 1)) & (vertex-seq Ck) . ((len Ck) + 1) = v & (vertex-seq Ck) . 1 = the_sort_of t1 )

A46: k < n by A45, NAT_1:13;

per cases
( k = 0 or k <> 0 )
;

end;

suppose A47:
k = 0
; :: thesis: ex Ck being directed Chain of InducedGraph S ex t1 being Term of S,X st

( Ck = C . (k + 1) & len Ck = k + 1 & t1 = t | (p | (k + 1)) & (vertex-seq Ck) . ((len Ck) + 1) = v & (vertex-seq Ck) . 1 = the_sort_of t1 )

( Ck = C . (k + 1) & len Ck = k + 1 & t1 = t | (p | (k + 1)) & (vertex-seq Ck) . ((len Ck) + 1) = v & (vertex-seq Ck) . 1 = the_sort_of t1 )

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: ex t1 being Term of S,X st

( C1 = C . (k + 1) & len C1 = k + 1 & t1 = t | (p | (k + 1)) & (vertex-seq C1) . ((len C1) + 1) = v & (vertex-seq C1) . 1 = the_sort_of t1 )

take t2 ; :: thesis: ( C1 = C . (k + 1) & len C1 = k + 1 & t2 = t | (p | (k + 1)) & (vertex-seq C1) . ((len C1) + 1) = v & (vertex-seq C1) . 1 = the_sort_of t2 )

thus C1 = C . (k + 1) by A1, A41, A47; :: thesis: ( len C1 = k + 1 & t2 = t | (p | (k + 1)) & (vertex-seq C1) . ((len C1) + 1) = v & (vertex-seq C1) . 1 = the_sort_of t2 )

thus len C1 = k + 1 by A47, FINSEQ_1:39; :: thesis: ( t2 = t | (p | (k + 1)) & (vertex-seq C1) . ((len C1) + 1) = v & (vertex-seq C1) . 1 = the_sort_of t2 )

thus t2 = t | (p | (k + 1)) by A47; :: thesis: ( (vertex-seq C1) . ((len C1) + 1) = v & (vertex-seq C1) . 1 = the_sort_of t2 )

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, FINSEQ_1:44

.= 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: (vertex-seq C1) . 1 = the_sort_of t2

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, FINSEQ_1:44

.= [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: verum

end;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: ex t1 being Term of S,X st

( C1 = C . (k + 1) & len C1 = k + 1 & t1 = t | (p | (k + 1)) & (vertex-seq C1) . ((len C1) + 1) = v & (vertex-seq C1) . 1 = the_sort_of t1 )

take t2 ; :: thesis: ( C1 = C . (k + 1) & len C1 = k + 1 & t2 = t | (p | (k + 1)) & (vertex-seq C1) . ((len C1) + 1) = v & (vertex-seq C1) . 1 = the_sort_of t2 )

thus C1 = C . (k + 1) by A1, A41, A47; :: thesis: ( len C1 = k + 1 & t2 = t | (p | (k + 1)) & (vertex-seq C1) . ((len C1) + 1) = v & (vertex-seq C1) . 1 = the_sort_of t2 )

thus len C1 = k + 1 by A47, FINSEQ_1:39; :: thesis: ( t2 = t | (p | (k + 1)) & (vertex-seq C1) . ((len C1) + 1) = v & (vertex-seq C1) . 1 = the_sort_of t2 )

thus t2 = t | (p | (k + 1)) by A47; :: thesis: ( (vertex-seq C1) . ((len C1) + 1) = v & (vertex-seq C1) . 1 = the_sort_of t2 )

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, FINSEQ_1:44

.= 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: (vertex-seq C1) . 1 = the_sort_of t2

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, FINSEQ_1:44

.= [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: verum

suppose A51:
k <> 0
; :: thesis: ex Ck being directed Chain of InducedGraph S ex t1 being Term of S,X st

( Ck = C . (k + 1) & len Ck = k + 1 & t1 = t | (p | (k + 1)) & (vertex-seq Ck) . ((len Ck) + 1) = v & (vertex-seq Ck) . 1 = the_sort_of t1 )

( Ck = C . (k + 1) & len Ck = k + 1 & t1 = t | (p | (k + 1)) & (vertex-seq Ck) . ((len Ck) + 1) = v & (vertex-seq Ck) . 1 = the_sort_of t1 )

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, FINSEQ_1:44

.= 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: ex t1 being Term of S,X st

( d = C . (k + 1) & len d = k + 1 & t1 = t | (p | (k + 1)) & (vertex-seq d) . ((len d) + 1) = v & (vertex-seq d) . 1 = the_sort_of t1 )

take t2 ; :: thesis: ( d = C . (k + 1) & len d = k + 1 & t2 = t | (p | (k + 1)) & (vertex-seq d) . ((len d) + 1) = v & (vertex-seq d) . 1 = the_sort_of t2 )

thus d = C . (k + 1) by A61, A55; :: thesis: ( len d = k + 1 & t2 = t | (p | (k + 1)) & (vertex-seq d) . ((len d) + 1) = v & (vertex-seq d) . 1 = the_sort_of t2 )

thus len d = (len C1) + k by A62, FINSEQ_1:22

.= k + 1 by FINSEQ_1:39 ; :: thesis: ( t2 = t | (p | (k + 1)) & (vertex-seq d) . ((len d) + 1) = v & (vertex-seq d) . 1 = the_sort_of t2 )

thus t2 = t | (p | (k + 1)) by A53; :: thesis: ( (vertex-seq d) . ((len d) + 1) = v & (vertex-seq d) . 1 = the_sort_of t2 )

thus (vertex-seq d) . ((len d) + 1) = v by A51, A62, A64, A59, CARD_1:27, MSSCYC_1:16; :: thesis: (vertex-seq d) . 1 = the_sort_of t2

(vertex-seq C1) . 1 = the Source of (InducedGraph S) . [o,rs1] by A60, FINSEQ_1:44

.= [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: verum

end;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, FINSEQ_1:44

.= 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: ex t1 being Term of S,X st

( d = C . (k + 1) & len d = k + 1 & t1 = t | (p | (k + 1)) & (vertex-seq d) . ((len d) + 1) = v & (vertex-seq d) . 1 = the_sort_of t1 )

take t2 ; :: thesis: ( d = C . (k + 1) & len d = k + 1 & t2 = t | (p | (k + 1)) & (vertex-seq d) . ((len d) + 1) = v & (vertex-seq d) . 1 = the_sort_of t2 )

thus d = C . (k + 1) by A61, A55; :: thesis: ( len d = k + 1 & t2 = t | (p | (k + 1)) & (vertex-seq d) . ((len d) + 1) = v & (vertex-seq d) . 1 = the_sort_of t2 )

thus len d = (len C1) + k by A62, FINSEQ_1:22

.= k + 1 by FINSEQ_1:39 ; :: thesis: ( t2 = t | (p | (k + 1)) & (vertex-seq d) . ((len d) + 1) = v & (vertex-seq d) . 1 = the_sort_of t2 )

thus t2 = t | (p | (k + 1)) by A53; :: thesis: ( (vertex-seq d) . ((len d) + 1) = v & (vertex-seq d) . 1 = the_sort_of t2 )

thus (vertex-seq d) . ((len d) + 1) = v by A51, A62, A64, A59, CARD_1:27, MSSCYC_1:16; :: thesis: (vertex-seq d) . 1 = the_sort_of t2

(vertex-seq C1) . 1 = the Source of (InducedGraph S) . [o,rs1] by A60, FINSEQ_1:44

.= [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: verum

for k being Nat holds S

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: verum

A68: (vertex-seq c) . ((len c) + 1) = v ; :: thesis: ex t being Element of the Sorts of (FreeMSA X) . v st depth t = n

set EG = the carrier' of (InducedGraph S);

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

deffunc H

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

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

defpred S

( 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

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

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

A81:
dom a = Seg (len (the_arity_of o))
by A77, FINSEQ_1:def 3;
let i be Nat; :: thesis: ( i in dom a implies ex t being Term of S,X st

( t = a . i & the_sort_of t = (the_arity_of o) . i ) )

assume A80: i in dom a ; :: thesis: ex t being Term of S,X st

( t = a . i & the_sort_of t = (the_arity_of o) . i )

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: ( t = a . i & the_sort_of t = (the_arity_of o) . i )

thus t = a . i by A77, A80; :: thesis: the_sort_of t = (the_arity_of o) . i

thus the_sort_of t = (the_arity_of o) . i by MSATERM:14; :: thesis: verum

end;( t = a . i & the_sort_of t = (the_arity_of o) . i ) )

assume A80: i in dom a ; :: thesis: ex t being Term of S,X st

( t = a . i & the_sort_of t = (the_arity_of o) . i )

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: ( t = a . i & the_sort_of t = (the_arity_of o) . i )

thus t = a . i by A77, A80; :: thesis: the_sort_of t = (the_arity_of o) . i

thus the_sort_of t = (the_arity_of o) . i by MSATERM:14; :: thesis: verum

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

proof

consider C being FinSequence of S -Terms X such that
let k be Nat; :: thesis: ( 1 <= k & k < n1 implies for x being Element of S -Terms X ex y being Element of S -Terms X st S_{1}[k,x,y] )

assume that

1 <= k and

A83: k < n1 ; :: thesis: for x being Element of S -Terms X ex y being Element of S -Terms X st S_{1}[k,x,y]

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: ex y being Element of S -Terms X st S_{1}[k,x,y]

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_{2}[ 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_{2}[e,u] )

A92: for e being object st e in dom (the_arity_of o) holds

S_{2}[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;

reconsider y = [o, the carrier of S] -tree a as Term of S,X by MSATERM:1;

take y ; :: thesis: S_{1}[k,x,y]

take o ; :: thesis: ex rs1 being SortSymbol of S ex Ck, Ck1 being Term of S,X ex a being ArgumentSeq of Sym (o,X) st

( Ck = x & y = Ck1 & c . (k + 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)] ) ) ) )

take rs1 ; :: thesis: ex Ck, Ck1 being Term of S,X ex a being ArgumentSeq of Sym (o,X) st

( Ck = x & y = Ck1 & c . (k + 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)] ) ) ) )

take x ; :: thesis: ex Ck1 being Term of S,X ex a being ArgumentSeq of Sym (o,X) st

( x = x & y = Ck1 & c . (k + 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 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)] ) ) ) )

take y ; :: thesis: ex a being ArgumentSeq of Sym (o,X) st

( x = x & y = y & c . (k + 1) = [o,rs1] & y = [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 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)] ) ) ) )

take a ; :: thesis: ( x = x & y = y & c . (k + 1) = [o,rs1] & y = [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 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)] ) ) ) )

thus ( x = x & y = y ) ; :: thesis: ( c . (k + 1) = [o,rs1] & y = [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 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)] ) ) ) )

thus c . (k + 1) = [o,rs1] by A85; :: thesis: ( y = [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 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)] ) ) ) )

thus y = [o, the carrier of S] -tree a ; :: thesis: 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 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)] ) )

let i be Nat; :: thesis: ( i in dom a implies 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 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)] ) ) )

assume A97: i in dom a ; :: thesis: 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 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)] ) )

then reconsider t = a . i as Term of S,X by DTCONSTR:2;

take t ; :: thesis: ( t = a . i & the_sort_of t = (the_arity_of o) . i & ( 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)] ) )

thus t = a . i ; :: thesis: ( the_sort_of t = (the_arity_of o) . i & ( 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)] ) )

thus the_sort_of t = (the_arity_of o) . i by A97, MSATERM:23; :: thesis: ( ( 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)] ) )

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: verum

end;assume that

1 <= k and

A83: k < n1 ; :: thesis: for x being Element of S -Terms X ex y being Element of S -Terms X st S

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: ex y being Element of S -Terms X st S

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

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

proof

consider a being Function of (dom (the_arity_of o)),(S -Terms X) such that
let e be object ; :: thesis: ( e in dom (the_arity_of o) implies ex u being object st

( u in S -Terms X & S_{2}[e,u] ) )

assume A89: e in dom (the_arity_of o) ; :: thesis: ex u being object st

( u in S -Terms X & S_{2}[e,u] )

end;( u in S -Terms X & S

assume A89: e in dom (the_arity_of o) ; :: thesis: ex u being object st

( u in S -Terms X & S

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

end;

suppose A90:
( (the_arity_of o) . e = rs1 & the_sort_of x = rs1 )
; :: thesis: ex u being object st

( u in S -Terms X & S_{2}[e,u] )

( u in S -Terms X & S

take
x
; :: thesis: ( x in S -Terms X & S_{2}[e,x] )

thus ( x in S -Terms X & S_{2}[e,x] )
by A90; :: thesis: verum

end;thus ( x in S -Terms X & S

suppose A91:
( (the_arity_of o) . e <> rs1 or the_sort_of x <> rs1 )
; :: thesis: ex u being object st

( u in S -Terms X & S_{2}[e,u] )

( u in S -Terms X & S

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: ( t in S -Terms X & S_{2}[e,t] )

thus ( t in S -Terms X & S_{2}[e,t] )
by A91; :: thesis: verum

end;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: ( t in S -Terms X & S

thus ( t in S -Terms X & S

A92: for e being object st e in dom (the_arity_of o) holds

S

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: 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 )

then reconsider a = a as ArgumentSeq of Sym (o,X) by A93, MSATERM:24;ex t being Term of S,X st

( t = a . i & the_sort_of t = (the_arity_of o) . i )

let i be Nat; :: thesis: ( i in dom a implies ex t being Term of S,X st

( t = a . i & the_sort_of b_{3} = (the_arity_of o) . b_{2} ) )

assume A94: i in dom a ; :: thesis: ex t being Term of S,X st

( t = a . i & the_sort_of b_{3} = (the_arity_of o) . b_{2} )

then reconsider t = a . i as Term of S,X by DTCONSTR:2;

take t = t; :: thesis: ( t = a . i & the_sort_of b_{2} = (the_arity_of o) . b_{1} )

thus t = a . i ; :: thesis: the_sort_of b_{2} = (the_arity_of o) . b_{1}

end;( t = a . i & the_sort_of b

assume A94: i in dom a ; :: thesis: ex t being Term of S,X st

( t = a . i & the_sort_of b

then reconsider t = a . i as Term of S,X by DTCONSTR:2;

take t = t; :: thesis: ( t = a . i & the_sort_of b

thus t = a . i ; :: thesis: the_sort_of b

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

end;

suppose
( (the_arity_of o) . i = rs1 & the_sort_of x = rs1 )
; :: thesis: the_sort_of b_{2} = (the_arity_of o) . b_{1}

end;

end;

suppose A95:
( (the_arity_of o) . i <> rs1 or the_sort_of x <> rs1 )
; :: thesis: the_sort_of b_{2} = (the_arity_of o) . b_{1}

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: verum

end;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: verum

reconsider y = [o, the carrier of S] -tree a as Term of S,X by MSATERM:1;

take y ; :: thesis: S

take o ; :: thesis: ex rs1 being SortSymbol of S ex Ck, Ck1 being Term of S,X ex a being ArgumentSeq of Sym (o,X) st

( Ck = x & y = Ck1 & c . (k + 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)] ) ) ) )

take rs1 ; :: thesis: ex Ck, Ck1 being Term of S,X ex a being ArgumentSeq of Sym (o,X) st

( Ck = x & y = Ck1 & c . (k + 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)] ) ) ) )

take x ; :: thesis: ex Ck1 being Term of S,X ex a being ArgumentSeq of Sym (o,X) st

( x = x & y = Ck1 & c . (k + 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 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)] ) ) ) )

take y ; :: thesis: ex a being ArgumentSeq of Sym (o,X) st

( x = x & y = y & c . (k + 1) = [o,rs1] & y = [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 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)] ) ) ) )

take a ; :: thesis: ( x = x & y = y & c . (k + 1) = [o,rs1] & y = [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 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)] ) ) ) )

thus ( x = x & y = y ) ; :: thesis: ( c . (k + 1) = [o,rs1] & y = [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 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)] ) ) ) )

thus c . (k + 1) = [o,rs1] by A85; :: thesis: ( y = [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 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)] ) ) ) )

thus y = [o, the carrier of S] -tree a ; :: thesis: 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 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)] ) )

let i be Nat; :: thesis: ( i in dom a implies 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 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)] ) ) )

assume A97: i in dom a ; :: thesis: 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 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)] ) )

then reconsider t = a . i as Term of S,X by DTCONSTR:2;

take t ; :: thesis: ( t = a . i & the_sort_of t = (the_arity_of o) . i & ( 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)] ) )

thus t = a . i ; :: thesis: ( the_sort_of t = (the_arity_of o) . i & ( 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)] ) )

thus the_sort_of t = (the_arity_of o) . i by A97, MSATERM:23; :: thesis: ( ( 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)] ) )

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: verum

A98: ( len C = n1 & ( C . 1 = C1 or n1 = 0 ) & ( for k being Nat st 1 <= k & k < n1 holds

S

defpred S

( 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

S

proof

set cn = c . (len c);
let k be Nat; :: thesis: ( S_{2}[k] implies S_{2}[k + 1] )

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: S_{2}[k + 1]

assume that

A102: 1 <= k + 1 and

A103: k + 1 <= n ; :: thesis: ex C0 being Term of S,X ex o being OperSymbol of S st

( C0 = C . (k + 1) & o = (c . (k + 1)) `1 & the_sort_of C0 = the_result_sort_of o & height (dom C0) = k + 1 )

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;

end;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: S

assume that

A102: 1 <= k + 1 and

A103: k + 1 <= n ; :: thesis: ex C0 being Term of S,X ex o being OperSymbol of S st

( C0 = C . (k + 1) & o = (c . (k + 1)) `1 & the_sort_of C0 = the_result_sort_of o & height (dom C0) = k + 1 )

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
( k = 0 or k <> 0 )
;

end;

suppose A107:
k = 0
; :: thesis: ex C0 being Term of S,X ex o being OperSymbol of S st

( C0 = C . (k + 1) & o = (c . (k + 1)) `1 & the_sort_of C0 = the_result_sort_of o & height (dom C0) = k + 1 )

( C0 = C . (k + 1) & o = (c . (k + 1)) `1 & the_sort_of C0 = the_result_sort_of o & height (dom C0) = k + 1 )

take
C1
; :: thesis: ex o being OperSymbol of S st

( C1 = C . (k + 1) & o = (c . (k + 1)) `1 & the_sort_of C1 = the_result_sort_of o & height (dom C1) = k + 1 )

take o ; :: thesis: ( C1 = C . (k + 1) & o = (c . (k + 1)) `1 & the_sort_of C1 = the_result_sort_of o & height (dom C1) = k + 1 )

thus C1 = C . (k + 1) by A1, A98, A107; :: thesis: ( o = (c . (k + 1)) `1 & the_sort_of C1 = the_result_sort_of o & height (dom C1) = k + 1 )

thus o = (c . (k + 1)) `1 by A73, A107; :: thesis: ( the_sort_of C1 = the_result_sort_of o & height (dom C1) = k + 1 )

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: height (dom C1) = k + 1

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;

hence height (dom C1) = k + 1 by A107, A113, A115, TREES_1:42, TREES_3:79; :: thesis: verum

end;( C1 = C . (k + 1) & o = (c . (k + 1)) `1 & the_sort_of C1 = the_result_sort_of o & height (dom C1) = k + 1 )

take o ; :: thesis: ( C1 = C . (k + 1) & o = (c . (k + 1)) `1 & the_sort_of C1 = the_result_sort_of o & height (dom C1) = k + 1 )

thus C1 = C . (k + 1) by A1, A98, A107; :: thesis: ( o = (c . (k + 1)) `1 & the_sort_of C1 = the_result_sort_of o & height (dom C1) = k + 1 )

thus o = (c . (k + 1)) `1 by A73, A107; :: thesis: ( the_sort_of C1 = the_result_sort_of o & height (dom C1) = k + 1 )

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: height (dom C1) = k + 1

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: for t9 being finite Tree st t9 in rng w holds

height t9 <= height dt

dom t = elementary_tree 0
by A114, TREES_4:3;height t9 <= height dt

let t9 be finite Tree; :: thesis: ( t9 in rng w implies height t9 <= height dt )

assume t9 in rng w ; :: thesis: height t9 <= height dt

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: verum

end;assume t9 in rng w ; :: thesis: height t9 <= height dt

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: verum

hence height (dom C1) = k + 1 by A107, A113, A115, TREES_1:42, TREES_3:79; :: thesis: verum

suppose A119:
k <> 0
; :: thesis: ex C0 being Term of S,X ex o being OperSymbol of S st

( C0 = C . (k + 1) & o = (c . (k + 1)) `1 & the_sort_of C0 = the_result_sort_of o & height (dom C0) = k + 1 )

( C0 = C . (k + 1) & o = (c . (k + 1)) `1 & the_sort_of C0 = the_result_sort_of o & height (dom C0) = k + 1 )

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: ex o being OperSymbol of S st

( Ck1 = C . (k + 1) & o = (c . (k + 1)) `1 & the_sort_of Ck1 = the_result_sort_of o & height (dom Ck1) = k + 1 )

take o1 ; :: thesis: ( Ck1 = C . (k + 1) & o1 = (c . (k + 1)) `1 & the_sort_of Ck1 = the_result_sort_of o1 & height (dom Ck1) = k + 1 )

thus Ck1 = C . (k + 1) by A125; :: thesis: ( o1 = (c . (k + 1)) `1 & the_sort_of Ck1 = the_result_sort_of o1 & height (dom Ck1) = k + 1 )

thus o1 = (c . (k + 1)) `1 by A126; :: thesis: ( the_sort_of Ck1 = the_result_sort_of o1 & height (dom Ck1) = k + 1 )

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: height (dom Ck1) = k + 1

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;

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: verum

end;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: ex o being OperSymbol of S st

( Ck1 = C . (k + 1) & o = (c . (k + 1)) `1 & the_sort_of Ck1 = the_result_sort_of o & height (dom Ck1) = k + 1 )

take o1 ; :: thesis: ( Ck1 = C . (k + 1) & o1 = (c . (k + 1)) `1 & the_sort_of Ck1 = the_result_sort_of o1 & height (dom Ck1) = k + 1 )

thus Ck1 = C . (k + 1) by A125; :: thesis: ( o1 = (c . (k + 1)) `1 & the_sort_of Ck1 = the_result_sort_of o1 & height (dom Ck1) = k + 1 )

thus o1 = (c . (k + 1)) `1 by A126; :: thesis: ( the_sort_of Ck1 = the_result_sort_of o1 & height (dom Ck1) = k + 1 )

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: height (dom Ck1) = k + 1

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: for t9 being finite Tree st t9 in rng w holds

height t9 <= height dt

(doms a) . i = dom t
by A135, A133, A137, A140, A139, A141, FUNCT_6:22;height t9 <= height dt

let t9 be finite Tree; :: thesis: ( t9 in rng w implies height b_{1} <= height dt )

assume t9 in rng w ; :: thesis: height b_{1} <= height dt

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;

end;assume t9 in rng w ; :: thesis: height b

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
( ( the_sort_of t99 = rs1 & the_sort_of Ck9 = rs1 ) or the_sort_of t99 <> rs1 or the_sort_of Ck9 <> rs1 )
;

end;

suppose
( the_sort_of t99 = rs1 & the_sort_of Ck9 = rs1 )
; :: thesis: height b_{1} <= height dt

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

end;suppose
( the_sort_of t99 <> rs1 or the_sort_of Ck9 <> rs1 )
; :: thesis: height b_{1} <= height dt

end;

end;

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: verum

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

for k being Nat holds S

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: depth Cn = n

thus depth Cn = n by A156, MSAFREE2:def 14; :: thesis: verum