let n be Nat; for X being non empty finite set
for f being Function of (n -tuples_on X),X
for p being FinSeqLen of n
for s being State of (1GateCircuit (p,f)) holds (Following s) . [p,f] = f . (s * p)
let X be non empty finite set ; for f being Function of (n -tuples_on X),X
for p being FinSeqLen of n
for s being State of (1GateCircuit (p,f)) holds (Following s) . [p,f] = f . (s * p)
let f be Function of (n -tuples_on X),X; for p being FinSeqLen of n
for s being State of (1GateCircuit (p,f)) holds (Following s) . [p,f] = f . (s * p)
let p be FinSeqLen of n; for s being State of (1GateCircuit (p,f)) holds (Following s) . [p,f] = f . (s * p)
let s be State of (1GateCircuit (p,f)); (Following s) . [p,f] = f . (s * p)
set S = 1GateCircStr (p,f);
set A = 1GateCircuit (p,f);
set IV = InnerVertices (1GateCircStr (p,f));
InnerVertices (1GateCircStr (p,f)) = {[p,f]}
by Th42;
then reconsider v = [p,f] as Element of InnerVertices (1GateCircStr (p,f)) by TARSKI:def 1;
the carrier' of (1GateCircStr (p,f)) = {[p,f]}
by Def6;
then reconsider o = [p,f] as Gate of (1GateCircStr (p,f)) by TARSKI:def 1;
the_result_sort_of o = v
by Def6;
then A1:
action_at v = o
by MSAFREE2:def 7;
the_arity_of o = p
by Def6;
then A2:
o depends_on_in s = s * p
by CIRCUIT1:def 3;
(Following s) . v = (Den ((action_at v),(1GateCircuit (p,f)))) . ((action_at v) depends_on_in s)
by CIRCUIT2:def 5;
hence
(Following s) . [p,f] = f . (s * p)
by A1, A2, Def13; verum