Changeset 2127


Ignore:
Timestamp:
Jun 27, 2012, 4:59:10 PM (5 years ago)
Author:
sacerdot
Message:

Last daemon closed

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplitSplit.ma

    r2123 r2127  
    203203    |2:
    204204      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
    214210    ]
    215211  |5: (* Call *)
Note: See TracChangeset for help on using the changeset viewer.