let IIG be non empty non void Circuit-like monotonic ManySortedSign ; for A being non-empty Circuit of IIG
for v being Vertex of IIG
for e being Element of the Sorts of (FreeEnv A) . v
for p being DTree-yielding FinSequence st v in InnerVertices IIG & e = [(action_at v), the carrier of IIG] -tree p & ( for k being Element of NAT st k in dom p holds
ex ek being Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k) st
( ek = p . k & card ek = size (((the_arity_of (action_at v)) /. k),A) ) ) holds
card e = size (v,A)
let A be non-empty Circuit of IIG; for v being Vertex of IIG
for e being Element of the Sorts of (FreeEnv A) . v
for p being DTree-yielding FinSequence st v in InnerVertices IIG & e = [(action_at v), the carrier of IIG] -tree p & ( for k being Element of NAT st k in dom p holds
ex ek being Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k) st
( ek = p . k & card ek = size (((the_arity_of (action_at v)) /. k),A) ) ) holds
card e = size (v,A)
let v be Vertex of IIG; for e being Element of the Sorts of (FreeEnv A) . v
for p being DTree-yielding FinSequence st v in InnerVertices IIG & e = [(action_at v), the carrier of IIG] -tree p & ( for k being Element of NAT st k in dom p holds
ex ek being Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k) st
( ek = p . k & card ek = size (((the_arity_of (action_at v)) /. k),A) ) ) holds
card e = size (v,A)
let e be Element of the Sorts of (FreeEnv A) . v; for p being DTree-yielding FinSequence st v in InnerVertices IIG & e = [(action_at v), the carrier of IIG] -tree p & ( for k being Element of NAT st k in dom p holds
ex ek being Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k) st
( ek = p . k & card ek = size (((the_arity_of (action_at v)) /. k),A) ) ) holds
card e = size (v,A)
let p be DTree-yielding FinSequence; ( v in InnerVertices IIG & e = [(action_at v), the carrier of IIG] -tree p & ( for k being Element of NAT st k in dom p holds
ex ek being Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k) st
( ek = p . k & card ek = size (((the_arity_of (action_at v)) /. k),A) ) ) implies card e = size (v,A) )
assume that
A1:
v in InnerVertices IIG
and
A2:
e = [(action_at v), the carrier of IIG] -tree p
and
A3:
for k being Element of NAT st k in dom p holds
ex ek being Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k) st
( ek = p . k & card ek = size (((the_arity_of (action_at v)) /. k),A) )
; card e = size (v,A)
consider s being non empty finite Subset of NAT such that
A4:
s = { (card t) where t is Element of the Sorts of (FreeEnv A) . v : verum }
and
A5:
size (v,A) = max s
by Def4;
reconsider S = s as non empty finite real-membered set ;
A6:
now for r being ExtReal st r in S holds
r <= card ereconsider e9 =
e as
finite set ;
let r be
ExtReal;
( r in S implies b1 <= card e )A7:
1
<= card e9
by NAT_1:14;
assume
r in S
;
b1 <= card ethen consider t being
Element of the
Sorts of
(FreeEnv A) . v such that A8:
r = card t
by A4;
FreeEnv A = MSAlgebra(#
(FreeSort the Sorts of A),
(FreeOper the Sorts of A) #)
by MSAFREE:def 14;
then
the
Sorts of
(FreeEnv A) . v = FreeSort ( the
Sorts of
A,
v)
by MSAFREE:def 11;
then
t in FreeSort ( the
Sorts of
A,
v)
;
then
t in { a9 where a9 is Element of TS (DTConMSA the Sorts of A) : ( ex x being set st
( x in the Sorts of A . v & a9 = root-tree [x,v] ) or ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a9 . {} & the_result_sort_of o = v ) ) }
by MSAFREE:def 10;
then consider a9 being
Element of
TS (DTConMSA the Sorts of A) such that A9:
a9 = t
and A10:
( ex
x being
set st
(
x in the
Sorts of
A . v &
a9 = root-tree [x,v] ) or ex
o being
OperSymbol of
IIG st
(
[o, the carrier of IIG] = a9 . {} &
the_result_sort_of o = v ) )
;
per cases
( ex x being set st
( x in the Sorts of A . v & a9 = root-tree [x,v] ) or ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a9 . {} & the_result_sort_of o = v ) )
by A10;
suppose
ex
o being
OperSymbol of
IIG st
(
[o, the carrier of IIG] = a9 . {} &
the_result_sort_of o = v )
;
b1 <= card ethen
a9 . {} = [(action_at v), the carrier of IIG]
by A1, MSAFREE2:def 7;
then consider q being
DTree-yielding FinSequence such that A12:
t = [(action_at v), the carrier of IIG] -tree q
by A9, Th9;
deffunc H1(
Nat)
-> set =
p +* (q | (Seg $1));
consider T being
FinSequence such that A13:
len T = len p
and A14:
for
k being
Nat st
k in dom T holds
T . k = H1(
k)
from FINSEQ_1:sch 2();
A15:
dom T = dom p
by A13, FINSEQ_3:29;
A16:
the_result_sort_of (action_at v) = v
by A1, MSAFREE2:def 7;
A17:
dom p = Seg (len p)
by FINSEQ_1:def 3;
now r <= card eper cases
( len q = 0 or len q <> 0 )
;
suppose A18:
len q <> 0
;
r <= card edefpred S2[
Nat]
means ( $1
in dom p implies for
qk being
DTree-yielding FinSequence st
qk = T . $1 holds
for
tk being
finite set st
tk = [(action_at v), the carrier of IIG] -tree qk holds
card tk <= card e );
A19:
len p = len (the_arity_of (action_at v))
by A2, A16, MSAFREE2:10;
then A20:
len p = len q
by A12, A16, MSAFREE2:10;
then A21:
1
+ 0 <= len p
by A18, NAT_1:14;
A22:
dom p = dom q
by A20, FINSEQ_3:29;
A23:
dom p = dom (the_arity_of (action_at v))
by A19, FINSEQ_3:29;
A24:
now for k being Nat st S2[k] holds
S2[k + 1]let k be
Nat;
( S2[k] implies S2[k + 1] )assume A25:
S2[
k]
;
S2[k + 1]thus
S2[
k + 1]
verumproof
reconsider tree0 =
[(action_at v), the carrier of IIG] -tree p as
finite DecoratedTree by A2;
assume A26:
k + 1
in dom p
;
for qk being DTree-yielding FinSequence st qk = T . (k + 1) holds
for tk being finite set st tk = [(action_at v), the carrier of IIG] -tree qk holds
card tk <= card e
let qk1 be
DTree-yielding FinSequence;
( qk1 = T . (k + 1) implies for tk being finite set st tk = [(action_at v), the carrier of IIG] -tree qk1 holds
card tk <= card e )
assume A27:
qk1 = T . (k + 1)
;
for tk being finite set st tk = [(action_at v), the carrier of IIG] -tree qk1 holds
card tk <= card e
let tk1 be
finite set ;
( tk1 = [(action_at v), the carrier of IIG] -tree qk1 implies card tk1 <= card e )
assume A28:
tk1 = [(action_at v), the carrier of IIG] -tree qk1
;
card tk1 <= card e
then reconsider treek1 =
tk1 as
finite DecoratedTree ;
per cases
( k = 0 or k <> 0 )
;
suppose A29:
k = 0
;
card tk1 <= card eset v1 =
(the_arity_of (action_at v)) /. 1;
A30:
1
in dom p
by A21, FINSEQ_3:25;
then consider e1 being
Element of the
Sorts of
(FreeEnv A) . ((the_arity_of (action_at v)) /. 1) such that A31:
e1 = p . 1
and A32:
card e1 = size (
((the_arity_of (action_at v)) /. 1),
A)
by A3;
1
in Seg 1
by FINSEQ_1:3;
then A33:
1
in dom (q | (Seg 1))
by A22, A30, RELAT_1:57;
A34:
1
in dom (the_arity_of (action_at v))
by A19, A21, FINSEQ_3:25;
then
q . 1
in the
Sorts of
(FreeEnv A) . ((the_arity_of (action_at v)) . 1)
by A12, A16, MSAFREE2:11;
then reconsider T1 =
q . 1 as
Element of the
Sorts of
(FreeEnv A) . ((the_arity_of (action_at v)) /. 1) by A34, PARTFUN1:def 6;
reconsider Tx =
p . 1 as
finite DecoratedTree by A31;
(
{} is
Element of
dom Tx &
<*0*> = <*0*> ^ {} )
by FINSEQ_1:34, TREES_1:22;
then reconsider w0 =
<*0*> as
Element of
dom tree0 by A21, TREES_4:11;
consider q0 being
DTree-yielding FinSequence such that A35:
e with-replacement (
w0,
T1)
= [(action_at v), the carrier of IIG] -tree q0
and A36:
len q0 = len p
and A37:
q0 . (0 + 1) = T1
and A38:
for
i being
Nat st
i in dom p &
i <> 0 + 1 holds
q0 . i = p . i
by A2, PRE_CIRC:15;
A39:
1
in dom p
by A21, FINSEQ_3:25;
then A40:
qk1 . 1 =
(p +* (q | (Seg 1))) . 1
by A14, A15, A27, A29
.=
(q | (Seg 1)) . 1
by A33, FUNCT_4:13
.=
q . 1
by FINSEQ_1:3, FUNCT_1:49
;
A41:
now for k being Nat st 1 <= k & k <= len q0 holds
q0 . k = qk1 . klet k be
Nat;
( 1 <= k & k <= len q0 implies q0 . b1 = qk1 . b1 )assume
( 1
<= k &
k <= len q0 )
;
q0 . b1 = qk1 . b1then A42:
k in dom p
by A36, FINSEQ_3:25;
per cases
( k = 1 or k <> 1 )
;
suppose A43:
k <> 1
;
qk1 . b1 = q0 . b1A44:
dom (q | (Seg 1)) = (dom q) /\ (Seg 1)
by RELAT_1:61;
not
k in Seg 1
by A43, FINSEQ_1:2, TARSKI:def 1;
then A45:
not
k in dom (q | (Seg 1))
by A44, XBOOLE_0:def 4;
thus qk1 . k =
(p +* (q | (Seg 1))) . k
by A14, A15, A27, A29, A39
.=
p . k
by A45, FUNCT_4:11
.=
q0 . k
by A38, A42, A43
;
verum end; end; dom qk1 =
dom (p +* (q | (Seg 1)))
by A14, A15, A27, A29, A39
.=
(dom p) \/ (dom (q | (Seg 1)))
by FUNCT_4:def 1
.=
(dom p) \/ ((dom q) /\ (Seg 1))
by RELAT_1:61
.=
dom p
by A22, XBOOLE_1:22
;
then
len qk1 = len p
by FINSEQ_3:29;
then
treek1 = tree0 with-replacement (
w0,
T1)
by A2, A28, A35, A36, A41, FINSEQ_1:14;
then A46:
(card treek1) + (card (tree0 | w0)) = (card tree0) + (card T1)
by PRE_CIRC:18;
consider s1 being non
empty finite Subset of
NAT such that A47:
s1 = { (card t1) where t1 is Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. 1) : verum }
and A48:
card e1 = max s1
by A32, Def4;
reconsider S1 =
s1 as non
empty finite real-membered set ;
card T1 in S1
by A47;
then A49:
card T1 <= card e1
by A48, XXREAL_2:def 8;
tree0 | w0 = e1
by A21, A31, TREES_4:def 4;
hence
card tk1 <= card e
by A2, A49, A46, XREAL_1:8;
verum end; suppose A50:
k <> 0
;
card tk1 <= card eA51:
k + 1
<= len p
by A26, FINSEQ_3:25;
then A52:
k < len p
by NAT_1:13;
set v1 =
(the_arity_of (action_at v)) /. (k + 1);
( not
k + 1
in Seg k &
dom (q | (Seg k)) = (dom q) /\ (Seg k) )
by FINSEQ_3:8, RELAT_1:61;
then A53:
not
k + 1
in dom (q | (Seg k))
by XBOOLE_0:def 4;
k + 1
>= 1
by NAT_1:11;
then A54:
k + 1
in dom (the_arity_of (action_at v))
by A19, A51, FINSEQ_3:25;
then
p . (k + 1) in the
Sorts of
(FreeEnv A) . ((the_arity_of (action_at v)) . (k + 1))
by A2, A16, MSAFREE2:11;
then reconsider T1 =
p . (k + 1) as
Element of the
Sorts of
(FreeEnv A) . ((the_arity_of (action_at v)) /. (k + 1)) by A54, PARTFUN1:def 6;
k + 1
in Seg (k + 1)
by FINSEQ_1:3;
then A55:
k + 1
in dom (q | (Seg (k + 1)))
by A22, A26, RELAT_1:57;
A56:
k >= 1
by A50, NAT_1:14;
then A57:
k in dom p
by A52, FINSEQ_3:25;
then
T . k = p +* (q | (Seg k))
by A14, A15;
then reconsider qk =
T . k as
Function ;
A58:
dom qk =
dom (p +* (q | (Seg k)))
by A14, A15, A57
.=
(dom p) \/ (dom (q | (Seg k)))
by FUNCT_4:def 1
.=
(dom p) \/ ((dom q) /\ (Seg k))
by RELAT_1:61
.=
dom p
by A22, XBOOLE_1:22
;
then
dom qk = Seg (len p)
by FINSEQ_1:def 3;
then reconsider qk =
qk as
FinSequence by FINSEQ_1:def 2;
A59:
for
x being
set st
x in dom qk holds
qk . x is
finite DecoratedTree
proof
let x be
set ;
( x in dom qk implies qk . x is finite DecoratedTree )
assume A60:
x in dom qk
;
qk . x is finite DecoratedTree
then reconsider n =
x as
Element of
NAT ;
set v1 =
(the_arity_of (action_at v)) /. n;
(
qk . n = q . n or
qk . n = p . n )
proof
per cases
( n <= k or n > k )
;
suppose A61:
n <= k
;
( qk . n = q . n or qk . n = p . n )
n >= 1
by A60, FINSEQ_3:25;
then A62:
n in Seg k
by A61, FINSEQ_1:1;
dom (q | (Seg k)) = (dom q) /\ (Seg k)
by RELAT_1:61;
then A63:
n in dom (q | (Seg k))
by A22, A58, A60, A62, XBOOLE_0:def 4;
qk . n =
(p +* (q | (Seg k))) . n
by A14, A15, A57
.=
(q | (Seg k)) . n
by A63, FUNCT_4:13
.=
q . n
by A63, FUNCT_1:47
;
hence
(
qk . n = q . n or
qk . n = p . n )
;
verum end;
end;
then
qk . n in the
Sorts of
(FreeEnv A) . ((the_arity_of (action_at v)) . n)
by A2, A12, A16, A23, A58, A60, MSAFREE2:11;
then reconsider T1 =
qk . n as
Element of the
Sorts of
(FreeEnv A) . ((the_arity_of (action_at v)) /. n) by A23, A58, A60, PARTFUN1:def 6;
T1 in the
Sorts of
(FreeEnv A) . ((the_arity_of (action_at v)) /. n)
;
hence
qk . x is
finite DecoratedTree
;
verum
end; then
for
x being
object st
x in dom qk holds
qk . x is
DecoratedTree
;
then reconsider qk =
qk as
DTree-yielding FinSequence by TREES_3:24;
A67:
len qk = len p
by A58, FINSEQ_3:29;
A68:
qk . (k + 1) =
(p +* (q | (Seg k))) . (k + 1)
by A14, A15, A57
.=
p . (k + 1)
by A53, FUNCT_4:11
;
then reconsider qkf =
doms qk as
FinTree-yielding FinSequence by TREES_3:23;
(
tree qkf is
finite & ex
q being
DTree-yielding FinSequence st
(
qk = q &
dom ([(action_at v), the carrier of IIG] -tree qk) = tree (doms q) ) )
by TREES_4:def 4;
then reconsider tk =
[(action_at v), the carrier of IIG] -tree qk as
finite DecoratedTree by FINSET_1:10;
consider e1 being
Element of the
Sorts of
(FreeEnv A) . ((the_arity_of (action_at v)) /. (k + 1)) such that A70:
e1 = p . (k + 1)
and A71:
card e1 = size (
((the_arity_of (action_at v)) /. (k + 1)),
A)
by A3, A26;
T1 in the
Sorts of
(FreeEnv A) . ((the_arity_of (action_at v)) /. (k + 1))
;
then reconsider Tx =
qk . (k + 1) as
finite DecoratedTree by A68;
(the_arity_of (action_at v)) /. (k + 1) = (the_arity_of (action_at v)) . (k + 1)
by A54, PARTFUN1:def 6;
then reconsider T1 =
q . (k + 1) as
Element of the
Sorts of
(FreeEnv A) . ((the_arity_of (action_at v)) /. (k + 1)) by A12, A16, A54, MSAFREE2:11;
A72:
k in NAT
by ORDINAL1:def 12;
A73:
(
{} is
Element of
dom Tx &
<*k*> = <*k*> ^ {} )
by FINSEQ_1:34, TREES_1:22;
then
<*k*> in dom tk
by A52, A67, TREES_4:11;
then consider q0 being
DTree-yielding FinSequence such that A74:
tk with-replacement (
<*k*>,
T1)
= [(action_at v), the carrier of IIG] -tree q0
and A75:
len q0 = len qk
and A76:
q0 . (k + 1) = T1
and A77:
for
i being
Nat st
i in dom qk &
i <> k + 1 holds
q0 . i = qk . i
by PRE_CIRC:15, A72;
A78:
qk1 . (k + 1) =
(p +* (q | (Seg (k + 1)))) . (k + 1)
by A14, A15, A26, A27
.=
(q | (Seg (k + 1))) . (k + 1)
by A55, FUNCT_4:13
.=
q . (k + 1)
by FINSEQ_1:3, FUNCT_1:49
;
A79:
now for n being Nat st 1 <= n & n <= len q0 holds
q0 . n = qk1 . nlet n be
Nat;
( 1 <= n & n <= len q0 implies q0 . b1 = qk1 . b1 )assume that A80:
1
<= n
and A81:
n <= len q0
;
q0 . b1 = qk1 . b1A82:
n in dom qk
by A75, A80, A81, FINSEQ_3:25;
per cases
( n = k + 1 or n > k + 1 or n < k + 1 )
by XXREAL_0:1;
suppose A83:
n > k + 1
;
qk1 . b1 = q0 . b1
k + 1
>= k
by NAT_1:11;
then
n > k
by A83, XXREAL_0:2;
then A84:
not
n in Seg k
by FINSEQ_1:1;
dom (q | (Seg k)) = (dom q) /\ (Seg k)
by RELAT_1:61;
then A85:
not
n in dom (q | (Seg k))
by A84, XBOOLE_0:def 4;
A86:
dom (q | (Seg (k + 1))) = (dom q) /\ (Seg (k + 1))
by RELAT_1:61;
not
n in Seg (k + 1)
by A83, FINSEQ_1:1;
then A87:
not
n in dom (q | (Seg (k + 1)))
by A86, XBOOLE_0:def 4;
thus qk1 . n =
(p +* (q | (Seg (k + 1)))) . n
by A14, A15, A26, A27
.=
p . n
by A87, FUNCT_4:11
.=
(p +* (q | (Seg k))) . n
by A85, FUNCT_4:11
.=
qk . n
by A14, A15, A57
.=
q0 . n
by A77, A82, A83
;
verum end; suppose A88:
n < k + 1
;
qk1 . b1 = q0 . b1A89:
n in dom q
by A20, A67, A75, A80, A81, FINSEQ_3:25;
n <= k
by A88, NAT_1:13;
then A90:
n in Seg k
by A80, FINSEQ_1:1;
dom (q | (Seg k)) = (dom q) /\ (Seg k)
by RELAT_1:61;
then A91:
n in dom (q | (Seg k))
by A89, A90, XBOOLE_0:def 4;
A92:
dom (q | (Seg (k + 1))) = (dom q) /\ (Seg (k + 1))
by RELAT_1:61;
n in Seg (k + 1)
by A80, A88, FINSEQ_1:1;
then A93:
n in dom (q | (Seg (k + 1)))
by A89, A92, XBOOLE_0:def 4;
thus qk1 . n =
(p +* (q | (Seg (k + 1)))) . n
by A14, A15, A26, A27
.=
(q | (Seg (k + 1))) . n
by A93, FUNCT_4:13
.=
q . n
by A93, FUNCT_1:47
.=
(q | (Seg k)) . n
by A91, FUNCT_1:47
.=
(p +* (q | (Seg k))) . n
by A91, FUNCT_4:13
.=
qk . n
by A14, A15, A57
.=
q0 . n
by A77, A82, A88
;
verum end; end;
k < len qk
by A52, A58, FINSEQ_3:29;
then reconsider w0 =
<*k*> as
Element of
dom tk by A73, TREES_4:11;
dom qk1 =
dom (p +* (q | (Seg (k + 1))))
by A14, A15, A26, A27
.=
(dom p) \/ (dom (q | (Seg (k + 1))))
by FUNCT_4:def 1
.=
(dom p) \/ ((dom q) /\ (Seg (k + 1)))
by RELAT_1:61
.=
dom p
by A22, XBOOLE_1:22
;
then
len qk1 = len p
by FINSEQ_3:29;
then
treek1 = tk with-replacement (
w0,
T1)
by A28, A67, A74, A75, A79, FINSEQ_1:14;
then A94:
(card treek1) + (card (tk | w0)) = (card tk) + (card T1)
by PRE_CIRC:18;
consider s1 being non
empty finite Subset of
NAT such that A95:
s1 = { (card t1) where t1 is Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. (k + 1)) : verum }
and A96:
card e1 = max s1
by A71, Def4;
reconsider S1 =
s1 as non
empty finite real-membered set ;
card T1 in S1
by A95;
then A97:
card T1 <= card e1
by A96, XXREAL_2:def 8;
tk | w0 = e1
by A52, A70, A68, A67, TREES_4:def 4;
then A98:
card tk1 <= card tk
by A97, A94, XREAL_1:8;
card tk <= card e
by A25, A56, A52, FINSEQ_3:25;
hence
card tk1 <= card e
by A98, XXREAL_0:2;
verum end;
end; end; A99:
S2[
0 ]
by FINSEQ_3:25;
A100:
for
k being
Nat holds
S2[
k]
from NAT_1:sch 2(A99, A24);
dom p = Seg (len p)
by FINSEQ_1:def 3;
then A101:
dom p = dom q
by A20, FINSEQ_1:def 3;
A102:
len p in dom p
by A21, FINSEQ_3:25;
then T . (len p) =
p +* (q | (dom p))
by A14, A15, A17
.=
p +* q
by A101
.=
q
by A22, FUNCT_4:19
;
hence
r <= card e
by A8, A12, A100, A102;
verum end; hence
r <= card e
;
verum end; end;
card e in S
by A4;
hence
card e = size (v,A)
by A5, A6, XXREAL_2:def 8; verum