Changeset 1958


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

Marked divergence in StatusProofs?.ma

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r1952 r1958  
    2626  whd in match ticks_of; normalize nodelta <EQppc #H2 >EQ2 normalize nodelta
    2727  lapply (snd_fetch_pseudo_instruction instr_list ppc) >EQ2 #EQnewppc >EQnewppc
     28  inversion pi
     29  [2,3:
     30    #comment_or_cost #instr_refl #next_internal_pseudo_refl
     31    %{0} @split_eq_status whd in match execute_1_pseudo_instruction;
     32    whd in match execute_1_pseudo_instruction0; normalize nodelta
     33    whd in match ticks_of0; normalize nodelta //
     34    [1:
     35      destruct /demod/
     36    |2:
     37    |3:
     38    |4:
     39    |5:
     40    |6:
     41    ]
     42 
    2843  lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … policy … ppc pi … EQlookup_labels EQlookup_datalabels ?)
    2944  [>EQ2 %]
  • 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.