| 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 ]] |
