let IIG be non empty non void Circuit-like monotonic ManySortedSign ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 )
; :: thesis: 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:
card e in S
by A4;
now let r be
ext-real number ;
:: thesis: ( r in S implies b1 <= card e )
FreeEnv A = MSAlgebra(#
(FreeSort the Sorts of A),
(FreeOper the Sorts of A) #)
by MSAFREE:def 16;
then A7:
the
Sorts of
(FreeEnv A) . v = FreeSort the
Sorts of
A,
v
by MSAFREE:def 13;
reconsider e' =
e as
finite set ;
A8:
1
<= card e'
by NAT_1:14;
assume
r in S
;
:: thesis: b1 <= card ethen consider t being
Element of the
Sorts of
(FreeEnv A) . v such that A9:
r = card t
by A4;
t in FreeSort the
Sorts of
A,
v
by A7;
then
t in { a' where a' is Element of TS (DTConMSA the Sorts of A) : ( ex x being set st
( x in the Sorts of A . v & a' = root-tree [x,v] ) or ex o being OperSymbol of IIG st
( [o,the carrier of IIG] = a' . {} & the_result_sort_of o = v ) ) }
by MSAFREE:def 12;
then consider a' being
Element of
TS (DTConMSA the Sorts of A) such that A10:
a' = t
and A11:
( ex
x being
set st
(
x in the
Sorts of
A . v &
a' = root-tree [x,v] ) or ex
o being
OperSymbol of
IIG st
(
[o,the carrier of IIG] = a' . {} &
the_result_sort_of o = v ) )
;
per cases
( ex x being set st
( x in the Sorts of A . v & a' = root-tree [x,v] ) or ex o being OperSymbol of IIG st
( [o,the carrier of IIG] = a' . {} & the_result_sort_of o = v ) )
by A11;
suppose
ex
o being
OperSymbol of
IIG st
(
[o,the carrier of IIG] = a' . {} &
the_result_sort_of o = v )
;
:: thesis: b1 <= card ethen consider o being
OperSymbol of
IIG such that A13:
(
[o,the carrier of IIG] = a' . {} &
the_result_sort_of o = v )
;
a' . {} = [(action_at v),the carrier of IIG]
by A1, A13, MSAFREE2:def 7;
then consider q being
DTree-yielding FinSequence such that A14:
t = [(action_at v),the carrier of IIG] -tree q
by A10, Th10;
deffunc H1(
Nat)
-> set =
p +* (q | (Seg $1));
consider T being
FinSequence such that A15:
len T = len p
and A16:
for
k being
Nat st
k in dom T holds
T . k = H1(
k)
from FINSEQ_1:sch 2();
A17:
dom T = dom p
by A15, FINSEQ_3:31;
A18:
dom p = Seg (len p)
by FINSEQ_1:def 3;
A19:
the_result_sort_of (action_at v) = v
by A1, MSAFREE2:def 7;
now per cases
( len q = 0 or len q <> 0 )
;
suppose A20:
len q <> 0
;
:: thesis: r <= card eA21:
len p = len (the_arity_of (action_at v))
by A2, A19, MSAFREE2:13;
then A22:
len p = len q
by A14, A19, MSAFREE2:13;
then A23:
dom p = dom q
by FINSEQ_3:31;
A24:
dom p = dom (the_arity_of (action_at v))
by A21, FINSEQ_3:31;
A25:
1
+ 0 <= len p
by A20, A22, NAT_1:14;
defpred S2[
Element of
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 );
A26:
S2[
0 ]
by FINSEQ_3:27;
A27:
now let k be
Element of
NAT ;
:: thesis: ( S2[k] implies S2[k + 1] )assume A28:
S2[
k]
;
:: thesis: S2[k + 1]thus
S2[
k + 1]
:: thesis: verumproof
assume A29:
k + 1
in dom p
;
:: thesis: 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;
:: thesis: ( 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 A30:
qk1 = T . (k + 1)
;
:: thesis: 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 ;
:: thesis: ( tk1 = [(action_at v),the carrier of IIG] -tree qk1 implies card tk1 <= card e )
assume A31:
tk1 = [(action_at v),the carrier of IIG] -tree qk1
;
:: thesis: card tk1 <= card e
then reconsider treek1 =
tk1 as
finite DecoratedTree ;
reconsider tree0 =
[(action_at v),the carrier of IIG] -tree p as
finite DecoratedTree by A2;
per cases
( k = 0 or k <> 0 )
;
suppose A32:
k = 0
;
:: thesis: card tk1 <= card eset v1 =
(the_arity_of (action_at v)) /. 1;
A33:
1
in dom p
by A25, FINSEQ_3:27;
then consider e1 being
Element of the
Sorts of
(FreeEnv A) . ((the_arity_of (action_at v)) /. 1) such that A34:
e1 = p . 1
and A35:
card e1 = size ((the_arity_of (action_at v)) /. 1),
A
by A3;
consider s1 being non
empty finite Subset of
NAT such that A36:
s1 = { (card t1) where t1 is Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. 1) : verum }
and A37:
card e1 = max s1
by A35, Def4;
reconsider S1 =
s1 as non
empty finite real-membered set ;
A38:
1
in dom (the_arity_of (action_at v))
by A21, A25, FINSEQ_3:27;
A39:
1
in dom p
by A25, FINSEQ_3:27;
1
in Seg 1
by FINSEQ_1:5;
then A40:
1
in dom (q | (Seg 1))
by A23, A33, RELAT_1:86;
A41:
qk1 . 1 =
(p +* (q | (Seg 1))) . 1
by A16, A30, A32, A39, A17
.=
(q | (Seg 1)) . 1
by A40, FUNCT_4:14
.=
q . 1
by FINSEQ_1:5, FUNCT_1:72
;
dom qk1 =
dom (p +* (q | (Seg 1)))
by A16, A30, A32, A39, A17
.=
(dom p) \/ (dom (q | (Seg 1)))
by FUNCT_4:def 1
.=
(dom p) \/ ((dom q) /\ (Seg 1))
by RELAT_1:90
.=
dom p
by A23, XBOOLE_1:22
;
then A42:
len qk1 = len p
by FINSEQ_3:31;
q . 1
in the
Sorts of
(FreeEnv A) . ((the_arity_of (action_at v)) . 1)
by A14, A19, A38, MSAFREE2:14;
then reconsider T1 =
q . 1 as
Element of the
Sorts of
(FreeEnv A) . ((the_arity_of (action_at v)) /. 1) by A38, PARTFUN1:def 8;
card T1 in S1
by A36;
then A43:
card T1 <= card e1
by A37, XXREAL_2:def 8;
reconsider Tx =
p . 1 as
finite DecoratedTree by A34;
A44:
{} is
Element of
dom Tx
by TREES_1:47;
<*0 *> = <*0 *> ^ {}
by FINSEQ_1:47;
then reconsider w0 =
<*0 *> as
Element of
dom tree0 by A25, A44, TREES_4:11;
A45:
tree0 | w0 = e1
by A25, A34, TREES_4:def 4;
consider q0 being
DTree-yielding FinSequence such that A46:
e with-replacement w0,
T1 = [(action_at v),the carrier of IIG] -tree q0
and A47:
len q0 = len p
and A48:
q0 . (0 + 1) = T1
and A49:
for
i being
Element of
NAT st
i in dom p &
i <> 0 + 1 holds
q0 . i = p . i
by A2, PRE_CIRC:19;
then
treek1 = tree0 with-replacement w0,
T1
by A2, A31, A42, A46, A47, FINSEQ_1:18;
then
(card treek1) + (card (tree0 | w0)) = (card tree0) + (card T1)
by PRE_CIRC:23;
hence
card tk1 <= card e
by A2, A43, A45, XREAL_1:10;
:: thesis: verum end; suppose
k <> 0
;
:: thesis: card tk1 <= card ethen A54:
k >= 1
by NAT_1:14;
A55:
k + 1
<= len p
by A29, FINSEQ_3:27;
then A56:
k < len p
by NAT_1:13;
then A57:
k in dom p
by A54, FINSEQ_3:27;
A58:
k + 1
>= 1
by NAT_1:11;
T . k = p +* (q | (Seg k))
by A16, A57, A17;
then reconsider qk =
T . k as
Function ;
A59:
dom qk1 =
dom (p +* (q | (Seg (k + 1))))
by A16, A29, A30, A17
.=
(dom p) \/ (dom (q | (Seg (k + 1))))
by FUNCT_4:def 1
.=
(dom p) \/ ((dom q) /\ (Seg (k + 1)))
by RELAT_1:90
.=
dom p
by A23, XBOOLE_1:22
;
A60:
dom qk =
dom (p +* (q | (Seg k)))
by A16, A57, A17
.=
(dom p) \/ (dom (q | (Seg k)))
by FUNCT_4:def 1
.=
(dom p) \/ ((dom q) /\ (Seg k))
by RELAT_1:90
.=
dom p
by A23, 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;
A61:
for
x being
set st
x in dom qk holds
qk . x is
finite DecoratedTree
proof
let x be
set ;
:: thesis: ( x in dom qk implies qk . x is finite DecoratedTree )
assume A62:
x in dom qk
;
:: thesis: 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 A63:
n <= k
;
:: thesis: ( qk . n = q . n or qk . n = p . n )
n >= 1
by A62, FINSEQ_3:27;
then A64:
n in Seg k
by A63, FINSEQ_1:3;
dom (q | (Seg k)) = (dom q) /\ (Seg k)
by RELAT_1:90;
then A65:
n in dom (q | (Seg k))
by A23, A60, A62, A64, XBOOLE_0:def 4;
qk . n =
(p +* (q | (Seg k))) . n
by A16, A57, A17
.=
(q | (Seg k)) . n
by A65, FUNCT_4:14
.=
q . n
by A65, FUNCT_1:70
;
hence
(
qk . n = q . n or
qk . n = p . n )
;
:: thesis: verum end;
end;
then
qk . n in the
Sorts of
(FreeEnv A) . ((the_arity_of (action_at v)) . n)
by A2, A14, A19, A24, A60, A62, MSAFREE2:14;
then reconsider T1 =
qk . n as
Element of the
Sorts of
(FreeEnv A) . ((the_arity_of (action_at v)) /. n) by A24, A60, A62, PARTFUN1:def 8;
T1 in the
Sorts of
(FreeEnv A) . ((the_arity_of (action_at v)) /. n)
;
hence
qk . x is
finite DecoratedTree
;
:: thesis: verum
end; then
for
x being
set st
x in dom qk holds
qk . x is
DecoratedTree
;
then reconsider qk =
qk as
DTree-yielding FinSequence by TREES_3:26;
set v1 =
(the_arity_of (action_at v)) /. (k + 1);
then reconsider qkf =
doms qk as
FinTree-yielding FinSequence by TREES_3:25;
A69:
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 A69, FINSET_1:29;
A70:
card tk <= card e
by A28, A54, A56, FINSEQ_3:27;
consider e1 being
Element of the
Sorts of
(FreeEnv A) . ((the_arity_of (action_at v)) /. (k + 1)) such that A71:
e1 = p . (k + 1)
and A72:
card e1 = size ((the_arity_of (action_at v)) /. (k + 1)),
A
by A3, A29;
A73:
not
k + 1
in Seg k
by FINSEQ_3:9;
dom (q | (Seg k)) = (dom q) /\ (Seg k)
by RELAT_1:90;
then A74:
not
k + 1
in dom (q | (Seg k))
by A73, XBOOLE_0:def 4;
A75:
qk . (k + 1) =
(p +* (q | (Seg k))) . (k + 1)
by A16, A57, A17
.=
p . (k + 1)
by A74, FUNCT_4:12
;
A76:
k + 1
in dom (the_arity_of (action_at v))
by A21, A55, A58, FINSEQ_3:27;
then A77:
p . (k + 1) in the
Sorts of
(FreeEnv A) . ((the_arity_of (action_at v)) . (k + 1))
by A2, A19, MSAFREE2:14;
A78:
(the_arity_of (action_at v)) /. (k + 1) = (the_arity_of (action_at v)) . (k + 1)
by A76, PARTFUN1:def 8;
reconsider T1 =
p . (k + 1) as
Element of the
Sorts of
(FreeEnv A) . ((the_arity_of (action_at v)) /. (k + 1)) by A76, A77, PARTFUN1:def 8;
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 A75;
consider s1 being non
empty finite Subset of
NAT such that A79:
s1 = { (card t1) where t1 is Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. (k + 1)) : verum }
and A80:
card e1 = max s1
by A72, Def4;
reconsider S1 =
s1 as non
empty finite real-membered set ;
k + 1
in Seg (k + 1)
by FINSEQ_1:5;
then A81:
k + 1
in dom (q | (Seg (k + 1)))
by A23, A29, RELAT_1:86;
A82:
qk1 . (k + 1) =
(p +* (q | (Seg (k + 1)))) . (k + 1)
by A16, A29, A30, A17
.=
(q | (Seg (k + 1))) . (k + 1)
by A81, FUNCT_4:14
.=
q . (k + 1)
by FINSEQ_1:5, FUNCT_1:72
;
A83:
len qk1 = len p
by A59, FINSEQ_3:31;
reconsider T1 =
q . (k + 1) as
Element of the
Sorts of
(FreeEnv A) . ((the_arity_of (action_at v)) /. (k + 1)) by A14, A19, A76, A78, MSAFREE2:14;
card T1 in S1
by A79;
then A84:
card T1 <= card e1
by A80, XXREAL_2:def 8;
A85:
{} is
Element of
dom Tx
by TREES_1:47;
A86:
len qk = len p
by A60, FINSEQ_3:31;
A87:
k < len qk
by A56, A60, FINSEQ_3:31;
A88:
<*k*> = <*k*> ^ {}
by FINSEQ_1:47;
then A89:
<*k*> in dom tk
by A56, A85, A86, TREES_4:11;
reconsider w0 =
<*k*> as
Element of
dom tk by A85, A87, A88, TREES_4:11;
A90:
tk | w0 = e1
by A56, A71, A75, A86, TREES_4:def 4;
consider q0 being
DTree-yielding FinSequence such that A91:
tk with-replacement <*k*>,
T1 = [(action_at v),the carrier of IIG] -tree q0
and A92:
len q0 = len qk
and A93:
q0 . (k + 1) = T1
and A94:
for
i being
Element of
NAT st
i in dom qk &
i <> k + 1 holds
q0 . i = qk . i
by A89, PRE_CIRC:19;
now let n be
Nat;
:: thesis: ( 1 <= n & n <= len q0 implies q0 . b1 = qk1 . b1 )assume A95:
( 1
<= n &
n <= len q0 )
;
:: thesis: q0 . b1 = qk1 . b1then A96:
n in dom qk
by A92, FINSEQ_3:27;
per cases
( n = k + 1 or n > k + 1 or n < k + 1 )
by XXREAL_0:1;
suppose A97:
n > k + 1
;
:: thesis: qk1 . b1 = q0 . b1then A98:
not
n in Seg (k + 1)
by FINSEQ_1:3;
dom (q | (Seg (k + 1))) = (dom q) /\ (Seg (k + 1))
by RELAT_1:90;
then A99:
not
n in dom (q | (Seg (k + 1)))
by A98, XBOOLE_0:def 4;
k + 1
>= k
by NAT_1:11;
then
n > k
by A97, XXREAL_0:2;
then A100:
not
n in Seg k
by FINSEQ_1:3;
dom (q | (Seg k)) = (dom q) /\ (Seg k)
by RELAT_1:90;
then A101:
not
n in dom (q | (Seg k))
by A100, XBOOLE_0:def 4;
thus qk1 . n =
(p +* (q | (Seg (k + 1)))) . n
by A16, A29, A30, A17
.=
p . n
by A99, FUNCT_4:12
.=
(p +* (q | (Seg k))) . n
by A101, FUNCT_4:12
.=
qk . n
by A16, A57, A17
.=
q0 . n
by A94, A96, A97
;
:: thesis: verum end; suppose A102:
n < k + 1
;
:: thesis: qk1 . b1 = q0 . b1then A103:
n in Seg (k + 1)
by A95, FINSEQ_1:3;
A104:
n in dom q
by A22, A86, A92, A95, FINSEQ_3:27;
dom (q | (Seg (k + 1))) = (dom q) /\ (Seg (k + 1))
by RELAT_1:90;
then A105:
n in dom (q | (Seg (k + 1)))
by A103, A104, XBOOLE_0:def 4;
n <= k
by A102, NAT_1:13;
then A106:
n in Seg k
by A95, FINSEQ_1:3;
dom (q | (Seg k)) = (dom q) /\ (Seg k)
by RELAT_1:90;
then A107:
n in dom (q | (Seg k))
by A104, A106, XBOOLE_0:def 4;
thus qk1 . n =
(p +* (q | (Seg (k + 1)))) . n
by A16, A29, A30, A17
.=
(q | (Seg (k + 1))) . n
by A105, FUNCT_4:14
.=
q . n
by A105, FUNCT_1:70
.=
(q | (Seg k)) . n
by A107, FUNCT_1:70
.=
(p +* (q | (Seg k))) . n
by A107, FUNCT_4:14
.=
qk . n
by A16, A57, A17
.=
q0 . n
by A94, A96, A102
;
:: thesis: verum end; end; then
treek1 = tk with-replacement w0,
T1
by A31, A83, A86, A91, A92, FINSEQ_1:18;
then
(card treek1) + (card (tk | w0)) = (card tk) + (card T1)
by PRE_CIRC:23;
then
card tk1 <= card tk
by A84, A90, XREAL_1:10;
hence
card tk1 <= card e
by A70, XXREAL_0:2;
:: thesis: verum end;
end; end; A108:
for
k being
Element of
NAT holds
S2[
k]
from NAT_1:sch 1(A26, A27);
dom p = Seg (len p)
by FINSEQ_1:def 3;
then A109:
dom p = dom q
by A22, FINSEQ_1:def 3;
A110:
len p in dom p
by A25, FINSEQ_3:27;
then T . (len p) =
p +* (q | (dom p))
by A16, A18, A17
.=
p +* q
by A109, RELAT_1:98
.=
q
by A23, FUNCT_4:20
;
hence
r <= card e
by A9, A14, A108, A110;
:: thesis: verum end; hence
r <= card e
;
:: thesis: verum end; end;
hence
card e = size v,A
by A5, A6, XXREAL_2:def 8; :: thesis: verum