+(* we say that a tape is regular if for any trace after the first blank we
+ only have other blanks *)
+
+definition all_blanks_in ≝ λsig,l.
+ ∀x. mem ? x l → x = blank sig.
+
+definition regular_i ≝ λsig,n.λl:list (multi_sig sig n).λi.
+ all_blanks_in ? (after_blank ? (trace sig n i l)).
+
+definition regular_trace ≝ λsig,n,a.λls,rs:list (multi_sig sig n).λi.
+ Or (And (regular_i sig n (a::ls) i) (regular_i sig n rs i))
+ (And (regular_i sig n ls i) (regular_i sig n (a::rs) i)).
+
+axiom regular_tail: ∀sig,n,l,i.
+ regular_i sig n l i → regular_i sig n (tail ? l) i.
+
+axiom regular_extend: ∀sig,n,l,i.
+ regular_i sig n l i → regular_i sig n (l@[all_blank sig n]) i.
+
+axiom all_blank_after_blank: ∀sig,n,l1,b,l2,i.
+ nth i ? (vec … b) (blank ?) = blank ? →
+ regular_i sig n (l1@b::l2) i → all_blanks_in ? (trace sig n i l2).
+
+lemma regular_trace_extl: ∀sig,n,a,ls,rs,i.
+ regular_trace sig n a ls rs i →
+ regular_trace sig n a (ls@[all_blank sig n]) rs i.
+#sig #n #a #ls #rs #i *
+ [* #H1 #H2 % % // @(regular_extend … H1)
+ |* #H1 #H2 %2 % // @(regular_extend … H1)
+ ]
+qed.
+
+lemma regular_cons_hd_rs: ∀sig,n.∀a:multi_sig sig n.∀ls,rs1,rs2,i.
+ regular_trace sig n a ls (rs1@rs2) i →
+ regular_trace sig n a ls (rs1@((hd ? rs2 (all_blank …))::(tail ? rs2))) i.
+#sig #n #a #ls #rs1 #rs2 #i cases rs2 [2: #b #tl #H @H]
+*[* #H1 >append_nil #H2 %1 %
+ [@H1 | whd in match (hd ???); @(regular_extend … rs1) //]
+ |* #H1 >append_nil #H2 %2 %
+ [@H1 | whd in match (hd ???); @(regular_extend … (a::rs1)) //]
+ ]
+qed.
+
+lemma eq_trace_to_regular : ∀sig,n.∀a1,a2:multi_sig sig n.∀ls1,ls2,rs1,rs2,i.
+ nth i ? (vec … a1) (blank ?) = nth i ? (vec … a2) (blank ?) →
+ trace sig n i ls1 = trace sig n i ls2 →
+ trace sig n i rs1 = trace sig n i rs2 →
+ regular_trace sig n a1 ls1 rs1 i →
+ regular_trace sig n a2 ls2 rs2 i.
+#sig #n #a1 #a2 #ls1 #ls2 #rs1 #rs2 #i #H1 #H2 #H3 #H4
+whd in match (regular_trace ??????); whd in match (regular_i ????);
+whd in match (regular_i ?? rs2 ?); whd in match (regular_i ?? ls2 ?);
+whd in match (regular_i ?? (a2::rs2) ?); whd in match (trace ????);
+<trace_def whd in match (trace ??? (a2::rs2)); <trace_def
+<H1 <H2 <H3 @H4
+qed.
+