\ / GNU General Public License Version 2
V_____________________________________________________________*)
-include "turing/multi_universal/moves_2.ma".
-include "turing/multi_universal/match.ma".
-include "turing/multi_universal/copy.ma".
+include "turing/auxiliary_machines.ma".
+include "turing/auxiliary_multi_machines.ma".
include "turing/multi_universal/alphabet.ma".
include "turing/multi_universal/tuples.ma".
(mk_tape ? [ ] (option_hd FSUnialpha (reverse ? (null::ls)))
(tail ? (reverse ? (null::ls)))) cfg).
+(*
axiom accRealize_to_Realize :
∀sig,n.∀M:mTM sig n.∀Rtrue,Rfalse,acc.
M ⊨ [ acc: Rtrue, Rfalse ] → M ⊨ Rtrue ∪ Rfalse.
+*)
lemma eq_mk_tape_rightof :
∀alpha,a,al.mk_tape alpha (a::al) (None ?) [ ] = rightof ? a al.