let IIG be non empty non void Circuit-like monotonic ManySortedSign ; :: thesis:
let A be non-empty Circuit of IIG; :: thesis:
let v be Vertex of IIG; :: thesis:
let e be Element of the Sorts of (FreeEnv A) . v; :: thesis:
let p be DTree-yielding FinSequence; :: thesis:
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:
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 :: thesis:

reconsider e9 = e as finite set ;
let r be ExtReal; :: thesis:
A7: 1 <= card e9 by NAT_1:14;
assume r in S ; :: thesis:
then 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 by A10;

suppose ex x being set st
( x in the Sorts of A . v & a9 = root-tree [x,v] ) ; :: thesis:

then consider x being set such that
x in the Sorts of A . v and
A11: a9 = root-tree [x,v] ;
root-tree [x,v] = {[{},[x,v]]} by TREES_4:6;
hence r <= card e by A7, A8, A9, A11, CARD_1:30; :: thesis:

end;

suppose ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a9 . {} & the_result_sort_of o = v ) ; :: thesis:

then 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 H₁( 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 = H₁(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 :: thesis:

per cases ;

suppose len q = 0 ; :: thesis:

then q = {} ;
then t = root-tree [(action_at v), the carrier of IIG] by A12, TREES_4:20;
hence r <= card e by A7, A8, PRE_CIRC:19; :: thesis:

end;

suppose A18: len q <> 0 ; :: thesis:

defpred S₂[ 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 :: thesis:

let k be Nat; :: thesis:
assume A25: S₂[k] ; :: thesis:
thus S₂[k + 1] :: thesis:

proof

reconsider tree0 = [(action_at v), the carrier of IIG] -tree p as finite DecoratedTree by A2;
assume A26: k + 1 in dom p ; :: thesis:
let qk1 be DTree-yielding FinSequence; :: thesis:
assume A27: qk1 = T . (k + 1) ; :: thesis:
let tk1 be finite set ; :: thesis:
assume A28: tk1 = [(action_at v), the carrier of IIG] -tree qk1 ; :: thesis:
then reconsider treek1 = tk1 as finite DecoratedTree ;

per cases ;

suppose A29: k = 0 ; :: thesis:

set 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 :: thesis:

let k be Nat; :: thesis:
assume ( 1 <= k & k <= len q0 ) ; :: thesis:
then A42: k in dom p by A36, FINSEQ_3:25;

per cases ;

suppose k = 1 ; :: thesis:

hence q0 . k = qk1 . k by A40, A37; :: thesis:

end;

suppose A43: k <> 1 ; :: thesis:

A44: 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 ; :: thesis:

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; :: thesis:

end;

suppose A50: k <> 0 ; :: thesis:

A51: 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 ; :: thesis:
assume A60: x in dom qk ; :: thesis:
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 ;

suppose A61: n <= k ; :: thesis:

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

end;

suppose A64: n > k ; :: thesis:

A65: dom (q | (Seg k)) = (dom q) /\ (Seg k) by RELAT_1:61;
not n in Seg k by A64, FINSEQ_1:1;
then A66: not n in dom (q | (Seg k)) by A65, XBOOLE_0:def 4;
qk . n = (p +* (q | (Seg k))) . n by A14, A15, A57
.= p . n by A66, FUNCT_4:11 ;
hence ( qk . n = q . n or qk . n = p . n ) ; :: thesis:

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 ; :: thesis:

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 ;

now :: thesis:

let x be object ; :: thesis:
assume x in dom (doms qk) ; :: thesis:
then A69: x in dom qk by TREES_3:37;
then reconsider T1 = qk . x as finite DecoratedTree by A59;
dom T1 is finite Tree ;
hence (doms qk) . x is finite Tree by A69, FUNCT_6:22; :: thesis:

end;

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

let n be Nat; :: thesis:
assume that
A80: 1 <= n and
A81: n <= len q0 ; :: thesis:
A82: n in dom qk by A75, A80, A81, FINSEQ_3:25;

per cases by XXREAL_0:1;

suppose n = k + 1 ; :: thesis:

hence q0 . n = qk1 . n by A78, A76; :: thesis:

end;

suppose A83: n > k + 1 ; :: thesis:

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 ; :: thesis:

end;

suppose A88: n < k + 1 ; :: thesis:

A89: 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 ; :: thesis:

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; :: thesis:

end;

A99: S₂[ 0 ] by FINSEQ_3:25;
A100: for k being Nat holds S₂[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; :: thesis:

end;

hence r <= card e ; :: thesis:

end;

card e in S by A4;
hence card e = size (v,A) by A5, A6, XXREAL_2:def 8; :: thesis: