Changeset 2307 for src/RTLabs/Traces.ma


Ignore:
Timestamp:
Aug 30, 2012, 4:47:58 PM (7 years ago)
Author:
campbell
Message:

Half the proofs for sound cost labelling check.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r2300 r2307  
    722722  @bind_res_value #v #Ev @bind_ok * #Eb whd in ⊢ (??%? → ?); #E destruct
    723723  lapply (Hbody (next fr) (next_ok fr))
    724   generalize in ⊢ (???% → ?);
    725   >Estmt #LP'
    726   whd in ⊢ (% → ?);
    727   * #H1 #H2 [ @H1 | @H2 ]
     724  generalize in ⊢ (?(???%) → ?);
     725  >Estmt #LP' #WS
     726  cases (andb_Prop_true … WS) #H1 #H2 [ @H1 | @H2 ]
    728727(*| * #r * #ls #Estmt
    729728  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
     
    29552954] qed.
    29562955
    2957 lemma Prop_notb : ∀b:bool. notb b → Not (bool_to_Prop b).
    2958 * /2/
    2959 qed.
    2960 
    29612956(* And then we get our counterpart to no_loops_in_tal for calls: *)
    29622957
Note: See TracChangeset for help on using the changeset viewer.