union Nat {
zero
suc(Nat)
}
recursive operator +(Nat,Nat) -> Nat{
operator +(0, m) = m
operator +(suc(n), m) = suc(n + m)
}
recursive operator *(Nat,Nat) -> Nat{
operator *(0, m) = 0
operator *(suc(n), m) = m + n * m
}
recursive expt(Nat,Nat) -> Nat{
expt(0, n) = 1
expt(suc(p), n) = n * expt(p, n)
}
fun operator ^(a:Nat, b:Nat) {
expt(b, a)
}
recursive max(Nat,Nat) -> Nat{
max(0, n) = n
max(suc(m'), n) =
switch n {
case 0 {
suc(m')
}
case suc(n') {
suc(max(m', n'))
}
}
}
recursive min(Nat,Nat) -> Nat{
min(0, n) = 0
min(suc(m'), n) =
switch n {
case 0 {
0
}
case suc(n') {
suc(min(m', n'))
}
}
}
fun pred(n:Nat) {
switch n {
case 0 {
0
}
case suc(n') {
n'
}
}
}
recursive operator -(Nat,Nat) -> Nat{
operator -(0, m) = 0
operator -(suc(n), m) =
switch m {
case 0 {
suc(n)
}
case suc(m') {
n - m'
}
}
}
recursive operator ≤(Nat,Nat) -> bool{
operator ≤(0, m) = true
operator ≤(suc(n'), m) =
switch m {
case 0 {
false
}
case suc(m') {
n' ≤ m'
}
}
}
fun operator <(x:Nat, y:Nat) {
suc(x) ≤ y
}
fun operator >(x:Nat, y:Nat) {
y < x
}
fun operator ≥(x:Nat, y:Nat) {
y ≤ x
}
recursive summation(Nat,Nat,(fn Nat -> Nat)) -> Nat{
summation(0, begin, f) = 0
summation(suc(k), begin, f) = f(begin) + summation(k, suc(begin), f)
}
recursive iterate<T>(Nat,T,(fn T -> T)) -> T{
iterate(0, init, f) = init
iterate(suc(n), init, f) = f(iterate(n, init, f))
}
recursive pow2(Nat) -> Nat{
pow2(0) = 1
pow2(suc(n')) = 2 * pow2(n')
}
recursive equal(Nat,Nat) -> bool{
equal(0, n) =
switch n {
case 0 {
true
}
case suc(n') {
false
}
}
equal(suc(m'), n) =
switch n {
case 0 {
false
}
case suc(n') {
equal(m', n')
}
}
}
recursive dist(Nat,Nat) -> Nat{
dist(0, n) = n
dist(suc(m), n) =
switch n {
case 0 {
suc(m)
}
case suc(n') {
dist(m, n')
}
}
}
zero_add: (all n:Nat. 0 + n = n)
add_zero: (all n:Nat. n + 0 = n)
suc_add: (all m:Nat, n:Nat. suc(m) + n = suc(m + n))
suc_one_add: (all n:Nat. suc(n) = 1 + n)
one_add_suc: (all n:Nat. 1 + n = suc(n))
not_one_add_zero: (all n:Nat. not (1 + n = 0))
add_suc: (all m:Nat. (all n:Nat. m + suc(n) = suc(m + n)))
add_commute: (all n:Nat. (all m:Nat. n + m = m + n))
one_add: (all m:Nat. 1 + m = suc(m))
add_one: (all m:Nat. m + 1 = suc(m))
add_assoc: (all m:Nat, n:Nat, o:Nat. (m + n) + o = m + (n + o))
assoc_add: (all m:Nat, n:Nat, o:Nat. m + (n + o) = (m + n) + o)
add_both_sides_of_equal: (all x:Nat. (all y:Nat, z:Nat. ((x + y = x + z) ⇔ (y = z))))
left_cancel: (all x:Nat. (all y:Nat, z:Nat. (if x + y = x + z then y = z)))
add_to_zero: (all n:Nat. (all m:Nat. (if n + m = 0 then (n = 0 and m = 0))))
zero_sub: (all x:Nat. 0 - x = 0)
sub_cancel: (all n:Nat. n - n = 0)
sub_zero: (all n:Nat. n - 0 = n)
pred_one: pred(1) = 0
pred_suc_n: (all n:Nat. pred(suc(n)) = n)
sub_one_pred: (all x:Nat. x - 1 = pred(x))
add_sub_identity: (all m:Nat. (all n:Nat. (m + n) - m = n))
sub_sub_eq_sub_add: (all x:Nat. (all y:Nat. (all z:Nat. (x - y) - z = x - (y + z))))
sub_order: (all x:Nat, y:Nat, z:Nat. (x - y) - z = (x - z) - y)
zero_mult: (all n:Nat. 0 * n = 0)
mult_zero: (all n:Nat. n * 0 = 0)
suc_mult: (all m:Nat, n:Nat. suc(m) * n = n + m * n)
mult_suc: (all m:Nat. (all n:Nat. m * suc(n) = m + m * n))
mult_commute: (all m:Nat. (all n:Nat. m * n = n * m))
one_mult: (all n:Nat. 1 * n = n)
mult_one: (all n:Nat. n * 1 = n)
mult_to_zero: (all n:Nat, m:Nat. (if m * n = 0 then (m = 0 or n = 0)))
one_mult_one: (all x:Nat, y:Nat. (if x * y = 1 then (x = 1 and y = 1)))
two_mult: (all n:Nat. 2 * n = n + n)
dist_mult_add: (all a:Nat, x:Nat, y:Nat. a * (x + y) = a * x + a * y)
dist_mult_add_right: (all x:Nat, y:Nat, a:Nat. (x + y) * a = x * a + y * a)
mult_assoc: (all m:Nat. (all n:Nat, o:Nat. (m * n) * o = m * (n * o)))
mult_right_cancel: (all m:Nat, n:Nat, o:Nat. (if m * suc(o) = n * suc(o) then m = n))
mult_left_cancel: (all m:Nat, a:Nat, b:Nat. (if suc(m) * a = suc(m) * b then a = b))
suc_less_equal_iff_less_equal_suc: (all x:Nat, y:Nat. ((x ≤ y) ⇔ (suc(x) ≤ suc(y))))
less_suc_iff_suc_less: (all x:Nat, y:Nat. ((x < y) ⇔ (suc(x) < suc(y))))
not_less_zero: (all x:Nat. not (x < 0))
less_equal_implies_less_or_equal: (all x:Nat. (all y:Nat. (if x ≤ y then (x < y or x = y))))
less_equal_not_equal_implies_less: (all x:Nat, y:Nat. (if (x ≤ y and not (x = y)) then x < y))
less_implies_less_equal: (all x:Nat. (all y:Nat. (if x < y then x ≤ y)))
less_equal_refl: (all n:Nat. n ≤ n)
equal_implies_less_equal: (all x:Nat, y:Nat. (if x = y then x ≤ y))
less_equal_antisymmetric: (all x:Nat. (all y:Nat. (if (x ≤ y and y ≤ x) then x = y)))
less_equal_trans: (all m:Nat. (all n:Nat, o:Nat. (if (m ≤ n and n ≤ o) then m ≤ o)))
not_less_implies_less_equal: (all x:Nat. (all y:Nat. (if not (x < y) then y ≤ x)))
less_irreflexive: (all x:Nat. not (x < x))
less_not_equal: (all x:Nat, y:Nat. (if x < y then not (x = y)))
greater_not_equal: (all x:Nat, y:Nat. (if x > y then not (x = y)))
trichotomy: (all x:Nat. (all y:Nat. (x < y or x = y or y < x)))
trichotomy2: (all y:Nat, x:Nat. (if (not (x = y) and not (x < y)) then y < x))
dichotomy: (all x:Nat, y:Nat. (x ≤ y or y < x))
zero_or_positive: (all x:Nat. (x = 0 or 0 < x))
zero_le_zero: (all x:Nat. (if x ≤ 0 then x = 0))
not_less_equal_iff_greater: (all x:Nat, y:Nat. (not (x ≤ y) ⇔ (y < x)))
less_implies_not_greater: (all x:Nat. (all y:Nat. (if x < y then not (y < x))))
not_less_equal_less_equal: (all x:Nat, y:Nat. (if not (x ≤ y) then y ≤ x))
not_zero_suc: (all n:Nat. (if not (n = 0) then some n':Nat. n = suc(n')))
positive_suc: (all n:Nat. (if 0 < n then some n':Nat. n = suc(n')))
less_equal_add: (all x:Nat. (all y:Nat. x ≤ x + y))
less_equal_add_left: (all x:Nat, y:Nat. y ≤ x + y)
less_equal_suc: (all n:Nat. n ≤ suc(n))
add_mono: (all a:Nat, b:Nat, c:Nat, d:Nat. (if (a ≤ c and b ≤ d) then a + b ≤ c + d))
add_pos_nonneg: (all a:Nat, b:Nat. (if 0 < a then 0 < a + b))
less_one_add: (all n:Nat. 0 < 1 + n)
add_both_sides_of_less_equal: (all x:Nat. (all y:Nat, z:Nat. ((x + y ≤ x + z) ⇔ (y ≤ z))))
add_both_sides_of_less: (all x:Nat, y:Nat, z:Nat. ((x + y < x + z) ⇔ (y < z)))
mult_mono_le: (all n:Nat. (all x:Nat, y:Nat. (if x ≤ y then n * x ≤ n * y)))
mult_mono_le_r: (all n:Nat. (all x:Nat, y:Nat. (if x ≤ y then x * n ≤ y * n)))
sub_add_assoc: (all n:Nat. (all l:Nat, m:Nat. (if m ≤ n then l + (n - m) = (l + n) - m)))
sub_suc_identity: (all n:Nat. (if 0 < n then suc(n - 1) = n))
sub_add_identity: (all n:Nat. (all m:Nat. (if m ≤ n then m + (n - m) = n)))
sub_right_cancel: (all x:Nat, y:Nat, a:Nat. (if (x - a = y - a and a ≤ x and a ≤ y) then x = y))
less_equal_add_sub: (all m:Nat. (all n:Nat, o:Nat. (if (n ≤ m and m ≤ n + o) then m - n ≤ o)))
sub_zero_iff_less_eq: (all x:Nat, y:Nat. ((x ≤ y) ⇔ (x - y = 0)))
sub_pos_iff_less: (all x:Nat, y:Nat. ((y < x) ⇔ (0 < x - y)))
le_exists_sub: (all n:Nat, m:Nat. (if n ≤ m then some x:Nat. m = n + x))
less_trans: (all m:Nat, n:Nat, o:Nat. (if (m < n and n < o) then m < o))
greater_any_zero: (all x:Nat, y:Nat. (if x < y then 0 < y))
dist_mult_sub: (all x:Nat. (all y:Nat, z:Nat. x * (y - z) = x * y - x * z))
mult_pos_nonneg: (all a:Nat, b:Nat. (if (0 < a and 0 < b) then 0 < a * b))
mult_lt_mono_l: (all c:Nat, a:Nat, b:Nat. (if c > 0 then (if a < b then a * c < b * c)))
mult_lt_mono_r: (all c:Nat, a:Nat, b:Nat. (if 0 < c then (if a * c < b * c then a < b)))
max_greater_right: (all y:Nat, x:Nat. y ≤ max(x, y))
max_greater_left: (all x:Nat, y:Nat. x ≤ max(x, y))
max_is_left_or_right: (all x:Nat, y:Nat. (max(x, y) = x or max( x,y
)=y))zero_max: (allx: Nat.max(0 , x)
=x)max_zero:(allx:Nat .max(x ,0 ) =x
)max_symmetric :(allx:Nat, y:Nat. max(x, y) = max(y, x))
max_assoc: (all x:Nat, y:Nat, z:Nat. max(max(x, y), z) = max(x, max(y, z)))
max_equal_greater_right: (all x:Nat, y:Nat. (if x ≤ y then max(x, y) = y))
max_equal_greater_left: (all x:Nat, y:Nat. (if y ≤ x then max(x, y) = x))
max_less_equal: (all x:Nat, y:Nat, z:Nat. (if (x ≤ z and y ≤ z) then max(x, y) ≤ z))
recursive parity(Nat,bool) -> bool{
parity(0, b) = b
parity(suc(n'), b) = parity(n', not b)
}
fun is_even(n:Nat) {
parity(n, true)
}
fun is_odd(n:Nat) {
parity(n, false)
}
fun Even(n:Nat) {
some m:Nat. n = 2 * m
}
fun Odd(n:Nat) {
some m:Nat. n = suc(2 * m)
}
two_even: (all n:Nat. Even(2 * n))
one_two_odd: (all n:Nat. Odd(1 + 2 * n))
even_or_odd: (all n:Nat. (is_even(n) or is_odd(n)))
addition_of_evens: (all x:Nat, y:Nat. (if (Even(x) and Even(y)) then Even(x + y)))
is_even_odd: (all n:Nat. ((if is_even(n) then Even(n)) and (if is_odd(n) then Odd(n))))
Even_or_Odd: (all n:Nat. (Even(n) or Odd(n)))
odd_one_even: (all n:Nat. (if Odd(1 + n) then Even(n)))
even_one_odd: (all n:Nat. (if Even(1 + n) then Odd(n)))
Even_not_Odd: (all n:Nat. (Even(n) ⇔ not Odd(n)))
summation_cong: (all k:Nat. (all f:(fn Nat -> Nat), g:(fn Nat -> Nat), s:Nat, t:Nat. (if (all i:Nat. (if i < k then f(s + i) = g(t + i))) then summation(k, s, f) = summation(k, t, g))))
summation_suc: (all k:Nat. (all f:(fn Nat -> Nat), g:(fn Nat -> Nat), s:Nat. (if (all i:Nat. f(i) = g(suc(i))) then summation(k, s, f) = summation(k, suc(s), g))))
summation_add: (all a:Nat. (all b:Nat, s:Nat, t:Nat, f:(fn Nat -> Nat), g:(fn Nat -> Nat), h:(fn Nat -> Nat). (if ((all i:Nat. (if i < a then g(s + i) = f(s + i))) and (all i:Nat. (if i < b then h(t + i) = f((s + a) + i)))) then summation(a + b, s, f) = summation(a, s, g) + summation(b, t, h))))
summation_next: (all n:Nat, s:Nat, f:(fn Nat -> Nat). summation(1 + n, s, f) = summation(n, s, f) + f(s + n))
equal_refl: (all n:Nat. equal(n, n))
equal_complete_sound: (all m:Nat. (all n:Nat. ((m = n) ⇔ equal(m, n))))
not_equal_not_eq: (all m:Nat, n:Nat. (if not equal(m, n) then not (m = n)))
pow_positive: (all n:Nat. 0 < pow2(n))
recfun operator /(n:Nat, m:Nat) -> Nat
measure n {
if n < m then
0
else
if m = 0 then
0
else
1 + (n - m) / m
}
fun operator %(n:Nat, m:Nat) {
n - (n / m) * m
}
strong_induction: (all P:(fn Nat -> bool), n:Nat. (if (all j:Nat. (if (all i:Nat. (if i < j then P(i))) then P(j))) then P(n)))
div_mod: (all n:Nat, m:Nat. (if 0 < m then (n / m) * m + n % m = n))
mod_less_divisor: (all n:Nat, m:Nat. (if 0 < m then n % m < m))
div_cancel: (all y:Nat. (if 0 < y then y / y = 1))
mod_self_zero: (all y:Nat. y % y = 0)
zero_mod: (all x:Nat. 0 % x = 0)
zero_div: (all x:Nat. (if 0 < x then 0 / x = 0))
mod_one: (all n:Nat. n % 1 = 0)
div_one: (all n:Nat. n / 1 = n)
add_div_one: (all n:Nat, m:Nat. (if 0 < m then (n + m) / m = 1 + n / m))
mult_div_inverse: (all n:Nat, m:Nat. (if 0 < m then (n * m) / m = n))
expt_one: (all n:Nat. n ^ 1 = n)
one_expt: (all n:Nat. 1 ^ n = 1)
pow_add_r: (all n:Nat, m:Nat, o:Nat. m ^ (n + o) = m ^ n * m ^ o)
pow_mul_l: (all o:Nat, m:Nat, n:Nat. (m * n) ^ o = m ^ o * n ^ o)
pow_mul_r: (all o:Nat, m:Nat, n:Nat. (m ^ n) ^ o = m ^ (n * o))
pow_pos_nonneg: (all b:Nat, a:Nat. (if 0 < a then 0 < a ^ b))
pow_0_l: (all a:Nat. (if 0 < a then 0 ^ a = 0))
pow_eq_0: (all n:Nat, m:Nat. (if m ^ n = 0 then m = 0))
exp_one_implies_zero_or_one: (all m:Nat, n:Nat. (if m ^ n = 1 then (n = 0 or m = 1)))
pow_lt_mono_l: (all c:Nat, a:Nat, b:Nat. (if 0 < c then (if a < b then a ^ c < b ^ c)))
pow_gt_1: (all n:Nat, m:Nat. (if 1 < n then ((0 < m) ⇔ (1 < n ^ m))))
pow_le_mono_l: (all c:Nat, a:Nat, b:Nat. (if a ≤ b then a ^ c ≤ b ^ c))
pow_lt_mono_r: (all c:Nat, a:Nat, b:Nat. (if 1 < a then (if b < c then a ^ b < a ^ c)))
pow_inj_l: (all a:Nat, b:Nat, c:Nat. (if 0 < c then (if a ^ c = b ^ c then a = b)))
pow_inj_r: (all a:Nat, b:Nat, c:Nat. (if 1 < a then (if a ^ b = a ^ c then b = c)))