let S be 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 ) )
let X be 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 v be 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 n be Nat; ( 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
; ( 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 ) )
( 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
;
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 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
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
Nat;
( 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;
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
;
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;
then consider o being
OperSymbol of
S such that A27:
t1 . {} = [o, the carrier of S]
by MSSCYC_1:20;
consider a being
ArgumentSeq of
Sym (
o,
X)
such that A28:
t1 = [o, the carrier of S] -tree a
by A27, MSATERM:10;
A29:
(p /^ k) | 1
= <*((p /^ k) . 1)*>
by A21, CARD_1:27, FINSEQ_5:20;
consider i being
Nat,
T being
DecoratedTree,
q being
Node of
T such that A30:
i < len a
and
T = a . (i + 1)
and A31:
p /^ k = <*i*> ^ q
by A21, A24, A28, CARD_1:27, TREES_4:11;
reconsider pk9 =
p /^ k as
Node of
t1 by A5, A23, TREES_2:def 10;
reconsider p1 =
pk9 | (0 + 1) as
Node of
t1 by MSSCYC_1:19;
reconsider t29 =
t1 | p1 as
Term of
S,
X ;
A32:
(p | (k + 1)) | k =
(p | (k + 1)) | (Seg k)
by FINSEQ_1:def 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) * ;
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
;
S1[k,x,y]
take
t1
;
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
;
( 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)) )
;
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
;
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
;
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
;
( 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 )
;
( [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;
( 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;
[o,rs1] in the carrier' of (InducedGraph S)
thus
[o,rs1] in the
carrier' of
(InducedGraph S)
by A39, A40, Def1;
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
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;
( 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 ) )
;
S2[k + 1]
A44:
k <= k + 1
by NAT_1:11;
assume that
1
<= k + 1
and A45:
k + 1
<= n
;
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 )
;
suppose A47:
k = 0
;
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
;
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
;
( 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;
( 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;
( 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;
( (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
;
(vertex-seq C1) . 1 = the_sort_of t2p | 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
;
verum end; suppose A51:
k <> 0
;
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 )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
;
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
;
( 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;
( 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
;
( 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;
( (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;
(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;
verum 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 )
;
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
; 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( 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
H1(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 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 )
A81:
dom a = Seg (len (the_arity_of o))
by A77, FINSEQ_1:def 3;
reconsider a = a as ArgumentSeq of Sym (o,X) by A77, A79, MSATERM:24;
set C1 = [o, the carrier of S] -tree a;
reconsider C1 = [o, the carrier of S] -tree a as Term of S,X by MSATERM:1;
A82:
for k being Nat st 1 <= k & k < n1 holds
for x being Element of S -Terms X ex y being Element of S -Terms X st S1[k,x,y]
proof
let k be
Nat;
( 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
;
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;
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[
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 &
S2[
e,
u] )
consider a being
Function of
(dom (the_arity_of o)),
(S -Terms X) such that A92:
for
e being
object st
e in dom (the_arity_of o) holds
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;
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
;
S1[k,x,y]
take
o
;
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
;
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
;
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
;
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
;
( 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 )
;
( 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;
( 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
;
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;
( 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
;
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
;
( 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
;
( 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;
( ( 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;
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 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;
( 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 ) )
;
S2[k + 1]
assume that A102:
1
<= k + 1
and A103:
k + 1
<= n
;
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 )
;
suppose A107:
k = 0
;
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
;
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
;
( 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;
( 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;
( 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;
height (dom C1) = k + 1consider 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 for t9 being finite Tree st t9 in rng w holds
height t9 <= height dtlet t9 be
finite Tree;
( t9 in rng w implies height t9 <= height dt )assume
t9 in rng w
;
height t9 <= height dtthen 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;
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;
verum end; suppose A119:
k <> 0
;
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
;
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
;
( 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;
( 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;
( 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;
height (dom Ck1) = k + 1A134:
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 for t9 being finite Tree st t9 in rng w holds
height t9 <= height dtlet t9 be
finite Tree;
( t9 in rng w implies height b1 <= height dt )assume
t9 in rng w
;
height b1 <= height dtthen 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 )
;
suppose
(
the_sort_of t99 = rs1 &
the_sort_of Ck9 = rs1 )
;
height b1 <= height dthence
height t9 <= height dt
by A143, A133, A136, A138, A142, A145, A146, A147, A148, FUNCT_6:22, MSUALG_1:def 1;
verum 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
;
hence
height (dom Ck1) = k + 1
by A121, A123, A124, A134, A133, A136, A138, A142, A151, A144, MSUALG_1:def 1, TREES_3:79;
verum 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
; depth Cn = n
thus
depth Cn = n
by A156, MSAFREE2:def 14; verum