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;
A5: now :: thesis: for a being object st a in the carrier of (1GateCircStr (p,f)) holds
(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;
A8: now :: thesis: for i being object st i in dom p holds
((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;
( 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; :: thesis: 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; :: according to CIRCUIT2:def 6 :: thesis: verum