let IIG be non empty non void Circuit-like monotonic ManySortedSign ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ;
max Y in { (depth t) where t is Element of the Sorts of (FreeEnv A) . v : verum }
by A1, XXREAL_2:def 8;
then consider t being Element of the Sorts of (FreeEnv A) . v such that
A3:
depth t = max Y
;
consider t2 being Element of the Sorts of (FreeMSA the Sorts of A) . v such that
A4:
t = t2
and
A5:
depth t = depth t2
by Def5;
consider dt being finite DecoratedTree, t' being finite Tree such that
A6:
dt = t2
and
A7:
t' = dom dt
and
A8:
depth t2 = height t'
by MSAFREE2:def 14;
consider p being FinSequence of NAT such that
A9:
p in t'
and
A10:
len p = height t'
by TREES_1:def 15;
consider ss being non empty finite Subset of NAT such that
A11:
ss = { (card tt) where tt is Element of the Sorts of (FreeEnv A) . v : verum }
and
A12:
size v,A = max ss
by Def4;
reconsider YY = ss as non empty finite real-membered set ;
reconsider t'' = t as Function ;
thus
( not depth v,A = 0 or v in InputVertices IIG or v in SortsWithConstants IIG )
:: thesis: ( ( v in InputVertices IIG or v in SortsWithConstants IIG ) implies depth v,A = 0 )proof
assume A13:
depth v,
A = 0
;
:: thesis: ( v in InputVertices IIG or v in SortsWithConstants IIG )
then
rng t'' = {(t . {} )}
by A2, A3, A4, A5, A6, A7, A8, FUNCT_1:14, TREES_1:56, TREES_1:80;
then
t'' = {[{} ,(t . {} )]}
by A2, A3, A4, A5, A6, A7, A8, A13, PRE_CIRC:2, TREES_1:56, TREES_1:80;
then
card t = 1
by CARD_1:50;
then A14:
1
in YY
by A11;
for
kk being
ext-real number st
kk in YY holds
kk <= 1
proof
let kk be
ext-real number ;
:: thesis: ( kk in YY implies kk <= 1 )
assume
kk in YY
;
:: thesis: kk <= 1
then consider tt being
Element of the
Sorts of
(FreeEnv A) . v such that A15:
card tt = kk
by A11;
depth tt in Y
by A1;
then
depth tt <= 0
by A2, A13, XXREAL_2:def 8;
then A16:
depth tt = 0
;
consider tiv being
Element of the
Sorts of
(FreeMSA the Sorts of A) . v such that A17:
tt = tiv
and A18:
depth tt = depth tiv
by Def5;
consider dt' being
finite DecoratedTree,
t''' being
finite Tree such that A19:
dt' = tiv
and A20:
t''' = dom dt'
and A21:
depth tiv = height t'''
by MSAFREE2:def 14;
rng tt = {(tt . {} )}
by A16, A17, A18, A19, A20, A21, FUNCT_1:14, TREES_1:56, TREES_1:80;
then
tt = {[{} ,(tt . {} )]}
by A16, A17, A18, A19, A20, A21, PRE_CIRC:2, TREES_1:56, TREES_1:80;
hence
kk <= 1
by A15, CARD_1:50;
:: thesis: verum
end;
then
size v,
A = 1
by A12, A14, XXREAL_2:def 8;
then
v in (InputVertices IIG) \/ (SortsWithConstants IIG)
by Th11;
hence
(
v in InputVertices IIG or
v in SortsWithConstants IIG )
by XBOOLE_0:def 3;
:: thesis: verum
end;
assume
( v in InputVertices IIG or v in SortsWithConstants IIG )
; :: thesis: depth v,A = 0
then
v in (InputVertices IIG) \/ (SortsWithConstants IIG)
by XBOOLE_0:def 3;
then A22:
size v,A = 1
by Th11;
A23:
card t in ss
by A11;
card t in NAT
;
then reconsider ct = card t as Real ;
ct <= 1
by A12, A22, A23, XXREAL_2:def 8;
then A24:
( card t <= 0 or card t = 0 + 1 )
by NAT_1:8;
consider x being set such that
A25:
t = {x}
by A24, CARD_2:60;
{} in dom t
by TREES_1:47;
then consider y being set such that
A26:
[{} ,y] in t''
by RELAT_1:def 4;
A27:
x = [{} ,y]
by A25, A26, TARSKI:def 1;
consider y'' being set such that
A28:
[p,y''] in t''
by A4, A6, A7, A9, RELAT_1:def 4;
[p,y''] = [{} ,y]
by A25, A27, A28, TARSKI:def 1;
then
p = {}
by ZFMISC_1:33;
hence
depth v,A = 0
by A2, A3, A5, A8, A10; :: thesis: verum