Changeset 2195

Timestamp:

Jul 17, 2012, 10:48:45 AM (5 years ago)

Author:

mulligan

Message:

Got AssemblyProof?.ma compiling again using daemons.

File:

• src/ASM/AssemblyProof.ma (modified) (2 diffs)

src/ASM/AssemblyProof.ma

@@ -255 +255 @@
           >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels
           [>eq_assembly_1_pseudoinstruction |2: skip] #OK >OK <EQlen *
-          [2: * #EQ1 #EQ2 @⊥ <EQ1 in EQlen_assembled';
-              <add_bitvector_of_nat_Sm >add_commutative
-              >bitvector_of_nat_inverse_nat_of_bitvector >OK >EQ2
-              lapply (eq_f … (bitvector_of_nat 16) … EQ2) -EQ2
-              <add_bitvector_of_nat_plus >bitvector_of_nat_inverse_nat_of_bitvector
-              #X >X #Y @NOT_EMPTY <Y >bitvector_of_nat_exp_zero % ]
+          [2: * #EQ1 #EQ2
+              @(lt_to_le_to_lt … (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat … (|assembled|)))))
+              [1: @lt_to_lt_nat_of_bitvector_add try assumption
+                  cases daemon (* XXX: two cases to prove, both true *)
+              |2: cases daemon (* XXX: use monotonicity of sigma *)
+              ]
+          ]
           cases (le_to_or_lt_eq … instr_list_ok)
           [2: #abs @⊥ >abs in EQlen_assembled'; >bitvector_of_nat_exp_zero >sigma_zero
@@ -282 +283 @@
                 >nat_of_bitvector_add <plus_n_Sm <plus_n_O try assumption
                 @(transitive_le … instr_list_ok') @le_S_S assumption
-            | * #EQ1 @⊥ >EQ1 in EQlen_assembled'; assumption ]]]
+            | #EQ1 @⊥ >EQ1 in EQlen_assembled'; assumption ]]]
     |2:
       -assembly_ok -load_code_memory_ok generalize in match (sigma ppc); >EQlen -len