The Theory %int%

Parents

sets

Children

dyadic

Constants

Is__Rep	( ) SET BOOL

$~_Z
$+_Z
$-_Z
$*_Z
$_Z	BOOL
$<_Z	BOOL
$_Z	BOOL
$>_Z	BOOL
$Abs_Z
$Mod_Z
$Div_Z

Aliases

+	$+_Z :
-	$-_Z :
~	$~_Z :
*	$*_Z :
	$_Z : BOOL
<	$<_Z : BOOL
	$_Z : BOOL
>	$>_Z : BOOL
Abs	$Abs_Z :
Div	$Div_Z :
Mod	$Mod_Z :

Types

Fixity

Left Infix 305:

-_Z

Left Infix 315:

Div_Z

Mod_Z

Right Infix 210:

<_Z

>_Z

Right Infix 300:

+_Z

Right Infix 310:

*_Z

Prefix 350:

Abs_Z

~_Z

Definitions

Is__Rep	a Is__Rep a ( m n a = {(x, y)\|m + y = n + x})
_def	f TypeDefn Is__Rep f
+_Z ~_Z	ConstSpec ( (+_Z', ~_Z', $"'") ( i j k +_Z' (+_Z' i j) k = +_Z' i (+_Z' j k) +_Z' i j = +_Z' j i +_Z' i (~_Z' i) = $"'" 0 +_Z' i ($"'" 0) = i) ( m n +_Z' ($"'" m) ($"'" n) = $"'" (m + n)) OneOne $"'" ( i m i = $"'" m i = ~_Z' ($"'" m))) ($+, ~, )
-_Z	i j i - j = i + ~ j
*_Z	ConstSpec ( _Z' i j k _Z' i (j + k) = _Z' i j + _Z' i k _Z' i ( 1) = i) $
_Z	i j i j ( m i + m = j)
<_Z	i j i < j i + 1 j
_Z	i j i j j i
>_Z	i j i > j j < i
Abs_Z	i Abs i = (if 0 i then i else ~ i)
Div_Z Mod_Z	ConstSpec ( (Div_Z', Mod_Z') i j j = 0 i = Div_Z' i j * j + Mod_Z' i j 0 Mod_Z' i j Mod_Z' i j < Abs j) ($Div, $Mod)

Theorems

is__rep_consistent_thm	a Is__Rep a
+_Z_consistent ~_Z_consistent _consistent	Consistent ( (+_Z', ~_Z', $"'") ( i j k +_Z' (+_Z' i j) k = +_Z' i (+_Z' j k) +_Z' i j = +_Z' j i +_Z' i (~_Z' i) = $"'" 0 +_Z' i ($"'" 0) = i) ( m n +_Z' ($"'" m) ($"'" n) = $"'" (m + n)) OneOne $"'" ( i m i = $"'" m i = ~_Z' ($"'" m)))
_plus_comm_thm	i j i + j = j + i
_plus_assoc_thm	i j k (i + j) + k = i + j + k
_plus_assoc_thm1	i j k i + j + k = (i + j) + k
_plus_order_thm	i j k j + i = i + j (i + j) + k = i + j + k j + i + k = i + j + k
_cases_thm	i m i = m i = ~ ( m)
_plus0_thm	i i + 0 = i 0 + i = i
_plus_minus_thm	i i + ~ i = 0 ~ i + i = 0
_eq_thm	i j i = j i + ~ j = 0
_plus_homomorphism_thm	m n (m + n) = m + n
_minus_clauses	i j ~ (~ i) = i i + ~ i = 0 ~ i + i = 0 ~ (i + j) = ~ i + ~ j ~ ( 0) = 0
_cases_thm1	i m i = m i = ~ ( (m + 1))
_induction_thm	p p ( 1) ( i p i p (~ i)) ( i j p i p j p (i + j)) ( i p i)
_one_one_thm	m n m = n m = n
_plus_clauses	i j k (i + k = j + k i = j) (k + i = j + k i = j) (i + k = k + j i = j) (k + i = k + j i = j) (i + k = k i = 0) (k + i = k i = 0) (k = k + j j = 0) (k = j + k j = 0) i + 0 = i 0 + i = i 1 = 0 0 = 1
___0_thm	i j i j i + ~ j 0
_minus__thm	i j ~ i ~ j j i
__minus_thm	i j i j ~ j ~ i
__clauses	i j k (i + k j + k i j) (k + i j + k i j) (i + k k + j i j) (k + i k + j i j) (i + k k i 0) (k + i k i 0) (k k + j 0 j) (k j + k 0 j) i i 1 0 0 1
__thm	m n m n m n
*_Z_consistent	Consistent ( _Z' i j k _Z' i (j + k) = _Z' i j + _Z' i k *_Z' i ( 1) = i)
_times_homomorphism_thm	m n (m * n) = m * n
_times_minus_thm	i j ~ i * j = ~ (i * j) i * ~ j = ~ (i * j) ~ i * ~ j = i * j
_times_comm_thm	i j i * j = j * i
_times_assoc_thm	i j k (i * j) * k = i * j * k
Div_Z_consistent Mod_Z_consistent	Consistent ( (Div_Z', Mod_Z') i j j = 0 i = Div_Z' i j * j + Mod_Z' i j 0 Mod_Z' i j Mod_Z' i j < Abs j)
_plus_homomorphism_thm1	m n m + n = (m + n)
__induction_thm	p p ( 0) ( i 0 i p i p (i + 1)) ( m 0 m p m)
__plus_thm	i j 0 i 0 j 0 i + j
__plus1_thm	i 0 i 0 i + 1
_minus_thm	i j ~ (~ i) = i i + ~ i = 0 ~ i + i = 0 ~ (i + j) = ~ i + ~ j ~ ( 0) = 0
__cases_thm	i 0 i i = 0 ( j 0 j i = j + 1)
___minus_thm	i 0 i i = 0 0 ~ i
___thm	i 0 i 0 ~ i
_plus_eq_thm	i j k i + j = k i = k + ~ j
___plus1_thm	i 0 i i + 1 = 0
_times_assoc_thm1	i j k i * j * k = (i * j) * k
_times_order_thm	i j k j * i = i * j (i * j) * k = i * j * k j * i * k = i * j * k
_times_homomorphism_thm1	m n m * n = (m * n)
_times1_thm	i i * 1 = i 1 * i = i
_times_plus_distrib_thm	i j k i * (j + k) = i * j + i * k (i + j) * k = i * k + j * k
_times0_thm	i 0 * i = 0 i * 0 = 0
_eq_thm1	i j i = j ~ i + j = 0
_times_eq_0_thm	i j i * j = 0 i = 0 j = 0
_times_clauses	i j 0 * i = 0 i * 0 = 0 i * 1 = i 1 * i = i
__times_thm	i j 0 i 0 j 0 i * j
__trans_thm	i j k i j j k i k
__cases_thm	i j i j j i
__refl_thm	i i i
___0_thm1	i j i j 0 j + ~ i
__antisym_thm	i j i j j i i = j
_less_trans_thm	i j k i < j j < k i < k
_less_irrefl_thm	i j (i < j j < i)
_less_cases_thm	i j i < j i = j j < i
_less_thm	m n m < n m < n
_less_less_0_thm	i j i < j i + ~ j < 0
_less_less_0_thm1	i j i < j 0 < j + ~ i
_minus_less_thm	i j ~ i < ~ j j < i
__less_thm	i j i < j j i
___thm	i j i j j < i
__less_eq_thm	i j i j i < j i = j
_less__trans_thm	i j k i < j j k i < k
__less_trans_thm	i j k i j j < k i < k
_minus___thm	i m i + ~ ( m) i
__plus__thm	i m i i + m
___thm	i 0 i ( m i = m)
_less_clauses	i j k (i + k < j + k i < j) (k + i < j + k i < j) (i + k < k + j i < j) (k + i < k + j i < j) (i + k < k i < 0) (k + i < k i < 0) (i < k + i 0 < k) (i < i + k 0 < k) i < i 0 < 1 1 < 0
__abs_thm	m Abs ( m) = m Abs (~ ( m)) = m
_abs_thm	i 0 i Abs i = i Abs (~ i) = i
_abs__thm	i 0 Abs i
_abs_eq_0_thm	i Abs i = 0 i = 0
_abs_minus_thm	i Abs (~ i) = Abs i
__abs_minus_thm	i j 0 i 0 j j i Abs (i + ~ j) i
_abs_times_thm	i j Abs (i * j) = Abs i * Abs j
_abs_plus_thm	i j Abs (i + j) Abs i + Abs j
_div_mod_unique_lemma1	i j 0 i 0 j i * j < j i = 0
_div_mod_unique_lemma2	j d r j = 0 d * j + r = 0 0 r r < Abs j d = 0 r = 0
_div_mod_unique_lemma3	i j d r D R j = 0 D * j + R = d * j + r 0 r r R R < Abs j D = d R = r
_div_mod_unique_thm	i j d r j = 0 (i = d * j + r 0 r r < Abs j d = i Div j r = i Mod j)
__induction_thm	j p p j ( i j i p i p (i + 1)) ( i j i p i)
_cov_induction_thm	j p ( i j i ( k j k k < i p k) p i) ( i j i p i)
_fun__thm	f g z ( x g (f x) = x) ( y f (g y) = y) (₁ h h ( 0) = z ( i h (i + 1) = f (h i)) ( i h (i - 1) = g (h i)))