-(*
-definition R_match_m ≝
- λi,j,sig,n,is_startc,is_endc.λint,outt: Vector (tape sig) (S n).
- (((∃x.current ? (nth i ? int (niltape ?)) = Some ? x ∧ is_endc x = true) ∨
- current ? (nth i ? int (niltape ?)) = None ? ∨
- current ? (nth j ? int (niltape ?)) = None ?) → outt = int) ∧
- (∀ls,x,xs,ci,rs,ls0,x0,rs0.
- (∀x. is_startc x ≠ is_endc x) →
- is_startc x = true → is_endc ci = true →
- (∀z. memb ? z (x::xs) = true → is_endc x = false) →
- nth i ? int (niltape ?) = midtape sig ls x (xs@ci::rs) →
- nth j ? int (niltape ?) = midtape sig ls0 x0 rs0 →
- (∃l,l1.x0::rs0 = l@x::xs@l1 ∧
- ∀cj,l2.l1=cj::l2 →
- outt = change_vec ??
- (change_vec ?? int (midtape sig (reverse ? xs@x::ls) ci rs) i)
- (midtape sig ((reverse ? (l@x::xs))@ls0) cj l2) j) ∨
- ∀l,l1.x0::rs0 ≠ l@x::xs@l1).
-*)
-
-(*
-axiom sub_list_dec: ∀A.∀l,ls:list A.
- ∃l1,l2. l = l1@ls@l2 ∨ ∀l1,l2. l ≠ l1@ls@l2.
-*)
-