-
-
-
-
-(*
-
- cut (∀j.i ≠ j →
- trace sig n j (reverse (multi_sig sig n) rss@ls2) =
- trace sig n j (ls10@a1::ls20))
- [#j #ineqj >trace_def <map_append in ⊢ (??%?);
- <reverse_map lapply (trace_shift_neq …lt_in ? ineqj … Hrss) [//] #Htr
- <trace_def <trace_def >Htr >reverse_cons *)
-
- %{ls20} %{a1} %{(reverse ? (b0::ls10)@tail (multi_sig sig n) rs2)}
- %[%[%[%[%[@Htout
- |#j #lejn #jneqi <(Hls1 … lejn) -Hls1
- >to_blank_i_def >to_blank_i_def @eq_f
- @(injective_append_l … (trace sig n j (reverse ? rs))) (* >trace_def >trace_def *)
- >map_append >map_append
-
- ]
- |@daemon]
- |@daemon]
- |@daemon]
- |
-
-
- [(* the current character on trace i is blank *)
- * #Hblank #Ht1 <Ht1 in Htin; #Ht1a >Ht1a in Ht2;
- #Ht2 lapply (Ht2 … (refl …)) *
- [(* we reach the margin of the i-th trace *)
- * #rs1 * #b * #rs2 * #a1 * #rss * * * * #H1 #H2 #H3 #H4 #Ht2
- lapply (Htout … Ht2) -Htout *
- [(* the head is on b: this is absurd *)
- * #Hhb @False_ind >Hnohead_rs in Hhb;
- [#H destruct (H) | >H1 @mem_append_l2 %1 //]
- |*
- [(* we reach the head position *)
- * #ls1 * #b0 * #ls2 * * * #H5 #H6 #H7 #Htout
- %{ls2} %{b0} %{(reverse ? (b::ls1)@rs2)}
- cut (ls2 = ls)
- [@daemon (* da finire
- lapply H5 lapply H4 -H5 -H4 cases rss
- [* normalize in ⊢ (%→?); #H destruct (H)
- |#rssa #rsstl #H >reverse_cons >associative_append
- normalize in ⊢ (??(???%)%→?); #H8 @sym_eq
- @(first_P_to_eq (multi_sig sig n)
- (λa.nth n (sig_ext sig) (vec … a) (blank ?) = head ?) ?????? H8)
- *)
- ] #Hls
- %[%[%[%[%[@Htout|>Hls //]
- | #j #lejn #neji >to_blank_i_def >to_blank_i_def
- @eq_f >H1 >trace_def >trace_def >reverse_cons
- >associative_append <map_append <map_append in ⊢ (???%); @eq_f2 //
- @daemon]
- |//]
- |* #H @False_ind @H @daemon
- ]
- |>H1 @daemon
- ]
- |(* we do not find the head: absurd *)
- cut (nth n (sig_ext sig) (vec … a1) (blank sig)=head sig)
- [lapply (trace_shift_neq ??? n … lt_in … H4)
- [@lt_to_not_eq // |//]
- whd in match (trace ????); whd in match (trace ???(a::rs1));
- #H <Hhead @(cons_injective_l … H)]
- #Hcut * #b0 * #lss * * #H @False_ind
- @(absurd (true=false)) [2://] <(H a1)
- [whd in match (no_head ???); >Hcut //
- |%2 @mem_append_l1 >reverse_cons @mem_append_l2 %1 //
- ]
- ]
-
-theorem sem_Rmtil: ∀sig,n,i. i < n → mtiL sig n i ⊨ Rmtil sig n i.
-#sig #n #i #lt_in
-@(sem_seq_app ??????
- (sem_move_to_blank_L … )
- (sem_seq ????? (sem_shift_i_L …)
- (ssem_move_until_L ? (no_head sig n))))
-#tin #tout * #t1 * * #_ #Ht1 * #t2 * #Ht2 * #_ #Htout
-(* we start looking into Rmitl *)
-#ls #a #rs #Htin (* tin is a midtape *)
-#Hhead #Hnohead_ls #Hnohead_rs
-cases (Ht1 … Htin) -Ht1
- [(* the current character on trace i is blank *)
- * #Hblank #Ht1 <Ht1 in Htin; #Ht1a >Ht1a in Ht2;
- #Ht2 lapply (Ht2 … (refl …)) *
- [(* we reach the margin of the i-th trace *)
- * #rs1 * #b * #rs2 * #a1 * #rss * * * * #H1 #H2 #H3 #H4 #Ht2
- lapply (Htout … Ht2) -Htout *
- [(* the head is on b: this is absurd *)
- * #Hhb @False_ind >Hnohead_rs in Hhb;
- [#H destruct (H) | >H1 @mem_append_l2 %1 //]
- |*
- [(* we reach the head position *)
- * #ls1 * #b0 * #ls2 * * * #H5 #H6 #H7 #Htout
- %{ls2} %{b0} %{(reverse ? (b::ls1)@rs2)}
- cut (ls2 = ls)
- [@daemon (* da finire
- lapply H5 lapply H4 -H5 -H4 cases rss
- [* normalize in ⊢ (%→?); #H destruct (H)
- |#rssa #rsstl #H >reverse_cons >associative_append
- normalize in ⊢ (??(???%)%→?); #H8 @sym_eq
- @(first_P_to_eq (multi_sig sig n)
- (λa.nth n (sig_ext sig) (vec … a) (blank ?) = head ?) ?????? H8)
- *)
- ] #Hls
- %[%[%[%[%[@Htout|>Hls //]
- | #j #lejn #neji >to_blank_i_def >to_blank_i_def
- @eq_f >H1 >trace_def >trace_def >reverse_cons
- >associative_append <map_append <map_append in ⊢ (???%); @eq_f2 //
- @daemon]
- |//]
- |* #H @False_ind @H @daemon
- ]
- |>H1 @daemon
- ]
- |(* we do not find the head: absurd *)
- cut (nth n (sig_ext sig) (vec … a1) (blank sig)=head sig)
- [lapply (trace_shift_neq ??? n … lt_in … H4)
- [@lt_to_not_eq // |//]
- whd in match (trace ????); whd in match (trace ???(a::rs1));
- #H <Hhead @(cons_injective_l … H)]
- #Hcut * #b0 * #lss * * #H @False_ind
- @(absurd (true=false)) [2://] <(H a1)
- [whd in match (no_head ???); >Hcut //
- |%2 @mem_append_l1 >reverse_cons @mem_append_l2 %1 //
- ]
- ]
-
-
-theorem sem_Rmtil: ∀sig,n,i. mtiL sig n i ⊨ Rmtil sig n i.
-#sig #n #i
-@(sem_seq_app ??????
- (ssem_move_until_L ? (no_blank sig n i))
- (sem_seq ????? (sem_extend ? (all_blank sig n))
- (sem_seq ????? (sem_ncombf_r (multi_sig sig n) (shift_i sig n i)(all_blank sig n))
- (sem_seq ????? (ssem_mti sig n i)
- (sem_seq ????? (sem_extend ? (all_blank sig n))
- (ssem_move_until_L ? (no_head sig n)))))))
-#tin #tout * #t1 * * #_ #Ht1 * #t2 * * #Ht2a #Ht2b * #t3 * * #Ht3a #Ht3b
-* #t4 * * #Ht4a #Ht4b * #t5 * * #Ht5a #Ht5b * #t6 #Htout
-(* we start looking into Rmitl *)
-#ls #a #rs #Htin (* tin is a midtape *)
-#Hhead #Hnohead_ls #Hnohead_rs
-cases (Ht1 … Htin) -Ht1
- [(* the current character on trace i is blank *)
- -Ht2a * #Hblank #Ht1 <Ht1 in Htin; #Ht1a >Ht1a in Ht2b;
- #Ht2b lapply (Ht2b ?) [% normalize #H destruct] -Ht2b -Ht1 -Ht1a
- lapply Hnohead_rs -Hnohead_rs
- (* by cases on rs *) cases rs
- [#_ (* rs is empty *) #Ht2 -Ht3b lapply (Ht3a … Ht2)
- #Ht3 -Ht4b lapply (Ht4a … Ht3) -Ht4a #Ht4 -Ht5b
- >Ht4 in Ht5a; >Ht3 #Ht5a lapply (Ht5a (refl … )) -Ht5a #Ht5
- cases (Htout … Ht5) -Htout
- [(* the current symbol on trace n is the head: this is absurd *)
- * whd in ⊢ (??%?→?); >all_blank_n whd in ⊢ (??%?→?); #H destruct (H)
- |*
- [(* we return to the head *)
- * #ls1 * #b * #ls2 * * * whd in ⊢ (??%?→?);
- #H1 #H2 #H3
- (* ls1 must be empty *)
- cut (ls1=[])
- [lapply H3 lapply H1 -H3 -H1 cases ls1 // #c #ls3
- whd in ⊢ (???%→?); #H1 destruct (H1)
- >blank_all_blank [|@daemon] #H @False_ind
- lapply (H … (change_vec (sig_ext sig) n a (blank sig) i) ?)
- [%2 %1 // | whd in match (no_head ???); >nth_change_vec_neq [|@daemon]
- >Hhead whd in ⊢ (??%?→?); #H1 destruct (H1)]]
- #Hls1_nil >Hls1_nil in H1; whd in ⊢ (???%→?); #H destruct (H)
- >reverse_single >blank_all_blank [|@daemon]
- whd in match (right ??) ; >append_nil #Htout
- %{ls2} %{(change_vec (sig_ext sig) n a (blank sig) i)} %{[all_blank sig n]}
- %[%[%[%[%[//|//]|@daemon]|//] |(*absurd*)@daemon]
- |normalize >nth_change_vec // @daemon]
- |(* we do not find the head: this is absurd *)
- * #b * #lss * * whd in match (left ??); #HF @False_ind
- lapply (HF … (shift_i sig n i a (all_blank sig n)) ?) [%2 %1 //]
- whd in match (no_head ???); >nth_change_vec_neq [|@daemon]
- >Hhead whd in ⊢ (??%?→?); #H destruct (H)
- ]
- ]
- |(* rs = c::rs1 *)
- #c #rs1 #Hnohead_rs #Ht2 -Ht3a lapply (Ht3b … Ht2) -Ht3b
- #Ht3 -Ht4a lapply (Ht4b … Ht3) -Ht4b *
- [(* the first character is blank *) *
- #Hblank #Ht4 -Ht5a >Ht4 in Ht5b; >Ht3
- normalize in ⊢ ((%→?)→?); #Ht5 lapply (Ht5 ?) [% #H destruct (H)]
- -Ht2 -Ht3 -Ht4 -Ht5 #Ht5 cases (Htout … Ht5) -Htout
- [(* the current symbol on trace n is the head: this is absurd *)
- * >Hnohead_rs [#H destruct (H) |%1 //]
- |*
- [(* we return to the head *)
- * #ls1 * #b * #ls2 * * * whd in ⊢ (??%?→?);
- #H1 #H2 #H3
- (* ls1 must be empty *)
- cut (ls1=[])
- [lapply H3 lapply H1 -H3 -H1 cases ls1 // #x #ls3
- whd in ⊢ (???%→?); #H1 destruct (H1) #H @False_ind
- lapply (H (change_vec (sig_ext sig) n a (nth i (sig_ext sig) (vec … c) (blank sig)) i) ?)
- [%2 %1 // | whd in match (no_head ???); >nth_change_vec_neq [|@daemon]
- >Hhead whd in ⊢ (??%?→?); #H1 destruct (H1)]]
- #Hls1_nil >Hls1_nil in H1; whd in ⊢ (???%→?); #H destruct (H)
- >reverse_single #Htout
- %{ls2} %{(change_vec (sig_ext sig) n a (nth i (sig_ext sig) (vec … c) (blank sig)) i)}
- %{(c::rs1)}
- %[%[%[%[%[@Htout|//]|//]|//] |(*absurd*)@daemon]
- |>to_blank_cons_b
- [>(to_blank_cons_b … Hblank) //| >nth_change_vec [@Hblank |@daemon]]
- ]
- |(* we do not find the head: this is absurd *)
- * #b * #lss * * #HF @False_ind
- lapply (HF … (shift_i sig n i a c) ?) [%2 %1 //]
- whd in match (no_head ???); >nth_change_vec_neq [|@daemon]
- >Hhead whd in ⊢ (??%?→?); #H destruct (H)
- ]
- ]
- |
-
- (* end of the first case !! *)
-
-
-
- #Ht2
-
-cut (∃rs11,rs12. b::rs1 = rs11@a::rs12 ∧ no_head_in ?? rs11)
- [cut (ls1 = [ ] ∨ ∃aa,tlls1. ls1 = aa::tlls1)
- [cases ls1 [%1 // | #aa #tlls1 %2 %{aa} %{tlls1} //]] *
- [#H1ls1 %{[ ]} %{rs1} %
- [ @eq_f2 // >H1ls1 in Hls1; whd in match ([]@b::ls2);
- #Hls1 @(to_blank_hd … Hls1)
- |normalize #x @False_ind
- ]
- |* #aa * #tlls1 #H1ls1 >H1ls1 in Hrs1;
- cut (aa = a) [>H1ls1 in Hls1; #H @(to_blank_hd … H)] #eqaa >eqaa
- #Hrs1_aux cases (compare_append … (sym_eq … Hrs1_aux)) #l *
- [* #H1 #H2 %{(b::(reverse ? tlls1))} %{l} %
- [@eq_f >H1 >reverse_cons >associative_append //
- |@daemon (* is a sublit of the tail of ls1, and hence of ls *)
- ]
- |(* this is absurd : if l is empty, the case is as before.
- if l is not empty then it must start with a blank, since it is the
- frist character in rs2. But in this case we would have a blank
- inside ls1=attls1 that is absurd *)
- @daemon
- ]]]
-
-