let x, y, z be object ; :: thesis: for X being non empty finite set

for f being Function of (3 -tuples_on X),X

for s being State of (1GateCircuit (<*x,y,z*>,f)) holds Following s is stable

let X be non empty finite set ; :: thesis: for f being Function of (3 -tuples_on X),X

for s being State of (1GateCircuit (<*x,y,z*>,f)) holds Following s is stable

let f be Function of (3 -tuples_on X),X; :: thesis: for s being State of (1GateCircuit (<*x,y,z*>,f)) holds Following s is stable

set p = <*x,y,z*>;

set S = 1GateCircStr (<*x,y,z*>,f);

let s be State of (1GateCircuit (<*x,y,z*>,f)); :: thesis: Following s is stable

set s1 = Following s;

set s2 = Following (Following s);

A1: the carrier of (1GateCircStr (<*x,y,z*>,f)) = (rng <*x,y,z*>) \/ {[<*x,y,z*>,f]} by CIRCCOMB:def 6

.= {x,y,z} \/ {[<*x,y,z*>,f]} by FINSEQ_2:128 ;

hence Following s = Following (Following s) by A2, FUNCT_1:2; :: according to CIRCUIT2:def 6 :: thesis: verum

for f being Function of (3 -tuples_on X),X

for s being State of (1GateCircuit (<*x,y,z*>,f)) holds Following s is stable

let X be non empty finite set ; :: thesis: for f being Function of (3 -tuples_on X),X

for s being State of (1GateCircuit (<*x,y,z*>,f)) holds Following s is stable

let f be Function of (3 -tuples_on X),X; :: thesis: for s being State of (1GateCircuit (<*x,y,z*>,f)) holds Following s is stable

set p = <*x,y,z*>;

set S = 1GateCircStr (<*x,y,z*>,f);

let s be State of (1GateCircuit (<*x,y,z*>,f)); :: thesis: Following s is stable

set s1 = Following s;

set s2 = Following (Following s);

A1: the carrier of (1GateCircStr (<*x,y,z*>,f)) = (rng <*x,y,z*>) \/ {[<*x,y,z*>,f]} by CIRCCOMB:def 6

.= {x,y,z} \/ {[<*x,y,z*>,f]} by FINSEQ_2:128 ;

A2: now :: thesis: for a being object st a in the carrier of (1GateCircStr (<*x,y,z*>,f)) holds

(Following (Following s)) . a = (Following s) . a

( dom (Following s) = the carrier of (1GateCircStr (<*x,y,z*>,f)) & dom (Following (Following s)) = the carrier of (1GateCircStr (<*x,y,z*>,f)) )
by CIRCUIT1:3;(Following (Following s)) . a = (Following s) . a

let a be object ; :: thesis: ( a in the carrier of (1GateCircStr (<*x,y,z*>,f)) implies (Following (Following s)) . a = (Following s) . a )

A3: ( (Following s) . z = s . z & (Following (Following s)) . [<*x,y,z*>,f] = f . <*((Following s) . x),((Following s) . y),((Following s) . z)*> ) by Th52;

assume a in the carrier of (1GateCircStr (<*x,y,z*>,f)) ; :: thesis: (Following (Following s)) . a = (Following s) . a

then ( a in {x,y,z} or a in {[<*x,y,z*>,f]} ) by A1, XBOOLE_0:def 3;

then A4: ( a = x or a = y or a = z or a = [<*x,y,z*>,f] ) by ENUMSET1:def 1, TARSKI:def 1;

( (Following s) . x = s . x & (Following s) . y = s . y ) by Th52;

hence (Following (Following s)) . a = (Following s) . a by A4, A3, Th52; :: thesis: verum

end;A3: ( (Following s) . z = s . z & (Following (Following s)) . [<*x,y,z*>,f] = f . <*((Following s) . x),((Following s) . y),((Following s) . z)*> ) by Th52;

assume a in the carrier of (1GateCircStr (<*x,y,z*>,f)) ; :: thesis: (Following (Following s)) . a = (Following s) . a

then ( a in {x,y,z} or a in {[<*x,y,z*>,f]} ) by A1, XBOOLE_0:def 3;

then A4: ( a = x or a = y or a = z or a = [<*x,y,z*>,f] ) by ENUMSET1:def 1, TARSKI:def 1;

( (Following s) . x = s . x & (Following s) . y = s . y ) by Th52;

hence (Following (Following s)) . a = (Following s) . a by A4, A3, Th52; :: thesis: verum

hence Following s = Following (Following s) by A2, FUNCT_1:2; :: according to CIRCUIT2:def 6 :: thesis: verum