let x, y be object ; :: thesis: for X being non empty finite set
for f being Function of (2 -tuples_on X),X
for s being State of (1GateCircuit (<*x,y*>,f)) holds
( (Following s) . [<*x,y*>,f] = f . <*(s . x),(s . y)*> & (Following s) . x = s . x & (Following s) . y = s . y )
let X be non empty finite set ; :: thesis: for f being Function of (2 -tuples_on X),X
for s being State of (1GateCircuit (<*x,y*>,f)) holds
( (Following s) . [<*x,y*>,f] = f . <*(s . x),(s . y)*> & (Following s) . x = s . x & (Following s) . y = s . y )
let f be Function of (2 -tuples_on X),X; :: thesis: for s being State of (1GateCircuit (<*x,y*>,f)) holds
( (Following s) . [<*x,y*>,f] = f . <*(s . x),(s . y)*> & (Following s) . x = s . x & (Following s) . y = s . y )
let s be State of (1GateCircuit (<*x,y*>,f)); :: thesis: ( (Following s) . [<*x,y*>,f] = f . <*(s . x),(s . y)*> & (Following s) . x = s . x & (Following s) . y = s . y )
set p = <*x,y*>;
dom s = the carrier of (1GateCircStr (<*x,y*>,f)) by CIRCUIT1:3;
then A1: dom s = (rng <*x,y*>) \/ {[<*x,y*>,f]} by CIRCCOMB:def 6;
y in {x,y} by TARSKI:def 2;
then y in rng <*x,y*> by FINSEQ_2:127;
then A2: y in dom s by A1, XBOOLE_0:def 3;
x in {x,y} by TARSKI:def 2;
then x in rng <*x,y*> by FINSEQ_2:127;
then A3: x in dom s by A1, XBOOLE_0:def 3;
thus (Following s) . [<*x,y*>,f] = f . (s * <*x,y*>) by CIRCCOMB:56
.= f . <*(s . x),(s . y)*> by A3, A2, FINSEQ_2:125 ; :: thesis: ( (Following s) . x = s . x & (Following s) . y = s . y )
reconsider x = x, y = y as Vertex of (1GateCircStr (<*x,y*>,f)) by Th43;
InputVertices (1GateCircStr (<*x,y*>,f)) = rng <*x,y*> by CIRCCOMB:42
.= {x,y} by FINSEQ_2:127 ;
then ( x in InputVertices (1GateCircStr (<*x,y*>,f)) & y in InputVertices (1GateCircStr (<*x,y*>,f)) ) by TARSKI:def 2;
hence ( (Following s) . x = s . x & (Following s) . y = s . y ) by CIRCUIT2:def 5; :: thesis: verum