let IIG be non empty non void Circuit-like monotonic ManySortedSign ; for A being non-empty finite-yielding MSAlgebra over 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 over 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 v, v1 be SortSymbol of IIG; ( 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))
; depth (v1,A) < depth (v,A)
size (v1,A) > 0
by Th15;
then A3:
0 + 1 <= size (v1,A)
by NAT_1:13;
size (v1,A) < size (v,A)
by A1, A2, Th14;
then A4:
not v in (InputVertices IIG) \/ (SortsWithConstants IIG)
by A3, Th10;
then A5:
not v in SortsWithConstants IIG
by XBOOLE_0:def 3;
then A6:
v in (InnerVertices IIG) \ (SortsWithConstants IIG)
by A1, XBOOLE_0:def 5;
consider s1 being non empty finite Subset of NAT such that
A7:
s1 = { (depth t1) where t1 is Element of the Sorts of (FreeEnv A) . v1 : verum }
and
A8:
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 A7, XXREAL_2:def 8;
then consider t1 being Element of the Sorts of (FreeEnv A) . v1 such that
A9:
depth t1 = max Y1
;
reconsider av = action_at v as OperSymbol of IIG ;
consider s being non empty finite Subset of NAT such that
A10:
s = { (depth t) where t is Element of the Sorts of (FreeEnv A) . v : verum }
and
A11:
depth (v,A) = max s
by Def6;
consider x being object such that
A12:
x in dom (the_arity_of av)
and
A13:
v1 = (the_arity_of av) . x
by A2, FUNCT_1:def 3;
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 A10, XXREAL_2:def 8;
then consider t being Element of the Sorts of (FreeEnv A) . v such that
A14:
depth t = max Y
;
FreeEnv A = MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #)
by MSAFREE:def 14;
then
the Sorts of (FreeEnv A) . v = FreeSort ( the Sorts of A,v)
by MSAFREE:def 11;
then
t in FreeSort ( the Sorts of A,v)
;
then A15:
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 10;
reconsider k = x as Element of NAT by A12;
reconsider k1 = k - 1 as Element of NAT by A12, FINSEQ_3:26;
reconsider f = <*k1*> as FinSequence of NAT ;
A16:
k1 + 1 = k
;
reconsider tft = t with-replacement (f,t1) as DecoratedTree ;
consider e9 being Element of the Sorts of (FreeMSA the Sorts of A) . v1 such that
A17:
t1 = e9
and
A18:
depth t1 = depth e9
by Def5;
consider dt19 being finite DecoratedTree, t19 being finite Tree such that
A19:
( dt19 = e9 & t19 = dom dt19 )
and
A20:
depth e9 = height t19
by MSAFREE2:def 14;
consider a being Element of TS (DTConMSA the Sorts of A) such that
A21:
a = t
and
A22:
( 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 A15;
A23:
not v in InputVertices IIG
by A4, XBOOLE_0:def 3;
then consider o being OperSymbol of IIG such that
A26:
[o, the carrier of IIG] = a . {}
and
A27:
the_result_sort_of o = v
by A22;
( NonTerminals (DTConMSA the Sorts of A) = [: the carrier' of IIG,{ the carrier of IIG}:] & the carrier of IIG in { the carrier of IIG} )
by MSAFREE:6, TARSKI:def 1;
then reconsider o9 = [o, the carrier of IIG] as NonTerminal of (DTConMSA the Sorts of A) by ZFMISC_1:87;
consider q being FinSequence of TS (DTConMSA the Sorts of A) such that
A28:
a = o9 -tree q
and
o9 ==> roots q
by A26, DTCONSTR:10;
consider q9 being DTree-yielding FinSequence such that
A29:
q = q9
and
A30:
dom a = tree (doms q9)
by A28, TREES_4:def 4;
A31:
t = [av, the carrier of IIG] -tree q9
by A1, A21, A27, A28, A29, MSAFREE2:def 7;
A32:
o = av
by A1, A27, MSAFREE2:def 7;
then A33:
len q9 = len (the_arity_of av)
by A21, A27, A28, A29, MSAFREE2:10;
then A34:
k in dom q9
by A12, FINSEQ_3:29;
A35:
dom q9 = dom (the_arity_of av)
by A33, FINSEQ_3:29;
then consider qq being DTree-yielding FinSequence such that
A36:
t with-replacement (f,t1) = o9 -tree qq
and
A37:
len qq = len q9
and
qq . (k1 + 1) = t1
and
for i being Nat st i in dom q9 & i <> k1 + 1 holds
qq . i = q9 . i
by A21, A28, A29, A30, A12, PRE_CIRC:13, PRE_CIRC:15;
A38:
k in dom qq
by A12, A33, A37, FINSEQ_3:29;
q9 . k in the Sorts of (FreeEnv A) . v1
by A21, A27, A28, A29, A12, A13, A32, MSAFREE2:11;
then reconsider tft = tft as Element of the Sorts of (FreeEnv A) . v by A6, A34, A16, A31, Th6;
reconsider dtft = depth tft as Real ;
dtft in Y
by A10;
then A39:
dtft <= depth t
by A14, XXREAL_2:def 8;
consider e9 being Element of the Sorts of (FreeMSA the Sorts of A) . v such that
A40:
tft = e9
and
A41:
depth tft = depth e9
by Def5;
consider dttft being finite DecoratedTree, ttft being finite Tree such that
A42:
( dttft = e9 & ttft = dom dttft )
and
A43:
depth e9 = height ttft
by MSAFREE2:def 14;
ex qq9 being DTree-yielding FinSequence st
( qq = qq9 & dom tft = tree (doms qq9) )
by A36, TREES_4:def 4;
then reconsider f9 = f as Element of ttft by A16, A40, A42, A38, PRE_CIRC:13;
<*k1*> in tree (doms q9)
by A12, A35, A16, PRE_CIRC:13;
then
dom tft = (dom t) with-replacement (f,(dom t1))
by A21, A30, TREES_2:def 11;
then
( f9 <> {} & ttft | f = t19 )
by A17, A19, A21, A30, A34, A16, A40, A42, PRE_CIRC:13, TREES_1:33;
hence
depth (v1,A) < depth (v,A)
by A11, A14, A8, A9, A18, A20, A39, A41, A43, TREES_1:48, XXREAL_0:2; verum