Changeset 2244


Ignore:
Timestamp:
Jul 24, 2012, 2:47:26 PM (7 years ago)
Author:
sacerdot
Message:

Technical lemma used.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyStep.ma

    r2243 r2244  
    15701570    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    15711571    *)
    1572   | (* out_of_program_none *) cases daemon(*
    1573     @jump_expansion_step7 try assumption
    1574     @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))))
    1575     *)
    1576   | (* lookup p = lookup old_sigma + added *) cases daemon(*
    1577     @jump_expansion_step8 try assumption
    1578     try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))   
    1579     @(proj2 ?? (proj1 ?? Hpolicy)) *)
     1572  | (* out_of_program_none *)
     1573    @(jump_expansion_step7 … Heq2b)
     1574    @(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)))
     1575  | (* lookup p = lookup old_sigma + added *)
     1576    @(jump_expansion_step8 (pi1 ?? program) (pi1 ?? labels) (pi1 ?? old_sigma) … Holdeq … Heq1 Heq2a Heq2b) try assumption
     1577    [ cases (pi2 … old_sigma) * #_ #H1 #H2 % assumption
     1578    | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
     1579    | @(proj2 ?? (proj1 ?? Hpolicy)) ]
    15801580  | (* sigma_safe *) cases daemon (*
    15811581    @jump_expansion_step9 try assumption
Note: See TracChangeset for help on using the changeset viewer.