Nuprl - hol_prim

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
hol_prim_recNuprl Section: hol_prim_rec

Selected Objects
def pre pre(n) == if n=0 then 0 else n-1 fi

THM pre_nuprl n:. n>0  pre(n) = n-1

THM iff_refl (P  P)  True

def hlt lt == m:. n:. m<n

def hsimp_rec_rel simp_rec_rel
== fun:'a. x:'a. f:'a'a. n:. (fun(0) = x
== & (m:. m<n  fun(m+1) = f(fun(m))))

def hsimp_rec_fun simp_rec_fun == x:'a. f:'a'a. n:. @fun:'a. (simp_rec_rel(fun,x,f,n))

def hsimp_rec simp_rec == x:'a. f:'a'a. n:. ncompose(f;n;x)

def hpre pre == n:. pre(n)

def hprim_rec_fun prim_rec_fun
== x:'a. f:'a'a. simp_rec((n:. x),fun:'a. n:. f(fun(pre(n)),n))

def hprim_rec prim_rec == x:'a. f:'a'a. m:. prim_rec_fun(x,f,m,pre(m))

THM hless_def all
(m:hnum. all
(m:hnum. (n:hnum. equal
(m:hnum. (n:hnum. (lt(m,n)
(m:hnum. (n:hnum. ,exists
(m:hnum. (n:hnum. ,(P:hnum  hbool. and
(m:hnum. (n:hnum. ,(P:hnum  hbool. (all(n:hnum. implies(P(suc(n)),P(n)))
(m:hnum. (n:hnum. ,(P:hnum  hbool. ,and(P(m),not(P(n))))))))

THM hsimp_rec_rel_wd 'a:S.
all
(fun:hnum
( 'a. all
( 'a. (x:'a. all
( 'a. (x:'a. (f:'a  'a. all
( 'a. (x:'a. (f:'a  'a. (n:hnum. equal
( 'a. (x:'a. (f:'a  'a. (n:hnum. (simp_rec_rel(fun,x,f,n)
( 'a. (x:'a. (f:'a  'a. (n:hnum. ,and
( 'a. (x:'a. (f:'a  'a. (n:hnum. ,(equal(fun(0),x)
( 'a. (x:'a. (f:'a  'a. (n:hnum. ,,all
( 'a. (x:'a. (f:'a  'a. (n:hnum. ,,(m:hnum. implies
( 'a. (x:'a. (f:'a  'a. (n:hnum. ,,(m:hnum. (lt(m,n)
( 'a. (x:'a. (f:'a  'a. (n:hnum. ,,(m:hnum. ,equal
( 'a. (x:'a. (f:'a  'a. (n:hnum. ,,(m:hnum. ,(fun(suc(m))
( 'a. (x:'a. (f:'a  'a. (n:hnum. ,,(m:hnum. ,,f(fun(m)))))))))))

THM hsimp_rec_fun_wd 'a:S.
all
(x:'a. all
(x:'a. (f:'a  'a. all
(x:'a. (f:'a  'a. (n:hnum. equal
(x:'a. (f:'a  'a. (n:hnum. (simp_rec_fun(x,f,n)
(x:'a. (f:'a  'a. (n:hnum. ,select
(x:'a. (f:'a  'a. (n:hnum. ,(fun:hnum  'a. simp_rec_rel(fun,x,f,n))))))

THM hsimp_rec_wd 'a:S.
all
(x:'a. all
(x:'a. (f:'a  'a. all
(x:'a. (f:'a  'a. (n:hnum. equal
(x:'a. (f:'a  'a. (n:hnum. (simp_rec(x,f,n)
(x:'a. (f:'a  'a. (n:hnum. ,simp_rec_fun(x,f,suc(n),n)))))

THM hpre_def all(m:hnum. equal(pre(m),cond(equal(m,0),0,select(n:hnum. equal(m,suc(n))))))

THM hprim_rec_fun_wd 'a:S.
all
(x:'a. all
(x:'a. (f:'a  hnum  'a. equal
(x:'a. (f:'a  hnum  'a. (prim_rec_fun(x,f)
(x:'a. (f:'a  hnum  'a. ,simp_rec
(x:'a. (f:'a  hnum  'a. ,((n:hnum. x)
(x:'a. (f:'a  hnum  'a. ,,fun:hnum  'a. n:hnum. f(fun(pre(n)),n)))))

THM hprim_rec_wd 'a:S.
all
(x:'a. all
(x:'a. (f:'a  hnum  'a. all
(x:'a. (f:'a  hnum  'a. (m:hnum. equal
(x:'a. (f:'a  hnum  'a. (m:hnum. (prim_rec(x,f,m)
(x:'a. (f:'a  hnum  'a. (m:hnum. ,prim_rec_fun(x,f,m,pre(m))))))

THM hinv_suc_eq all(m:hnum. all(n:hnum. equal(equal(suc(m),suc(n)),equal(m,n))))

THM hless_refl all(n:hnum. not(lt(n,n)))

THM hsuc_less all(m:hnum. all(n:hnum. implies(lt(suc(m),n),lt(m,n))))

THM hnot_less_0 all(n:hnum. not(lt(n,0)))

THM hless_0_0 lt(0,suc(0))

THM hless_mono all(m:hnum. all(n:hnum. implies(lt(m,n),lt(suc(m),suc(n)))))

THM hless_suc_refl all(n:hnum. lt(n,suc(n)))

THM hless_suc all(m:hnum. all(n:hnum. implies(lt(m,n),lt(m,suc(n)))))

THM hless_lemma1 all(m:hnum. all(n:hnum. implies(lt(m,suc(n)),or(equal(m,n),lt(m,n)))))

THM hless_lemma2 all(m:hnum. all(n:hnum. implies(or(equal(m,n),lt(m,n)),lt(m,suc(n)))))

THM hless_thm all(m:hnum. all(n:hnum. equal(lt(m,suc(n)),or(equal(m,n),lt(m,n)))))

THM hless_suc_imp all
(m:hnum. all(n:hnum. implies(lt(m,suc(n)),implies(not(equal(m,n)),lt(m,n)))))

THM hless_0 all(n:hnum. lt(0,suc(n)))

THM heq_less all(m:hnum. all(n:hnum. implies(equal(suc(m),n),lt(m,n))))

THM hsuc_id all(n:hnum. not(equal(suc(n),n)))

THM hnot_less_eq all(m:hnum. all(n:hnum. implies(equal(m,n),not(lt(m,n)))))

THM hless_not_eq all(m:hnum. all(n:hnum. implies(lt(m,n),not(equal(m,n)))))

THM hsimp_rec_fun_lemma 'a:S.
all
(n:hnum. all
(n:hnum. (f:'a  'a. all
(n:hnum. (f:'a  'a. (x:'a. equal
(n:hnum. (f:'a  'a. (x:'a. (exists
(n:hnum. (f:'a  'a. (x:'a. ((fun:hnum  'a. simp_rec_rel(fun,x,f,n))
(n:hnum. (f:'a  'a. (x:'a. ,and
(n:hnum. (f:'a  'a. (x:'a. ,(equal(simp_rec_fun(x,f,n,0),x)
(n:hnum. (f:'a  'a. (x:'a. ,,all
(n:hnum. (f:'a  'a. (x:'a. ,,(m:hnum. implies
(n:hnum. (f:'a  'a. (x:'a. ,,(m:hnum. (lt(m,n)
(n:hnum. (f:'a  'a. (x:'a. ,,(m:hnum. ,equal
(n:hnum. (f:'a  'a. (x:'a. ,,(m:hnum. ,(simp_rec_fun(x,f,n,suc(m))
(n:hnum. (f:'a  'a. (x:'a. ,,(m:hnum. ,,f(simp_rec_fun(x,f,n,m))))))))))

THM hsimp_rec_exists 'a:S.
all
(x:'a. all
(x:'a. (f:'a  'a. all
(x:'a. (f:'a  'a. (n:hnum. exists
(x:'a. (f:'a  'a. (n:hnum. (fun:hnum  'a. simp_rec_rel(fun,x,f,n)))))

THM hless_suc_suc all(m:hnum. and(lt(m,suc(m)),lt(m,suc(suc(m)))))

THM hsimp_rec_thm 'a:S.
all
(x:'a. all
(x:'a. (f:'a  'a. and
(x:'a. (f:'a  'a. (equal(simp_rec(x,f,0),x)
(x:'a. (f:'a  'a. ,all
(x:'a. (f:'a  'a. ,(m:hnum. equal
(x:'a. (f:'a  'a. ,(m:hnum. (simp_rec(x,f,suc(m))
(x:'a. (f:'a  'a. ,(m:hnum. ,f(simp_rec(x,f,m)))))))

THM hpre_suc and(equal(pre(0),0),all(m:hnum. equal(pre(suc(m)),m)))

THM hprim_rec_eqn 'a:S.
all
(x:'a. all
(x:'a. (f:'a  hnum  'a. and
(x:'a. (f:'a  hnum  'a. (all(n:hnum. equal(prim_rec_fun(x,f,0,n),x))
(x:'a. (f:'a  hnum  'a. ,all
(x:'a. (f:'a  hnum  'a. ,(m:hnum. all
(x:'a. (f:'a  hnum  'a. ,(m:hnum. (n:hnum. equal
(x:'a. (f:'a  hnum  'a. ,(m:hnum. (n:hnum. (prim_rec_fun(x,f,suc(m),n)
(x:'a. (f:'a  hnum  'a. ,(m:hnum. (n:hnum. ,f
(x:'a. (f:'a  hnum  'a. ,(m:hnum. (n:hnum. ,(prim_rec_fun(x,f,m,pre(n))
(x:'a. (f:'a  hnum  'a. ,(m:hnum. (n:hnum. ,,n)))))))

THM hprim_rec_thm 'a:S.
all
(x:'a. all
(x:'a. (f:'a  hnum  'a. and
(x:'a. (f:'a  hnum  'a. (equal(prim_rec(x,f,0),x)
(x:'a. (f:'a  hnum  'a. ,all
(x:'a. (f:'a  hnum  'a. ,(m:hnum. equal
(x:'a. (f:'a  hnum  'a. ,(m:hnum. (prim_rec(x,f,suc(m))
(x:'a. (f:'a  hnum  'a. ,(m:hnum. ,f(prim_rec(x,f,m),m))))))

THM hnum_axiom 'a:S.
all
(e:'a. all
(e:'a. (f:'a  hnum  'a. exists_unique
(e:'a. (f:'a  hnum  'a. (fn1:hnum  'a. and
(e:'a. (f:'a  hnum  'a. (fn1:hnum  'a. (equal(fn1(0),e)
(e:'a. (f:'a  hnum  'a. (fn1:hnum  'a. ,all
(e:'a. (f:'a  hnum  'a. (fn1:hnum  'a. ,(n:hnum. equal
(e:'a. (f:'a  hnum  'a. (fn1:hnum  'a. ,(n:hnum. (fn1(suc(n))
(e:'a. (f:'a  hnum  'a. (fn1:hnum  'a. ,(n:hnum. ,f(fn1(n),n)))))))

THM inv_suc_eq m,n:. m+1 = n+1    m = n

THM less_refl n:. n<n

THM suc_less m,n:. m+1<n  m<n

THM not_less_0 n:. n<0

THM less_0_0 0<0+1

THM less_mono m,n:. m<n  m+1<n+1

THM less_suc_refl n:. n<n+1

THM less_suc m,n:. m<n  m<n+1

THM less_lemma1 m,n:. m<n+1  m = n  m<n

THM less_lemma2 m,n:. m = n  m<n  m<n+1

THM less_thm m,n:. m<n+1  m = n  m<n

THM less_suc_imp m,n:. m<n+1  m = n  m<n

THM less_0 n:. 0<n+1

THM eq_less m,n:. m+1 = n    m<n

THM suc_id n:. n+1 = n

THM not_less_eq m,n:. m = n  m<n

THM less_not_eq m,n:. m<n  m = n

THM simp_rec_fun_lemma 'a:S, n:, f:('a'a), x:'a.
(fun:('a). simp_rec_rel(fun,x,f,n))

simp_rec_fun(x,f,n,0) = x
& (m:. m<n  simp_rec_fun(x,f,n,m+1) = f(simp_rec_fun(x,f,n,m)))

THM simp_rec_exists 'a:S, x:'a, f:('a'a), n:. fun:('a). simp_rec_rel(fun,x,f,n)

THM less_suc_suc m:. m<m+1 & m<m+1+1

THM simp_rec_thm 'a:S, x:'a, f:('a'a).
simp_rec(x,f,0) = x & (m:. simp_rec(x,f,m+1) = f(simp_rec(x,f,m)))

THM pre_suc pre(0) = 0 & (m:. pre(m+1) = m)

THM prim_rec_eqn 'a:S, x:'a, f:('a'a).
(n:. prim_rec_fun(x,f,0,n) = x)
& (m,n:. prim_rec_fun(x,f,m+1,n) = f(prim_rec_fun(x,f,m,pre(n)),n))

THM prim_rec_thm 'a:S, x:'a, f:('a'a).
prim_rec(x,f,0) = x & (m:. prim_rec(x,f,m+1) = f(prim_rec(x,f,m),m))

THM num_axiom 'a:S, e:'a, f:('a'a).
(fn1:('a). fn1(0) = e & (n:. fn1(n+1) = f(fn1(n),n)))
& (fn1,y:('a).
& (fn1(0) = e & (n:. fn1(n+1) = f(fn1(n),n))
& (& y(0) = e
& (& (n:. y(n+1) = f(y(n),n))
& (
& (fn1 = y)

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Selected Objects
def	pre	pre(n) == if n=0 then 0 else n-1 fi
THM	pre_nuprl	n:. n>0 pre(n) = n-1
THM	iff_refl	(P P) True
def	hlt	lt == m:. n:. m<n
def	hsimp_rec_rel	simp_rec_rel == fun:'a. x:'a. f:'a'a. n:. (fun(0) = x == & (m:. m<n fun(m+1) = f(fun(m))))
def	hsimp_rec_fun	simp_rec_fun == x:'a. f:'a'a. n:. @fun:'a. (simp_rec_rel(fun,x,f,n))
def	hsimp_rec	simp_rec == x:'a. f:'a'a. n:. ncompose(f;n;x)
def	hpre	pre == n:. pre(n)
def	hprim_rec_fun	prim_rec_fun == x:'a. f:'a'a. simp_rec((n:. x),fun:'a. n:. f(fun(pre(n)),n))
def	hprim_rec	prim_rec == x:'a. f:'a'a. m:. prim_rec_fun(x,f,m,pre(m))
THM	hless_def	all (m:hnum. all (m:hnum. (n:hnum. equal (m:hnum. (n:hnum. (lt(m,n) (m:hnum. (n:hnum. ,exists (m:hnum. (n:hnum. ,(P:hnum hbool. and (m:hnum. (n:hnum. ,(P:hnum hbool. (all(n:hnum. implies(P(suc(n)),P(n))) (m:hnum. (n:hnum. ,(P:hnum hbool. ,and(P(m),not(P(n))))))))
THM	hsimp_rec_rel_wd	'a:S. all (fun:hnum ( 'a. all ( 'a. (x:'a. all ( 'a. (x:'a. (f:'a 'a. all ( 'a. (x:'a. (f:'a 'a. (n:hnum. equal ( 'a. (x:'a. (f:'a 'a. (n:hnum. (simp_rec_rel(fun,x,f,n) ( 'a. (x:'a. (f:'a 'a. (n:hnum. ,and ( 'a. (x:'a. (f:'a 'a. (n:hnum. ,(equal(fun(0),x) ( 'a. (x:'a. (f:'a 'a. (n:hnum. ,,all ( 'a. (x:'a. (f:'a 'a. (n:hnum. ,,(m:hnum. implies ( 'a. (x:'a. (f:'a 'a. (n:hnum. ,,(m:hnum. (lt(m,n) ( 'a. (x:'a. (f:'a 'a. (n:hnum. ,,(m:hnum. ,equal ( 'a. (x:'a. (f:'a 'a. (n:hnum. ,,(m:hnum. ,(fun(suc(m)) ( 'a. (x:'a. (f:'a 'a. (n:hnum. ,,(m:hnum. ,,f(fun(m)))))))))))
THM	hsimp_rec_fun_wd	'a:S. all (x:'a. all (x:'a. (f:'a 'a. all (x:'a. (f:'a 'a. (n:hnum. equal (x:'a. (f:'a 'a. (n:hnum. (simp_rec_fun(x,f,n) (x:'a. (f:'a 'a. (n:hnum. ,select (x:'a. (f:'a 'a. (n:hnum. ,(fun:hnum 'a. simp_rec_rel(fun,x,f,n))))))
THM	hsimp_rec_wd	'a:S. all (x:'a. all (x:'a. (f:'a 'a. all (x:'a. (f:'a 'a. (n:hnum. equal (x:'a. (f:'a 'a. (n:hnum. (simp_rec(x,f,n) (x:'a. (f:'a 'a. (n:hnum. ,simp_rec_fun(x,f,suc(n),n)))))
THM	hpre_def	all(m:hnum. equal(pre(m),cond(equal(m,0),0,select(n:hnum. equal(m,suc(n))))))
THM	hprim_rec_fun_wd	'a:S. all (x:'a. all (x:'a. (f:'a hnum 'a. equal (x:'a. (f:'a hnum 'a. (prim_rec_fun(x,f) (x:'a. (f:'a hnum 'a. ,simp_rec (x:'a. (f:'a hnum 'a. ,((n:hnum. x) (x:'a. (f:'a hnum 'a. ,,fun:hnum 'a. n:hnum. f(fun(pre(n)),n)))))
THM	hprim_rec_wd	'a:S. all (x:'a. all (x:'a. (f:'a hnum 'a. all (x:'a. (f:'a hnum 'a. (m:hnum. equal (x:'a. (f:'a hnum 'a. (m:hnum. (prim_rec(x,f,m) (x:'a. (f:'a hnum 'a. (m:hnum. ,prim_rec_fun(x,f,m,pre(m))))))
THM	hinv_suc_eq	all(m:hnum. all(n:hnum. equal(equal(suc(m),suc(n)),equal(m,n))))
THM	hless_refl	all(n:hnum. not(lt(n,n)))
THM	hsuc_less	all(m:hnum. all(n:hnum. implies(lt(suc(m),n),lt(m,n))))
THM	hnot_less_0	all(n:hnum. not(lt(n,0)))
THM	hless_0_0	lt(0,suc(0))
THM	hless_mono	all(m:hnum. all(n:hnum. implies(lt(m,n),lt(suc(m),suc(n)))))
THM	hless_suc_refl	all(n:hnum. lt(n,suc(n)))
THM	hless_suc	all(m:hnum. all(n:hnum. implies(lt(m,n),lt(m,suc(n)))))
THM	hless_lemma1	all(m:hnum. all(n:hnum. implies(lt(m,suc(n)),or(equal(m,n),lt(m,n)))))
THM	hless_lemma2	all(m:hnum. all(n:hnum. implies(or(equal(m,n),lt(m,n)),lt(m,suc(n)))))
THM	hless_thm	all(m:hnum. all(n:hnum. equal(lt(m,suc(n)),or(equal(m,n),lt(m,n)))))
THM	hless_suc_imp	all (m:hnum. all(n:hnum. implies(lt(m,suc(n)),implies(not(equal(m,n)),lt(m,n)))))
THM	hless_0	all(n:hnum. lt(0,suc(n)))
THM	heq_less	all(m:hnum. all(n:hnum. implies(equal(suc(m),n),lt(m,n))))
THM	hsuc_id	all(n:hnum. not(equal(suc(n),n)))
THM	hnot_less_eq	all(m:hnum. all(n:hnum. implies(equal(m,n),not(lt(m,n)))))
THM	hless_not_eq	all(m:hnum. all(n:hnum. implies(lt(m,n),not(equal(m,n)))))
THM	hsimp_rec_fun_lemma	'a:S. all (n:hnum. all (n:hnum. (f:'a 'a. all (n:hnum. (f:'a 'a. (x:'a. equal (n:hnum. (f:'a 'a. (x:'a. (exists (n:hnum. (f:'a 'a. (x:'a. ((fun:hnum 'a. simp_rec_rel(fun,x,f,n)) (n:hnum. (f:'a 'a. (x:'a. ,and (n:hnum. (f:'a 'a. (x:'a. ,(equal(simp_rec_fun(x,f,n,0),x) (n:hnum. (f:'a 'a. (x:'a. ,,all (n:hnum. (f:'a 'a. (x:'a. ,,(m:hnum. implies (n:hnum. (f:'a 'a. (x:'a. ,,(m:hnum. (lt(m,n) (n:hnum. (f:'a 'a. (x:'a. ,,(m:hnum. ,equal (n:hnum. (f:'a 'a. (x:'a. ,,(m:hnum. ,(simp_rec_fun(x,f,n,suc(m)) (n:hnum. (f:'a 'a. (x:'a. ,,(m:hnum. ,,f(simp_rec_fun(x,f,n,m))))))))))
THM	hsimp_rec_exists	'a:S. all (x:'a. all (x:'a. (f:'a 'a. all (x:'a. (f:'a 'a. (n:hnum. exists (x:'a. (f:'a 'a. (n:hnum. (fun:hnum 'a. simp_rec_rel(fun,x,f,n)))))
THM	hless_suc_suc	all(m:hnum. and(lt(m,suc(m)),lt(m,suc(suc(m)))))
THM	hsimp_rec_thm	'a:S. all (x:'a. all (x:'a. (f:'a 'a. and (x:'a. (f:'a 'a. (equal(simp_rec(x,f,0),x) (x:'a. (f:'a 'a. ,all (x:'a. (f:'a 'a. ,(m:hnum. equal (x:'a. (f:'a 'a. ,(m:hnum. (simp_rec(x,f,suc(m)) (x:'a. (f:'a 'a. ,(m:hnum. ,f(simp_rec(x,f,m)))))))
THM	hpre_suc	and(equal(pre(0),0),all(m:hnum. equal(pre(suc(m)),m)))
THM	hprim_rec_eqn	'a:S. all (x:'a. all (x:'a. (f:'a hnum 'a. and (x:'a. (f:'a hnum 'a. (all(n:hnum. equal(prim_rec_fun(x,f,0,n),x)) (x:'a. (f:'a hnum 'a. ,all (x:'a. (f:'a hnum 'a. ,(m:hnum. all (x:'a. (f:'a hnum 'a. ,(m:hnum. (n:hnum. equal (x:'a. (f:'a hnum 'a. ,(m:hnum. (n:hnum. (prim_rec_fun(x,f,suc(m),n) (x:'a. (f:'a hnum 'a. ,(m:hnum. (n:hnum. ,f (x:'a. (f:'a hnum 'a. ,(m:hnum. (n:hnum. ,(prim_rec_fun(x,f,m,pre(n)) (x:'a. (f:'a hnum 'a. ,(m:hnum. (n:hnum. ,,n)))))))
THM	hprim_rec_thm	'a:S. all (x:'a. all (x:'a. (f:'a hnum 'a. and (x:'a. (f:'a hnum 'a. (equal(prim_rec(x,f,0),x) (x:'a. (f:'a hnum 'a. ,all (x:'a. (f:'a hnum 'a. ,(m:hnum. equal (x:'a. (f:'a hnum 'a. ,(m:hnum. (prim_rec(x,f,suc(m)) (x:'a. (f:'a hnum 'a. ,(m:hnum. ,f(prim_rec(x,f,m),m))))))
THM	hnum_axiom	'a:S. all (e:'a. all (e:'a. (f:'a hnum 'a. exists_unique (e:'a. (f:'a hnum 'a. (fn1:hnum 'a. and (e:'a. (f:'a hnum 'a. (fn1:hnum 'a. (equal(fn1(0),e) (e:'a. (f:'a hnum 'a. (fn1:hnum 'a. ,all (e:'a. (f:'a hnum 'a. (fn1:hnum 'a. ,(n:hnum. equal (e:'a. (f:'a hnum 'a. (fn1:hnum 'a. ,(n:hnum. (fn1(suc(n)) (e:'a. (f:'a hnum 'a. (fn1:hnum 'a. ,(n:hnum. ,f(fn1(n),n)))))))
THM	inv_suc_eq	m,n:. m+1 = n+1 m = n
THM	less_refl	n:. n<n
THM	suc_less	m,n:. m+1<n m<n
THM	not_less_0	n:. n<0
THM	less_0_0	0<0+1
THM	less_mono	m,n:. m<n m+1<n+1
THM	less_suc_refl	n:. n<n+1
THM	less_suc	m,n:. m<n m<n+1
THM	less_lemma1	m,n:. m<n+1 m = n m<n
THM	less_lemma2	m,n:. m = n m<n m<n+1
THM	less_thm	m,n:. m<n+1 m = n m<n
THM	less_suc_imp	m,n:. m<n+1 m = n m<n
THM	less_0	n:. 0<n+1
THM	eq_less	m,n:. m+1 = n m<n
THM	suc_id	n:. n+1 = n
THM	not_less_eq	m,n:. m = n m<n
THM	less_not_eq	m,n:. m<n m = n
THM	simp_rec_fun_lemma	'a:S, n:, f:('a'a), x:'a. (fun:('a). simp_rec_rel(fun,x,f,n)) simp_rec_fun(x,f,n,0) = x & (m:. m<n simp_rec_fun(x,f,n,m+1) = f(simp_rec_fun(x,f,n,m)))
THM	simp_rec_exists	'a:S, x:'a, f:('a'a), n:. fun:('a). simp_rec_rel(fun,x,f,n)
THM	less_suc_suc	m:. m<m+1 & m<m+1+1
THM	simp_rec_thm	'a:S, x:'a, f:('a'a). simp_rec(x,f,0) = x & (m:. simp_rec(x,f,m+1) = f(simp_rec(x,f,m)))
THM	pre_suc	pre(0) = 0 & (m:. pre(m+1) = m)
THM	prim_rec_eqn	'a:S, x:'a, f:('a'a). (n:. prim_rec_fun(x,f,0,n) = x) & (m,n:. prim_rec_fun(x,f,m+1,n) = f(prim_rec_fun(x,f,m,pre(n)),n))
THM	prim_rec_thm	'a:S, x:'a, f:('a'a). prim_rec(x,f,0) = x & (m:. prim_rec(x,f,m+1) = f(prim_rec(x,f,m),m))
THM	num_axiom	'a:S, e:'a, f:('a'a). (fn1:('a). fn1(0) = e & (n:. fn1(n+1) = f(fn1(n),n))) & (fn1,y:('a). & (fn1(0) = e & (n:. fn1(n+1) = f(fn1(n),n)) & (& y(0) = e & (& (n:. y(n+1) = f(y(n),n)) & ( & (fn1 = y)

Origin Definitions Sections HOLlib Doc