Changeset 3495


Ignore:
Timestamp:
Sep 25, 2014, 2:24:12 PM (5 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3494 r3495  
    987987      #EQlabels >act_op @IH
    988988  ]
     989  try //
     990  [2: cases(static_analisys_ok … c … (pc … st3) … EQmap) // #EQ #_ <EQ whd in match (big_op ??);
     991      >neutral_l assumption
     992   |3: >neutral_r lapply(instr_map_ok … good … good_a1)
     993       [ whd in ⊢ (??%?); @eqb_elim
     994         [ #ABS cases(absurd ? ABS Hpc) ] #_ normalize nodelta whd in match fetch_state;
     995         normalize nodelta >EQi in ⊢ (??%?); %
     996       | assumption
     997       |*:
     998       ]
     999       normalize in ⊢ (% → ?); #H @H
     1000   
     1001 
    9891002   [2: assumption | | assumption | assumption | cases daemon (*TODO*)|
    9901003      whd in ⊢ (??%%);
Note: See TracChangeset for help on using the changeset viewer.