let IIG be non empty non void Circuit-like monotonic ManySortedSign ; :: thesis: for A being non-empty finite-yielding MSAlgebra of IIG
for v, v1 being SortSymbol of IIG st v in InnerVertices IIG & v1 in rng (the_arity_of (action_at v)) holds
depth v1,A < depth v,A
let A be non-empty finite-yielding MSAlgebra of IIG; :: thesis: for v, v1 being SortSymbol of IIG st v in InnerVertices IIG & v1 in rng (the_arity_of (action_at v)) holds
depth v1,A < depth v,A
let v, v1 be SortSymbol of IIG; :: thesis: ( v in InnerVertices IIG & v1 in rng (the_arity_of (action_at v)) implies depth v1,A < depth v,A )
assume that
A1:
v in InnerVertices IIG
and
A2:
v1 in rng (the_arity_of (action_at v))
; :: thesis: depth v1,A < depth v,A
consider s being non empty finite Subset of NAT such that
A3:
s = { (depth t) where t is Element of the Sorts of (FreeEnv A) . v : verum }
and
A4:
depth v,A = max s
by Def6;
reconsider Y = s as non empty finite real-membered set ;
max Y in { (depth t) where t is Element of the Sorts of (FreeEnv A) . v : verum }
by A3, XXREAL_2:def 8;
then consider t being Element of the Sorts of (FreeEnv A) . v such that
A5:
depth t = max Y
;
consider s1 being non empty finite Subset of NAT such that
A6:
s1 = { (depth t1) where t1 is Element of the Sorts of (FreeEnv A) . v1 : verum }
and
A7:
depth v1,A = max s1
by Def6;
reconsider Y1 = s1 as non empty finite real-membered set ;
max Y1 in { (depth t1) where t1 is Element of the Sorts of (FreeEnv A) . v1 : verum }
by A6, XXREAL_2:def 8;
then consider t1 being Element of the Sorts of (FreeEnv A) . v1 such that
A8:
depth t1 = max Y1
;
consider e' being Element of the Sorts of (FreeMSA the Sorts of A) . v1 such that
A9:
t1 = e'
and
A10:
depth t1 = depth e'
by Def5;
consider dt1' being finite DecoratedTree, t1' being finite Tree such that
A11:
dt1' = e'
and
A12:
t1' = dom dt1'
and
A13:
depth e' = height t1'
by MSAFREE2:def 14;
A14:
size v1,A < size v,A
by A1, A2, Th15;
size v1,A > 0
by Th16;
then
0 + 1 <= size v1,A
by NAT_1:13;
then
not v in (InputVertices IIG) \/ (SortsWithConstants IIG)
by A14, Th11;
then A15:
( not v in InputVertices IIG & not v in SortsWithConstants IIG )
by XBOOLE_0:def 3;
then A16:
v in (InnerVertices IIG) \ (SortsWithConstants IIG)
by A1, XBOOLE_0:def 5;
FreeEnv A = MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #)
by MSAFREE:def 16;
then
the Sorts of (FreeEnv A) . v = FreeSort the Sorts of A,v
by MSAFREE:def 13;
then
t in FreeSort the Sorts of A,v
;
then
t in { a where a is Element of TS (DTConMSA the Sorts of A) : ( ex x being set st
( x in the Sorts of A . v & a = root-tree [x,v] ) or ex o being OperSymbol of IIG st
( [o,the carrier of IIG] = a . {} & the_result_sort_of o = v ) ) }
by MSAFREE:def 12;
then consider a being Element of TS (DTConMSA the Sorts of A) such that
A17:
a = t
and
A18:
( ex x being set st
( x in the Sorts of A . v & a = root-tree [x,v] ) or ex o being OperSymbol of IIG st
( [o,the carrier of IIG] = a . {} & the_result_sort_of o = v ) )
;
now given x being
set such that
x in the
Sorts of
A . v
and A19:
a = root-tree [x,v]
;
:: thesis: contradictionconsider e' being
Element of the
Sorts of
(FreeMSA the Sorts of A) . v such that A20:
t = e'
and A21:
depth t = depth e'
by Def5;
consider dta being
finite DecoratedTree,
ta being
finite Tree such that A22:
dta = e'
and A23:
ta = dom dta
and A24:
depth e' = height ta
by MSAFREE2:def 14;
depth t = 0
by A17, A19, A20, A21, A22, A23, A24, TREES_1:79, TREES_4:3;
hence
contradiction
by A4, A5, A15, Th19;
:: thesis: verum end;
then consider o being OperSymbol of IIG such that
A25:
[o,the carrier of IIG] = a . {}
and
A26:
the_result_sort_of o = v
by A18;
A27:
NonTerminals (DTConMSA the Sorts of A) = [:the carrier' of IIG,{the carrier of IIG}:]
by MSAFREE:6;
the carrier of IIG in {the carrier of IIG}
by TARSKI:def 1;
then reconsider o' = [o,the carrier of IIG] as NonTerminal of (DTConMSA the Sorts of A) by A27, ZFMISC_1:106;
consider q being FinSequence of TS (DTConMSA the Sorts of A) such that
A28:
a = o' -tree q
and
o' ==> roots q
by A25, DTCONSTR:10;
consider q' being DTree-yielding FinSequence such that
A29:
q = q'
and
A30:
dom a = tree (doms q')
by A28, TREES_4:def 4;
reconsider av = action_at v as OperSymbol of IIG ;
consider x being set such that
A31:
x in dom (the_arity_of av)
and
A32:
v1 = (the_arity_of av) . x
by A2, FUNCT_1:def 5;
reconsider k = x as Element of NAT by A31;
A33:
o = av
by A1, A26, MSAFREE2:def 7;
then A34:
len q' = len (the_arity_of av)
by A17, A26, A28, A29, MSAFREE2:13;
then A35:
dom q' = dom (the_arity_of av)
by FINSEQ_3:31;
A36:
k in dom q'
by A31, A34, FINSEQ_3:31;
reconsider k1 = k - 1 as Element of NAT by A31, FINSEQ_3:28;
A37:
k1 + 1 = k
;
then A38:
<*k1*> in tree (doms q')
by A31, A35, PRE_CIRC:17;
reconsider f = <*k1*> as FinSequence of NAT ;
consider qq being DTree-yielding FinSequence such that
A39:
t with-replacement f,t1 = o' -tree qq
and
A40:
len qq = len q'
and
qq . (k1 + 1) = t1
and
for i being Element of NAT st i in dom q' & i <> k1 + 1 holds
qq . i = q' . i
by A17, A28, A29, A30, A38, PRE_CIRC:19;
A41:
q' . k in the Sorts of (FreeEnv A) . v1
by A17, A26, A28, A29, A31, A32, A33, MSAFREE2:14;
reconsider tft = t with-replacement f,t1 as DecoratedTree ;
t = [av,the carrier of IIG] -tree q'
by A1, A17, A26, A28, A29, MSAFREE2:def 7;
then reconsider tft = tft as Element of the Sorts of (FreeEnv A) . v by A16, A36, A37, A41, Th7;
reconsider dtft = depth tft as Real ;
dtft in Y
by A3;
then A42:
dtft <= depth t
by A5, XXREAL_2:def 8;
consider e' being Element of the Sorts of (FreeMSA the Sorts of A) . v such that
A43:
tft = e'
and
A44:
depth tft = depth e'
by Def5;
consider dttft being finite DecoratedTree, ttft being finite Tree such that
A45:
dttft = e'
and
A46:
ttft = dom dttft
and
A47:
depth e' = height ttft
by MSAFREE2:def 14;
A48:
k in dom qq
by A31, A34, A40, FINSEQ_3:31;
consider qq' being DTree-yielding FinSequence such that
A49:
qq = qq'
and
A50:
dom tft = tree (doms qq')
by A39, TREES_4:def 4;
reconsider f' = f as Element of ttft by A37, A43, A45, A46, A48, A49, A50, PRE_CIRC:17;
A51:
f' <> {}
;
dom tft = (dom t) with-replacement f,(dom t1)
by A17, A30, A38, TREES_2:def 12;
then
ttft | f = t1'
by A9, A11, A12, A17, A30, A36, A37, A43, A45, A46, PRE_CIRC:17, TREES_1:66;
hence
depth v1,A < depth v,A
by A4, A5, A7, A8, A10, A13, A42, A44, A47, A51, TREES_1:85, XXREAL_0:2; :: thesis: verum