Changeset 2191


Ignore:
Timestamp:
Jul 17, 2012, 2:01:05 AM (5 years ago)
Author:
sacerdot
Message:

Only one daemon left.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2190 r2191  
    10421042      cases (IH ?) -IH
    10431043      [2: %1 cases OR_lt_eq
    1044         [ normalize nodelta >nat_of_bitvector_add
    1045           [2: cases daemon (*CSC: should be true*)]
     1044        [ normalize nodelta #LT lapply LT >nat_of_bitvector_add
     1045          [2: >nat_of_bitvector_bitvector_of_nat_inverse [2: //]
     1046            cases (le_to_or_lt_eq … (? : nat_of_bitvector … ppc < 2^16))
     1047            [ #X <plus_n_Sm <plus_n_O @X
     1048            | #abs @⊥
     1049              cut (∀n,m,r. m + r = 2^n → add n (bitvector_of_nat n m) (bitvector_of_nat n r) = zero n)
     1050              [ cases daemon (* CSC: put in library *) ] #add_overflow
     1051              <(bitvector_of_nat_inverse_nat_of_bitvector … ppc) in LT;
     1052              >add_overflow [2: <plus_n_Sm <plus_n_O assumption ]
     1053              #abs' @(absurd … abs') normalize in ⊢ (? (??%));
     1054              @not_le_Sn_O
     1055            | @(lt_to_le_to_lt … ppc_ok) assumption ]]
    10461056          >nat_of_bitvector_bitvector_of_nat_inverse [2: // ]
    10471057          <plus_n_Sm <plus_n_O #X lapply (le_S_S_to_le … X) -X #X
Note: See TracChangeset for help on using the changeset viewer.