let IIG be non empty non void Circuit-like monotonic ManySortedSign ; :: thesis: for SCS being non-empty finite-yielding MSAlgebra of 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 of IIG; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: card e2 = size w,SCS
assume A5: card e2 <> size w,SCS ; :: thesis: contradiction
consider sw being non empty finite Subset of NAT such that
A6: sw = { (card t) where t is Element of the Sorts of (FreeEnv SCS) . w : verum } and
A7: size w,SCS = max sw by Def4;
reconsider Y = sw as non empty finite real-membered set ;
card e2 in Y by A6;
then card e2 <= max Y by XXREAL_2:def 8;
then A8: card e2 < max Y by A5, A7, XXREAL_0:1;
reconsider m = max Y as real number ;
m in { (card t) where t is Element of the Sorts of (FreeEnv SCS) . w : verum } by A6, XXREAL_2:def 8;
then consider e3 being Element of the Sorts of (FreeEnv SCS) . w such that
A9: card e3 = m ;
consider sv being non empty finite Subset of NAT such that
A10: sv = { (card t) where t is Element of the Sorts of (FreeEnv SCS) . v : verum } and
A11: size v,SCS = max sv by Def4;
reconsider Z = sv as non empty finite real-membered set ;
reconsider q1' = q1 as Function ;
consider k being set such that
A12: k in dom q1' and
A13: e2 = q1' . k by A4, FUNCT_1:def 5;
k in dom q1 by A12;
then reconsider kN = k as Element of NAT ;
reconsider k1 = kN - 1 as Element of NAT by A12, FINSEQ_3:28;
A14: k1 + 1 = kN ;
A15: kN <= len q1 by A12, FINSEQ_3:27;
k1 < kN by A14, XREAL_1:31;
then A16: k1 < len q1 by A15, XXREAL_0:2;
reconsider e1' = e1 as DecoratedTree ;
consider p being DTree-yielding FinSequence such that
A17: p = q1 and
A18: dom e1' = tree (doms p) by A3, TREES_4:def 4;
reconsider k' = <*k1*> as Element of dom e1 by A12, A14, A17, A18, PRE_CIRC:17;
reconsider e3' = e3 as DecoratedTree ;
reconsider k'' = k' as FinSequence of NAT ;
reconsider eke = e1' with-replacement k'',e3' as DecoratedTree ;
reconsider eke = eke as Element of the Sorts of (FreeEnv SCS) . v by A1, A3, A12, A13, A14, Th7;
A19: card eke in Z by A10;
A20: (card (e1 with-replacement k',e3)) + (card (e1 | k')) = (card e1) + (card e3) by PRE_CIRC:23;
e1 | k' = e2 by A3, A13, A14, A16, TREES_4:def 4;
then (card e1) + (card (e1 | k')) < (card e1) + (card e3) by A8, A9, XREAL_1:8;
then card e1 < card (e1 with-replacement k',e3) by A20, XREAL_1:8;
hence contradiction by A2, A11, A19, XXREAL_2:def 8; :: thesis: verum