Nuprl - Some Definitions

Thms decidability Sections ClassicalProps(jlc) Doc

sequent_rank	`Def (S) == (S.H)+(S.C)` `Thm* Sequent`
C	`Def s.C == s.2` `Thm* s:Sequent. s.C Formula List`
Sequent	`Def Sequent == (Formula List)(Formula List)` `Thm* Sequent Type`
Formula	`Def Formula == rec(formula.Var+formula+(formulaformula)+(formulaformula)+(formulaformula))` `Thm* Formula Type`
H	`Def s.H == s.1` `Thm* s:Sequent. s.H Formula List`
Three	`Def == Unit+Unit+Unit` `Thm* Type`
Three_0	`Def 3 == inl()` `Thm* 3`
Three_1	`Def 3 == inr(inl())` `Thm* 3`
Three_2	`Def 3 == inr(inr())` `Thm* 3`
Var	`Def Var == Atom` `Thm* Var Type`
discrete_equality	`Def {T=} == {eq:(TT)\| x,y:T. (eq(x,y)) x = y }` `Thm* T:Type. {T=} Type`
disjoint	`Def disjoint(eq;L1;L2) == xL1.x(eq) L2` `Thm* T:Type, eq:(TT), L1,L2:T List. disjoint(eq;L1;L2) Type`
assert	`Def b == if b True else False fi` `Thm* b:. b Prop`
fvar	`Def F == inl(F)` `Thm* x:Var. x Formula`
is_member	`Def x(eq) L == (letrec is_member x eq L = (Case of L nil false h.t if eq(x,h) true else is_member(x,eq,t) fi) ) (x ,eq ,L) Thm* T:Type, eq:(TT), u:T. u(eq) nil` `Thm* T:Type, eq:(TT), x:T, L:T List. x(eq) L`
list_all	`Def xL.P(x) == (letrec list_all L = (Case of L; nil True ; h.t P(h) & list_all(t)) ) (L) Thm* T:Type, P:(TProp), L:T List. xL.P(x) Type` `Thm* T:Type, P:(TType). xnil.P(x) Type`
list_exists	`Def xL.P(x) == (letrec list_exists L = (Case of L; nil False ; h.t P(h) list_exists(t)) ) (L)` `Thm* T:Type, P:(TProp), L:T List. xL.P(x) Type`
iff	`Def P Q == (P Q) & (P Q)` `Thm* A,B:Prop. (A B) Prop`
bnot	`Def b == if b false else true fi` `Thm* b:. b`
list_rank	`Def (L) == reduce(x,y. (x)+y;0;L)` `Thm* (Formula List)`
formula_rank	`Def == (letrec formula_rank f = case f: x 0; p (formula_rank(p)+1); pq (formula_rank(p)+formula_rank(q)+1); pq (formula_rank(p)+formula_rank(q)+1); pq (formula_rank(p)+formula_rank(q)+1); )` `Thm* Formula`
letrec_body	`Def = b == b`
letrec_arg	`Def x b(x) (x) == b(x)`
letrec	`Def (letrec f b(f)) == b((letrec f b(f)) ) (recursive)`
rev_implies	`Def P Q == Q P` `Thm* A,B:Prop. (A B) Prop`
reduce	`Def reduce(f;k;as) == Case of as; nil k ; a.as' f(a,reduce(f;k;as')) (recursive)` `Thm* A,B:Type, f:(ABB), k:B, as:A List. reduce(f;k;as) B`
formula_case	`Def case F: x varC(x); p1 notC(p1); p2p3 andC(p2;p3); p4p5 orC(p4;p5); p6p7 impC(p6;p7); == InjCase(F; x. varC(x); F. InjCase(F; p1. notC(p1); F. InjCase(F; x. x/p2,p3.andC(p2;p3); F. InjCase(F; x. x/p4,p5.orC(p4;p5), x/p6,p7.impC(p6;p7)))))`

About: