Changeset 3592

Timestamp:

Jul 25, 2015, 6:09:09 PM (4 years ago)

Author:

pellitta

Message:

 

File:

• LTS/variable_stack_pass.ma (modified) (1 diff)

LTS/variable_stack_pass.ma

@@ -474 +474 @@
 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 ⊢(%→?); 
+#act_frm (* [|#x #xs]*) #i #seq #ol #ct whd in ⊢(%→?); 
 <(append_nil … [?]) >divide_continuation_on_frame_app
 inversion(divide_continuation_on_frames ct ?)
-normalize nodelta [2,4: #y #ys #_] #EQdivide
-[1,3:#ABS cases ABS
-|2,4:
-** * [2,4:#m #Hm] #H2 #H3 whd in match(var_instr_bond_ok ???);
-inversion (divide_continuation_on_frames ct [i]) normalize nodelta
-<(append_nil … [?]) >divide_continuation_on_frame_app
->EQdivide normalize nodelta /2 by absurd/
-#lfi #llfi #H9 #H10 destruct % 
-[1,3,5,7: %
-  [1,3,5,7: 
-  |2,4,6,8: /2 by / 
-  ]
-|2,4,6,8:
-]
-
-]
-
-
-
-(*
- [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 …);
-]
-]
-]
-*)
+normalize nodelta [2,4: #x #xs #_] #EQdivide 
+
+cases act_frm -act_frm [2,4: #y #ys] **
+#H1 #H2 #H3 whd in match (var_instr_bond_ok ???);
+<(append_nil … [?]) >divide_continuation_on_frame_app >EQdivide normalize nodelta
+% // % //
 cases daemon
 qed.