let IIG be non empty non void Circuit-like monotonic ManySortedSign ; 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; 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; ( 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))
; 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;
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; verum