-lemma terminate_move_char_r :
- ∀alpha,sep.∀t,b,a,ls,rs. t = midtape alpha (a::ls) b rs →
- (b = sep ∨ memb ? sep rs = true) → Terminate alpha (move_char_r alpha sep) t.
-#alpha #sep #t #b #a #ls #rs #Ht #Hsep
-@(terminate_while … (sem_mcr_step alpha sep))
- [%
- |generalize in match Hsep; -Hsep
- generalize in match Ht; -Ht
- generalize in match ls; -ls
- generalize in match a; -a
- generalize in match b; -b
- generalize in match t; -t
- elim rs
- [#t #b #a #ls #Ht #Hsep % #tinit
- whd in ⊢ (%→?); #H @False_ind
- cases (H … Ht) #Hb #_ cases Hb #eqb @eqb
- cases Hsep // whd in ⊢ ((??%?)→?); #abs destruct
- |#r0 #rs0 #Hind #t #b #a #ls #Ht #Hsep % #tinit
- whd in ⊢ (%→?); #H
- cases (H … Ht) #Hbsep #Htinit
- @(Hind … Htinit) cases Hsep
- [#Hb @False_ind /2/ | #Hmemb cases (orb_true_l … Hmemb)
- [#eqsep %1 >(\P eqsep) // | #H %2 //]
- ]
+lemma WF_mcr_niltape:
+ ∀alpha,sep. WF ? (inv ? (Rmcr_step_true alpha sep)) (niltape alpha).
+#alpha #sep @wf #t1 whd in ⊢ (%→?); * #b * #_ *
+ [* #a * #ls * #rs * #H destruct | * #rs * #H destruct ]
+qed.
+
+lemma WF_mcr_rightof:
+ ∀alpha,sep,a,ls. WF ? (inv ? (Rmcr_step_true alpha sep)) (rightof alpha a ls).
+#alpha #sep #a #ls @wf #t1 whd in ⊢ (%→?); * #b * #_ *
+ [* #a * #ls * #rs * #H destruct | * #rs * #H destruct ]