Ignore:
Timestamp:
May 16, 2012, 4:47:56 PM (8 years ago)
Author:
mulligan
Message:

Marked divergence in StatusProofs?.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/StatusProofs.ma

    r1710 r1958  
    282282qed.
    283283
     284lemma set_clock_set_program_counter:
     285  ∀T,cm,s,x,y.
     286    set_clock T cm (set_program_counter … s x) y =
     287      set_program_counter … (set_clock … s y) x.
     288 //
     289qed.
     290
    284291lemma set_low_internal_ram_set_high_internal_ram:
    285292 ∀T,cm,s,x,y.
     
    354361qed.
    355362
     363(* XXX: this was compiling before! *)
    356364lemma program_counter_set_arg_1:
    357365  ∀m, cm, s, addr, v.
Note: See TracChangeset for help on using the changeset viewer.