Changeset 3586

Timestamp:

Jul 18, 2015, 6:39:51 PM (4 years ago)

Author:

pellitta

Message:

 

File:

• LTS/variable_stack_pass.ma (modified) (2 diffs)

LTS/variable_stack_pass.ma

@@ -461 +461 @@
 inversion(divide_continuation_on_frames ct [i]) 
 #IH normalize nodelta whd in ⊢(?→%→%); [#_|3:#ABS cases ABS]
-[>IH whd in match (frame_assign_var ???); #HN
+[>IH whd in match (frame_assign_var ???); inversion(new_st)
+#l #p #Hns #HN]
 cases daemon
 qed.
@@ -469 +470 @@
 var_instr_bond_ok st (SEQ … seq opt_l i) ct → 
 var_instr_bond_ok st i ct.
+* [|#x #xs] #i #seq #ol #ct whd in ⊢(%→?); inversion(divide_continuation_on_frames ct ?)
+normalize nodelta [2: #H1 #H2 #H3 #H4|3:#H] [1,2:#ABS cases ABS]
+cases i whd in match(var_instr_bond_ok ??); inversion(ct)
+[1,3,5,7: whd in match(var_instr_bond_ok ???);]
+[#_ whd in match(divide_continuation_on_frames ??);
+#ABS destruct| #H1 #H2 whd in match (divide_continuation_on_frames ??);
+#ABS destruct| #H1 #H2 #H3 #H4 whd in match (divide_continuation_on_frames ??); #ABS destruct
+|#H8 #H9 #H10 #H11 #H12 #H13 #H14 whd in match (divide_continuation_on_frames ??); #ABS destruct
+|* #fl #fi #H10 cases fl [#fn #ccl|2,3:#op] #H20 [2,3:#H21 whd in match (divide_continuation_on_frames ??);
+#ABS destruct|whd in match (divide_continuation_on_frames ??);
+#H29 cases H10 [2:#al #l] whd in match (divide_continuation_on_frames ??);
+[2:#ABS destruct
+|1: whd in match(var_instr_bond_ok …);
+]
+]
+]
+
 cases daemon
 qed.