mem ? 〈〈q,l〉,〈q1,mvs〉〉 (trans ? M) ∧
state ?? c1 = q1 ∧
tapes ?? c1 = (compose_vec ??? (tape_move sig) ? (tapes ?? c) mvs).
mem ? 〈〈q,l〉,〈q1,mvs〉〉 (trans ? M) ∧
state ?? c1 = q1 ∧
tapes ?? c1 = (compose_vec ??? (tape_move sig) ? (tapes ?? c) mvs).
definition accepted ≝ λsig.λM:NTM sig.λw:(list sig).
∃c. star ? (reach sig M) (init sig M w) c ∧
accept ?? (state ?? c) = true.
definition accepted ≝ λsig.λM:NTM sig.λw:(list sig).
∃c. star ? (reach sig M) (init sig M w) c ∧
accept ?? (state ?? c) = true.