horizon := 1;; thm `; !R. (!x. R x x) /\ (!x y z. R x y /\ R y z ==> R x z) ==> ((!m n. m <= n ==> R m n) <=> (!n. R n (SUC n))) proof let R be num->num->bool; assume !x. R x x [1]; assume !x y z. R x y /\ R y z ==> R x z [2]; !n. n <= SUC n by ARITH_TAC; (!m n. m <= n ==> R m n) ==> (!n. R n (SUC n)) [3] by SIMP_TAC; now assume !n. R n (SUC n) [4]; !m n d. n = m + d ==> R m (m + d) proof let m be num; R m m by MESON_TAC,1; R m (m + 0) [5] by REWRITE_TAC,ADD_CLAUSES; !d. R m (m + d) ==> R m (m + SUC d) proof let d be num; assume R m (m + d); R m (SUC (m + d)) by MESON_TAC,2,4; qed by REWRITE_TAC,ADD_CLAUSES; !d. R m (m + d) by INDUCT_TAC,5; !d n. n = m + d ==> R m (m + d) by REWRITE_TAC,LEFT_FORALL_IMP_THM,EXISTS_REFL,ADD_CLAUSES; qed by ONCE_REWRITE_TAC,SWAP_FORALL_THM; thus !m n. m <= n ==> R m n by SIMP_TAC,LE_EXISTS,LEFT_IMP_EXISTS_THM; end; qed by EQ_TAC,3`;; thm `; !s. INFINITE s ==> ?x:A. x IN s proof let s be A->bool; assume INFINITE s; ~(s = {}) by INFINITE_NONEMPTY; consider x such that ~(x IN s <=> x IN {}) [1] by EXTENSION; take x; ~(x IN {}) by NOT_IN_EMPTY; qed by 1`;; let NOT_EVEN = thm `; !n. ~EVEN n <=> ODD n proof ~EVEN 0 <=> ODD 0 [1] by EVEN,ODD; !n. (~EVEN n <=> ODD n) ==> (~EVEN (SUC n) <=> ODD (SUC n)) by EVEN,ODD; qed by 1,INDUCT_TAC`;;