let X be non empty finite set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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)); :: thesis: 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;

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

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; :: thesis: 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; :: thesis: 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; :: thesis: 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)); :: thesis: 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 :: thesis: for a being object st a in the carrier of (1GateCircStr (p,f)) holds

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

dom (Following (Following s)) = the carrier of (1GateCircStr (p,f))
by CIRCUIT1:3;(Following (Following s)) . a = (Following s) . a

let a be object ; :: thesis: ( 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)) ; :: thesis: (Following (Following s)) . a = (Following s) . a

then 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;

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; :: thesis: verum

end;assume a in the carrier of (1GateCircStr (p,f)) ; :: thesis: (Following (Following s)) . a = (Following s) . a

then 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;

A8: now :: thesis: for i being object st i in dom p holds

((Following s) * p) . i = (s * p) . i

( v in rng p or v in {[p,f]} )
by A2, XBOOLE_0:def 3;((Following s) * p) . i = (s * p) . i

let i be object ; :: thesis: ( i in dom p implies ((Following s) * p) . i = (s * p) . i )

assume A9: i in dom p ; :: thesis: ((Following s) * p) . i = (s * p) . i

then A10: p . i in rng p by FUNCT_1:3;

( ((Following s) * p) . i = (Following s) . (p . i) & (s * p) . i = s . (p . i) ) by A7, A6, A9, FUNCT_1:12;

hence ((Following s) * p) . i = (s * p) . i by A3, A10, CIRCUIT2:def 5; :: thesis: verum

end;assume A9: i in dom p ; :: thesis: ((Following s) * p) . i = (s * p) . i

then A10: p . i in rng p by FUNCT_1:3;

( ((Following s) * p) . i = (Following s) . (p . i) & (s * p) . i = s . (p . i) ) by A7, A6, A9, FUNCT_1:12;

hence ((Following s) * p) . i = (s * p) . i by A3, A10, CIRCUIT2:def 5; :: thesis: verum

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; :: thesis: verum

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