-lemma sem_mtestR: ∀sig,i,n,test. i ≤ n →
- mtestR sig i n test ⊨
- [mtestR_acc sig i n test:
- RmtestR_true sig i (S n) test, RmtestR_false sig i (S n) test].
-#sig #i #n #test #Hlein
-@(acc_sem_seq_app sig n … (sem_move_multi … R Hlein)
- (acc_sem_if sig n ????????
- (sem_test_char_multi sig test n i Hlein)
- (sem_move_multi … L Hlein)
- (sem_move_multi … L Hlein)))
- [#t1 #t2 #t3 whd in ⊢ (%→?); #Hmove * #tx * whd in ⊢ (%→?); * *
- #cx #Hcx #Htx #Ht2 #ls #c #c1 #rs #Ht1
- >Ht1 in Hmove; whd in match (tape_move ???); #Ht3
- >Ht3 in Hcx; >nth_change_vec [|@le_S_S //] * whd in ⊢ (??%?→?);
- #Hsome destruct (Hsome) #Htest % [2:@Htest]
- >Htx in Ht2; whd in ⊢ (%→?); #Ht2 @(eq_vec … (niltape ?))
- #j #lejn cases (true_or_false (eqb i j)) #Hij
- [lapply lejn <(eqb_true_to_eq … Hij) #lein >Ht2 >nth_change_vec [2://]
- >Ht3 >nth_change_vec >Ht1 //
- |lapply (eqb_false_to_not_eq … Hij) #Hneq >Ht2 >nth_change_vec_neq [2://]
- >Ht3 >nth_change_vec_neq //
- ]
- |#t1 #t2 #t3 whd in ⊢ (%→?); #Hmove * #tx * whd in ⊢ (%→?); *
- #Hcx #Heqtx #Htx #ls #c #c1 #rs #Ht1
- >Ht1 in Hmove; whd in match (tape_move ???); #Ht3
- >Ht3 in Hcx; >nth_change_vec [2:@le_S_S //] #Hcx lapply (Hcx ? (refl ??))
- #Htest % // @(eq_vec … (niltape ?))
- #j #lejn cases (true_or_false (eqb i j)) #Hij
- [lapply lejn <(eqb_true_to_eq … Hij) #lein >Htx >nth_change_vec [2://]
- >Heqtx >Ht3 >nth_change_vec >Ht1 //
- |lapply (eqb_false_to_not_eq … Hij) #Hneq >Htx >nth_change_vec_neq [2://]
- >Heqtx >Ht3 >nth_change_vec_neq //
- ]
- ]
-qed.