let IIG be non empty non void Circuit-like monotonic ManySortedSign ; :: thesis: for A being non-empty finite-yielding MSAlgebra of 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 of 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 set such that
A3:
x in dom (the_arity_of av)
and
A4:
w = (the_arity_of av) . x
by A2, FUNCT_1:def 5;
reconsider k = x as Element of NAT by A3;
consider sv being non empty finite Subset of NAT such that
A5:
sv = { (card tv) where tv is Element of the Sorts of (FreeEnv A) . v : verum }
and
A6:
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
A7:
card tv = max Yv
by A5;
reconsider e1 = tv as finite DecoratedTree ;
then A13:
v in (InnerVertices IIG) \ (SortsWithConstants IIG)
by A1, XBOOLE_0:def 5;
then consider p being DTree-yielding FinSequence such that
A14:
tv = [av,the carrier of IIG] -tree p
by A6, A7, Th13;
consider sw being non empty finite Subset of NAT such that
A15:
sw = { (card tw) where tw is Element of the Sorts of (FreeEnv A) . w : verum }
and
A16:
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
A17:
card tw = max Yw
by A15;
reconsider e2 = tw as finite DecoratedTree ;
consider p' being DTree-yielding FinSequence such that
A18:
p' = p
and
A19:
dom e1 = tree (doms p')
by A14, TREES_4:def 4;
A20:
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 A14, MSAFREE2:13;
then A21:
k in dom p
by A3, FINSEQ_3:31;
reconsider k1 = k - 1 as Element of NAT by A3, FINSEQ_3:28;
A22:
k1 + 1 = k
;
reconsider o = <*k1*> as FinSequence of NAT ;
reconsider o = o as Element of dom e1 by A18, A19, A21, A22, PRE_CIRC:17;
reconsider eoe = e1 with-replacement o,e2 as finite Function ;
reconsider de1 = dom e1 as finite Tree ;
reconsider de2 = dom e2 as finite Tree ;
reconsider o = o as Element of de1 ;
A23:
dom eoe = de1 with-replacement o,de2
by TREES_2:def 12;
reconsider deoe = dom eoe as finite Tree ;
p . k in the Sorts of (FreeEnv A) . ((the_arity_of av) . k)
by A3, A14, A20, MSAFREE2:14;
then reconsider eoe = eoe as Element of the Sorts of (FreeEnv A) . v by A4, A13, A14, A21, A22, Th7;
card eoe in Yv
by A5;
then A24:
card eoe <= size v,A
by A6, XXREAL_2:def 8;
A25:
(card deoe) + (card (de1 | o)) = (card de1) + (card de2)
by A23, PRE_CIRC:22;
card (de1 | o) < card de1
by PRE_CIRC:20;
then
(card (de1 | o)) + (card de2) < (card deoe) + (card (de1 | o))
by A25, XREAL_1:8;
then
card de2 < card deoe
by XREAL_1:8;
then A26:
card e2 < card deoe
by CARD_1:104;
card deoe <= size v,A
by A24, CARD_1:104;
hence
size w,A < size v,A
by A16, A17, A26, XXREAL_0:2; :: thesis: verum