let IIG be non empty non void Circuit-like monotonic ManySortedSign ; :: thesis: for A being non-empty finite-yielding MSAlgebra over IIG
for v, w being Element of IIG st v in InnerVertices IIG & w in rng (the_arity_of (action_at v)) holds
size (w,A) < size (v,A)
let A be non-empty finite-yielding MSAlgebra over IIG; :: thesis: for v, w being Element of IIG st v in InnerVertices IIG & w in rng (the_arity_of (action_at v)) holds
size (w,A) < size (v,A)
let v, w be Element of IIG; :: thesis: ( v in InnerVertices IIG & w in rng (the_arity_of (action_at v)) implies size (w,A) < size (v,A) )
assume that
A1: v in InnerVertices IIG and
A2: w in rng (the_arity_of (action_at v)) ; :: thesis: size (w,A) < size (v,A)
reconsider av = action_at v as OperSymbol of IIG ;
consider x being object such that
A3: x in dom (the_arity_of av) and
A4: w = (the_arity_of av) . x by A2, FUNCT_1:def 3;
reconsider k = x as Element of NAT by A3;
reconsider k1 = k - 1 as Element of NAT by A3, FINSEQ_3:26;
A5: k1 + 1 = k ;
reconsider o = <*k1*> as FinSequence of NAT ;
consider sv being non empty finite Subset of NAT such that
A6: sv = { (card tv) where tv is Element of the Sorts of (FreeEnv A) . v : verum } and
A7: size (v,A) = max sv by Def4;
reconsider Yv = sv as non empty finite real-membered set ;
max Yv in Yv by XXREAL_2:def 8;
then consider tv being Element of the Sorts of (FreeEnv A) . v such that
A8: card tv = max Yv by A6;

now :: thesis: not v in SortsWithConstants IIG

assume v in SortsWithConstants IIG ; :: thesis: contradiction
then v in { v9 where v9 is SortSymbol of IIG : v9 is with_const_op } by MSAFREE2:def 1;
then consider v9 being SortSymbol of IIG such that
A9: v9 = v and
A10: v9 is with_const_op ;
consider oo being OperSymbol of IIG such that
A11: the Arity of IIG . oo = {} and
A12: the ResultSort of IIG . oo = v9 by A10, MSUALG_2:def 1;
the_result_sort_of oo = v by A9, A12, MSUALG_1:def 2
.= the_result_sort_of av by A1, MSAFREE2:def 7 ;
then A13: av = oo by MSAFREE2:def 6;
reconsider aoo = the Arity of IIG . oo as FinSequence ;
dom aoo = {} by A11;
hence contradiction by A3, A13, MSUALG_1:def 1; :: thesis: verum

end;

then A14: v in (InnerVertices IIG) \ (SortsWithConstants IIG) by A1, XBOOLE_0:def 5;
then consider p being DTree-yielding FinSequence such that
A15: tv = [av, the carrier of IIG] -tree p by A7, A8, Th12;
A16: the Sorts of (FreeEnv A) . v = the Sorts of (FreeEnv A) . (the_result_sort_of av) by A1, MSAFREE2:def 7;
then len p = len (the_arity_of av) by A15, MSAFREE2:10;
then A17: k in dom p by A3, FINSEQ_3:29;
reconsider e1 = tv as finite DecoratedTree ;
reconsider de1 = dom e1 as finite Tree ;
consider sw being non empty finite Subset of NAT such that
A18: sw = { (card tw) where tw is Element of the Sorts of (FreeEnv A) . w : verum } and
A19: size (w,A) = max sw by Def4;
reconsider Yw = sw as non empty finite real-membered set ;
max Yw in Yw by XXREAL_2:def 8;
then consider tw being Element of the Sorts of (FreeEnv A) . w such that
A20: card tw = max Yw by A18;
reconsider e2 = tw as finite DecoratedTree ;
reconsider de2 = dom e2 as finite Tree ;
ex p9 being DTree-yielding FinSequence st
( p9 = p & dom e1 = tree (doms p9) ) by A15, TREES_4:def 4;
then reconsider o = o as Element of dom e1 by A17, A5, PRE_CIRC:13;
reconsider eoe = e1 with-replacement (o,e2) as finite Function ;
reconsider o = o as Element of de1 ;
reconsider deoe = dom eoe as finite Tree ;
A21: card (de1 | o) < card de1 by PRE_CIRC:16;
dom eoe = de1 with-replacement (o,de2) by TREES_2:def 11;
then (card deoe) + (card (de1 | o)) = (card de1) + (card de2) by PRE_CIRC:17;
then (card (de1 | o)) + (card de2) < (card deoe) + (card (de1 | o)) by A21, XREAL_1:6;
then card de2 < card deoe by XREAL_1:6;
then A22: card e2 < card deoe by CARD_1:62;
p . k in the Sorts of (FreeEnv A) . ((the_arity_of av) . k) by A3, A15, A16, MSAFREE2:11;
then reconsider eoe = eoe as Element of the Sorts of (FreeEnv A) . v by A4, A14, A15, A17, A5, Th6;
card eoe in Yv by A6;
then card eoe <= size (v,A) by A7, XXREAL_2:def 8;
then card deoe <= size (v,A) by CARD_1:62;
hence size (w,A) < size (v,A) by A19, A20, A22, XXREAL_0:2; :: thesis: verum