Nuprl - hol_prim_rec Citations of hand

hol prim rec Sections HOLlib Doc

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

. p

is mentioned by

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

Thm* 'a:S.
Thm* all
Thm* (x:'a. all
Thm* (x:'a. (f:'a  hnum  'a. and
Thm* (x:'a. (f:'a  hnum  'a. (equal(prim_rec(x,f,0),x)
Thm* (x:'a. (f:'a  hnum  'a. ,all
Thm* (x:'a. (f:'a  hnum  'a. ,(m:hnum. equal
Thm* (x:'a. (f:'a  hnum  'a. ,(m:hnum. (prim_rec(x,f,suc(m))
Thm* (x:'a. (f:'a  hnum  'a. ,(m:hnum. ,f(prim_rec(x,f,m),m)))))) [hprim_rec_thm]

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

Thm* and(equal(pre(0),0),all(m:hnum. equal(pre(suc(m)),m))) [hpre_suc]

Thm* 'a:S.
Thm* all
Thm* (x:'a. all
Thm* (x:'a. (f:'a  'a. and
Thm* (x:'a. (f:'a  'a. (equal(simp_rec(x,f,0),x)
Thm* (x:'a. (f:'a  'a. ,all
Thm* (x:'a. (f:'a  'a. ,(m:hnum. equal
Thm* (x:'a. (f:'a  'a. ,(m:hnum. (simp_rec(x,f,suc(m))
Thm* (x:'a. (f:'a  'a. ,(m:hnum. ,f(simp_rec(x,f,m))))))) [hsimp_rec_thm]

Thm* all(m:hnum. and(lt(m,suc(m)),lt(m,suc(suc(m))))) [hless_suc_suc]

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

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

Thm* all
Thm* (m:hnum. all
Thm* (m:hnum. (n:hnum. equal
Thm* (m:hnum. (n:hnum. (lt(m,n)
Thm* (m:hnum. (n:hnum. ,exists
Thm* (m:hnum. (n:hnum. ,(P:hnum  hbool. and
Thm* (m:hnum. (n:hnum. ,(P:hnum  hbool. (all
Thm* (m:hnum. (n:hnum. ,(P:hnum  hbool. ((n:hnum. implies(P(suc(n)),P(n)))
Thm* (m:hnum. (n:hnum. ,(P:hnum  hbool. ,and(P(m),not(P(n)))))))) [hless_def]

In prior sections: hol bool hol num

Try larger context: HOLlib IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

hol prim rec Sections HOLlib Doc

Thm* 'a:S. Thm* all Thm* (e:'a. all Thm* (e:'a. (f:'a hnum 'a. exists_unique Thm* (e:'a. (f:'a hnum 'a. (fn1:hnum 'a. and Thm* (e:'a. (f:'a hnum 'a. (fn1:hnum 'a. (equal(fn1(0),e) Thm* (e:'a. (f:'a hnum 'a. (fn1:hnum 'a. ,all Thm* (e:'a. (f:'a hnum 'a. (fn1:hnum 'a. ,(n:hnum. equal Thm* (e:'a. (f:'a hnum 'a. (fn1:hnum 'a. ,(n:hnum. (fn1(suc(n)) Thm* (e:'a. (f:'a hnum 'a. (fn1:hnum 'a. ,(n:hnum. ,f Thm* (e:'a. (f:'a hnum 'a. (fn1:hnum 'a. ,(n:hnum. ,(fn1(n) Thm* (e:'a. (f:'a hnum 'a. (fn1:hnum 'a. ,(n:hnum. ,,n)))))))	[hnum_axiom]
Thm* 'a:S. Thm* all Thm* (x:'a. all Thm* (x:'a. (f:'a hnum 'a. and Thm* (x:'a. (f:'a hnum 'a. (equal(prim_rec(x,f,0),x) Thm* (x:'a. (f:'a hnum 'a. ,all Thm* (x:'a. (f:'a hnum 'a. ,(m:hnum. equal Thm* (x:'a. (f:'a hnum 'a. ,(m:hnum. (prim_rec(x,f,suc(m)) Thm* (x:'a. (f:'a hnum 'a. ,(m:hnum. ,f(prim_rec(x,f,m),m))))))	[hprim_rec_thm]
Thm* 'a:S. Thm* all Thm* (x:'a. all Thm* (x:'a. (f:'a hnum 'a. and Thm* (x:'a. (f:'a hnum 'a. (all(n:hnum. equal(prim_rec_fun(x,f,0,n),x)) Thm* (x:'a. (f:'a hnum 'a. ,all Thm* (x:'a. (f:'a hnum 'a. ,(m:hnum. all Thm* (x:'a. (f:'a hnum 'a. ,(m:hnum. (n:hnum. equal Thm* (x:'a. (f:'a hnum 'a. ,(m:hnum. (n:hnum. (prim_rec_fun Thm* (x:'a. (f:'a hnum 'a. ,(m:hnum. (n:hnum. ((x Thm* (x:'a. (f:'a hnum 'a. ,(m:hnum. (n:hnum. (,f Thm* (x:'a. (f:'a hnum 'a. ,(m:hnum. (n:hnum. (,suc(m) Thm* (x:'a. (f:'a hnum 'a. ,(m:hnum. (n:hnum. (,n) Thm* (x:'a. (f:'a hnum 'a. ,(m:hnum. (n:hnum. ,f Thm* (x:'a. (f:'a hnum 'a. ,(m:hnum. (n:hnum. ,(prim_rec_fun Thm* (x:'a. (f:'a hnum 'a. ,(m:hnum. (n:hnum. ,((x Thm* (x:'a. (f:'a hnum 'a. ,(m:hnum. (n:hnum. ,(,f Thm* (x:'a. (f:'a hnum 'a. ,(m:hnum. (n:hnum. ,(,m Thm* (x:'a. (f:'a hnum 'a. ,(m:hnum. (n:hnum. ,(,pre(n)) Thm* (x:'a. (f:'a hnum 'a. ,(m:hnum. (n:hnum. ,,n)))))))	[hprim_rec_eqn]
Thm* and(equal(pre(0),0),all(m:hnum. equal(pre(suc(m)),m)))	[hpre_suc]
Thm* 'a:S. Thm* all Thm* (x:'a. all Thm* (x:'a. (f:'a 'a. and Thm* (x:'a. (f:'a 'a. (equal(simp_rec(x,f,0),x) Thm* (x:'a. (f:'a 'a. ,all Thm* (x:'a. (f:'a 'a. ,(m:hnum. equal Thm* (x:'a. (f:'a 'a. ,(m:hnum. (simp_rec(x,f,suc(m)) Thm* (x:'a. (f:'a 'a. ,(m:hnum. ,f(simp_rec(x,f,m)))))))	[hsimp_rec_thm]
Thm* all(m:hnum. and(lt(m,suc(m)),lt(m,suc(suc(m)))))	[hless_suc_suc]
Thm* 'a:S. Thm* all Thm* (n:hnum. all Thm* (n:hnum. (f:'a Thm* (n:hnum. ( 'a. all Thm* (n:hnum. ( 'a. (x:'a. equal Thm* (n:hnum. ( 'a. (x:'a. (exists(fun:hnum 'a. simp_rec_rel(fun,x,f,n)) Thm* (n:hnum. ( 'a. (x:'a. ,and Thm* (n:hnum. ( 'a. (x:'a. ,(equal(simp_rec_fun(x,f,n,0),x) Thm* (n:hnum. ( 'a. (x:'a. ,,all Thm* (n:hnum. ( 'a. (x:'a. ,,(m:hnum. implies Thm* (n:hnum. ( 'a. (x:'a. ,,(m:hnum. (lt(m,n) Thm* (n:hnum. ( 'a. (x:'a. ,,(m:hnum. ,equal Thm* (n:hnum. ( 'a. (x:'a. ,,(m:hnum. ,(simp_rec_fun(x,f,n,suc(m)) Thm* (n:hnum. ( 'a. (x:'a. ,,(m:hnum. ,,f(simp_rec_fun(x,f,n,m))))))))))	[hsimp_rec_fun_lemma]
Thm* 'a:S. Thm* all Thm* (fun:hnum Thm* ( 'a. all Thm* ( 'a. (x:'a. all Thm* ( 'a. (x:'a. (f:'a 'a. all Thm* ( 'a. (x:'a. (f:'a 'a. (n:hnum. equal Thm* ( 'a. (x:'a. (f:'a 'a. (n:hnum. (simp_rec_rel(fun,x,f,n) Thm* ( 'a. (x:'a. (f:'a 'a. (n:hnum. ,and Thm* ( 'a. (x:'a. (f:'a 'a. (n:hnum. ,(equal(fun(0),x) Thm* ( 'a. (x:'a. (f:'a 'a. (n:hnum. ,,all Thm* ( 'a. (x:'a. (f:'a 'a. (n:hnum. ,,(m:hnum. implies Thm* ( 'a. (x:'a. (f:'a 'a. (n:hnum. ,,(m:hnum. (lt(m,n) Thm* ( 'a. (x:'a. (f:'a 'a. (n:hnum. ,,(m:hnum. ,equal Thm* ( 'a. (x:'a. (f:'a 'a. (n:hnum. ,,(m:hnum. ,(fun(suc(m)) Thm* ( 'a. (x:'a. (f:'a 'a. (n:hnum. ,,(m:hnum. ,,f(fun(m)))))))))))	[hsimp_rec_rel_wd]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. equal Thm* (m:hnum. (n:hnum. (lt(m,n) Thm* (m:hnum. (n:hnum. ,exists Thm* (m:hnum. (n:hnum. ,(P:hnum hbool. and Thm* (m:hnum. (n:hnum. ,(P:hnum hbool. (all Thm* (m:hnum. (n:hnum. ,(P:hnum hbool. ((n:hnum. implies(P(suc(n)),P(n))) Thm* (m:hnum. (n:hnum. ,(P:hnum hbool. ,and(P(m),not(P(n))))))))	[hless_def]