+(* new script *)
+
+include "basics/logic.ma".
+include "basics/types.ma".
+include "basics/bool.ma".
+include "arithmetics/nat.ma".
+include "basics/list.ma".
+
+axiom Vector : Type[0] → nat → Type[0].
+axiom tape : Type[0] → Type[0].
+axiom current : ∀T:Type[0]. tape T → option T.
+axiom vec : ∀T:Type[0].∀n:nat.Vector T n → list T.
+coercion vec : ∀T:Type[0].∀n:nat.∀v:Vector T n.list T ≝ vec on _v:Vector ?? to list ?.
+axiom niltape : ∀T.tape T.
+axiom midtape : ∀T.list T → T → list T → tape T.
+axiom change_vec : ∀T,n.Vector T n → T → nat → Vector T n.
+axiom move : Type[0].
+axiom R : move.
+axiom tape_move : ∀T.tape T → option (T × move) → tape T.
+axiom memb: ∀T.T → list T → bool.
+interpretation "boolean membership" 'mem a l = (memb ? a l).
+axiom right : ∀T.tape T → list T.
+
+
+definition R_match_step_true ≝
+ λsrc,dst,sig,n,is_startc,is_endc.λint,outt: Vector (tape sig) (S n).
+ ∀s.current sig (nth src (tape sig) int (niltape sig)) = Some ? s →
+ current sig (nth dst (tape sig) int (niltape sig)) ≠ None ? ∧
+ (is_startc s = true →
+ (∀c.c ∈ right ? (nth src (tape sig) int (niltape sig)) = true → is_startc c = false) →
+ (∀s1.current sig (nth dst (tape sig) int (niltape sig)) = Some ? s1 → s ≠ s1 →
+ outt = change_vec ?? int
+ (tape_move … (nth dst ? int (niltape ?)) (Some ? 〈s1,R〉)) dst ∧ is_endc s = false) ∧
+ (∀ls,x,xs,ci,rs,ls0,rs0.
+ nth src ? int (niltape ?) = midtape ls x (xs@ci::rs) →
+ nth dst ? int (niltape ?) = midtape sig ls0 x (xs@rs0) →
+ (∀c0. memb ? c0 (x::xs) = true → is_endc c0 = false) →
+ is_endc ci = false ∧ rs0 ≠ [] ∧
+ ∀cj,rs1.rs0 = cj::rs1 →
+ ci ≠ cj →
+ (outt = change_vec ?? int
+ (tape_move … (nth dst ? int (niltape ?)) (Some ? 〈x,R〉)) dst ∧ is_endc ci = false))).
+