let x, b be non pair set ; for s being State of (BitCompCirc (x,b)) holds Following s is stable
set p = <*x,b*>;
set S = BitCompStr (x,b);
let s be State of (BitCompCirc (x,b)); Following s is stable
set s1 = Following s;
set s2 = Following (Following s);
A1:
the carrier of (BitCompStr (x,b)) = {x,b} \/ {[<*x,b*>,xor2a],[<*x,b*>,and2a]}
by Th37;
A2:
now for a being object st a in the carrier of (BitCompStr (x,b)) holds
(Following (Following s)) . a = (Following s) . alet a be
object ;
( a in the carrier of (BitCompStr (x,b)) implies (Following (Following s)) . a = (Following s) . a )A3:
(Following s) . [<*x,b*>,xor2a] =
(Following s) . (CompOutput (x,b))
.=
xor2a . <*(s . x),(s . b)*>
by Th45
;
assume
a in the
carrier of
(BitCompStr (x,b))
;
(Following (Following s)) . a = (Following s) . athen
(
a in {x,b} or
a in {[<*x,b*>,xor2a],[<*x,b*>,and2a]} )
by A1, XBOOLE_0:def 3;
then A4:
(
a = x or
a = b or
a = [<*x,b*>,xor2a] or
a = [<*x,b*>,and2a] )
by TARSKI:def 2;
A5:
(Following (Following s)) . [<*x,b*>,and2a] =
(Following (Following s)) . (IncrementOutput (x,b))
.=
and2a . <*((Following s) . x),((Following s) . b)*>
by Th49
;
A6:
(Following (Following s)) . [<*x,b*>,xor2a] =
(Following (Following s)) . (CompOutput (x,b))
.=
xor2a . <*((Following s) . x),((Following s) . b)*>
by Th45
;
A7:
(Following s) . [<*x,b*>,and2a] =
(Following s) . (IncrementOutput (x,b))
.=
and2a . <*(s . x),(s . b)*>
by Th49
;
(Following s) . x = s . x
by Th45;
hence
(Following (Following s)) . a = (Following s) . a
by A4, A3, A7, A6, A5, Th45;
verum end;
( dom (Following s) = the carrier of (BitCompStr (x,b)) & dom (Following (Following s)) = the carrier of (BitCompStr (x,b)) )
by CIRCUIT1:3;
hence
Following s = Following (Following s)
by A2, FUNCT_1:2; CIRCUIT2:def 6 verum