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 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 ) :: 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 ExtReal st kk in YY holds
kk <= 1

proof

let kk be ExtReal; :: 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: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; :: thesis: 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; :: thesis: 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 ) ; :: thesis: 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; :: thesis: verum