+ ]
+]
+qed.
+
+(*
+if is_false(current) (* current state is not final *)
+ then init_match;
+ match_tuple;
+ if is_marked(current) = false (* match ok *)
+ then
+ exec_action
+ move_r;
+ else sink;
+ else nop;
+*)
+
+definition uni_step ≝
+ ifTM ? (test_char STape (λc.\fst c == bit false))
+ (single_finalTM ?
+ (init_match · match_tuple ·
+ (ifTM ? (test_char ? (λc.¬is_marked ? c))
+ (exec_action · move_r …)
+ (nop ?) tc_true)))
+ (nop ?) tc_true.
+
+definition R_uni_step_true ≝ λt1,t2.
+ ∀n,table,s0,s1,c0,c1,ls,rs,curconfig,newconfig,mv.
+ 0 < |table| → table_TM (S n) table →
+ match_in_table (S n) (〈s0,false〉::curconfig) 〈c0,false〉
+ (〈s1,false〉::newconfig) 〈c1,false〉 〈mv,false〉 table →
+ legal_tape ls 〈c0,false〉 rs →
+ t1 = midtape STape (〈grid,false〉::ls) 〈s0,false〉
+ (curconfig@〈c0,false〉::〈grid,false〉::table@〈grid,false〉::rs) →
+ ∀t1'.t1' = lift_tape ls 〈c0,false〉 rs →
+ s0 = bit false ∧
+ ∃ls1,rs1,c2.
+ (t2 = midtape STape (〈grid,false〉::ls1) 〈s1,false〉
+ (newconfig@〈c2,false〉::〈grid,false〉::table@〈grid,false〉::rs1) ∧
+ lift_tape ls1 〈c2,false〉 rs1 =
+ tape_move STape t1' (map_move c1 mv) ∧ legal_tape ls1 〈c2,false〉 rs1).
+
+definition R_uni_step_false ≝ λt1,t2.
+ ∀b. current STape t1 = Some ? 〈bit b,false〉 → b = true ∧ t2 = t1.
+
+(*axiom sem_match_tuple : Realize ? match_tuple R_match_tuple.*)
+
+definition us_acc : states ? uni_step ≝ (inr … (inl … (inr … start_nop))).
+
+definition Pre_uni_step ≝ λt1.
+ ∃n,table,s0,s1,c0,c1,ls,rs,curconfig,newconfig,mv.
+ 0 < |table| ∧ table_TM (S n) table ∧
+ match_in_table (S n) (〈s0,false〉::curconfig) 〈c0,false〉
+ (〈s1,false〉::newconfig) 〈c1,false〉 〈mv,false〉 table ∧
+ legal_tape ls 〈c0,false〉 rs ∧
+ t1 = midtape STape (〈grid,false〉::ls) 〈s0,false〉
+ (curconfig@〈c0,false〉::〈grid,false〉::table@〈grid,false〉::rs).
+
+lemma sem_uni_step :
+ accGRealize ? uni_step us_acc Pre_uni_step
+ R_uni_step_true R_uni_step_false.
+@(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