let x, y be object ; 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 is stable
let X be 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 is stable
let f be Function of (2 -tuples_on X),X; for s being State of (1GateCircuit (<*x,y*>,f)) holds Following s is stable
set S = 1GateCircStr (<*x,y*>,f);
let s be State of (1GateCircuit (<*x,y*>,f)); Following s is stable
set s1 = Following s;
set s2 = Following (Following s);
set p = <*x,y*>;
A1: the carrier of (1GateCircStr (<*x,y*>,f)) =
(rng <*x,y*>) \/ {[<*x,y*>,f]}
by CIRCCOMB:def 6
.=
{x,y} \/ {[<*x,y*>,f]}
by FINSEQ_2:127
;
A2:
now for a being object st a in the carrier of (1GateCircStr (<*x,y*>,f)) holds
(Following (Following s)) . a = (Following s) . alet a be
object ;
( a in the carrier of (1GateCircStr (<*x,y*>,f)) implies (Following (Following s)) . a = (Following s) . a )A3:
(Following (Following s)) . [<*x,y*>,f] = f . <*((Following s) . x),((Following s) . y)*>
by Th48;
assume
a in the
carrier of
(1GateCircStr (<*x,y*>,f))
;
(Following (Following s)) . a = (Following s) . athen
(
a in {x,y} or
a in {[<*x,y*>,f]} )
by A1, XBOOLE_0:def 3;
then A4:
(
a = x or
a = y or
a = [<*x,y*>,f] )
by TARSKI:def 1, TARSKI:def 2;
(
(Following s) . x = s . x &
(Following s) . y = s . y )
by Th48;
hence
(Following (Following s)) . a = (Following s) . a
by A4, A3, Th48;
verum end;
( dom (Following s) = the carrier of (1GateCircStr (<*x,y*>,f)) & dom (Following (Following s)) = the carrier of (1GateCircStr (<*x,y*>,f)) )
by CIRCUIT1:3;
hence
Following s = Following (Following s)
by A2, FUNCT_1:2; CIRCUIT2:def 6 verum