let x, b be non pair set ; :: thesis: for s being State of (BitCompCirc x,b) holds
( (Following s) . (IncrementOutput x,b) = and2a . <*(s . x),(s . b)*> & (Following s) . x = s . x & (Following s) . b = s . b )
let s be State of (BitCompCirc x,b); :: thesis: ( (Following s) . (IncrementOutput x,b) = and2a . <*(s . x),(s . b)*> & (Following s) . x = s . x & (Following s) . b = s . b )
set p = <*x,b*>;
set S = BitCompStr x,b;
InputVertices (BitCompStr x,b) = {x,b} by Th51;
then A1: ( x in InputVertices (BitCompStr x,b) & b in InputVertices (BitCompStr x,b) ) by TARSKI:def 2;
A2: InnerVertices (BitCompStr x,b) = the carrier' of (BitCompStr x,b) by FACIRC_1:37;
A3: dom s = the carrier of (BitCompStr x,b) by CIRCUIT1:4;
A4: ( x in the carrier of (BitCompStr x,b) & b in the carrier of (BitCompStr x,b) ) by Th47;
[<*x,b*>,and2a ] in InnerVertices (BitCompStr x,b) by Th50;
hence (Following s) . (IncrementOutput x,b) = and2a . (s * <*x,b*>) by A2, FACIRC_1:35
.= and2a . <*(s . x),(s . b)*> by A3, A4, FINSEQ_2:145 ;
:: thesis: ( (Following s) . x = s . x & (Following s) . b = s . b )
thus ( (Following s) . x = s . x & (Following s) . b = s . b ) by A1, CIRCUIT2:def 5; :: thesis: verum