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 ;
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 15;
consider y99 being set such that
A13: [p,y99] in t99 by A7, A9, A11, RELAT_1:def 4;
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 A14: depth v,A = 0 ; :: thesis: ( v in InputVertices IIG or v in SortsWithConstants IIG )
A15: 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
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:14, TREES_1:56, TREES_1:80;
then tt = {[{} ,(tt . {} )]} by A18, A17, A19, PRE_CIRC:2, TREES_1:56, TREES_1:80;
hence kk <= 1 by A16, CARD_1:50; :: thesis: verum

end;

rng t99 = {(t . {} )} by A2, A6, A7, A8, A9, A10, A14, FUNCT_1:14, TREES_1:56, TREES_1:80;
then t99 = {[{} ,(t . {} )]} by A2, A6, A7, A8, A9, A10, A14, PRE_CIRC:2, TREES_1:56, TREES_1:80;
then card t = 1 by CARD_1:50;
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 Th11;
hence ( v in InputVertices IIG or v in SortsWithConstants IIG ) by XBOOLE_0:def 3; :: thesis: verum

end;

card t in NAT ;
then reconsider ct = card t as Real ;
{} in dom t by TREES_1:47;
then consider y being set such that
A20: [{} ,y] in t99 by RELAT_1:def 4;
A21: card t in ss by A4;
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 size v,A = 1 by Th11;
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 set such that
A22: t = {x} by CARD_2:60;
x = [{} ,y] by A22, A20, TARSKI:def 1;
then [p,y99] = [{} ,y] by A22, A13, TARSKI:def 1;
then p = {} by ZFMISC_1:33;
hence depth v,A = 0 by A2, A6, A8, A10, A12; :: thesis: verum