Changeset 2127 for src/ASM/AssemblyProofSplitSplit.ma
- Timestamp:
- Jun 27, 2012, 4:59:10 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProofSplitSplit.ma
r2123 r2127 203 203 |2: 204 204 whd in ⊢ (??(?%%)%); 205 cut (∃b1,b2,b3,b4,b5,b6,b7,b8,b9,b10,b11. address = [[b1;b2;b3;b4;b5;b6;b7;b8;b9;b10;b11]]) 206 [1: 207 cases daemon (* XXX: easy but massive proof, move into separate lemma *) 208 |2: 209 * * * * * * * #b4 * #b5 210 * #b6 * #b7 * #b8 * #b9 * #b10 * #b11 #address_refl >address_refl 211 normalize in match (fetch ??); <plus_n_Sm @eq_f 212 @commutative_plus 213 ] 205 cases (bitvector_11_cases address) 206 * * * * * * #b4 * #b5 207 * #b6 * #b7 * #b8 * #b9 * #b10 * #b11 #address_refl >address_refl 208 normalize in match (fetch ??); <plus_n_Sm @eq_f 209 @commutative_plus 214 210 ] 215 211 |5: (* Call *)
Note: See TracChangeset
for help on using the changeset viewer.