+@daemon (* this no longer works: TODO *) (*
+@(acc_sem_if_app_guarded STape … (sem_test_char ? (λc:STape.\fst c == bit false))
+ ? (test_char_inv …) (sem_nop …) …)
+[| @(sem_seq_app_guarded … (Realize_to_GRealize … sem_init_match) ???)
+ [ 5: @sub_reflexive
+ | 3: @(sem_seq_app_guarded … sem_match_tuple
+ (Realize_to_GRealize … (sem_if ????????? (sem_test_char … (λc.¬is_marked FSUnialpha c))
+ (sem_seq … sem_exec_action (sem_move_r …))
+ (sem_nop …))))
+ [@(λx.True)
+ |//
+ |@sub_reflexive]
+ ||| #t1 #t2 * #n * #table * #s0 * #s1 * #c0 * #c1 * #ls * #rs * #curconfig
+ * #newconfig * #mv * * * *
+ #Hlen1 #Htable #Hmatch #Hlegal #Ht1
+ whd in ⊢ (%→?);
+ cut (∃tup,table0.table = tup@table0 ∧ tuple_TM (S n) tup)
+ [@daemon]
+ * #tup * #table0 * #Htableeq * #qin * #cin * #qout * #cout * #mv0
+ * * * * * * * * * *
+ #Hqinnomarks #_ #Hqinbits #_ #_ #_ #_ #_ #Hqinlen #_ #Htupeq
+ cut (∃d,qin0.qin = 〈d,false〉::qin0)
+ [ lapply Hqinlen lapply Hqinnomarks -Hqinlen -Hqinnomarks cases qin
+ [ #_ normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
+ | * #d #bd #qin0 #Hqinnomarks #_ %{d} %{qin0}
+ >(?:bd=false) [%]
+ @(Hqinnomarks 〈d,bd〉) @memb_hd ] ]
+ * #d * #qin0 #Hqineq
+ #Ht2
+ lapply (Ht2 (〈grid,false〉::ls) (curconfig@[〈c0,false〉])
+ (qin0@〈cin,false〉::〈comma,false〉::qout@〈cout,false〉::〈comma,false〉::〈mv0,false〉::table0@〈grid,false〉::rs) s0 d ???)
+ [ >Ht1 @eq_f >associative_append @eq_f @eq_f @eq_f
+ >Htableeq >Htupeq >associative_append whd in ⊢ (??%?);
+ @eq_f >Hqineq >associative_append @eq_f whd in ⊢ (??%?);
+ @eq_f whd in ⊢ (??%?); @eq_f
+ >associative_append %
+ | @daemon
+ | @daemon
+ ]
+ #Ht2 % [| % [| % [| % [ @Ht2 ]
+ %2
+ (* ls0 = ls
+ c = s0
+ l1 = curconfig@[〈c0,false〉]
+ l2 = [〈bar,false〉]
+ c10 = d
+ l3 = qin0@[〈cin,false〉]
+ l4 = qout@〈cout,false〉::〈comma,false〉::〈mv0,false〉::table0
+ rs00 = rs
+ n0 = S n ?
+ *)
+ %{ls} %{s0} %{(curconfig@[〈c0,false〉])}
+ %{([〈bar,false〉])} %{d} %{(qin0@[〈cin,false〉])}
+ %{(qout@〈cout,false〉::〈comma,false〉::〈mv0,false〉::table0)}
+ %{rs} %{n} @daemon (* TODO *)
+ ]
+ ]
+ ]
+ ]
+ | #intape #outtape
+ #ta whd in ⊢ (%→?); #Hta #HR
+ #n #fulltable #s0 #s1 #c0 #c1 #ls #rs #curconfig #newconfig #mv
+ #Htable_len cut (∃t0,table. fulltable =〈bar,false〉::〈t0,false〉::table) [(* 0 < |table| *) @daemon]
+ * #t0 * #table #Hfulltable >Hfulltable -fulltable
+ #Htable #Hmatch #Htape #Hintape #t1' #Ht1'
+ >Hintape in Hta; * * * #c #bc *
+ whd in ⊢ (??%?→?); #HSome destruct (HSome) #Hc #Hta % [@(\P Hc)]
+ cases HR -HR
+ #tb * whd in ⊢ (%→?); #Htb
+ lapply (Htb (〈grid,false〉::ls) (curconfig@[〈c0,false〉]) (table@〈grid,false〉::rs) c t0 ???)
+ [ >Hta >associative_append %
+ | @daemon
+ | @daemon
+ | -Hta -Htb #Htb *
+ #tc * whd in ⊢ (%→?); #Htc cases (Htc … Htable … Htb) -Htb -Htc
+ [| * #Hcurrent #Hfalse @False_ind
+ (* absurd by Hmatch *) @daemon
+ | >(\P Hc) %
+ | (* Htable (con lemma) *) @daemon
+ | (* Hmatch *) @daemon
+ | (* Htable *) @daemon
+ | (* Htable, Hmatch → |config| = n
+ necessaria modifica in R_match_tuple, le dimensioni non corrispondono
+ *) @daemon
+ ]
+ * #table1 * #newc * #mv1 * #table2 * #Htableeq #Htc *
+ [ * #td * whd in ⊢ (%→?); >Htc -Htc * * #c2 * whd in ⊢ (??%?→?); #Hc2 destruct (Hc2)
+ #_ #Htd
+ cut (newc = 〈s1,false〉::newconfig@[〈c1,false〉]) [@daemon] #Hnewc
+ >Hnewc cut (mv1 = 〈mv,false〉)
+ [@daemon] #Hmv1
+ * #te * whd in ⊢ (%→?); #Hte
+ cut (td = midtape STape (〈c0,false〉::reverse STape curconfig@〈c,false〉::〈grid,false〉::ls)
+ 〈grid,false〉
+ ((table1@〈bar,false〉::〈c,false〉::curconfig@[〈c0,false〉])@〈comma,true〉::〈s1,false〉::
+ newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2@〈grid,false〉::rs))
+ [ >Htd @eq_f3 //
+ [ >reverse_append >reverse_single %
+ | >associative_append >associative_append normalize
+ >associative_append >Hmv1 >Hnewc @eq_f @eq_f @eq_f @eq_f @eq_f @eq_f
+ whd in ⊢ (??%?); >associative_append %
+ ]
+ ]
+ -Htd #Htd lapply (Hte … (S n) … Htd … Ht1') -Htd -Hte
+ [ //
+ | (*|curconfig| = |newconfig|*) @daemon
+ | (* Htable → bit_or_null c1 = true *) @daemon
+ | (* only_bits (〈s1,false〉::newconfig) *) @daemon
+ | (* only_bits (curconfig@[〈s0,false〉]) *) @daemon
+ | (* no_marks (reverse ? curconfig) *) @daemon
+ | >Hmv1 in Htableeq; >Hnewc
+ >associative_append >associative_append normalize
+ >associative_append >associative_append
+ #Htableeq <Htableeq // ]
+ * #ls1 * #rs1 * #c2 * * #Hte #Hliftte #Hlegalte
+ whd in ⊢ (%→?); * #_ #Houttape lapply (Houttape … Hte) -Houttape #Houttape
+ whd in Houttape:(???%); whd in Houttape:(???(??%%%));
+ @ex_intro [| @(ex_intro ?? rs1) @ex_intro [| % [ %
+ [ >Houttape @eq_f @eq_f @eq_f @eq_f
+ change with ((〈bar,false〉::〈t0,false〉::table)@?) in ⊢ (???%);
+ >Htableeq >associative_append >associative_append
+ >associative_append normalize >associative_append
+ >associative_append normalize >Hnewc <Hmv1
+ >associative_append normalize >associative_append
+ >Hmv1 %
+ | @Hliftte
+ ]
+ | //
+ ]
+ ]
+ ]
+ | * #td * whd in ⊢ (%→%→?); >Htc * #Htd
+ lapply (Htd ? (refl ??)) normalize in ⊢ (%→?);
+ #Hfalse destruct (Hfalse)
+ ]
+ ]
+| #t1 #t2 #t3 whd in ⊢ (%→%→?); #Ht1 #Ht2
+ #b #Hb >Hb in Ht1; * #Hc #Ht1 lapply (Hc ? (refl ??)) -Hc #Hb' %
+ // cases b in Hb'; normalize #H1 //
+]
+*)
+qed.
+
+(*