opaque union UInt
fun toNat(UInt) -> Nat
fun operator <(UInt,UInt) -> bool
fun operator ≤(x:UInt, y:UInt) {
(x < y or x = y)
}
fun operator >(x:UInt, y:UInt) {
y < x
}
fun operator ≥(x:UInt, y:UInt) {
y ≤ x
}
fun operator +(UInt,UInt) -> UInt
fun operator ∸(UInt,UInt) -> UInt
fun operator *(UInt,UInt) -> UInt
fun sqr(a:UInt) {
a * a
}
^ : (fn UInt, UInt -> UInt)
fun fromNat(Nat) -> UInt
fun max(x:UInt, y:UInt) {
if x < y then
y
else
x
}
fun min(x:UInt, y:UInt) {
if x < y then
x
else
y
}
to_fromNat: (all x:Nat. toNat(fromNat(x)) = x)
toNat_injective: (all x:UInt, y:UInt. (if toNat(x) = toNat(y) then x = y))
from_toNat: (all b:UInt. fromNat(toNat(b)) = b)
fromNat_injective: (all x:Nat, y:Nat. (if fromNat(x) = fromNat(y) then x = y))
toNat_less: (all x:UInt, y:UInt. (if x < y then toNat(x) < toNat(y)))
toNat_less_equal: (all x:UInt, y:UInt. (if x ≤ y then toNat(x) ≤ toNat(y)))
less_toNat: (all x:UInt, y:UInt. (if toNat(x) < toNat(y) then x < y))
uint_less_equal_refl: (all n:UInt. n ≤ n)
uint_less_implies_less_equal: (all x:UInt, y:UInt. (if x < y then x ≤ y))
less_equal_toNat: (all x:UInt, y:UInt. (if toNat(x) ≤ toNat(y) then x ≤ y))
uint_less_irreflexive: (all x:UInt. not (x < x))
uint_less_trans: (all x:UInt, y:UInt, z:UInt. (if (x < y and y < z) then x < z))
uint_not_less_zero: (all x:UInt. not (x < 0))
uint_not_less_implies_less_equal: (all x:UInt, y:UInt. (if not (x < y) then y ≤ x))
uint_le_refl: (all x:UInt. x ≤ x)
uint_le_trans: (all x:UInt, y:UInt, z:UInt. (if (x ≤ y and y ≤ z) then x ≤ z))
uint_bzero_le: (all x:UInt. bzero ≤ x)
uint_le_bzero: (all x:UInt. (if x ≤ bzero then x = bzero))
toNat_add: (all x:UInt, y:UInt. toNat(x + y) = toNat(x) + toNat(y))
fromNat_add: (all x:Nat, y:Nat. fromNat(x + y) = fromNat(x) + fromNat(y))
lit_add_fromNat: (all x:Nat, y:Nat. fromNat(lit(x)) + fromNat(lit(y)) = fromNat(lit(x) + lit(y)))
auto lit_add_fromNat
uint_add_commute: (all x:UInt, y:UInt. x + y = y + x)
uint_add_assoc: (all x:UInt, y:UInt, z:UInt. (x + y) + z = x + (y + z))
auto uint_bzero_add
auto uint_add_bzero
uint_bzero_less_one_add: (all n:UInt. bzero < 1 + n)
uint_add_both_sides_of_equal: (all x:UInt, y:UInt, z:UInt. ((x + y = x + z) ⇔ (y = z)))
uint_add_to_bzero: (all n:UInt, m:UInt. (if n + m = bzero then (n = bzero and m = bzero)))
uint_less_equal_add: (all x:UInt, y:UInt. x ≤ x + y)
uint_less_add_pos: (all x:UInt, y:UInt. (if bzero < y then x < x + y))
toNat_mult: (all x:UInt, y:UInt. toNat(x * y) = toNat(x) * toNat(y))
uint_mult_commute: (all m:UInt, n:UInt. m * n = n * m)
uint_mult_assoc: (all m:UInt, n:UInt, o:UInt. (m * n) * o = m * (n * o))
fromNat_mult: (all x:Nat, y:Nat. fromNat(x * y) = fromNat(x) * fromNat(y))
lit_mult_fromNat: (all x:Nat, y:Nat. fromNat(lit(x)) * fromNat(lit(y)) = fromNat(lit(x) * lit(y)))
auto lit_mult_fromNat
toNat_monus: (all x:UInt, y:UInt. toNat(x ∸ y) = toNat(x) ∸ toNat(y))
uint_bzero_monus: (all x:UInt. bzero ∸ x = bzero)
uint_monus_bzero: (all n:UInt. n ∸ bzero = n)
uint_monus_cancel_bzero: (all n:UInt. n ∸ n = bzero)
uint_add_monus_identity: (all m:UInt, n:UInt. (m + n) ∸ m = n)
auto uint_add_monus_identity
uint_monus_monus_eq_monus_add: (all x:UInt, y:UInt, z:UInt. (x ∸ y) ∸ z = x ∸ (y + z))
uint_monus_order: (all x:UInt, y:UInt, z:UInt. (x ∸ y) ∸ z = (x ∸ z) ∸ y)
uint_add_both_monus: (all z:UInt, y:UInt, x:UInt. (z + y) ∸ (z + x) = y ∸ x)
lit_monus_fromNat: (all x:Nat, y:Nat. fromNat(lit(x)) ∸ fromNat(lit(y)) = fromNat(lit(x) ∸ lit(y)))
auto lit_monus_fromNat
uint_induction: (all P:(fn UInt -> bool), n:UInt. (if (P(0) and (all m:UInt. (if P(m) then P(1 + m)))) then P(n)))
less_fromNat: (all x:Nat, y:Nat. (if x < y then fromNat(x) < fromNat(y)))
less_equal_fromNat: (all x:Nat, y:Nat. (if x ≤ y then fromNat(x) ≤ fromNat(y)))
uint_zero_or_positive: (all x:UInt. (x = 0 or 0 < x))
uint_less_plus1: (all n:UInt. n < 1 + n)
uint_add_both_sides_of_less: (all x:UInt, y:UInt, z:UInt. ((x + y < x + z) ⇔ (y < z)))
less_is_less_equal: (all x:UInt, y:UInt. (x < y) = (1 + x ≤ y))
uint_monus_add_identity: (all n:UInt. (all m:UInt. (if m ≤ n then m + (n ∸ m) = n)))
uint_not_one_add_zero: (all n:UInt. not (1 + n = 0))
uint_zero_le_zero: (all x:UInt. (if x ≤ 0 then x = 0))
uint_not_one_add_le_zero: (all n:UInt. not (1 + n ≤ 0))
uint_not_zero_pos: (all n:UInt. (if not (n = 0) then 0 < n))
uint_pos_not_zero: (all n:UInt. (if 0 < n then not (n = 0)))
recfun operator /(n:UInt, m:UInt) -> UInt
measure n {
if n < m then
0
else
if m = 0 then
0
else
1 + (n ∸ m) / m
}
fun operator %(n:UInt, m:UInt) {
n ∸ (n / m) * m
}
inc_add_one: (all n:UInt. inc(n) = 1 + n)
uint_pos_implies_one_le: (all n:UInt. (if 0 < n then 1 ≤ n))
uint_positive_add_one: (all n:UInt. (if 0 < n then some n':UInt. n = 1 + n'))
uint_zero_or_add_one: (all x:UInt. (x = 0 or some x':UInt. x = 1 + x'))
uint_trichotomy: (all x:UInt, y:UInt. (x < y or x = y or y < x))
uint_less_implies_not_greater: (all x:UInt, y:UInt. (if x < y then not (y < x)))
uint_monus_add_assoc: (all n:UInt, l:UInt, m:UInt. (if m ≤ n then l + (n ∸ m) = (l + n) ∸ m))
uint_zero_mult: (all n:UInt. 0 * n = 0)
auto uint_zero_mult
uint_mult_zero: (all n:UInt. n * 0 = 0)
auto uint_mult_zero
uint_one_mult: (all n:UInt. 1 * n = n)
auto uint_one_mult
uint_mult_one: (all n:UInt. n * 1 = n)
auto uint_mult_one
uint_dist_mult_add: (all a:UInt, x:UInt, y:UInt. a * (x + y) = a * x + a * y)
uint_dist_mult_add_right: (all x:UInt, y:UInt, a:UInt. (x + y) * a = x * a + y * a)
uint_mult_to_zero: (all n:UInt, m:UInt. (if n * m = 0 then (n = 0 or m = 0)))
uint_less_equal_trans: (all m:UInt. (all n:UInt, o:UInt. (if (m ≤ n and n ≤ o) then m ≤ o)))
uint_less_equal_antisymmetric: (all x:UInt, y:UInt. (if (x ≤ y and y ≤ x) then x = y))
fun Even(n:UInt) {
some m:UInt. n = 2 * m
}
fun Odd(n:UInt) {
some m:UInt. n = 1 + 2 * m
}
uint_Even_or_Odd: (all n:UInt. (Even(n) or Odd(n)))
uint_odd_one_even: (all n:UInt. (if Odd(1 + n) then Even(n)))
uint_even_one_odd: (all n:UInt. (if Even(1 + n) then Odd(n)))
uint_Even_not_Odd: (all n:UInt. (Even(n) ⇔ not Odd(n)))
uint_div_mod: (all n:UInt, m:UInt. (if 0 < m then (n / m) * m + n % m = n))
uint_mod_less_divisor: (all n:UInt, m:UInt. (if 0 < m then n % m < m))
fun divides(a:UInt, b:UInt) {
some k:UInt. a * k = b
}
uint_divides_mod: (all d:UInt, m:UInt, n:UInt. (if (divides(d, n) and divides(d, m % n) and 0 < n) then divides(d, m)))
uint_div_cancel: (all y:UInt. (if 0 < y then y / y = 1))
uint_mod_self_zero: (all y:UInt. y % y = 0)
uint_zero_mod: (all x:UInt. 0 % x = 0)
uint_zero_div: (all x:UInt. (if 0 < x then 0 / x = 0))
uint_mod_one: (all n:UInt. n % 1 = 0)
uint_div_one: (all n:UInt. n / 1 = n)
uint_add_div_one: (all n:UInt, m:UInt. (if 0 < m then (n + m) / m = 1 + n / m))
uint_mult_div_inverse: (all n:UInt, m:UInt. (if 0 < m then (n * m) / m = n))
uint_two_mult: (all n:UInt. 2 * n = n + n)
uint_equal_implies_less_equal: (all x:UInt, y:UInt. (if x = y then x ≤ y))
uint_add_both_sides_of_less_equal: (all x:UInt. (all y:UInt, z:UInt. ((x + y ≤ x + z) ⇔ (y ≤ z))))
uint_add_both_sides_of_le_equal: (all x:UInt. (all y:UInt, z:UInt. (x + y ≤ x + z) = (y ≤ z)))
auto uint_add_both_sides_of_le_equal
uint_zero_less_one_add: (all n:UInt. 0 < 1 + n)
uint_zero_le: (all x:UInt. 0 ≤ x)
uint_le_zero: (all x:UInt. (if x ≤ 0 then x = 0))
uint_monus_zero: (all n:UInt. n ∸ 0 = n)
auto uint_monus_zero
uint_zero_add: (all x:UInt. 0 + x = x)
auto uint_zero_add
uint_add_zero: (all x:UInt. x + 0 = x)
auto uint_add_zero
uint_equal: (all x:Nat, y:Nat. (fromNat(lit(x)) = fromNat(lit(y))) = (x = y))
auto uint_equal
uint_monus_cancel: (all n:UInt. n ∸ n = 0)
auto uint_monus_cancel
uint_lit_less_equal: (all x:Nat, y:Nat. (fromNat(lit(x)) ≤ fromNat(lit(y))) = (lit(x) ≤ lit(y)))
auto uint_lit_less_equal
uint_lit_less: (all x:Nat, y:Nat. (fromNat(lit(x)) < fromNat(lit(y))) = (lit(x) < lit(y)))
auto uint_lit_less
uint_zero_less_one_add_true: (all n:UInt. (0 < 1 + n) = true)
auto uint_zero_less_one_add_true
uint_add_to_zero: (all n:UInt, m:UInt. (if n + m = 0 then (n = 0 and m = 0)))
uint_lit_div: (all x:Nat, y:Nat. fromNat(lit(x)) / fromNat(lit(y)) = fromNat(lit(x) / lit(y)))
auto uint_lit_div
uint_less_refl_false: (all x:UInt. (x < x) = false)
auto uint_less_refl_false
uint_one_add_zero_false: (all n:UInt. (1 + n = 0) = false)
auto uint_one_add_zero_false
union Int {
pos(UInt)
negsuc(UInt)
}
abs : (fn Int -> UInt)
- : (fn Int -> Int)
- : (fn UInt -> Int)
+ : (fn Int, Int -> Int)
+ : (fn UInt, Int -> Int)
+ : (fn Int, UInt -> Int)
fun operator -(n:Int, m:Int) {
n + - m
}
- : (fn UInt, Int -> Int)
- : (fn Int, UInt -> Int)
- : (fn UInt, UInt -> Int)
* : (fn Int, Int -> Int)
* : (fn UInt, Int -> Int)
* : (fn Int, UInt -> Int)
/ : (fn Int, Int -> Int)
/ : (fn Int, UInt -> Int)
≤ : (fn Int, Int -> bool)
abs_neg: (all n:Int. abs(- n) = abs(n))
neg_zero: - +0 = +0
neg_involutive: (all n:Int. - (- n) = n)
int_zero_add: (all n:Int. +0 + n = n)
auto int_zero_add
int_add_zero: (all n:Int. n + +0 = n)
auto int_add_zero
int_add_commute: (all x:Int, y:Int. x + y = y + x)
suc_uint_monuso: (all x:UInt, y:UInt. (1 + x) ⊝ (1 + y) = x ⊝ y)
add_commute_uint_int: (all x:UInt, y:Int. x + y = y + x)
int_add_assoc: (all x:Int, y:Int, z:Int. (x + y) + z = x + (y + z))
int_add_inverse: (all x:Int. x + - x = +0)
neg_distr_add: (all x:Int, y:Int. - (x + y) = - x + - y)
int_sub_cancel: (all x:Int. x - x = +0)
int_one_mult: (all x:Int. +1 * x = x)
auto int_one_mult
int_zero_mult: (all x:Int. +0 * x = +0)
auto int_zero_mult
dist_neg_mult: (all x:Int, y:Int. - (x * y) = - x * y)
int_mult_commute: (all x:Int, y:Int. x * y = y * x)
int_mult_one: (all x:Int. x * +1 = x)
auto int_mult_one
int_mult_zero: (all x:Int. x * +0 = +0)
auto int_mult_zero
int_mult_assoc: (all x:Int, y:Int, z:Int. (x * y) * z = x * (y * z))
int_less_equal_refl: (all n:Int. n ≤ n)
int_less_equal_trans: (all m:Int, n:Int, o:Int. (if (m ≤ n and n ≤ o) then m ≤ o))
int_less_equal_antisymmetric: (all x:Int, y:Int. (if (x ≤ y and y ≤ x) then x = y))
lit_add_pos_pos: (all x:Nat, y:Nat. pos(fromNat(lit(x))) + pos(fromNat(lit(y))) = pos(fromNat(lit(x) + lit(y))))
auto lit_add_pos_pos
lit_add_pos_lit: (all x:Nat, y:Nat. pos(fromNat(lit(x))) + fromNat(lit(y)) = pos(fromNat(lit(x) + lit(y))))
auto lit_add_pos_lit
lit_add_lit_pos: (all x:Nat, y:Nat. fromNat(lit(x)) + pos(fromNat(lit(y))) = pos(fromNat(lit(x) + lit(y))))
auto lit_add_lit_pos
lit_add_pos_negsuc_suc: (all x:Nat, y:Nat. pos(fromNat(lit(suc(y)))) + negsuc(fromNat(lit(suc(x)))) = pos(fromNat(lit(y))) + negsuc(fromNat(lit(x))))
auto lit_add_pos_negsuc_suc
lit_add_negsuc_pos_suc: (all x:Nat, y:Nat. negsuc(fromNat(lit(suc(x)))) + pos(fromNat(lit(suc(y)))) = negsuc(fromNat(lit(x))) + pos(fromNat(lit(y))))
auto lit_add_negsuc_pos_suc
lit_add_pos_suc_negsuc_zero: (all x:Nat, y:Nat. pos(fromNat(lit(suc(y)))) + -1 = pos(fromNat(lit(y))))
auto lit_add_pos_suc_negsuc_zero
lit_add_negsuc_zero_pos_suc: (all x:Nat, y:Nat. -1 + pos(fromNat(lit(suc(y)))) = pos(fromNat(lit(y))))
auto lit_add_negsuc_zero_pos_suc
neg_lit_zero: - +0 = +0
auto neg_lit_zero
neg_uint_zero: - 0 = +0
auto neg_uint_zero
neg_pos_lit_suc: (all x:Nat. - pos(fromNat(lit(suc(x)))) = negsuc(fromNat(lit(x))))
auto neg_pos_lit_suc
neg_lit_suc: (all x:Nat. - fromNat(lit(suc(x))) = negsuc(fromNat(lit(x))))
auto neg_lit_suc
neg_negsuc_lit: (all x:Nat. - negsuc(fromNat(lit(x))) = pos(fromNat(lit(suc(x)))))
auto neg_negsuc_lit
abs_lit: (all x:Nat. abs(pos(fromNat(lit(x)))) = fromNat(lit(x)))
auto abs_lit
sign_pos_lit: (all x:Nat. sign(pos(fromNat(lit(x)))) = positive)
auto sign_pos_lit
sign_neg_lit: (all x:Nat. sign(negsuc(fromNat(lit(x)))) = negative)
auto sign_neg_lit
mult_pos_lit_pos_lit: (all x:Nat, y:Nat. pos(fromNat(lit(x))) * pos(fromNat(lit(y))) = pos(fromNat(lit(x) * lit(y))))
auto mult_pos_lit_pos_lit
mult_lit_pos_lit: (all x:Nat, y:Nat. fromNat(lit(x)) * pos(fromNat(lit(y))) = pos(fromNat(lit(x) * lit(y))))
auto mult_lit_pos_lit
mult_pos_lit_lit: (all x:Nat, y:Nat. pos(fromNat(lit(x))) * fromNat(lit(y)) = pos(fromNat(lit(x) * lit(y))))
auto mult_pos_lit_lit
mult_pos_lit_neg_lit: (all x:Nat, y:Nat. pos(fromNat(lit(x))) * negsuc(fromNat(lit(y))) = - pos(fromNat(lit(x)) + fromNat(lit(x)) * fromNat(lit(y))))
auto mult_pos_lit_neg_lit
mult_lit_neg_lit: (all x:Nat, y:Nat. fromNat(lit(x)) * negsuc(fromNat(lit(y))) = - pos(fromNat(lit(x)) + fromNat(lit(x)) * fromNat(lit(y))))
auto mult_lit_neg_lit
mult_neg_lit_pos: (all x:Nat, y:Nat. negsuc(fromNat(lit(x))) * pos(fromNat(lit(y))) = - pos(fromNat(lit(y)) + fromNat(lit(y)) * fromNat(lit(x))))
auto mult_neg_lit_pos
mult_neg_lit_lit: (all x:Nat, y:Nat. negsuc(fromNat(lit(x))) * fromNat(lit(y)) = - pos(fromNat(lit(y)) + fromNat(lit(y)) * fromNat(lit(x))))
auto mult_neg_lit_lit