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)) . (2GatesCircOutput (x,y,c,f)) = f . <*(f . <*(s . x),(s . y)*>),(s . c)*> & (Following (s,2)) . [<*x,y*>,f] = f . <*(s . x),(s . y)*> & (Following (s,2)) . x = s . x & (Following (s,2)) . y = s . y & (Following (s,2)) . c = s . c )

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)) . (2GatesCircOutput (x,y,c,f)) = f . <*(f . <*(s . x),(s . y)*>),(s . c)*> & (Following (s,2)) . [<*x,y*>,f] = f . <*(s . x),(s . y)*> & (Following (s,2)) . x = s . x & (Following (s,2)) . y = s . y & (Following (s,2)) . c = s . c )

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

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

A1: rng <*x,y*> = {x,y} by FINSEQ_2:127;

reconsider xx = x, yy = y, cc = c as Vertex of (2GatesCircStr (x,y,c,f)) by Th60;

set p = <*[<*x,y*>,f],c*>;

set xyf = [<*x,y*>,f];

set S1 = 1GateCircStr (<*x,y*>,f);

set A1 = 1GateCircuit (x,y,f);

set S2 = 1GateCircStr (<*[<*x,y*>,f],c*>,f);

set A2 = 1GateCircuit ([<*x,y*>,f],c,f);

A2: x in {x,y} by TARSKI:def 2;

assume c <> [<*x,y*>,f] ; :: thesis: ( (Following (s,2)) . (2GatesCircOutput (x,y,c,f)) = f . <*(f . <*(s . x),(s . y)*>),(s . c)*> & (Following (s,2)) . [<*x,y*>,f] = f . <*(s . x),(s . y)*> & (Following (s,2)) . x = s . x & (Following (s,2)) . y = s . y & (Following (s,2)) . c = s . c )

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

then A4: x in InputVertices (2GatesCircStr (x,y,c,f)) by ENUMSET1:def 1;

then A5: (Following s) . xx = s . x by CIRCUIT2:def 5;

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

then reconsider xyf = [<*x,y*>,f] as Element of InnerVertices (2GatesCircStr (x,y,c,f)) by TARSKI:def 2;

A6: rng <*[<*x,y*>,f],c*> = {xyf,c} by FINSEQ_2:127;

then c in rng <*[<*x,y*>,f],c*> by TARSKI:def 2;

then A7: c in InputVertices (1GateCircStr (<*[<*x,y*>,f],c*>,f)) by CIRCCOMB:42;

xyf in rng <*[<*x,y*>,f],c*> by A6, TARSKI:def 2;

then xyf in InputVertices (1GateCircStr (<*[<*x,y*>,f],c*>,f)) by CIRCCOMB:42;

then reconsider xyf9 = xyf, c9 = c as Vertex of (1GateCircStr (<*[<*x,y*>,f],c*>,f)) by A7;

reconsider vx = x, vy = y as Vertex of (1GateCircStr (<*x,y*>,f)) by Th43;

set fs = Following s;

reconsider fs1 = (Following s) | the carrier of (1GateCircStr (<*x,y*>,f)) as State of (1GateCircuit (x,y,f)) by Th26;

A8: y in {x,y} by TARSKI:def 2;

reconsider fs2 = (Following s) | the carrier of (1GateCircStr (<*[<*x,y*>,f],c*>,f)) as State of (1GateCircuit ([<*x,y*>,f],c,f)) by Th26;

reconsider s1 = s | the carrier of (1GateCircStr (<*x,y*>,f)) as State of (1GateCircuit (x,y,f)) by Th26;

A9: dom fs2 = the carrier of (1GateCircStr (<*[<*x,y*>,f],c*>,f)) by CIRCUIT1:3;

A10: c in InputVertices (2GatesCircStr (x,y,c,f)) by A3, ENUMSET1:def 1;

then (Following s) . cc = s . c by CIRCUIT2:def 5;

then A11: (Following (Following s)) . cc = s . c by A10, CIRCUIT2:def 5;

reconsider xyf1 = xyf as Element of InnerVertices (1GateCircStr (<*x,y*>,f)) by Th47;

A12: dom fs1 = the carrier of (1GateCircStr (<*x,y*>,f)) by CIRCUIT1:3;

reconsider v2 = [<*[<*x,y*>,f],c*>,f] as Element of InnerVertices (1GateCircStr (<*[<*x,y*>,f],c*>,f)) by Th47;

A13: xyf in InnerVertices (1GateCircStr (<*x,y*>,f)) by Th47;

A14: ( dom s1 = the carrier of (1GateCircStr (<*x,y*>,f)) & InputVertices (1GateCircStr (<*x,y*>,f)) = rng <*x,y*> ) by CIRCCOMB:42, CIRCUIT1:3;

A15: Following (s,(1 + 1)) = Following (Following s) by Th15;

hence (Following (s,2)) . (2GatesCircOutput (x,y,c,f)) = (Following fs2) . v2 by CIRCCOMB:64

.= f . <*(fs2 . xyf9),(fs2 . c9)*> by Th48

.= f . <*((Following s) . xyf),(fs2 . c)*> by A9, FUNCT_1:47

.= f . <*((Following s) . xyf),((Following s) . c9)*> by A9, FUNCT_1:47

.= f . <*((Following s) . xyf),(s . cc)*> by A10, CIRCUIT2:def 5

.= f . <*((Following s1) . xyf),(s . cc)*> by A13, CIRCCOMB:64

.= f . <*(f . <*(s1 . x),(s1 . y)*>),(s . cc)*> by Th48

.= f . <*(f . <*(s . x),(s1 . y)*>),(s . cc)*> by A2, A14, A1, FUNCT_1:47

.= f . <*(f . <*(s . x),(s . y)*>),(s . c)*> by A8, A14, A1, FUNCT_1:47 ;

:: thesis: ( (Following (s,2)) . [<*x,y*>,f] = f . <*(s . x),(s . y)*> & (Following (s,2)) . x = s . x & (Following (s,2)) . y = s . y & (Following (s,2)) . c = s . c )

A16: y in InputVertices (2GatesCircStr (x,y,c,f)) by A3, ENUMSET1:def 1;

then A17: (Following s) . yy = s . y by CIRCUIT2:def 5;

then A18: (Following (Following s)) . yy = s . y by A16, CIRCUIT2:def 5;

thus (Following (s,2)) . [<*x,y*>,f] = (Following fs1) . xyf1 by A15, CIRCCOMB:64

.= f . <*(fs1 . vx),(fs1 . vy)*> by Th48

.= f . <*(s . x),(fs1 . vy)*> by A5, A12, FUNCT_1:47

.= f . <*(s . x),(s . y)*> by A17, A12, FUNCT_1:47 ; :: thesis: ( (Following (s,2)) . x = s . x & (Following (s,2)) . y = s . y & (Following (s,2)) . c = s . c )

(Following (Following s)) . xx = s . x by A4, A5, CIRCUIT2:def 5;

hence ( (Following (s,2)) . x = s . x & (Following (s,2)) . y = s . y & (Following (s,2)) . c = s . c ) by A18, A11, Th15; :: thesis: verum

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

( (Following (s,2)) . (2GatesCircOutput (x,y,c,f)) = f . <*(f . <*(s . x),(s . y)*>),(s . c)*> & (Following (s,2)) . [<*x,y*>,f] = f . <*(s . x),(s . y)*> & (Following (s,2)) . x = s . x & (Following (s,2)) . y = s . y & (Following (s,2)) . c = s . c )

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)) . (2GatesCircOutput (x,y,c,f)) = f . <*(f . <*(s . x),(s . y)*>),(s . c)*> & (Following (s,2)) . [<*x,y*>,f] = f . <*(s . x),(s . y)*> & (Following (s,2)) . x = s . x & (Following (s,2)) . y = s . y & (Following (s,2)) . c = s . c )

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

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

A1: rng <*x,y*> = {x,y} by FINSEQ_2:127;

reconsider xx = x, yy = y, cc = c as Vertex of (2GatesCircStr (x,y,c,f)) by Th60;

set p = <*[<*x,y*>,f],c*>;

set xyf = [<*x,y*>,f];

set S1 = 1GateCircStr (<*x,y*>,f);

set A1 = 1GateCircuit (x,y,f);

set S2 = 1GateCircStr (<*[<*x,y*>,f],c*>,f);

set A2 = 1GateCircuit ([<*x,y*>,f],c,f);

A2: x in {x,y} by TARSKI:def 2;

assume c <> [<*x,y*>,f] ; :: thesis: ( (Following (s,2)) . (2GatesCircOutput (x,y,c,f)) = f . <*(f . <*(s . x),(s . y)*>),(s . c)*> & (Following (s,2)) . [<*x,y*>,f] = f . <*(s . x),(s . y)*> & (Following (s,2)) . x = s . x & (Following (s,2)) . y = s . y & (Following (s,2)) . c = s . c )

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

then A4: x in InputVertices (2GatesCircStr (x,y,c,f)) by ENUMSET1:def 1;

then A5: (Following s) . xx = s . x by CIRCUIT2:def 5;

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

then reconsider xyf = [<*x,y*>,f] as Element of InnerVertices (2GatesCircStr (x,y,c,f)) by TARSKI:def 2;

A6: rng <*[<*x,y*>,f],c*> = {xyf,c} by FINSEQ_2:127;

then c in rng <*[<*x,y*>,f],c*> by TARSKI:def 2;

then A7: c in InputVertices (1GateCircStr (<*[<*x,y*>,f],c*>,f)) by CIRCCOMB:42;

xyf in rng <*[<*x,y*>,f],c*> by A6, TARSKI:def 2;

then xyf in InputVertices (1GateCircStr (<*[<*x,y*>,f],c*>,f)) by CIRCCOMB:42;

then reconsider xyf9 = xyf, c9 = c as Vertex of (1GateCircStr (<*[<*x,y*>,f],c*>,f)) by A7;

reconsider vx = x, vy = y as Vertex of (1GateCircStr (<*x,y*>,f)) by Th43;

set fs = Following s;

reconsider fs1 = (Following s) | the carrier of (1GateCircStr (<*x,y*>,f)) as State of (1GateCircuit (x,y,f)) by Th26;

A8: y in {x,y} by TARSKI:def 2;

reconsider fs2 = (Following s) | the carrier of (1GateCircStr (<*[<*x,y*>,f],c*>,f)) as State of (1GateCircuit ([<*x,y*>,f],c,f)) by Th26;

reconsider s1 = s | the carrier of (1GateCircStr (<*x,y*>,f)) as State of (1GateCircuit (x,y,f)) by Th26;

A9: dom fs2 = the carrier of (1GateCircStr (<*[<*x,y*>,f],c*>,f)) by CIRCUIT1:3;

A10: c in InputVertices (2GatesCircStr (x,y,c,f)) by A3, ENUMSET1:def 1;

then (Following s) . cc = s . c by CIRCUIT2:def 5;

then A11: (Following (Following s)) . cc = s . c by A10, CIRCUIT2:def 5;

reconsider xyf1 = xyf as Element of InnerVertices (1GateCircStr (<*x,y*>,f)) by Th47;

A12: dom fs1 = the carrier of (1GateCircStr (<*x,y*>,f)) by CIRCUIT1:3;

reconsider v2 = [<*[<*x,y*>,f],c*>,f] as Element of InnerVertices (1GateCircStr (<*[<*x,y*>,f],c*>,f)) by Th47;

A13: xyf in InnerVertices (1GateCircStr (<*x,y*>,f)) by Th47;

A14: ( dom s1 = the carrier of (1GateCircStr (<*x,y*>,f)) & InputVertices (1GateCircStr (<*x,y*>,f)) = rng <*x,y*> ) by CIRCCOMB:42, CIRCUIT1:3;

A15: Following (s,(1 + 1)) = Following (Following s) by Th15;

hence (Following (s,2)) . (2GatesCircOutput (x,y,c,f)) = (Following fs2) . v2 by CIRCCOMB:64

.= f . <*(fs2 . xyf9),(fs2 . c9)*> by Th48

.= f . <*((Following s) . xyf),(fs2 . c)*> by A9, FUNCT_1:47

.= f . <*((Following s) . xyf),((Following s) . c9)*> by A9, FUNCT_1:47

.= f . <*((Following s) . xyf),(s . cc)*> by A10, CIRCUIT2:def 5

.= f . <*((Following s1) . xyf),(s . cc)*> by A13, CIRCCOMB:64

.= f . <*(f . <*(s1 . x),(s1 . y)*>),(s . cc)*> by Th48

.= f . <*(f . <*(s . x),(s1 . y)*>),(s . cc)*> by A2, A14, A1, FUNCT_1:47

.= f . <*(f . <*(s . x),(s . y)*>),(s . c)*> by A8, A14, A1, FUNCT_1:47 ;

:: thesis: ( (Following (s,2)) . [<*x,y*>,f] = f . <*(s . x),(s . y)*> & (Following (s,2)) . x = s . x & (Following (s,2)) . y = s . y & (Following (s,2)) . c = s . c )

A16: y in InputVertices (2GatesCircStr (x,y,c,f)) by A3, ENUMSET1:def 1;

then A17: (Following s) . yy = s . y by CIRCUIT2:def 5;

then A18: (Following (Following s)) . yy = s . y by A16, CIRCUIT2:def 5;

thus (Following (s,2)) . [<*x,y*>,f] = (Following fs1) . xyf1 by A15, CIRCCOMB:64

.= f . <*(fs1 . vx),(fs1 . vy)*> by Th48

.= f . <*(s . x),(fs1 . vy)*> by A5, A12, FUNCT_1:47

.= f . <*(s . x),(s . y)*> by A17, A12, FUNCT_1:47 ; :: thesis: ( (Following (s,2)) . x = s . x & (Following (s,2)) . y = s . y & (Following (s,2)) . c = s . c )

(Following (Following s)) . xx = s . x by A4, A5, CIRCUIT2:def 5;

hence ( (Following (s,2)) . x = s . x & (Following (s,2)) . y = s . y & (Following (s,2)) . c = s . c ) by A18, A11, Th15; :: thesis: verum