let X be non empty finite set ; for n being Nat
for p being FinSeqLen of n
for f being Function of (n -tuples_on X),X
for s being State of (1GateCircuit (p,f)) holds Following s is stable
let n be Nat; for p being FinSeqLen of n
for f being Function of (n -tuples_on X),X
for s being State of (1GateCircuit (p,f)) holds Following s is stable
let p be FinSeqLen of n; for f being Function of (n -tuples_on X),X
for s being State of (1GateCircuit (p,f)) holds Following s is stable
let f be Function of (n -tuples_on X),X; for s being State of (1GateCircuit (p,f)) holds Following s is stable
set S = 1GateCircStr (p,f);
let s be State of (1GateCircuit (p,f)); Following s is stable
set s1 = Following s;
set s2 = Following (Following s);
A1:
dom (Following s) = the carrier of (1GateCircStr (p,f))
by CIRCUIT1:3;
A2:
the carrier of (1GateCircStr (p,f)) = (rng p) \/ {[p,f]}
by CIRCCOMB:def 6;
A3:
InputVertices (1GateCircStr (p,f)) = rng p
by CIRCCOMB:42;
A4:
InnerVertices (1GateCircStr (p,f)) = {[p,f]}
by CIRCCOMB:42;
A5:
now for a being object st a in the carrier of (1GateCircStr (p,f)) holds
(Following (Following s)) . a = (Following s) . alet a be
object ;
( a in the carrier of (1GateCircStr (p,f)) implies (Following (Following s)) . a = (Following s) . a )assume
a in the
carrier of
(1GateCircStr (p,f))
;
(Following (Following s)) . a = (Following s) . athen reconsider v =
a as
Vertex of
(1GateCircStr (p,f)) ;
dom s = the
carrier of
(1GateCircStr (p,f))
by CIRCUIT1:3;
then A6:
dom (s * p) = dom p
by A2, RELAT_1:27, XBOOLE_1:7;
A7:
dom ((Following s) * p) = dom p
by A1, A2, RELAT_1:27, XBOOLE_1:7;
(
v in rng p or
v in {[p,f]} )
by A2, XBOOLE_0:def 3;
then
(
(Following (Following s)) . v = (Following s) . v or (
v = [p,f] & (
v = [p,f] implies
action_at v = v ) &
(Following (Following s)) . v = (Den ((action_at v),(1GateCircuit (p,f)))) . ((action_at v) depends_on_in (Following s)) &
(Following s) . v = (Den ((action_at v),(1GateCircuit (p,f)))) . ((action_at v) depends_on_in s) & (
action_at v = [p,f] implies (
(action_at v) depends_on_in s = s * p &
(action_at v) depends_on_in (Following s) = (Following s) * p ) ) ) )
by A3, A4, Th1, CIRCCOMB:41, CIRCUIT2:def 5, TARSKI:def 1;
hence
(Following (Following s)) . a = (Following s) . a
by A7, A6, A8, FUNCT_1:2;
verum end;
dom (Following (Following s)) = the carrier of (1GateCircStr (p,f))
by CIRCUIT1:3;
hence
Following s = Following (Following s)
by A1, A5, FUNCT_1:2; CIRCUIT2:def 6 verum