:: MSSCYC_2 semantic presentation
begin
definition
let S be ManySortedSign ;
defpred S1[ set ] means ex op, v being set st
( $1 = [op,v] & op in the carrier' of S & v in the carrier of S & ex n being Nat ex args being Element of the carrier of S * st
( the Arity of S . op = args & n in dom args & args . n = v ) );
func InducedEdges S -> set means :Def1: :: MSSCYC_2:def 1
for x being set holds
( x in it iff ex op, v being set st
( x = [op,v] & op in the carrier' of S & v in the carrier of S & ex n being Nat ex args being Element of the carrier of S * st
( the Arity of S . op = args & n in dom args & args . n = v ) ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ex op, v being set st
( x = [op,v] & op in the carrier' of S & v in the carrier of S & ex n being Nat ex args being Element of the carrier of S * st
( the Arity of S . op = args & n in dom args & args . n = v ) ) )
proof
set XX = [: the carrier' of S, the carrier of S:];
consider X being set such that
A1: for x being set holds
( x in X iff ( x in [: the carrier' of S, the carrier of S:] & S1[x] ) ) from XBOOLE_0:sch_1();
take X ; ::_thesis: for x being set holds
( x in X iff ex op, v being set st
( x = [op,v] & op in the carrier' of S & v in the carrier of S & ex n being Nat ex args being Element of the carrier of S * st
( the Arity of S . op = args & n in dom args & args . n = v ) ) )
let x be set ; ::_thesis: ( x in X iff ex op, v being set st
( x = [op,v] & op in the carrier' of S & v in the carrier of S & ex n being Nat ex args being Element of the carrier of S * st
( the Arity of S . op = args & n in dom args & args . n = v ) ) )
thus ( x in X implies S1[x] ) by A1; ::_thesis: ( ex op, v being set st
( x = [op,v] & op in the carrier' of S & v in the carrier of S & ex n being Nat ex args being Element of the carrier of S * st
( the Arity of S . op = args & n in dom args & args . n = v ) ) implies x in X )
assume A2: S1[x] ; ::_thesis: x in X
then x in [: the carrier' of S, the carrier of S:] by ZFMISC_1:def_2;
hence x in X by A1, A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex op, v being set st
( x = [op,v] & op in the carrier' of S & v in the carrier of S & ex n being Nat ex args being Element of the carrier of S * st
( the Arity of S . op = args & n in dom args & args . n = v ) ) ) ) & ( for x being set holds
( x in b2 iff ex op, v being set st
( x = [op,v] & op in the carrier' of S & v in the carrier of S & ex n being Nat ex args being Element of the carrier of S * st
( the Arity of S . op = args & n in dom args & args . n = v ) ) ) ) holds
b1 = b2
proof
for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3();
hence for b1, b2 being set st ( for x being set holds
( x in b1 iff ex op, v being set st
( x = [op,v] & op in the carrier' of S & v in the carrier of S & ex n being Nat ex args being Element of the carrier of S * st
( the Arity of S . op = args & n in dom args & args . n = v ) ) ) ) & ( for x being set holds
( x in b2 iff ex op, v being set st
( x = [op,v] & op in the carrier' of S & v in the carrier of S & ex n being Nat ex args being Element of the carrier of S * st
( the Arity of S . op = args & n in dom args & args . n = v ) ) ) ) holds
b1 = b2 ; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines InducedEdges MSSCYC_2:def_1_:_
for S being ManySortedSign
for b2 being set holds
( b2 = InducedEdges S iff for x being set holds
( x in b2 iff ex op, v being set st
( x = [op,v] & op in the carrier' of S & v in the carrier of S & ex n being Nat ex args being Element of the carrier of S * st
( the Arity of S . op = args & n in dom args & args . n = v ) ) ) );
theorem Th1: :: MSSCYC_2:1
for S being ManySortedSign holds InducedEdges S c= [: the carrier' of S, the carrier of S:]
proof
let S be ManySortedSign ; ::_thesis: InducedEdges S c= [: the carrier' of S, the carrier of S:]
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in InducedEdges S or x in [: the carrier' of S, the carrier of S:] )
assume x in InducedEdges S ; ::_thesis: x in [: the carrier' of S, the carrier of S:]
then ex op, v being set st
( x = [op,v] & op in the carrier' of S & v in the carrier of S & ex n being Nat ex args being Element of the carrier of S * st
( the Arity of S . op = args & n in dom args & args . n = v ) ) by Def1;
hence x in [: the carrier' of S, the carrier of S:] by ZFMISC_1:def_2; ::_thesis: verum
end;
definition
let S be ManySortedSign ;
set IE = InducedEdges S;
set IV = the carrier of S;
func InducedSource S -> Function of (InducedEdges S), the carrier of S means :Def2: :: MSSCYC_2:def 2
for e being set st e in InducedEdges S holds
it . e = e `2 ;
existence
ex b1 being Function of (InducedEdges S), the carrier of S st
for e being set st e in InducedEdges S holds
b1 . e = e `2
proof
deffunc H1( set ) -> set = $1 `2 ;
A1: for x being set st x in InducedEdges S holds
H1(x) in the carrier of S
proof
let x be set ; ::_thesis: ( x in InducedEdges S implies H1(x) in the carrier of S )
assume A2: x in InducedEdges S ; ::_thesis: H1(x) in the carrier of S
InducedEdges S c= [: the carrier' of S, the carrier of S:] by Th1;
hence H1(x) in the carrier of S by A2, MCART_1:10; ::_thesis: verum
end;
ex f being Function of (InducedEdges S), the carrier of S st
for x being set st x in InducedEdges S holds
f . x = H1(x) from FUNCT_2:sch_2(A1);
hence ex b1 being Function of (InducedEdges S), the carrier of S st
for e being set st e in InducedEdges S holds
b1 . e = e `2 ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of (InducedEdges S), the carrier of S st ( for e being set st e in InducedEdges S holds
b1 . e = e `2 ) & ( for e being set st e in InducedEdges S holds
b2 . e = e `2 ) holds
b1 = b2
proof
let F1, F2 be Function of (InducedEdges S), the carrier of S; ::_thesis: ( ( for e being set st e in InducedEdges S holds
F1 . e = e `2 ) & ( for e being set st e in InducedEdges S holds
F2 . e = e `2 ) implies F1 = F2 )
assume that
A3: for e being set st e in InducedEdges S holds
F1 . e = e `2 and
A4: for e being set st e in InducedEdges S holds
F2 . e = e `2 ; ::_thesis: F1 = F2
A5: now__::_thesis:_for_x_being_set_st_x_in_InducedEdges_S_holds_
F1_._x_=_F2_._x
let x be set ; ::_thesis: ( x in InducedEdges S implies F1 . x = F2 . x )
assume A6: x in InducedEdges S ; ::_thesis: F1 . x = F2 . x
then F1 . x = x `2 by A3;
hence F1 . x = F2 . x by A4, A6; ::_thesis: verum
end;
now__::_thesis:_(_the_carrier_of_S_is_empty_implies_InducedEdges_S_is_empty_)
assume the carrier of S is empty ; ::_thesis: InducedEdges S is empty
then [: the carrier' of S, the carrier of S:] is empty by ZFMISC_1:90;
hence InducedEdges S is empty by Th1, XBOOLE_1:3; ::_thesis: verum
end;
then ( dom F1 = InducedEdges S & dom F2 = InducedEdges S ) by FUNCT_2:def_1;
hence F1 = F2 by A5, FUNCT_1:2; ::_thesis: verum
end;
set OS = the carrier' of S;
set RS = the ResultSort of S;
func InducedTarget S -> Function of (InducedEdges S), the carrier of S means :Def3: :: MSSCYC_2:def 3
for e being set st e in InducedEdges S holds
it . e = the ResultSort of S . (e `1);
existence
ex b1 being Function of (InducedEdges S), the carrier of S st
for e being set st e in InducedEdges S holds
b1 . e = the ResultSort of S . (e `1)
proof
deffunc H1( set ) -> set = the ResultSort of S . ($1 `1);
A7: for x being set st x in InducedEdges S holds
H1(x) in the carrier of S
proof
let x be set ; ::_thesis: ( x in InducedEdges S implies H1(x) in the carrier of S )
assume A8: x in InducedEdges S ; ::_thesis: H1(x) in the carrier of S
InducedEdges S c= [: the carrier' of S, the carrier of S:] by Th1;
then ( x `1 in the carrier' of S & x `2 in the carrier of S ) by A8, MCART_1:10;
hence H1(x) in the carrier of S by FUNCT_2:5; ::_thesis: verum
end;
ex f being Function of (InducedEdges S), the carrier of S st
for x being set st x in InducedEdges S holds
f . x = H1(x) from FUNCT_2:sch_2(A7);
hence ex b1 being Function of (InducedEdges S), the carrier of S st
for e being set st e in InducedEdges S holds
b1 . e = the ResultSort of S . (e `1) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of (InducedEdges S), the carrier of S st ( for e being set st e in InducedEdges S holds
b1 . e = the ResultSort of S . (e `1) ) & ( for e being set st e in InducedEdges S holds
b2 . e = the ResultSort of S . (e `1) ) holds
b1 = b2
proof
let F1, F2 be Function of (InducedEdges S), the carrier of S; ::_thesis: ( ( for e being set st e in InducedEdges S holds
F1 . e = the ResultSort of S . (e `1) ) & ( for e being set st e in InducedEdges S holds
F2 . e = the ResultSort of S . (e `1) ) implies F1 = F2 )
assume that
A9: for e being set st e in InducedEdges S holds
F1 . e = the ResultSort of S . (e `1) and
A10: for e being set st e in InducedEdges S holds
F2 . e = the ResultSort of S . (e `1) ; ::_thesis: F1 = F2
A11: now__::_thesis:_for_x_being_set_st_x_in_InducedEdges_S_holds_
F1_._x_=_F2_._x
let x be set ; ::_thesis: ( x in InducedEdges S implies F1 . x = F2 . x )
assume A12: x in InducedEdges S ; ::_thesis: F1 . x = F2 . x
then F1 . x = the ResultSort of S . (x `1) by A9;
hence F1 . x = F2 . x by A10, A12; ::_thesis: verum
end;
now__::_thesis:_(_the_carrier_of_S_is_empty_implies_InducedEdges_S_is_empty_)
assume the carrier of S is empty ; ::_thesis: InducedEdges S is empty
then [: the carrier' of S, the carrier of S:] is empty by ZFMISC_1:90;
hence InducedEdges S is empty by Th1, XBOOLE_1:3; ::_thesis: verum
end;
then ( dom F1 = InducedEdges S & dom F2 = InducedEdges S ) by FUNCT_2:def_1;
hence F1 = F2 by A11, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines InducedSource MSSCYC_2:def_2_:_
for S being ManySortedSign
for b2 being Function of (InducedEdges S), the carrier of S holds
( b2 = InducedSource S iff for e being set st e in InducedEdges S holds
b2 . e = e `2 );
:: deftheorem Def3 defines InducedTarget MSSCYC_2:def_3_:_
for S being ManySortedSign
for b2 being Function of (InducedEdges S), the carrier of S holds
( b2 = InducedTarget S iff for e being set st e in InducedEdges S holds
b2 . e = the ResultSort of S . (e `1) );
definition
let S be non empty ManySortedSign ;
func InducedGraph S -> Graph equals :: MSSCYC_2:def 4
MultiGraphStruct(# the carrier of S,(InducedEdges S),(InducedSource S),(InducedTarget S) #);
coherence
MultiGraphStruct(# the carrier of S,(InducedEdges S),(InducedSource S),(InducedTarget S) #) is Graph ;
end;
:: deftheorem defines InducedGraph MSSCYC_2:def_4_:_
for S being non empty ManySortedSign holds InducedGraph S = MultiGraphStruct(# the carrier of S,(InducedEdges S),(InducedSource S),(InducedTarget S) #);
theorem Th2: :: MSSCYC_2:2
for S being non empty non void ManySortedSign
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 ) )
proof
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 )
proof
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 Element of 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 S1[ 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 Element of 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 S1[k,x,y]
proof
let k be Element of 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 S1[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;
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 S1[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;
now__::_thesis:_not_t1_is_root
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 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
.= <*((p /^ k) . 1)*> by A22, PARTFUN1:def_6 ;
consider i being Element of 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 S1[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: S1[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;
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 Element of NAT st 1 <= k & k < n1 holds
S1[k,C . k,C . (k + 1)] ) ) from RECDEF_1:sch_4(A17);
defpred S2[ 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 S2[i] holds
S2[i + 1]
proof
let k be Nat; ::_thesis: ( S2[k] implies S2[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: S2[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;
percases ( k = 0 or k <> 0 ) ;
supposeA47: 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 )
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
A49: 1 in dom p by A1, A4, A6, A11, CARD_1:27, FINSEQ_5:6;
p | 1 = <*(p9 /. 1)*> by A1, A4, A6, A11, CARD_1:27, FINSEQ_5:20
.= <*(p . 1)*> by A49, PARTFUN1:def_6
.= <*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;
supposeA51: 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 )
k in NAT by ORDINAL1:def_12;
then 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;
end;
end;
A66: S2[ 0 ] ;
for k being Nat holds S2[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;
given c being directed Chain of InducedGraph S such that A67: len c = n and
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 H1( set ) -> 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 set st e in the carrier of S holds
H1(e) <> {} ;
consider cX being ManySortedSet of the carrier of S such that
A70: for e being set st e in the carrier of S holds
cX . e in H1(e) from PBOOLE:sch_1(A69);
defpred S1[ 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 H2( 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 = H2(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: ( 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;
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 Element of NAT st 1 <= k & k < n1 holds
for x being Element of S -Terms X ex y being Element of S -Terms X st S1[k,x,y]
proof
let k be Element of NAT ; ::_thesis: ( 1 <= k & k < n1 implies for x being Element of S -Terms X ex y being Element of S -Terms X st S1[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 S1[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 S1[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 S2[ set , set ] 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 set st e in dom (the_arity_of o) holds
ex u being set st
( u in S -Terms X & S2[e,u] )
proof
let e be set ; ::_thesis: ( e in dom (the_arity_of o) implies ex u being set st
( u in S -Terms X & S2[e,u] ) )
assume A89: e in dom (the_arity_of o) ; ::_thesis: ex u being set st
( u in S -Terms X & S2[e,u] )
percases ( ( (the_arity_of o) . e = rs1 & the_sort_of x = rs1 ) or (the_arity_of o) . e <> rs1 or the_sort_of x <> rs1 ) ;
supposeA90: ( (the_arity_of o) . e = rs1 & the_sort_of x = rs1 ) ; ::_thesis: ex u being set st
( u in S -Terms X & S2[e,u] )
take x ; ::_thesis: ( x in S -Terms X & S2[e,x] )
thus ( x in S -Terms X & S2[e,x] ) by A90; ::_thesis: verum
end;
supposeA91: ( (the_arity_of o) . e <> rs1 or the_sort_of x <> rs1 ) ; ::_thesis: ex u being set st
( u in S -Terms X & S2[e,u] )
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 & S2[e,t] )
thus ( t in S -Terms X & S2[e,t] ) by A91; ::_thesis: verum
end;
end;
end;
consider a being Function of (dom (the_arity_of o)),(S -Terms X) such that
A92: for e being set st e in dom (the_arity_of o) holds
S2[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:_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_)
let i be Nat; ::_thesis: ( i in dom a implies ex t being Term of S,X st
( t = a . i & the_sort_of b3 = (the_arity_of o) . b2 ) )
assume A94: i in dom a ; ::_thesis: ex t being Term of S,X st
( t = a . i & the_sort_of b3 = (the_arity_of o) . b2 )
then reconsider t = a . i as Term of S,X by DTCONSTR:2;
take t = t; ::_thesis: ( t = a . i & the_sort_of b2 = (the_arity_of o) . b1 )
thus t = a . i ; ::_thesis: the_sort_of b2 = (the_arity_of o) . b1
percases ( ( (the_arity_of o) . 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: the_sort_of b2 = (the_arity_of o) . b1
hence the_sort_of t = (the_arity_of o) . i by A92, A93, A94; ::_thesis: verum
end;
supposeA95: ( (the_arity_of o) . i <> rs1 or the_sort_of x <> rs1 ) ; ::_thesis: the_sort_of b2 = (the_arity_of o) . b1
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;
end;
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: S1[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;
consider C being FinSequence of S -Terms X such that
A98: ( len C = n1 & ( C . 1 = C1 or n1 = 0 ) & ( for k being Element of NAT st 1 <= k & k < n1 holds
S1[k,C . k,C . (k + 1)] ) ) from RECDEF_1:sch_4(A82);
defpred S2[ 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 S2[k] holds
S2[k + 1]
proof
let k be Nat; ::_thesis: ( S2[k] implies S2[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: S2[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;
percases ( k = 0 or k <> 0 ) ;
supposeA107: 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 )
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, MCART_1:7; ::_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
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;
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: verum
end;
supposeA119: 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 )
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, MCART_1:7; ::_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
let t9 be finite Tree; ::_thesis: ( t9 in rng w implies height b1 <= height dt )
assume t9 in rng w ; ::_thesis: height b1 <= 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;
percases ( ( the_sort_of t99 = rs1 & the_sort_of Ck9 = rs1 ) or the_sort_of t99 <> rs1 or the_sort_of Ck9 <> rs1 ) ;
suppose ( the_sort_of t99 = rs1 & the_sort_of Ck9 = rs1 ) ; ::_thesis: height b1 <= 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 b1 <= height dt
hence height t9 <= height dt by A146, A149, A150, TREES_1:42, TREES_4:3; ::_thesis: verum
end;
end;
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, MCART_1:7 ;
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;
end;
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: S2[ 0 ] ;
for k being Nat holds S2[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
end;
theorem :: MSSCYC_2:3
for S being non empty void ManySortedSign holds
( S is monotonic iff InducedGraph S is well-founded )
proof
let S be non empty void ManySortedSign ; ::_thesis: ( S is monotonic iff InducedGraph S is well-founded )
set G = InducedGraph S;
set OS = the carrier' of S;
set CA = the carrier of S;
set AR = the Arity of S;
hereby ::_thesis: ( InducedGraph S is well-founded implies S is monotonic )
assume S is monotonic ; ::_thesis: InducedGraph S is well-founded
assume not InducedGraph S is well-founded ; ::_thesis: contradiction
then consider v being Element of the carrier of (InducedGraph S) such that
A1: for n being Element of NAT ex c being directed Chain of InducedGraph S st
( not c is empty & (vertex-seq c) . ((len c) + 1) = v & len c > n ) by MSSCYC_1:def_4;
consider e being directed Chain of InducedGraph S such that
A2: not e is empty and
(vertex-seq e) . ((len e) + 1) = v and
len e > 0 by A1;
e is FinSequence of the carrier' of (InducedGraph S) by MSSCYC_1:def_1;
then A3: rng e c= the carrier' of (InducedGraph S) by FINSEQ_1:def_4;
1 in dom e by A2, FINSEQ_5:6;
then e . 1 in rng e by FUNCT_1:def_3;
then ex op, v being set st
( e . 1 = [op,v] & op in the carrier' of S & v in the carrier of S & ex n being Nat ex args being Element of the carrier of S * st
( the Arity of S . op = args & n in dom args & args . n = v ) ) by A3, Def1;
hence contradiction ; ::_thesis: verum
end;
assume InducedGraph S is well-founded ; ::_thesis: S is monotonic
let A be non-empty finitely-generated MSAlgebra over S; :: according to MSAFREE2:def_13 ::_thesis: A is finite-yielding
thus the Sorts of A is V34() by MSAFREE2:def_10; :: according to MSAFREE2:def_11 ::_thesis: verum
end;
theorem :: MSSCYC_2:4
for S being non empty non void ManySortedSign st S is monotonic holds
InducedGraph S is well-founded
proof
let S be non empty non void ManySortedSign ; ::_thesis: ( S is monotonic implies InducedGraph S is well-founded )
set G = InducedGraph S;
assume S is monotonic ; ::_thesis: InducedGraph S is well-founded
then reconsider S = S as non empty non void monotonic ManySortedSign ;
set A = the non-empty finite-yielding MSAlgebra over S;
assume not InducedGraph S is well-founded ; ::_thesis: contradiction
then consider v being Element of the carrier of (InducedGraph S) such that
A1: for n being Element of NAT ex c being directed Chain of InducedGraph S st
( not c is empty & (vertex-seq c) . ((len c) + 1) = v & len c > n ) by MSSCYC_1:def_4;
reconsider v = v as SortSymbol of S ;
consider s being non empty finite Subset of NAT such that
A2: s = { (depth t) where t is Element of the Sorts of (FreeEnv the non-empty finite-yielding MSAlgebra over S) . v : verum } and
depth (v, the non-empty finite-yielding MSAlgebra over S) = max s by CIRCUIT1:def_6;
max s in NAT by ORDINAL1:def_12;
then consider c being directed Chain of InducedGraph S such that
not c is empty and
A3: (vertex-seq c) . ((len c) + 1) = v and
A4: len c > max s by A1;
1 <= len c by A4, NAT_1:14;
then consider t being Element of the Sorts of (FreeMSA the Sorts of the non-empty finite-yielding MSAlgebra over S) . v such that
A5: depth t = len c by A3, Th2;
reconsider t9 = t as Element of the Sorts of (FreeEnv the non-empty finite-yielding MSAlgebra over S) . v ;
( ex t99 being Element of the Sorts of (FreeMSA the Sorts of the non-empty finite-yielding MSAlgebra over S) . v st
( t9 = t99 & depth t9 = depth t99 ) & depth t9 in s ) by A2, CIRCUIT1:def_5;
hence contradiction by A4, A5, XXREAL_2:def_8; ::_thesis: verum
end;
theorem Th5: :: MSSCYC_2:5
for S being non empty non void ManySortedSign
for X being V2() V34() ManySortedSet of the carrier of S st S is finitely_operated holds
for n being Nat
for v being SortSymbol of S holds { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= n } is finite
proof
let S be non empty non void ManySortedSign ; ::_thesis: for X being V2() V34() ManySortedSet of the carrier of S st S is finitely_operated holds
for n being Nat
for v being SortSymbol of S holds { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= n } is finite
let X be V2() V34() ManySortedSet of the carrier of S; ::_thesis: ( S is finitely_operated implies for n being Nat
for v being SortSymbol of S holds { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= n } is finite )
assume A1: S is finitely_operated ; ::_thesis: for n being Nat
for v being SortSymbol of S holds { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= n } is finite
set SF = the Sorts of (FreeMSA X);
defpred S1[ Nat] means for v being SortSymbol of S holds { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= $1 } is finite ;
A2: FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) by MSAFREE:def_14;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
deffunc H1( set ) -> set = $1;
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A4: for v being SortSymbol of S holds { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= n } is finite ; ::_thesis: S1[n + 1]
let v be SortSymbol of S; ::_thesis: { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= n + 1 } is finite
defpred S2[ Element of the Sorts of (FreeMSA X) . v] means depth $1 = n + 1;
defpred S3[ Element of the Sorts of (FreeMSA X) . v] means depth $1 <= n + 1;
defpred S4[ Element of the Sorts of (FreeMSA X) . v] means ( depth $1 <= n or depth $1 = n + 1 );
set dn1 = { H1(t) where t is Element of the Sorts of (FreeMSA X) . v : S3[t] } ;
set dn11 = { H1(t) where t is Element of the Sorts of (FreeMSA X) . v : S4[t] } ;
set den1 = { t where t is Element of the Sorts of (FreeMSA X) . v : S2[t] } ;
set ov = { o where o is OperSymbol of S : the_result_sort_of o = v } ;
A5: the Sorts of (FreeMSA X) . v = FreeSort (X,v) by A2, MSAFREE:def_11;
{ o where o is OperSymbol of S : the_result_sort_of o = v } is finite by A1, MSSCYC_1:def_5;
then consider ovs being FinSequence such that
A6: rng ovs = { o where o is OperSymbol of S : the_result_sort_of o = v } by FINSEQ_1:52;
deffunc H2( set ) -> set = { t where t is Element of the Sorts of (FreeMSA X) . v : ( depth t = n + 1 & t . {} = [(ovs . $1), the carrier of S] ) } ;
consider dvs being FinSequence such that
A7: ( len dvs = len ovs & ( for k being Nat st k in dom dvs holds
dvs . k = H2(k) ) ) from FINSEQ_1:sch_2();
A8: ( dom ovs = Seg (len ovs) & dom dvs = Seg (len dvs) ) by FINSEQ_1:def_3;
A9: FreeSort (X,v) c= S -Terms X by MSATERM:12;
A10: { t where t is Element of the Sorts of (FreeMSA X) . v : S2[t] } c= Union dvs
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { t where t is Element of the Sorts of (FreeMSA X) . v : S2[t] } or x in Union dvs )
assume x in { t where t is Element of the Sorts of (FreeMSA X) . v : S2[t] } ; ::_thesis: x in Union dvs
then consider t being Element of the Sorts of (FreeMSA X) . v such that
A11: x = t and
A12: depth t = n + 1 ;
t in FreeSort (X,v) by A5;
then reconsider t9 = t as Term of S,X by A9;
now__::_thesis:_not_t9_is_root
A13: ex dt being finite DecoratedTree ex tt being finite Tree st
( dt = t & tt = dom dt & depth t = height tt ) by MSAFREE2:def_14;
assume t9 is root ; ::_thesis: contradiction
hence contradiction by A12, A13, TREES_1:42, TREES_9:def_1; ::_thesis: verum
end;
then consider o being OperSymbol of S such that
A14: t9 . {} = [o, the carrier of S] by MSSCYC_1:20;
the_result_sort_of o = the_sort_of t9 by A14, MSATERM:17
.= v by A5, MSATERM:def_5 ;
then o in rng ovs by A6;
then consider k being set such that
A15: k in dom ovs and
A16: o = ovs . k by FUNCT_1:def_3;
dvs . k = { t1 where t1 is Element of the Sorts of (FreeMSA X) . v : ( depth t1 = n + 1 & t1 . {} = [(ovs . k), the carrier of S] ) } by A7, A8, A15;
then A17: t in dvs . k by A12, A14, A16;
dvs . k in rng dvs by A7, A8, A15, FUNCT_1:def_3;
then t in union (rng dvs) by A17, TARSKI:def_4;
hence x in Union dvs by A11, CARD_3:def_4; ::_thesis: verum
end;
for k being set st k in dom dvs holds
dvs . k is finite
proof
let k be set ; ::_thesis: ( k in dom dvs implies dvs . k is finite )
set dvsk = { t where t is Element of the Sorts of (FreeMSA X) . v : ( depth t = n + 1 & t . {} = [(ovs . k), the carrier of S] ) } ;
assume A18: k in dom dvs ; ::_thesis: dvs . k is finite
then ovs . k in rng ovs by A7, A8, FUNCT_1:def_3;
then consider o being OperSymbol of S such that
A19: o = ovs . k and
the_result_sort_of o = v by A6;
set davsk = { ([o, the carrier of S] -tree a) where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ;
A20: { t where t is Element of the Sorts of (FreeMSA X) . v : ( depth t = n + 1 & t . {} = [(ovs . k), the carrier of S] ) } c= { ([o, the carrier of S] -tree a) where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { t where t is Element of the Sorts of (FreeMSA X) . v : ( depth t = n + 1 & t . {} = [(ovs . k), the carrier of S] ) } or x in { ([o, the carrier of S] -tree a) where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } )
assume x in { t where t is Element of the Sorts of (FreeMSA X) . v : ( depth t = n + 1 & t . {} = [(ovs . k), the carrier of S] ) } ; ::_thesis: x in { ([o, the carrier of S] -tree a) where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) }
then consider t being Element of the Sorts of (FreeMSA X) . v such that
A21: x = t and
A22: depth t = n + 1 and
A23: t . {} = [o, the carrier of S] by A19;
t in FreeSort (X,v) by A5;
then reconsider t9 = t as Term of S,X by A9;
consider a being ArgumentSeq of Sym (o,X) such that
A24: t9 = [o, the carrier of S] -tree a by A23, MSATERM:10;
reconsider a9 = a as Element of (S -Terms X) * by FINSEQ_1:def_11;
[o, the carrier of S] -tree a9 in { ([o, the carrier of S] -tree a) where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } by A22, A24;
hence x in { ([o, the carrier of S] -tree a) where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } by A21, A24; ::_thesis: verum
end;
deffunc H3( Nat) -> set = { t where t is Element of the Sorts of (FreeMSA X) . ((the_arity_of o) /. $1) : depth t <= n } ;
set avsk = { a where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ;
A25: { a where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } , { ([o, the carrier of S] -tree a) where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } are_equipotent
proof
set Z = { [a,([o, the carrier of S] -tree a)] where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ;
take { [a,([o, the carrier of S] -tree a)] where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ; :: according to TARSKI:def_6 ::_thesis: ( ( for b1 being set holds
( not b1 in { a where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or ex b2 being set st
( b2 in { ([o, the carrier of S] -tree a) where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } & [b1,b2] in { [a,([o, the carrier of S] -tree a)] where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ) ) ) & ( for b1 being set holds
( not b1 in { ([o, the carrier of S] -tree a) where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or ex b2 being set st
( b2 in { a where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } & [b2,b1] in { [a,([o, the carrier of S] -tree a)] where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ) ) ) & ( for b1, b2, b3, b4 being set holds
( not [b1,b2] in { [a,([o, the carrier of S] -tree a)] where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or not [b3,b4] in { [a,([o, the carrier of S] -tree a)] where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or ( ( not b1 = b3 or b2 = b4 ) & ( not b2 = b4 or b1 = b3 ) ) ) ) )
hereby ::_thesis: ( ( for b1 being set holds
( not b1 in { ([o, the carrier of S] -tree a) where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or ex b2 being set st
( b2 in { a where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } & [b2,b1] in { [a,([o, the carrier of S] -tree a)] where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ) ) ) & ( for b1, b2, b3, b4 being set holds
( not [b1,b2] in { [a,([o, the carrier of S] -tree a)] where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or not [b3,b4] in { [a,([o, the carrier of S] -tree a)] where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or ( ( not b1 = b3 or b2 = b4 ) & ( not b2 = b4 or b1 = b3 ) ) ) ) )
let x be set ; ::_thesis: ( x in { a where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } implies ex y9 being set st
( y9 in { ([o, the carrier of S] -tree a) where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } & [x,y9] in { [a,([o, the carrier of S] -tree a)] where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ) )
assume x in { a where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ; ::_thesis: ex y9 being set st
( y9 in { ([o, the carrier of S] -tree a) where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } & [x,y9] in { [a,([o, the carrier of S] -tree a)] where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } )
then consider a being Element of (S -Terms X) * such that
A26: x = a and
A27: ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) ;
reconsider y9 = [o, the carrier of S] -tree a as set ;
take y9 = y9; ::_thesis: ( y9 in { ([o, the carrier of S] -tree a) where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } & [x,y9] in { [a,([o, the carrier of S] -tree a)] where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } )
thus y9 in { ([o, the carrier of S] -tree a) where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } by A27; ::_thesis: [x,y9] in { [a,([o, the carrier of S] -tree a)] where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) }
thus [x,y9] in { [a,([o, the carrier of S] -tree a)] where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } by A26, A27; ::_thesis: verum
end;
hereby ::_thesis: for b1, b2, b3, b4 being set holds
( not [b1,b2] in { [a,([o, the carrier of S] -tree a)] where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or not [b3,b4] in { [a,([o, the carrier of S] -tree a)] where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or ( ( not b1 = b3 or b2 = b4 ) & ( not b2 = b4 or b1 = b3 ) ) )
let y be set ; ::_thesis: ( y in { ([o, the carrier of S] -tree a) where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } implies ex a9 being set st
( a9 in { a where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } & [a9,y] in { [a,([o, the carrier of S] -tree a)] where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ) )
assume y in { ([o, the carrier of S] -tree a) where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ; ::_thesis: ex a9 being set st
( a9 in { a where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } & [a9,y] in { [a,([o, the carrier of S] -tree a)] where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } )
then consider a being Element of (S -Terms X) * such that
A28: y = [o, the carrier of S] -tree a and
A29: ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) ;
reconsider a9 = a as set ;
take a9 = a9; ::_thesis: ( a9 in { a where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } & [a9,y] in { [a,([o, the carrier of S] -tree a)] where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } )
thus a9 in { a where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } by A29; ::_thesis: [a9,y] in { [a,([o, the carrier of S] -tree a)] where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) }
thus [a9,y] in { [a,([o, the carrier of S] -tree a)] where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } by A28, A29; ::_thesis: verum
end;
let x, y, z, u be set ; ::_thesis: ( not [x,y] in { [a,([o, the carrier of S] -tree a)] where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or not [z,u] in { [a,([o, the carrier of S] -tree a)] where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or ( ( not x = z or y = u ) & ( not y = u or x = z ) ) )
assume [x,y] in { [a,([o, the carrier of S] -tree a)] where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ; ::_thesis: ( not [z,u] in { [a,([o, the carrier of S] -tree a)] where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or ( ( not x = z or y = u ) & ( not y = u or x = z ) ) )
then consider xa being Element of (S -Terms X) * such that
A30: [x,y] = [xa,([o, the carrier of S] -tree xa)] and
A31: xa is ArgumentSeq of Sym (o,X) and
ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree xa ) ;
A32: x = xa by A30, XTUPLE_0:1;
assume [z,u] in { [a,([o, the carrier of S] -tree a)] where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ; ::_thesis: ( ( not x = z or y = u ) & ( not y = u or x = z ) )
then consider za being Element of (S -Terms X) * such that
A33: [z,u] = [za,([o, the carrier of S] -tree za)] and
A34: za is ArgumentSeq of Sym (o,X) and
ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree za ) ;
A35: z = za by A33, XTUPLE_0:1;
hence ( x = z implies y = u ) by A30, A33, A32, XTUPLE_0:1; ::_thesis: ( not y = u or x = z )
A36: u = [o, the carrier of S] -tree za by A33, XTUPLE_0:1;
A37: y = [o, the carrier of S] -tree xa by A30, XTUPLE_0:1;
assume y = u ; ::_thesis: x = z
hence x = z by A31, A34, A32, A37, A35, A36, TREES_4:15; ::_thesis: verum
end;
consider nS being FinSequence such that
A38: ( len nS = len (the_arity_of o) & ( for k being Nat st k in dom nS holds
nS . k = H3(k) ) ) from FINSEQ_1:sch_2();
A39: dom nS = Seg (len nS) by FINSEQ_1:def_3;
A40: dom nS = Seg (len (the_arity_of o)) by A38, FINSEQ_1:def_3;
A41: { a where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } c= product nS
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { a where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or x in product nS )
assume x in { a where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ; ::_thesis: x in product nS
then consider a being Element of (S -Terms X) * such that
A42: x = a and
A43: a is ArgumentSeq of Sym (o,X) and
A44: ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ;
reconsider a = a as ArgumentSeq of Sym (o,X) by A43;
A45: ( len a = len (the_arity_of o) & dom a = Seg (len a) ) by FINSEQ_1:def_3, MSATERM:22;
now__::_thesis:_for_x_being_set_st_x_in_dom_a_holds_
a_._x_in_nS_._x
let x be set ; ::_thesis: ( x in dom a implies a . x in nS . x )
assume A46: x in dom a ; ::_thesis: a . x in nS . x
then reconsider k = x as Element of NAT ;
reconsider ak = a . k as Term of S,X by A46, MSATERM:22;
A47: the_sort_of ak = (the_arity_of o) /. k by A46, MSATERM:23;
the Sorts of (FreeMSA X) . (the_sort_of ak) = FreeSort (X,(the_sort_of ak)) by A2, MSAFREE:def_11;
then reconsider ak = ak as Element of the Sorts of (FreeMSA X) . ((the_arity_of o) /. k) by A47, MSATERM:def_5;
depth ak < n + 1 by A44, A46, MSSCYC_1:27;
then A48: depth ak <= n by NAT_1:13;
set nSk = { tk where tk is Element of the Sorts of (FreeMSA X) . ((the_arity_of o) /. k) : depth tk <= n } ;
{ tk where tk is Element of the Sorts of (FreeMSA X) . ((the_arity_of o) /. k) : depth tk <= n } = nS . x by A38, A40, A45, A46;
hence a . x in nS . x by A48; ::_thesis: verum
end;
hence x in product nS by A38, A39, A42, A45, CARD_3:def_5; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_dom_nS_holds_
nS_._x_is_finite
let x be set ; ::_thesis: ( x in dom nS implies nS . x is finite )
assume A49: x in dom nS ; ::_thesis: nS . x is finite
then reconsider k = x as Nat ;
set nSk = { t where t is Element of the Sorts of (FreeMSA X) . ((the_arity_of o) /. k) : depth t <= n } ;
nS . k = { t where t is Element of the Sorts of (FreeMSA X) . ((the_arity_of o) /. k) : depth t <= n } by A38, A49;
hence nS . x is finite by A4; ::_thesis: verum
end;
then nS is V34() by FINSET_1:def_4;
then product nS is finite ;
then { ([o, the carrier of S] -tree a) where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } is finite by A25, A41, CARD_1:38;
hence dvs . k is finite by A7, A18, A20; ::_thesis: verum
end;
then A50: Union dvs is finite by CARD_2:88;
defpred S5[ Element of the Sorts of (FreeMSA X) . v] means depth $1 <= n;
set dln = { t where t is Element of the Sorts of (FreeMSA X) . v : S5[t] } ;
A51: { t where t is Element of the Sorts of (FreeMSA X) . v : ( S5[t] or S2[t] ) } = { t where t is Element of the Sorts of (FreeMSA X) . v : S5[t] } \/ { t where t is Element of the Sorts of (FreeMSA X) . v : S2[t] } from TOPREAL1:sch_1();
A52: for t being Element of the Sorts of (FreeMSA X) . v holds
( S3[t] iff S4[t] ) by NAT_1:8, NAT_1:12;
A53: { H1(t) where t is Element of the Sorts of (FreeMSA X) . v : S3[t] } = { H1(t) where t is Element of the Sorts of (FreeMSA X) . v : S4[t] } from FRAENKEL:sch_3(A52);
{ t where t is Element of the Sorts of (FreeMSA X) . v : S5[t] } is finite by A4;
hence { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= n + 1 } is finite by A53, A51, A50, A10; ::_thesis: verum
end;
A54: S1[ 0 ]
proof
let v be SortSymbol of S; ::_thesis: { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= 0 } is finite
set dle0 = { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= 0 } ;
set d0 = { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } ;
A55: { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= 0 } c= { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= 0 } or x in { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } )
assume x in { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= 0 } ; ::_thesis: x in { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 }
then consider t being Element of the Sorts of (FreeMSA X) . v such that
A56: x = t and
A57: depth t <= 0 ;
depth t = 0 by A57;
hence x in { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } by A56; ::_thesis: verum
end;
( Constants ((FreeMSA X),v) is finite & { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } = (FreeGen (v,X)) \/ (Constants ((FreeMSA X),v)) ) by A1, MSSCYC_1:25, MSSCYC_1:26;
hence { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= 0 } is finite by A55; ::_thesis: verum
end;
thus for n being Nat holds S1[n] from NAT_1:sch_2(A54, A3); ::_thesis: verum
end;
theorem :: MSSCYC_2:6
for S being non empty non void ManySortedSign st S is finitely_operated & InducedGraph S is well-founded holds
S is monotonic
proof
let S be non empty non void ManySortedSign ; ::_thesis: ( S is finitely_operated & InducedGraph S is well-founded implies S is monotonic )
set G = InducedGraph S;
assume that
A1: S is finitely_operated and
A2: InducedGraph S is well-founded ; ::_thesis: S is monotonic
given A being non-empty finitely-generated MSAlgebra over S such that A3: not A is finite-yielding ; :: according to MSAFREE2:def_13 ::_thesis: contradiction
set GS = the V2() V34() GeneratorSet of A;
reconsider gs = the V2() V34() GeneratorSet of A as V2() V34() ManySortedSet of the carrier of S ;
not FreeMSA gs is finite-yielding by A3, MSSCYC_1:23;
then the Sorts of (FreeMSA gs) is V34() by MSAFREE2:def_11;
then consider v being set such that
A4: v in the carrier of S and
A5: not the Sorts of (FreeMSA gs) . v is finite by FINSET_1:def_5;
reconsider v = v as SortSymbol of S by A4;
consider n being Element of NAT such that
A6: for c being directed Chain of InducedGraph S st not c is empty & (vertex-seq c) . ((len c) + 1) = v holds
len c <= n by A2, MSSCYC_1:def_4;
set V = the Sorts of (FreeMSA gs) . v;
set Vn = { t where t is Element of the Sorts of (FreeMSA gs) . v : depth t <= n } ;
{ t where t is Element of the Sorts of (FreeMSA gs) . v : depth t <= n } is finite by A1, Th5;
then not the Sorts of (FreeMSA gs) . v c= { t where t is Element of the Sorts of (FreeMSA gs) . v : depth t <= n } by A5;
then consider t being set such that
A7: t in the Sorts of (FreeMSA gs) . v and
A8: not t in { t where t is Element of the Sorts of (FreeMSA gs) . v : depth t <= n } by TARSKI:def_3;
reconsider t = t as Element of the Sorts of (FreeMSA gs) . v by A7;
A9: not depth t <= n by A8;
then 1 <= depth t by NAT_1:14;
then ex d being directed Chain of InducedGraph S st
( len d = depth t & (vertex-seq d) . ((len d) + 1) = v ) by Th2;
hence contradiction by A6, A9, CARD_1:27; ::_thesis: verum
end;