let IIG be non empty non void Circuit-like monotonic ManySortedSign ; for SCS being non-empty finite-yielding MSAlgebra over IIG
for v, w being Vertex of IIG
for e1 being Element of the Sorts of (FreeEnv SCS) . v
for e2 being Element of the Sorts of (FreeEnv SCS) . w
for q1 being DTree-yielding FinSequence st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e1 = size (v,SCS) & e1 = [(action_at v), the carrier of IIG] -tree q1 & e2 in rng q1 holds
card e2 = size (w,SCS)
let SCS be non-empty finite-yielding MSAlgebra over IIG; for v, w being Vertex of IIG
for e1 being Element of the Sorts of (FreeEnv SCS) . v
for e2 being Element of the Sorts of (FreeEnv SCS) . w
for q1 being DTree-yielding FinSequence st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e1 = size (v,SCS) & e1 = [(action_at v), the carrier of IIG] -tree q1 & e2 in rng q1 holds
card e2 = size (w,SCS)
let v, w be Vertex of IIG; for e1 being Element of the Sorts of (FreeEnv SCS) . v
for e2 being Element of the Sorts of (FreeEnv SCS) . w
for q1 being DTree-yielding FinSequence st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e1 = size (v,SCS) & e1 = [(action_at v), the carrier of IIG] -tree q1 & e2 in rng q1 holds
card e2 = size (w,SCS)
let e1 be Element of the Sorts of (FreeEnv SCS) . v; for e2 being Element of the Sorts of (FreeEnv SCS) . w
for q1 being DTree-yielding FinSequence st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e1 = size (v,SCS) & e1 = [(action_at v), the carrier of IIG] -tree q1 & e2 in rng q1 holds
card e2 = size (w,SCS)
let e2 be Element of the Sorts of (FreeEnv SCS) . w; for q1 being DTree-yielding FinSequence st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e1 = size (v,SCS) & e1 = [(action_at v), the carrier of IIG] -tree q1 & e2 in rng q1 holds
card e2 = size (w,SCS)
let q1 be DTree-yielding FinSequence; ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e1 = size (v,SCS) & e1 = [(action_at v), the carrier of IIG] -tree q1 & e2 in rng q1 implies card e2 = size (w,SCS) )
assume that
A1:
v in (InnerVertices IIG) \ (SortsWithConstants IIG)
and
A2:
card e1 = size (v,SCS)
and
A3:
e1 = [(action_at v), the carrier of IIG] -tree q1
and
A4:
e2 in rng q1
; card e2 = size (w,SCS)
consider sw being non empty finite Subset of NAT such that
A5:
sw = { (card t) where t is Element of the Sorts of (FreeEnv SCS) . w : verum }
and
A6:
size (w,SCS) = max sw
by Def4;
reconsider Y = sw as non empty finite real-membered set ;
reconsider m = max Y as Real ;
m in { (card t) where t is Element of the Sorts of (FreeEnv SCS) . w : verum }
by A5, XXREAL_2:def 8;
then consider e3 being Element of the Sorts of (FreeEnv SCS) . w such that
A7:
card e3 = m
;
card e2 in Y
by A5;
then A8:
card e2 <= max Y
by XXREAL_2:def 8;
reconsider e39 = e3 as DecoratedTree ;
reconsider e19 = e1 as DecoratedTree ;
reconsider q19 = q1 as Function ;
consider k being object such that
A9:
k in dom q19
and
A10:
e2 = q19 . k
by A4, FUNCT_1:def 3;
k in dom q1
by A9;
then reconsider kN = k as Element of NAT ;
reconsider k1 = kN - 1 as Element of NAT by A9, FINSEQ_3:26;
A11:
k1 + 1 = kN
;
ex p being DTree-yielding FinSequence st
( p = q1 & dom e19 = tree (doms p) )
by A3, TREES_4:def 4;
then reconsider k9 = <*k1*> as Element of dom e1 by A9, A11, PRE_CIRC:13;
A12:
kN <= len q1
by A9, FINSEQ_3:25;
k1 < kN
by A11, XREAL_1:29;
then
k1 < len q1
by A12, XXREAL_0:2;
then A13:
e1 | k9 = e2
by A3, A10, A11, TREES_4:def 4;
assume
card e2 <> size (w,SCS)
; contradiction
then
card e2 < max Y
by A6, A8, XXREAL_0:1;
then
( (card (e1 with-replacement (k9,e3))) + (card (e1 | k9)) = (card e1) + (card e3) & (card e1) + (card (e1 | k9)) < (card e1) + (card e3) )
by A7, A13, PRE_CIRC:18, XREAL_1:6;
then A14:
card e1 < card (e1 with-replacement (k9,e3))
by XREAL_1:6;
reconsider k99 = k9 as FinSequence of NAT ;
reconsider eke = e19 with-replacement (k99,e39) as DecoratedTree ;
reconsider eke = eke as Element of the Sorts of (FreeEnv SCS) . v by A1, A3, A9, A10, A11, Th6;
consider sv being non empty finite Subset of NAT such that
A15:
sv = { (card t) where t is Element of the Sorts of (FreeEnv SCS) . v : verum }
and
A16:
size (v,SCS) = max sv
by Def4;
reconsider Z = sv as non empty finite real-membered set ;
card eke in Z
by A15;
hence
contradiction
by A2, A16, A14, XXREAL_2:def 8; verum