let IIG be non empty non void Circuit-like monotonic ManySortedSign ; for A being non-empty Circuit of IIG
for v being Vertex of IIG holds
( depth (v,A) = 0 iff ( v in InputVertices IIG or v in SortsWithConstants IIG ) )
let A be non-empty Circuit of IIG; for v being Vertex of IIG holds
( depth (v,A) = 0 iff ( v in InputVertices IIG or v in SortsWithConstants IIG ) )
let v be Vertex of IIG; ( depth (v,A) = 0 iff ( v in InputVertices IIG or v in SortsWithConstants IIG ) )
consider s being non empty finite Subset of NAT such that
A1:
s = { (depth t) where t is Element of the Sorts of (FreeEnv A) . v : verum }
and
A2:
depth (v,A) = max s
by Def6;
reconsider Y = s as non empty finite real-membered set ;
A3:
max Y in { (depth t) where t is Element of the Sorts of (FreeEnv A) . v : verum }
by A1, XXREAL_2:def 8;
consider ss being non empty finite Subset of NAT such that
A4:
ss = { (card tt) where tt is Element of the Sorts of (FreeEnv A) . v : verum }
and
A5:
size (v,A) = max ss
by Def4;
reconsider YY = ss as non empty finite real-membered set ;
consider t being Element of the Sorts of (FreeEnv A) . v such that
A6:
depth t = max Y
by A3;
reconsider t99 = t as Function ;
consider t2 being Element of the Sorts of (FreeMSA the Sorts of A) . v such that
A7:
t = t2
and
A8:
depth t = depth t2
by Def5;
consider dt being finite DecoratedTree, t9 being finite Tree such that
A9:
( dt = t2 & t9 = dom dt )
and
A10:
depth t2 = height t9
by MSAFREE2:def 14;
consider p being FinSequence of NAT such that
A11:
p in t9
and
A12:
len p = height t9
by TREES_1:def 12;
consider y99 being object such that
A13:
[p,y99] in t99
by A7, A9, A11, XTUPLE_0:def 12;
thus
( not depth (v,A) = 0 or v in InputVertices IIG or v in SortsWithConstants IIG )
( ( v in InputVertices IIG or v in SortsWithConstants IIG ) implies depth (v,A) = 0 )proof
assume A14:
depth (
v,
A)
= 0
;
( v in InputVertices IIG or v in SortsWithConstants IIG )
A15:
for
kk being
ExtReal st
kk in YY holds
kk <= 1
proof
let kk be
ExtReal;
( kk in YY implies kk <= 1 )
assume
kk in YY
;
kk <= 1
then consider tt being
Element of the
Sorts of
(FreeEnv A) . v such that A16:
card tt = kk
by A4;
consider tiv being
Element of the
Sorts of
(FreeMSA the Sorts of A) . v such that A17:
(
tt = tiv &
depth tt = depth tiv )
by Def5;
depth tt in Y
by A1;
then A18:
depth tt = 0
by A2, A14, XXREAL_2:def 8;
A19:
ex
dt9 being
finite DecoratedTree ex
t999 being
finite Tree st
(
dt9 = tiv &
t999 = dom dt9 &
depth tiv = height t999 )
by MSAFREE2:def 14;
then
rng tt = {(tt . {})}
by A18, A17, FUNCT_1:4, TREES_1:29, TREES_1:43;
then
tt = {[{},(tt . {})]}
by A18, A17, A19, RELAT_1:189, TREES_1:29, TREES_1:43;
hence
kk <= 1
by A16, CARD_1:30;
verum
end;
rng t99 = {(t . {})}
by A2, A6, A7, A8, A9, A10, A14, FUNCT_1:4, TREES_1:29, TREES_1:43;
then
t99 = {[{},(t . {})]}
by A2, A6, A7, A8, A9, A10, A14, RELAT_1:189, TREES_1:29, TREES_1:43;
then
card t = 1
by CARD_1:30;
then
1
in YY
by A4;
then
size (
v,
A)
= 1
by A5, A15, XXREAL_2:def 8;
then
v in (InputVertices IIG) \/ (SortsWithConstants IIG)
by Th10;
hence
(
v in InputVertices IIG or
v in SortsWithConstants IIG )
by XBOOLE_0:def 3;
verum
end;
reconsider ct = card t as Real ;
{} in dom t
by TREES_1:22;
then consider y being object such that
A20:
[{},y] in t99
by XTUPLE_0:def 12;
A21:
card t in ss
by A4;
assume
( v in InputVertices IIG or v in SortsWithConstants IIG )
; depth (v,A) = 0
then
v in (InputVertices IIG) \/ (SortsWithConstants IIG)
by XBOOLE_0:def 3;
then
size (v,A) = 1
by Th10;
then
ct <= 1
by A5, A21, XXREAL_2:def 8;
then
( card t <= 0 or card t = 0 + 1 )
by NAT_1:8;
then consider x being object such that
A22:
t = {x}
by CARD_2:42;
x = [{},y]
by A22, A20, TARSKI:def 1;
then
[p,y99] = [{},y]
by A22, A13, TARSKI:def 1;
then
p = {}
by XTUPLE_0:1;
hence
depth (v,A) = 0
by A2, A6, A8, A10, A12; verum