4 !R. (!x. R x x) /\ (!x y z. R x y /\ R y z ==> R x z)
5 ==> ((!m n. m <= n ==> R m n) <=> (!n. R n (SUC n)))
7 let R be num->num->bool;
9 assume !x y z. R x y /\ R y z ==> R x z [2];
10 !n. n <= SUC n by ARITH_TAC;
11 (!m n. m <= n ==> R m n) ==> (!n. R n (SUC n)) [3] by SIMP_TAC;
13 assume !n. R n (SUC n) [4];
14 !m n d. n = m + d ==> R m (m + d)
18 R m (m + 0) [5] by REWRITE_TAC,ADD_CLAUSES;
19 !d. R m (m + d) ==> R m (m + SUC d)
23 R m (SUC (m + d)) by MESON_TAC,2,4;
24 qed by REWRITE_TAC,ADD_CLAUSES;
25 !d. R m (m + d) by INDUCT_TAC,5;
26 !d n. n = m + d ==> R m (m + d)
27 by REWRITE_TAC,LEFT_FORALL_IMP_THM,EXISTS_REFL,ADD_CLAUSES;
28 qed by ONCE_REWRITE_TAC,SWAP_FORALL_THM;
29 thus !m n. m <= n ==> R m n by SIMP_TAC,LE_EXISTS,LEFT_IMP_EXISTS_THM;
34 !s. INFINITE s ==> ?x:A. x IN s
38 ~(s = {}) by INFINITE_NONEMPTY;
40 ~(x IN s <=> x IN {}) [1] by EXTENSION;
42 ~(x IN {}) by NOT_IN_EMPTY;
48 ~EVEN 0 <=> ODD 0 [1] by EVEN,ODD;
49 !n. (~EVEN n <=> ODD n) ==> (~EVEN (SUC n) <=> ODD (SUC n))
51 qed by 1,INDUCT_TAC`;;