Changeset 2463 for src/common


Ignore:
Timestamp:
Nov 14, 2012, 1:20:24 PM (7 years ago)
Author:
tranquil
Message:

swapped back call_rel and ret_rel...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StatusSimulation.ma

    r2457 r2463  
    3131     necessary for as_after_return (typically just the program counter)
    3232     maybe what function is called too? *)
    33   ; ret_rel : S1 → S2 → Prop
     33  ; call_rel : (Σs.as_classifier S1 s cl_call) →
     34               (Σs.as_classifier S2 s cl_call) → Prop
    3435  ; sim_final :
    3536    ∀st1,st2.sem_rel st1 st2 → as_final … st1 ↔ as_final … st2
     
    4748definition label_rel ≝ λS1,S2,st1,st2.as_label S1 st1 = as_label S2 st2.
    4849
    49 definition call_rel ≝ λS1,S2.λR : status_rel S1 S2.
    50   λs1_pre,s2_pre.
    51   ∀s1_ret,s2_ret.as_after_return S1 s1_pre s1_ret →
    52                  ret_rel ?? R s1_ret s2_ret
     50definition ret_rel ≝ λS1,S2.λR : status_rel S1 S2.
     51  λs1_ret,s2_ret.
     52  ∀s1_pre,s2_pre.as_after_return S1 s1_pre s1_ret →
     53                 call_rel ?? R s1_pre s2_pre
    5354                 as_after_return S2 s2_pre s2_ret.
    5455
     
    474475    ]
    475476  ]
    476   [1,3: @(st1_C_st2 … st1_Rret_st2') assumption
     477  [1,3: @(st1_Rret_st2' … st1_C_st2) assumption
    477478  |*: whd <st1_L_st2' assumption
    478479  ]
     
    514515    ]
    515516  ]
    516   [1,4,7,9: @(st1_C_st2 … st1_Rret_st2') assumption
     517  [1,4,7,9: @(st1_Rret_st2' … st1_C_st2) assumption
    517518  |2,5: lapply st1_L_st2' lapply taa_ncost cases taa2'' -st2_after_ret -st2'
    518519    [1,3: #st2_after_ret * #L whd in ⊢ (?%); <L assumption
Note: See TracChangeset for help on using the changeset viewer.