-
-lemma wsem_copy : ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n →
- copy src dst sig n ⊫ R_copy src dst sig n.
-#src #dst #sig #n #Hneq #Hsrc #Hdst #ta #k #outc #Hloop
-lapply (sem_while … (sem_copy_step src dst sig n Hneq Hsrc Hdst) … Hloop) //
--Hloop * #tb * #Hstar @(star_ind_l ??????? Hstar) -Hstar
-[ whd in ⊢ (%→?); * #Hnone #Hout %
- [#_ @Hout
- |#ls #x #x0 #rs #ls0 #rs0 #Hsrc1 #Hdst1 @False_ind cases Hnone
- [>Hsrc1 normalize #H destruct (H) | >Hdst1 normalize #H destruct (H)]
- ]
-|#tc #td * #x * #y * * #Hcx #Hcy #Htd #Hstar #IH #He lapply (IH He) -IH *
- #IH1 #IH2 %
- [* [>Hcx #H destruct (H) | >Hcy #H destruct (H)]
- |#ls #x' #y' #rs #ls0 #rs0 #Hnth_src #Hnth_dst
- >Hnth_src in Hcx; whd in ⊢ (??%?→?); #H destruct (H)
- >Hnth_dst in Hcy; whd in ⊢ (??%?→?); #H destruct (H)
- >Hnth_src in Htd; >Hnth_dst -Hnth_src -Hnth_dst
- cases rs
- [(* the source tape is empty after the move *)
- #Htd lapply (IH1 ?)
- [%1 >Htd >nth_change_vec_neq [2:@(not_to_not … Hneq) //] >nth_change_vec //]
- #Hout (* whd in match (tape_move ???); *) %1 %{([])} %{rs0} %
- [% [// | // ]
- |whd in match (reverse ??); whd in match (reverse ??);
- >Hout >Htd @eq_f2 // cases rs0 //
- ]
- |#c1 #tl1 cases rs0
- [(* the dst tape is empty after the move *)
- #Htd lapply (IH1 ?) [%2 >Htd >nth_change_vec //]
- #Hout (* whd in match (tape_move ???); *) %2 %{[ ]} %{(c1::tl1)} %
- [% [// | // ]
- |whd in match (reverse ??); whd in match (reverse ??);
- >Hout >Htd @eq_f2 //
- ]
- |#c2 #tl2 whd in match (tape_move_mono ???); whd in match (tape_move_mono ???);
- #Htd
- cut (nth src (tape sig) td (niltape sig)=midtape sig (x::ls) c1 tl1)
- [>Htd >nth_change_vec_neq [2:@(not_to_not … Hneq) //] @nth_change_vec //]
- #Hsrc_td
- cut (nth dst (tape sig) td (niltape sig)=midtape sig (x::ls0) c2 tl2)
- [>Htd @nth_change_vec //]
- #Hdst_td cases (IH2 … Hsrc_td Hdst_td) -Hsrc_td -Hdst_td
- [* #rs01 * #rs02 * * #H1 #H2 #H3 %1
- %{(c2::rs01)} %{rs02} % [% [@eq_f //|normalize @eq_f @H2]]
- >Htd in H3; >change_vec_commute // >change_vec_change_vec
- >change_vec_commute [2:@(not_to_not … Hneq) //] >change_vec_change_vec
- #H >reverse_cons >associative_append >associative_append @H
- |* #rs11 * #rs12 * * #H1 #H2 #H3 %2
- %{(c1::rs11)} %{rs12} % [% [@eq_f //|normalize @eq_f @H2]]
- >Htd in H3; >change_vec_commute // >change_vec_change_vec
- >change_vec_commute [2:@(not_to_not … Hneq) //] >change_vec_change_vec
- #H >reverse_cons >associative_append >associative_append @H
- ]
- ]
- ]
- ]
+
+definition test_null_char ≝ test_char FSUnialpha (λc.c == null).
+
+definition R_test_null_char_true ≝ λt1,t2.
+ current FSUnialpha t1 = Some ? null ∧ t1 = t2.
+
+definition R_test_null_char_false ≝ λt1,t2.
+ current FSUnialpha t1 ≠ Some ? null ∧ t1 = t2.
+
+lemma sem_test_null_char :
+ test_null_char ⊨ [ tc_true : R_test_null_char_true, R_test_null_char_false].
+#t1 cases (sem_test_char FSUnialpha (λc.c == null) t1) #k * #outc * * #Hloop #Htrue
+#Hfalse %{k} %{outc} % [ %
+[ @Hloop
+| #Houtc cases (Htrue ?) [| @Houtc] * #c * #Hcurt1 #Hcnull lapply (\P Hcnull)
+ -Hcnull #H destruct (H) #Houtc1 %
+ [ @Hcurt1 | <Houtc1 % ] ]
+| #Houtc cases (Hfalse ?) [| @Houtc] #Hc #Houtc %
+ [ % #Hcurt1 >Hcurt1 in Hc; #Hc lapply (Hc ? (refl ??))
+ >(?:((null:FSUnialpha) == null) = true) [|@(\b (refl ??)) ]
+ #H destruct (H)
+ | <Houtc % ] ]