λsig,n,test.λint,outt: Vector (tape sig) (S n).
test (current_chars ?? int) = false ∧ outt = int.
λsig,n,test.λint,outt: Vector (tape sig) (S n).
test (current_chars ?? int) = false ∧ outt = int.
∀sig,n,test,v.
test (current_chars ?? v) = true →
step sig n (partest sig n test)(mk_mconfig ??? partest0 v)
= mk_mconfig ??? partest1 v.
∀sig,n,test,v.
test (current_chars ?? v) = true →
step sig n (partest sig n test)(mk_mconfig ??? partest0 v)
= mk_mconfig ??? partest1 v.
∀sig,n,test,v.
test (current_chars ?? v) = false →
step sig n (partest sig n test)(mk_mconfig ??? partest0 v)
= mk_mconfig ??? partest2 v.
∀sig,n,test,v.
test (current_chars ?? v) = false →
step sig n (partest sig n test)(mk_mconfig ??? partest0 v)
= mk_mconfig ??? partest2 v.