let n be Nat; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: for s being State of (1GateCircuit (p,f)) holds (Following s) . [p,f] = f . (s * p)
let s be State of (1GateCircuit (p,f)); :: thesis: (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; :: thesis: verum