let x, y, c be object ; 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) . (2GatesCircOutput (x,y,c,f)) = f . <*(s . [<*x,y*>,f]),(s . c)*> & (Following s) . [<*x,y*>,f] = f . <*(s . x),(s . y)*> & (Following s) . x = s . x & (Following s) . y = s . y & (Following s) . c = s . c )
let f be 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) . (2GatesCircOutput (x,y,c,f)) = f . <*(s . [<*x,y*>,f]),(s . c)*> & (Following s) . [<*x,y*>,f] = f . <*(s . x),(s . y)*> & (Following s) . x = s . x & (Following s) . y = s . y & (Following s) . c = s . c )
let s be State of (2GatesCircuit (x,y,c,f)); ( c <> [<*x,y*>,f] implies ( (Following s) . (2GatesCircOutput (x,y,c,f)) = f . <*(s . [<*x,y*>,f]),(s . c)*> & (Following s) . [<*x,y*>,f] = f . <*(s . x),(s . y)*> & (Following s) . x = s . x & (Following s) . y = s . y & (Following s) . c = s . c ) )
set S1 = 1GateCircStr (<*x,y*>,f);
set A1 = 1GateCircuit (x,y,f);
reconsider vx = x, vy = y as Vertex of (1GateCircStr (<*x,y*>,f)) by Th43;
reconsider s1 = s | the carrier of (1GateCircStr (<*x,y*>,f)) as State of (1GateCircuit (x,y,f)) by Th26;
set p = <*[<*x,y*>,f],c*>;
set xyf = [<*x,y*>,f];
set S2 = 1GateCircStr (<*[<*x,y*>,f],c*>,f);
set A2 = 1GateCircuit ([<*x,y*>,f],c,f);
set S = 2GatesCircStr (x,y,c,f);
A1:
dom s1 = 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;
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;
A2:
rng <*[<*x,y*>,f],c*> = {xyf,c}
by FINSEQ_2:127;
then
c in rng <*[<*x,y*>,f],c*>
by TARSKI:def 2;
then A3:
c in InputVertices (1GateCircStr (<*[<*x,y*>,f],c*>,f))
by CIRCCOMB:42;
xyf in rng <*[<*x,y*>,f],c*>
by A2, 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 A3;
reconsider xyf1 = xyf as Element of InnerVertices (1GateCircStr (<*x,y*>,f)) by Th47;
reconsider s2 = s | the carrier of (1GateCircStr (<*[<*x,y*>,f],c*>,f)) as State of (1GateCircuit ([<*x,y*>,f],c,f)) by Th26;
A4:
dom s2 = the carrier of (1GateCircStr (<*[<*x,y*>,f],c*>,f))
by CIRCUIT1:3;
assume
c <> [<*x,y*>,f]
; ( (Following s) . (2GatesCircOutput (x,y,c,f)) = f . <*(s . [<*x,y*>,f]),(s . c)*> & (Following s) . [<*x,y*>,f] = f . <*(s . x),(s . y)*> & (Following s) . x = s . x & (Following s) . y = s . y & (Following s) . c = s . c )
then A5:
InputVertices (2GatesCircStr (x,y,c,f)) = {x,y,c}
by Th57;
then A6:
c in InputVertices (2GatesCircStr (x,y,c,f))
by ENUMSET1:def 1;
thus (Following s) . (2GatesCircOutput (x,y,c,f)) =
(Following s2) . v2
by CIRCCOMB:64
.=
f . <*(s2 . xyf9),(s2 . c9)*>
by Th48
.=
f . <*(s . [<*x,y*>,f]),(s2 . c9)*>
by A4, FUNCT_1:47
.=
f . <*(s . [<*x,y*>,f]),(s . c)*>
by A4, FUNCT_1:47
; ( (Following s) . [<*x,y*>,f] = f . <*(s . x),(s . y)*> & (Following s) . x = s . x & (Following s) . y = s . y & (Following s) . c = s . c )
thus (Following s) . [<*x,y*>,f] =
(Following s1) . xyf1
by CIRCCOMB:64
.=
f . <*(s1 . vx),(s1 . vy)*>
by Th48
.=
f . <*(s . x),(s1 . vy)*>
by A1, FUNCT_1:47
.=
f . <*(s . x),(s . y)*>
by A1, FUNCT_1:47
; ( (Following s) . x = s . x & (Following s) . y = s . y & (Following s) . c = s . c )
( x in InputVertices (2GatesCircStr (x,y,c,f)) & y in InputVertices (2GatesCircStr (x,y,c,f)) )
by A5, ENUMSET1:def 1;
hence
( (Following s) . x = s . x & (Following s) . y = s . y & (Following s) . c = s . c )
by A6, CIRCUIT2:def 5; verum