Def S == {T:Type| x:T. True }

is mentioned by

Thm* 'a:S, e:'a, f:('a'a). Thm* (fn1:('a). fn1(0) = e & (n:. fn1(n+1) = f(fn1(n),n))) Thm* & (fn1,y:('a). Thm* & (fn1(0) = e & (n:. fn1(n+1) = f(fn1(n),n)) Thm* & (& y(0) = e Thm* & (& (n:. y(n+1) = f(y(n),n)) Thm* & ( Thm* & (fn1 = y)	[num_axiom]
Thm* 'a:S, x:'a, f:('a'a). Thm* prim_rec(x,f,0) = x & (m:. prim_rec(x,f,m+1) = f(prim_rec(x,f,m),m))	[prim_rec_thm]
Thm* 'a:S, x:'a, f:('a'a). Thm* (n:. prim_rec_fun(x,f,0,n) = x) Thm* & (m,n:. prim_rec_fun(x,f,m+1,n) = f(prim_rec_fun(x,f,m,pre(n)),n))	[prim_rec_eqn]
Thm* 'a:S, x:'a, f:('a'a). Thm* simp_rec(x,f,0) = x & (m:. simp_rec(x,f,m+1) = f(simp_rec(x,f,m)))	[simp_rec_thm]
Thm* 'a:S, x:'a, f:('a'a), n:. fun:('a). simp_rec_rel(fun,x,f,n)	[simp_rec_exists]
Thm* 'a:S, n:, f:('a'a), x:'a. Thm* (fun:('a). simp_rec_rel(fun,x,f,n)) Thm*  Thm* simp_rec_fun(x,f,n,0) = x Thm* & (m:. m<n  simp_rec_fun(x,f,n,m+1) = f(simp_rec_fun(x,f,n,m)))	[simp_rec_fun_lemma]
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* '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* 'a:S.  Thm* all Thm* (x:'a. all Thm* (x:'a. (f:'a  'a. all Thm* (x:'a. (f:'a  'a. (n:hnum. exists Thm* (x:'a. (f:'a  'a. (n:hnum. (fun:hnum  'a. simp_rec_rel Thm* (x:'a. (f:'a  'a. (n:hnum. (fun:hnum  'a. (fun Thm* (x:'a. (f:'a  'a. (n:hnum. (fun:hnum  'a. ,x Thm* (x:'a. (f:'a  'a. (n:hnum. (fun:hnum  'a. ,f Thm* (x:'a. (f:'a  'a. (n:hnum. (fun:hnum  'a. ,n)))))	[hsimp_rec_exists]
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* (x:'a. all 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,m) Thm* (x:'a. (f:'a  hnum  'a. (m:hnum. ,prim_rec_fun(x,f,m,pre(m))))))	[hprim_rec_wd]
Thm* 'a:S.  Thm* all Thm* (x:'a. all Thm* (x:'a. (f:'a  hnum  'a. equal Thm* (x:'a. (f:'a  hnum  'a. (prim_rec_fun(x,f) Thm* (x:'a. (f:'a  hnum  'a. ,simp_rec Thm* (x:'a. (f:'a  hnum  'a. ,((n:hnum. x) Thm* (x:'a. (f:'a  hnum  'a. ,,fun:hnum  'a. n:hnum. f Thm* (x:'a. (f:'a  hnum  'a. ,,fun:hnum  'a. n:hnum. (fun(pre(n)) Thm* (x:'a. (f:'a  hnum  'a. ,,fun:hnum  'a. n:hnum. ,n)))))	[hprim_rec_fun_wd]
Thm* 'a:S.  Thm* all Thm* (x:'a. all Thm* (x:'a. (f:'a  'a. all Thm* (x:'a. (f:'a  'a. (n:hnum. equal Thm* (x:'a. (f:'a  'a. (n:hnum. (simp_rec(x,f,n) Thm* (x:'a. (f:'a  'a. (n:hnum. ,simp_rec_fun(x,f,suc(n),n)))))	[hsimp_rec_wd]
Thm* 'a:S.  Thm* all Thm* (x:'a. all Thm* (x:'a. (f:'a  'a. all Thm* (x:'a. (f:'a  'a. (n:hnum. equal Thm* (x:'a. (f:'a  'a. (n:hnum. (simp_rec_fun(x,f,n) Thm* (x:'a. (f:'a  'a. (n:hnum. ,select Thm* (x:'a. (f:'a  'a. (n:hnum. ,(fun:hnum  'a. simp_rec_rel Thm* (x:'a. (f:'a  'a. (n:hnum. ,(fun:hnum  'a. (fun Thm* (x:'a. (f:'a  'a. (n:hnum. ,(fun:hnum  'a. ,x Thm* (x:'a. (f:'a  'a. (n:hnum. ,(fun:hnum  'a. ,f Thm* (x:'a. (f:'a  'a. (n:hnum. ,(fun:hnum  'a. ,n))))))	[hsimp_rec_fun_wd]
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* 'a:S. simp_rec_fun  ('a  ('a  'a)  hnum  hnum  'a)	[hsimp_rec_fun_wf]
Thm* 'a:S. simp_rec_rel  ((hnum  'a)  'a  ('a  'a)  hnum  hbool)	[hsimp_rec_rel_wf]

In prior sections: hol hol min hol bool

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