-lemma sem_exec_action : Realize ? exec_action R_exec_action.
-#intape
-cases (sem_seq … sem_init_copy
- (sem_seq … sem_copy
- (sem_seq … (sem_move_r …) sem_move_tape )) intape)
-#k * #outc * #Hloop #HR
-@(ex_intro ?? k) @(ex_intro ?? outc) % [ @Hloop ] -Hloop
-#n #curconfig #ls #rs #c0 #c1 #s0 #s1 #table1 #newconfig #mv #table2
-#Htable #Hcurconfig1 #Hcurconfig2 #Hnewconfig #Hc1 #Hlen #Htape #Hintape #t1' #Ht1'
-cases HR -HR #ta * whd in ⊢ (%→?); #Hta
-lapply (Hta (〈c0,false〉::curconfig) table1 s0 ls s1
- (newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2@〈grid,false〉::rs) … Hintape) -Hta
+(*lemma GRealize_to_Realize :
+ ∀sig,M,R.GRealize sig M (λx.True) R → Realize sig M R.
+#sig #M #R #HR #t @HR //
+qed.*)
+
+lemma sem_exec_action : GRealize ? exec_action Pre_exec_action R_exec_action.
+@(sem_seq_app_guarded … (Realize_to_GRealize … sem_init_copy) ???)
+[3:@(sem_seq_app_guarded … sem_copy)
+ [3:@(sem_seq_app_guarded … (Realize_to_GRealize … (sem_move_r STape)))
+ [3:@(Realize_to_GRealize … (sem_move_tape …))
+ |@(λt.True)
+ |4://
+ |5:@sub_reflexive]
+ |@(λt.True)
+ |4://
+ |5:@sub_reflexive]
+|4:#t1 #t2
+ * #n * #curconfig * #ls * #rs * #c0 * #c1 * #s0 * #s1 * #table1 * #newconfig
+ * #mv * #table2 * * * * * * *
+ #Htable #Hcurconfig1 #Hcurconfig2 #Hnewconfig #Hc1 #Hlen #Htape #Ht1
+ whd in ⊢ (%→?); >Ht1 #HR
+ lapply (HR (〈c0,false〉::curconfig) table1 s0 ls s1
+ (newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2@〈grid,false〉::rs) ???? (refl ??))
+ [(*Hcurconfig2*) @daemon
+ |(*by Htable *) @daemon
+ |(*Hcurconfig2*) @daemon
+ |(*Hcurconfig1*) @daemon ]
+ -HR #Ht2 whd
+ %{(〈grid,false〉::ls)} %{s0} %{s1} %{c0} %{c1} %{(〈mv,false〉::table2@〈grid,false〉::rs)}
+ %{newconfig} %{(〈comma,false〉::reverse ? table1)} %{curconfig} >Ht2
+ % [ % [ % [ % [ % [ % [ % [ %
+ [ %
+ |(*by Htabel*) @daemon ]
+ |(*by Htable*) @daemon ]
+ |// ]
+ |>Hlen % ]
+ |@Hcurconfig2 ]
+ |@Hnewconfig ]
+ |cases Htape * * // ]
+ | // ]
+ |1,2:skip]
+#ta #outtape #HR #n #curconfig #ls #rs #c0 #c1 #s0 #s1 #table1 #newconfig #mv
+#table2 #Htable #Hcurconfig1 #Hcurconfig2 #Hnewconfig #Hbitnullc1 #Hlen #Htape
+#Hta #ta' #Hta'
+cases HR -HR #tb * whd in ⊢ (%→?); #Htb
+lapply (Htb (〈c0,false〉::curconfig) table1 s0 ls s1
+ (newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2@〈grid,false〉::rs)
+ ???? Hta) -Htb