let x, y, c be object ; :: thesis: for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN

for s being State of (2GatesCircuit (x,y,c,f)) st c <> [<*x,y*>,f] holds

Following (s,2) is stable

let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN; :: thesis: for s being State of (2GatesCircuit (x,y,c,f)) st c <> [<*x,y*>,f] holds

Following (s,2) is stable

let s be State of (2GatesCircuit (x,y,c,f)); :: thesis: ( c <> [<*x,y*>,f] implies Following (s,2) is stable )

set S = 2GatesCircStr (x,y,c,f);

assume A1: c <> [<*x,y*>,f] ; :: thesis: Following (s,2) is stable

for s being State of (2GatesCircuit (x,y,c,f)) st c <> [<*x,y*>,f] holds

Following (s,2) is stable

let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN; :: thesis: for s being State of (2GatesCircuit (x,y,c,f)) st c <> [<*x,y*>,f] holds

Following (s,2) is stable

let s be State of (2GatesCircuit (x,y,c,f)); :: thesis: ( c <> [<*x,y*>,f] implies Following (s,2) is stable )

set S = 2GatesCircStr (x,y,c,f);

assume A1: c <> [<*x,y*>,f] ; :: thesis: Following (s,2) is stable

now :: thesis: ( dom (Following (Following (s,2))) = the carrier of (2GatesCircStr (x,y,c,f)) & dom (Following (s,2)) = the carrier of (2GatesCircStr (x,y,c,f)) & ( for a being object st a in the carrier of (2GatesCircStr (x,y,c,f)) holds

(Following (Following (s,2))) . a = (Following (s,2)) . a ) )

hence
Following (s,2) = Following (Following (s,2))
by FUNCT_1:2; :: according to CIRCUIT2:def 6 :: thesis: verum(Following (Following (s,2))) . a = (Following (s,2)) . a ) )

thus
( dom (Following (Following (s,2))) = the carrier of (2GatesCircStr (x,y,c,f)) & dom (Following (s,2)) = the carrier of (2GatesCircStr (x,y,c,f)) )
by CIRCUIT1:3; :: thesis: for a being object st a in the carrier of (2GatesCircStr (x,y,c,f)) holds

(Following (Following (s,2))) . b_{2} = (Following (s,2)) . b_{2}

let a be object ; :: thesis: ( a in the carrier of (2GatesCircStr (x,y,c,f)) implies (Following (Following (s,2))) . b_{1} = (Following (s,2)) . b_{1} )

A2: (InputVertices (2GatesCircStr (x,y,c,f))) \/ (InnerVertices (2GatesCircStr (x,y,c,f))) = the carrier of (2GatesCircStr (x,y,c,f)) by XBOOLE_1:45;

assume a in the carrier of (2GatesCircStr (x,y,c,f)) ; :: thesis: (Following (Following (s,2))) . b_{1} = (Following (s,2)) . b_{1}

then reconsider v = a as Vertex of (2GatesCircStr (x,y,c,f)) ;

A3: InnerVertices (2GatesCircStr (x,y,c,f)) = {[<*x,y*>,f],(2GatesCircOutput (x,y,c,f))} by Th56;

A4: (Following (s,2)) . c = s . c by A1, Th62;

A5: ( (Following (s,2)) . x = s . x & (Following (s,2)) . y = s . y ) by A1, Th62;

A6: ( (Following (s,2)) . [<*x,y*>,f] = f . <*(s . x),(s . y)*> & (Following (s,2)) . (2GatesCircOutput (x,y,c,f)) = f . <*(f . <*(s . x),(s . y)*>),(s . c)*> ) by A1, Th62;

A7: InputVertices (2GatesCircStr (x,y,c,f)) = {x,y,c} by A1, Th57;

end;(Following (Following (s,2))) . b

let a be object ; :: thesis: ( a in the carrier of (2GatesCircStr (x,y,c,f)) implies (Following (Following (s,2))) . b

A2: (InputVertices (2GatesCircStr (x,y,c,f))) \/ (InnerVertices (2GatesCircStr (x,y,c,f))) = the carrier of (2GatesCircStr (x,y,c,f)) by XBOOLE_1:45;

assume a in the carrier of (2GatesCircStr (x,y,c,f)) ; :: thesis: (Following (Following (s,2))) . b

then reconsider v = a as Vertex of (2GatesCircStr (x,y,c,f)) ;

A3: InnerVertices (2GatesCircStr (x,y,c,f)) = {[<*x,y*>,f],(2GatesCircOutput (x,y,c,f))} by Th56;

A4: (Following (s,2)) . c = s . c by A1, Th62;

A5: ( (Following (s,2)) . x = s . x & (Following (s,2)) . y = s . y ) by A1, Th62;

A6: ( (Following (s,2)) . [<*x,y*>,f] = f . <*(s . x),(s . y)*> & (Following (s,2)) . (2GatesCircOutput (x,y,c,f)) = f . <*(f . <*(s . x),(s . y)*>),(s . c)*> ) by A1, Th62;

A7: InputVertices (2GatesCircStr (x,y,c,f)) = {x,y,c} by A1, Th57;

per cases
( v in InputVertices (2GatesCircStr (x,y,c,f)) or v in InnerVertices (2GatesCircStr (x,y,c,f)) )
by A2, XBOOLE_0:def 3;

end;

suppose
v in InputVertices (2GatesCircStr (x,y,c,f))
; :: thesis: (Following (Following (s,2))) . b_{1} = (Following (s,2)) . b_{1}

then
( v = x or v = y or v = c )
by A7, ENUMSET1:def 1;

hence (Following (Following (s,2))) . a = (Following (s,2)) . a by A1, Lm1; :: thesis: verum

end;hence (Following (Following (s,2))) . a = (Following (s,2)) . a by A1, Lm1; :: thesis: verum

suppose
v in InnerVertices (2GatesCircStr (x,y,c,f))
; :: thesis: (Following (Following (s,2))) . b_{1} = (Following (s,2)) . b_{1}

then
( v = [<*x,y*>,f] or v = 2GatesCircOutput (x,y,c,f) )
by A3, TARSKI:def 2;

hence (Following (Following (s,2))) . a = (Following (s,2)) . a by A1, A6, A5, A4, Lm1; :: thesis: verum

end;hence (Following (Following (s,2))) . a = (Following (s,2)) . a by A1, A6, A5, A4, Lm1; :: thesis: verum