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/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 %]
Note: See TracChangeset for help on using the changeset viewer.