let IIG be non empty finite non void Circuit-like monotonic ManySortedSign ; :: thesis: for SCS being non-empty Circuit of IIG

for InpFs being InputFuncs of SCS st commute InpFs is constant & not InputVertices IIG is empty holds

for s being State of SCS

for n being Element of NAT st n = depth SCS holds

(Computation (s,InpFs)) . n is stable

let SCS be non-empty Circuit of IIG; :: thesis: for InpFs being InputFuncs of SCS st commute InpFs is constant & not InputVertices IIG is empty holds

for s being State of SCS

for n being Element of NAT st n = depth SCS holds

(Computation (s,InpFs)) . n is stable

let InpFs be InputFuncs of SCS; :: thesis: ( commute InpFs is constant & not InputVertices IIG is empty implies for s being State of SCS

for n being Element of NAT st n = depth SCS holds

(Computation (s,InpFs)) . n is stable )

assume that

A1: commute InpFs is constant and

A2: not InputVertices IIG is empty ; :: thesis: for s being State of SCS

for n being Element of NAT st n = depth SCS holds

(Computation (s,InpFs)) . n is stable

A3: dom (commute InpFs) = NAT by A2, PRE_CIRC:5;

A4: IIG is with_input_V by A2;

then reconsider iv = (commute InpFs) . 0 as InputValues of SCS by CIRCUIT1:2;

let s be State of SCS; :: thesis: for n being Element of NAT st n = depth SCS holds

(Computation (s,InpFs)) . n is stable

let n be Element of NAT ; :: thesis: ( n = depth SCS implies (Computation (s,InpFs)) . n is stable )

assume A5: n = depth SCS ; :: thesis: (Computation (s,InpFs)) . n is stable

reconsider Cn = (Computation (s,InpFs)) . n as State of SCS ;

A6: iv c= Cn by A1, A2, Th14;

A7: (n + 1) -th_InputValues InpFs = (commute InpFs) . (n + 1) by A4, CIRCUIT1:def 2

.= (commute InpFs) . 0 by A1, A3, FUNCT_1:def 10 ;

reconsider Cn1 = (Computation (s,InpFs)) . (n + 1) as State of SCS ;

.= Following (Cn,((n + 1) -th_InputValues InpFs)) by Def9

.= Following ((Computation (s,InpFs)) . n) by A7, A6, FUNCT_4:98 ;

:: according to CIRCUIT2:def 6 :: thesis: verum

for InpFs being InputFuncs of SCS st commute InpFs is constant & not InputVertices IIG is empty holds

for s being State of SCS

for n being Element of NAT st n = depth SCS holds

(Computation (s,InpFs)) . n is stable

let SCS be non-empty Circuit of IIG; :: thesis: for InpFs being InputFuncs of SCS st commute InpFs is constant & not InputVertices IIG is empty holds

for s being State of SCS

for n being Element of NAT st n = depth SCS holds

(Computation (s,InpFs)) . n is stable

let InpFs be InputFuncs of SCS; :: thesis: ( commute InpFs is constant & not InputVertices IIG is empty implies for s being State of SCS

for n being Element of NAT st n = depth SCS holds

(Computation (s,InpFs)) . n is stable )

assume that

A1: commute InpFs is constant and

A2: not InputVertices IIG is empty ; :: thesis: for s being State of SCS

for n being Element of NAT st n = depth SCS holds

(Computation (s,InpFs)) . n is stable

A3: dom (commute InpFs) = NAT by A2, PRE_CIRC:5;

A4: IIG is with_input_V by A2;

then reconsider iv = (commute InpFs) . 0 as InputValues of SCS by CIRCUIT1:2;

let s be State of SCS; :: thesis: for n being Element of NAT st n = depth SCS holds

(Computation (s,InpFs)) . n is stable

let n be Element of NAT ; :: thesis: ( n = depth SCS implies (Computation (s,InpFs)) . n is stable )

assume A5: n = depth SCS ; :: thesis: (Computation (s,InpFs)) . n is stable

reconsider Cn = (Computation (s,InpFs)) . n as State of SCS ;

A6: iv c= Cn by A1, A2, Th14;

A7: (n + 1) -th_InputValues InpFs = (commute InpFs) . (n + 1) by A4, CIRCUIT1:def 2

.= (commute InpFs) . 0 by A1, A3, FUNCT_1:def 10 ;

reconsider Cn1 = (Computation (s,InpFs)) . (n + 1) as State of SCS ;

now :: thesis: ( the carrier of IIG = dom Cn & the carrier of IIG = dom Cn1 & ( for x being object st x in the carrier of IIG holds

Cn . x = Cn1 . x ) )

hence (Computation (s,InpFs)) . n =
(Computation (s,InpFs)) . (n + 1)
Cn . x = Cn1 . x ) )

thus
the carrier of IIG = dom Cn
by CIRCUIT1:3; :: thesis: ( the carrier of IIG = dom Cn1 & ( for x being object st x in the carrier of IIG holds

Cn . x = Cn1 . x ) )

thus the carrier of IIG = dom Cn1 by CIRCUIT1:3; :: thesis: for x being object st x in the carrier of IIG holds

Cn . x = Cn1 . x

let x be object ; :: thesis: ( x in the carrier of IIG implies Cn . x = Cn1 . x )

assume x in the carrier of IIG ; :: thesis: Cn . x = Cn1 . x

then reconsider x9 = x as Vertex of IIG ;

A8: depth (x9,SCS) <= n by A5, CIRCUIT1:17;

then Cn . x9 = IGValue (x9,iv) by A1, A2, Th16;

hence Cn . x = Cn1 . x by A1, A2, A8, Th16, NAT_1:12; :: thesis: verum

end;Cn . x = Cn1 . x ) )

thus the carrier of IIG = dom Cn1 by CIRCUIT1:3; :: thesis: for x being object st x in the carrier of IIG holds

Cn . x = Cn1 . x

let x be object ; :: thesis: ( x in the carrier of IIG implies Cn . x = Cn1 . x )

assume x in the carrier of IIG ; :: thesis: Cn . x = Cn1 . x

then reconsider x9 = x as Vertex of IIG ;

A8: depth (x9,SCS) <= n by A5, CIRCUIT1:17;

then Cn . x9 = IGValue (x9,iv) by A1, A2, Th16;

hence Cn . x = Cn1 . x by A1, A2, A8, Th16, NAT_1:12; :: thesis: verum

.= Following (Cn,((n + 1) -th_InputValues InpFs)) by Def9

.= Following ((Computation (s,InpFs)) . n) by A7, A6, FUNCT_4:98 ;

:: according to CIRCUIT2:def 6 :: thesis: verum