3 include "basics/logic.ma".
4 include "basics/types.ma".
5 include "basics/bool.ma".
6 include "arithmetics/nat.ma".
7 include "basics/list.ma".
9 axiom Vector : Type[0] → nat → Type[0].
10 axiom tape : Type[0] → Type[0].
11 axiom current : ∀T:Type[0]. tape T → option T.
12 axiom vec : ∀T:Type[0].∀n:nat.Vector T n → list T.
13 coercion vec : ∀T:Type[0].∀n:nat.∀v:Vector T n.list T ≝ vec on _v:Vector ?? to list ?.
14 axiom niltape : ∀T.tape T.
15 axiom midtape : ∀T.list T → T → list T → tape T.
16 axiom change_vec : ∀T,n.Vector T n → T → nat → Vector T n.
19 axiom tape_move : ∀T.tape T → option (T × move) → tape T.
20 axiom memb: ∀T.T → list T → bool.
21 interpretation "boolean membership" 'mem a l = (memb ? a l).
22 axiom right : ∀T.tape T → list T.
25 definition R_match_step_true ≝
26 λsrc,dst,sig,n,is_startc,is_endc.λint,outt: Vector (tape sig) (S n).
27 ∀s.current sig (nth src (tape sig) int (niltape sig)) = Some ? s →
28 current sig (nth dst (tape sig) int (niltape sig)) ≠ None ? ∧
30 (∀c.c ∈ right ? (nth src (tape sig) int (niltape sig)) = true → is_startc c = false) →
31 (∀s1.current sig (nth dst (tape sig) int (niltape sig)) = Some ? s1 → s ≠ s1 →
32 outt = change_vec ?? int
33 (tape_move … (nth dst ? int (niltape ?)) (Some ? 〈s1,R〉)) dst ∧ is_endc s = false) ∧
34 (∀ls,x,xs,ci,rs,ls0,rs0.
35 nth src ? int (niltape ?) = midtape ls x (xs@ci::rs) →
36 nth dst ? int (niltape ?) = midtape sig ls0 x (xs@rs0) →
37 (∀c0. memb ? c0 (x::xs) = true → is_endc c0 = false) →
38 is_endc ci = false ∧ rs0 ≠ [] ∧
39 ∀cj,rs1.rs0 = cj::rs1 →
41 (outt = change_vec ?? int
42 (tape_move … (nth dst ? int (niltape ?)) (Some ? 〈x,R〉)) dst ∧ is_endc ci = false))).