Changeset 3586 for LTS


Ignore:
Timestamp:
Jul 18, 2015, 6:39:51 PM (4 years ago)
Author:
pellitta
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/variable_stack_pass.ma

    r3585 r3586  
    461461inversion(divide_continuation_on_frames ct [i])
    462462#IH normalize nodelta whd in ⊢(?→%→%); [#_|3:#ABS cases ABS]
    463 [>IH whd in match (frame_assign_var ???); #HN
     463[>IH whd in match (frame_assign_var ???); inversion(new_st)
     464#l #p #Hns #HN]
    464465cases daemon
    465466qed.
     
    469470var_instr_bond_ok st (SEQ … seq opt_l i) ct →
    470471var_instr_bond_ok st i ct.
     472* [|#x #xs] #i #seq #ol #ct whd in ⊢(%→?); inversion(divide_continuation_on_frames ct ?)
     473normalize nodelta [2: #H1 #H2 #H3 #H4|3:#H] [1,2:#ABS cases ABS]
     474cases i whd in match(var_instr_bond_ok ??); inversion(ct)
     475[1,3,5,7: whd in match(var_instr_bond_ok ???);]
     476[#_ whd in match(divide_continuation_on_frames ??);
     477#ABS destruct| #H1 #H2 whd in match (divide_continuation_on_frames ??);
     478#ABS destruct| #H1 #H2 #H3 #H4 whd in match (divide_continuation_on_frames ??); #ABS destruct
     479|#H8 #H9 #H10 #H11 #H12 #H13 #H14 whd in match (divide_continuation_on_frames ??); #ABS destruct
     480|* #fl #fi #H10 cases fl [#fn #ccl|2,3:#op] #H20 [2,3:#H21 whd in match (divide_continuation_on_frames ??);
     481#ABS destruct|whd in match (divide_continuation_on_frames ??);
     482#H29 cases H10 [2:#al #l] whd in match (divide_continuation_on_frames ??);
     483[2:#ABS destruct
     484|1: whd in match(var_instr_bond_ok …);
     485]
     486]
     487]
     488
    471489cases daemon
    472490qed.
Note: See TracChangeset for help on using the changeset viewer.