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) . (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 ; :: thesis: 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); :: thesis: ( 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 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;
set S = 2GatesCircStr x,y,c,f;
assume c <> [<*x,y*>,f] ; :: thesis: ( (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 A1: InputVertices (2GatesCircStr x,y,c,f) = {x,y,c} by Th57;
A2: InnerVertices (2GatesCircStr x,y,c,f) = {[<*x,y*>,f],(2GatesCircOutput x,y,c,f)} by Th56;
A3: ( x in InputVertices (2GatesCircStr x,y,c,f) & y in InputVertices (2GatesCircStr x,y,c,f) & c in InputVertices (2GatesCircStr x,y,c,f) ) by A1, ENUMSET1:def 1;
reconsider xyf = [<*x,y*>,f] as Element of InnerVertices (2GatesCircStr x,y,c,f) by A2, TARSKI:def 2;
rng <*[<*x,y*>,f],c*> = {xyf,c} by FINSEQ_2:147;
then ( xyf in rng <*[<*x,y*>,f],c*> & c in rng <*[<*x,y*>,f],c*> ) by TARSKI:def 2;
then A4: ( xyf in InputVertices (1GateCircStr <*[<*x,y*>,f],c*>,f) & c in InputVertices (1GateCircStr <*[<*x,y*>,f],c*>,f) ) by CIRCCOMB:49;
reconsider s1 = s | the carrier of (1GateCircStr <*x,y*>,f) as State of (1GateCircuit x,y,f) by Th26;
reconsider s2 = s | the carrier of (1GateCircStr <*[<*x,y*>,f],c*>,f) as State of (1GateCircuit [<*x,y*>,f],c,f) by Th26;
A5: dom s2 = the carrier of (1GateCircStr <*[<*x,y*>,f],c*>,f) by CIRCUIT1:4;
A6: dom s1 = the carrier of (1GateCircStr <*x,y*>,f) by CIRCUIT1:4;
reconsider vx = x, vy = y as Vertex of (1GateCircStr <*x,y*>,f) by Th43;
reconsider xyf1 = xyf as Element of InnerVertices (1GateCircStr <*x,y*>,f) by Th47;
reconsider xyf' = xyf, c' = c as Vertex of (1GateCircStr <*[<*x,y*>,f],c*>,f) by A4;
reconsider v2 = [<*[<*x,y*>,f],c*>,f] as Element of InnerVertices (1GateCircStr <*[<*x,y*>,f],c*>,f) by Th47;
thus (Following s) . (2GatesCircOutput x,y,c,f) = (Following s2) . v2 by CIRCCOMB:72
.= f . <*(s2 . xyf'),(s2 . c')*> by Th48
.= f . <*(s . [<*x,y*>,f]),(s2 . c')*> by A5, FUNCT_1:70
.= f . <*(s . [<*x,y*>,f]),(s . c)*> by A5, FUNCT_1:70 ; :: thesis: ( (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:72
.= f . <*(s1 . vx),(s1 . vy)*> by Th48
.= f . <*(s . x),(s1 . vy)*> by A6, FUNCT_1:70
.= f . <*(s . x),(s . y)*> by A6, FUNCT_1:70 ; :: thesis: ( (Following s) . x = s . x & (Following s) . y = s . y & (Following s) . c = s . c )
thus ( (Following s) . x = s . x & (Following s) . y = s . y & (Following s) . c = s . c ) by A3, CIRCUIT2:def 5; :: thesis: verum