let c, x, y be set ; :: thesis:
let f be Function of (2 -tuples_on BOOLEAN ),BOOLEAN ; :: thesis:
let s be State of (2GatesCircuit x,y,c,f); :: thesis:
set S = 2GatesCircStr x,y,c,f;
A1: rng <*x,y*> = {x,y} by FINSEQ_2:147;
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:
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:147;
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:49;
xyf in rng <*[<*x,y*>,f],c*> by A6, TARSKI:def 2;
then xyf in InputVertices (1GateCircStr <*[<*x,y*>,f],c*>,f) by CIRCCOMB:49;
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:4;
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:4;
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:49, CIRCUIT1:4;
A15: Following s,(1 + 1) = Following (Following s) by Th15;
hence (Following s,2) . (2GatesCircOutput x,y,c,f) = (Following fs2) . v2 by CIRCCOMB:72
.= f . <*(fs2 . xyf9),(fs2 . c9)*> by Th48
.= f . <*((Following s) . xyf),(fs2 . c)*> by A9, FUNCT_1:70
.= f . <*((Following s) . xyf),((Following s) . c9)*> by A9, FUNCT_1:70
.= f . <*((Following s) . xyf),(s . cc)*> by A10, CIRCUIT2:def 5
.= f . <*((Following s1) . xyf),(s . cc)*> by A13, CIRCCOMB:72
.= f . <*(f . <*(s1 . x),(s1 . y)*>),(s . cc)*> by Th48
.= f . <*(f . <*(s . x),(s1 . y)*>),(s . cc)*> by A2, A14, A1, FUNCT_1:70
.= f . <*(f . <*(s . x),(s . y)*>),(s . c)*> by A8, A14, A1, FUNCT_1:70 ;
:: thesis:
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:72
.= f . <*(fs1 . vx),(fs1 . vy)*> by Th48
.= f . <*(s . x),(fs1 . vy)*> by A5, A12, FUNCT_1:70
.= f . <*(s . x),(s . y)*> by A17, A12, FUNCT_1:70 ; :: thesis:
(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: