let n be Element of 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) . (Output (1GateCircStr (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) . (Output (1GateCircStr (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) . (Output (1GateCircStr (p,f))) = f . (s * p)
let p be FinSeqLen of n; :: thesis: for s being State of (1GateCircuit (p,f)) holds (Following s) . (Output (1GateCircStr (p,f))) = f . (s * p)
let s be State of (1GateCircuit (p,f)); :: thesis: (Following s) . (Output (1GateCircStr (p,f))) = f . (s * p)
Output (1GateCircStr (p,f)) = [p,f] by Th15;
hence (Following s) . (Output (1GateCircStr (p,f))) = f . (s * p) by CIRCCOMB:56; :: thesis: verum