Changeset 2195


Ignore:
Timestamp:
Jul 17, 2012, 10:48:45 AM (5 years ago)
Author:
mulligan
Message:

Got AssemblyProof?.ma compiling again using daemons.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2194 r2195  
    255255          >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels
    256256          [>eq_assembly_1_pseudoinstruction |2: skip] #OK >OK <EQlen *
    257           [2: * #EQ1 #EQ2 @⊥ <EQ1 in EQlen_assembled';
    258               <add_bitvector_of_nat_Sm >add_commutative
    259               >bitvector_of_nat_inverse_nat_of_bitvector >OK >EQ2
    260               lapply (eq_f … (bitvector_of_nat 16) … EQ2) -EQ2
    261               <add_bitvector_of_nat_plus >bitvector_of_nat_inverse_nat_of_bitvector
    262               #X >X #Y @NOT_EMPTY <Y >bitvector_of_nat_exp_zero % ]
     257          [2: * #EQ1 #EQ2
     258              @(lt_to_le_to_lt … (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat … (|assembled|)))))
     259              [1: @lt_to_lt_nat_of_bitvector_add try assumption
     260                  cases daemon (* XXX: two cases to prove, both true *)
     261              |2: cases daemon (* XXX: use monotonicity of sigma *)
     262              ]
     263          ]
    263264          cases (le_to_or_lt_eq … instr_list_ok)
    264265          [2: #abs @⊥ >abs in EQlen_assembled'; >bitvector_of_nat_exp_zero >sigma_zero
     
    282283                >nat_of_bitvector_add <plus_n_Sm <plus_n_O try assumption
    283284                @(transitive_le … instr_list_ok') @le_S_S assumption
    284             | * #EQ1 @⊥ >EQ1 in EQlen_assembled'; assumption ]]]
     285            | #EQ1 @⊥ >EQ1 in EQlen_assembled'; assumption ]]]
    285286    |2:
    286287      -assembly_ok -load_code_memory_ok generalize in match (sigma ppc); >EQlen -len
Note: See TracChangeset for help on using the changeset viewer.