let c, x, y be set ; :: 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 )
assume A1: c <> [<*x,y*>,f] ; :: thesis: Following s,2 is stable
set S = 2GatesCircStr x,y,c,f;

now

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:4; :: thesis: for a being set st a in the carrier of (2GatesCircStr x,y,c,f) holds
(Following (Following s,2)) . b₂ = (Following s,2) . b₂
let a be set ; :: thesis: ( a in the carrier of (2GatesCircStr x,y,c,f) implies (Following (Following s,2)) . b₁ = (Following s,2) . b₁ )
assume a in the carrier of (2GatesCircStr x,y,c,f) ; :: thesis: (Following (Following s,2)) . b₁ = (Following s,2) . b₁
then reconsider v = a as Vertex of (2GatesCircStr x,y,c,f) ;
A2: InputVertices (2GatesCircStr x,y,c,f) = {x,y,c} by A1, Th57;
A3: InnerVertices (2GatesCircStr x,y,c,f) = {[<*x,y*>,f],(2GatesCircOutput x,y,c,f)} by Th56;
A4: (InputVertices (2GatesCircStr x,y,c,f)) \/ (InnerVertices (2GatesCircStr x,y,c,f)) = the carrier of (2GatesCircStr x,y,c,f) by XBOOLE_1:45;
A5: ( (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)*> & (Following s,2) . x = s . x & (Following s,2) . y = s . y & (Following s,2) . c = s . c ) by A1, Th62;

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

suppose v in InputVertices (2GatesCircStr x,y,c,f) ; :: thesis: (Following (Following s,2)) . b₁ = (Following s,2) . b₁

then ( v = x or v = y or v = c ) by A2, ENUMSET1:def 1;
hence (Following (Following s,2)) . a = (Following s,2) . a by A1, Lm2; :: thesis: verum

end;

suppose v in InnerVertices (2GatesCircStr x,y,c,f) ; :: thesis: (Following (Following s,2)) . b₁ = (Following s,2) . b₁

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, A5, Lm2; :: thesis: verum

end;

end;

end;

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