Who Cites Kind-deq?
Kind-deq	Def KindDeq == union-deq(IdLnkId;Id;product-deq(IdLnk;Id;IdLnkDeq;IdDeq);IdDeq)
idlnk-deq	Def IdLnkDeq == product-deq(Id;Id;IdDeq;product-deq(Id;;IdDeq;NatDeq))
id-deq	Def IdDeq == product-deq(Atom;;AtomDeq;NatDeq)
IdLnk	Def IdLnk == IdId
	Thm* IdLnk  Type
Id	Def Id == Atom
	Thm* Id  Type
product-deq	Def product-deq(A;B;a;b) == <proddeq(a;b),prod-deq(A;B;a;b)>
union-deq	Def union-deq(A;B;a;b) == <sumdeq(a;b),sum-deq(A;B;a;b)>
nat-deq	Def NatDeq == <a,b. a=b,nat_DASH_deq_DASH_aux{1:l}>
atom-deq	Def AtomDeq == <a,b. a=bAtom,atom_DASH_deq_DASH_aux{1:l}>
nat	Def  == {i:| 0i }
	Thm*   Type
prod-deq	Def prod-deq(A;B;a;b) Def == (A,B,a,b,p,q. q/q1,q2. Def == (p/p1,p2. Def == (b/eq,b1. Def == (a/e1,a1. Def == ((%1.%1 Def == ((%1.(<%.<(%1.%1(p1,q1)/%4,%5. %4((%1.%1)((%1.*)(*))))(a1) Def == ((%1.(<%.,(%1.%1(p2,q2)/%4,%5. %4((%1.%1)((%1.*)(*))))(b1)> Def == ((%1.(,%.%/%1,%2. *>)) Def == (((%1.%1.2) Def == ((((%1.%1 Def == ((((%1.(<p1,p2> = <q1,q2>  AB Def == ((((%1.,<p1,p2> = <q1,q2>  AB Def == ((((%1.,((e1(p1,q1))(eq(p2,q2))) Def == ((((%1.,(e1(p1,q1)) & (eq(p2,q2)) Def == ((((%1.,(%1.%1)((%1.<%2.%2,%2.%2>)(*)) Def == ((((%1.,(%1.%1) Def == ((((%1.,((%1.%1(e1(p1,q1),eq(p2,q2))) Def == ((((%1.,((p,q. InjCase(q; x. InjCase(p Def == ((((%1.,((p,q. InjCase(q; x. InjCase; x. <%.<*,*>,%.*> Def == ((((%1.,((p,q. InjCase(q; x. InjCase; y. <%.<any(%),*> Def == ((((%1.,((p,q. InjCase(q; x. InjCase; y. ,%.%/%1,%2. any(%1)>) Def == ((((%1.,((p,q. ; y. Def == ((((%1.,((p,q. InjCase(p Def == ((((%1.,((p,q. InjCase; x. <%.<*,any(%)>,%.%/%1,%2. any(%2)> Def == ((((%1.,((p,q. InjCase; y. <%.<any(%),any(%)> Def == ((((%1.,((p,q. InjCase; y. ,%.%/%1,%2. any(%2)>)))))) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.(%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.(%5 Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.(((%4.%4) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.((((%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.((((%5 Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.((((((%4.%4) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.(((((((%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.(((((((%6((%4.%4)((%4.%4)(%3)))) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.(((((((%)))) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.((((%2)))) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.(%1) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.(%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.(%5 Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.(((%4.%4) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.((((%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.((((%6 Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.((((((%4.%4) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.(((((((%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.(((((((%6((%4.%4)((%4.%4)(%3)))) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.(((((((%1)))) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.((((%2)))) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.(%)> Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.(%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.(%6 Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.(((%4.%4) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.((((%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.((((%5 Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.((((((%4.%4) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.(((((((%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.(((((((%5((%4.%4)((%4.%4)(%3)))) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.(((((((%)))) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.((((%2)))) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.(%1) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.(%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.(%6 Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.(((%4.%4) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.((((%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.((((%6 Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.((((((%4.%4) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.(((((((%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.(((((((%5((%4.%4)((%4.%4)(%3)))) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.(((((((%1)))) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.((((%2)))) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.(%)>>)))) Def == (A Def == ,B Def == ,a Def == ,b)
proddeq	Def proddeq(a;b)(p,q) == (1of(a)(1of(p),1of(q)))(1of(b)(2of(p),2of(q)))
	Thm* A,B:Type, a:EqDecider(A), b:EqDecider(B). proddeq(a;b)  ABAB
sum-deq	Def sum-deq(A;B;a;b) Def == (A,B,a,b,p,q. Def == (InjCase(q; x. InjCase(p Def == (InjCase(q; x. InjCase; x1. b/eq,b1. Def == (InjCase(q; x. InjCase; x1. a/e1,a1. Def == (InjCase(q; x. InjCase; x1. <%.(%1.%1(x1,x)/%4,%5. Def == (InjCase(q; x. InjCase; x1. <%.(%4 Def == (InjCase(q; x. InjCase; x1. <%.(((%1.%1) Def == (InjCase(q; x. InjCase; x1. <%.((((%1.*) Def == (InjCase(q; x. InjCase; x1. <%.(((((%1.%1(x)) Def == (InjCase(q; x. InjCase; x1. <%.((((((%1.%1(x1)) Def == (InjCase(q; x. InjCase; x1. <%.(((((((%1.%1(B)) Def == (InjCase(q; x. InjCase; x1. <%.((((((((%1.%1(A)) Def == (InjCase(q; x. InjCase; x1. <%.((((((((A,B,x1,x,%. (%1.%1) Def == (InjCase(q; x. InjCase; x1. <%.((((((((A,B,x1,x,%. ((%1.(%2.*)(*)) Def == (InjCase(q; x. InjCase; x1. <%.((((((((A,B,x1,x,%. ((%)))))))))) Def == (InjCase(q; x. InjCase; x1. <%.(a1) Def == (InjCase(q; x. InjCase; x1. ,%.*> Def == (InjCase(q; x. InjCase; y. b/eq,b1. Def == (InjCase(q; x. InjCase; y. a/e1,a1. Def == (InjCase(q; x. InjCase; y. <%.(%1.any((%1(*)))) Def == (InjCase(q; x. InjCase; y. <%.((%1.%1(x)) Def == (InjCase(q; x. InjCase; y. <%.(((%1.%1(y)) Def == (InjCase(q; x. InjCase; y. <%.((((%1.%1(B)) Def == (InjCase(q; x. InjCase; y. <%.(((((%1.%1(A)) Def == (InjCase(q; x. InjCase; y. <%.(((((A,B,y,x,%. Def == (InjCase(q; x. InjCase; y. <%.((((((%1. Def == (InjCase(q; x. InjCase; y. <%.((((((InjCase(%1 Def == (InjCase(q; x. InjCase; y. <%.((((((InjCase; %2. any(%2) Def == (InjCase(q; x. InjCase; y. <%.((((((InjCase; %3. (%4.any(%4)) Def == (InjCase(q; x. InjCase; y. <%.((((((InjCase; %3. ((%4.(%5.(%6. Def == (InjCase(q; x. InjCase; y. <%.((((((InjCase; %3. ((%4.(%5.(any(%6)) Def == (InjCase(q; x. InjCase; y. <%.((((((InjCase; %3. ((%4.(%5.(*)) Def == (InjCase(q; x. InjCase; y. <%.((((((InjCase; %3. ((%4.(*)) Def == (InjCase(q; x. InjCase; y. <%.((((((InjCase; %3. ((%)))) Def == (InjCase(q; x. InjCase; y. <%.(((((((%1.%1)(inr(%.*)))))))) Def == (InjCase(q; x. InjCase; y. ,%.*>) Def == (; y. Def == (InjCase(p Def == (InjCase; x. b/eq,b1. Def == (InjCase; x. a/e1,a1. Def == (InjCase; x. <%.(%1.any((%1(*)))) Def == (InjCase; x. <%.((%1.%1(y)) Def == (InjCase; x. <%.(((%1.%1(x)) Def == (InjCase; x. <%.((((%1.%1(B)) Def == (InjCase; x. <%.(((((%1.%1(A)) Def == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase(%1 Def == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase; %2. any(%2) Def == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase; %3. (%4.any(%4)) Def == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase; %3. ((%4.(%5.(%6. Def == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase; %3. ((%4.(%5.(any(%6)) Def == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase; %3. ((%4.(%5.(*)) Def == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase; %3. ((%4.(*)) Def == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase; %3. ((%)))) Def == (InjCase; x. <%.(((((A,B,x,y,%. ((%1.%1)(inr(%.*)))))))) Def == (InjCase; x. ,%.*> Def == (InjCase; y1. b/eq,b1. Def == (InjCase; y1. a/e1,a1. Def == (InjCase; y1. <%.(%1.%1(y1,y)/%4,%5. Def == (InjCase; y1. <%.(%4 Def == (InjCase; y1. <%.(((%1.%1) Def == (InjCase; y1. <%.((((%1.*) Def == (InjCase; y1. <%.(((((%1.%1(y)) Def == (InjCase; y1. <%.((((((%1.%1(y1)) Def == (InjCase; y1. <%.(((((((%1.%1(B)) Def == (InjCase; y1. <%.((((((((%1.%1(A)) Def == (InjCase; y1. <%.((((((((A,B,y1,y,%. (%1.%1) Def == (InjCase; y1. <%.((((((((A,B,y1,y,%. ((%1.(%2.*)(*))(%)))))))))) Def == (InjCase; y1. <%.(b1) Def == (InjCase; y1. ,%.*>))) Def == (A Def == ,B Def == ,a Def == ,b)
sumdeq	Def sumdeq(a;b)(p,q) Def == InjCase(p; pa. InjCase(q; qa. 1of(a)(pa,qa); qb. false); pb. Def == InjCase(q; qa. false; qb. 1of(b)(pb,qb)))
	Thm* A,B:Type, a:EqDecider(A), b:EqDecider(B). sumdeq(a;b)  (A+B)(A+B)
eq_int	Def i=j == if i=j true ; false fi
	Thm* i,j:. (i=j)
eq_atom	Def x=yAtom == if x=yAtomtrue; false fi
	Thm* x,y:Atom. x=yAtom
le	Def AB == B<A
	Thm* i,j:. (ij)  Prop
assert	Def b == if b True else False fi
	Thm* b:. b  Prop
band	Def pq == if p q else false fi
	Thm* p,q:. (pq)
pi2	Def 2of(t) == t.2
	Thm* A:Type, B:(AType), p:(a:AB(a)). 2of(p)  B(1of(p))
pi1	Def 1of(t) == t.1
	Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p)  A
not	Def A == A  False
	Thm* A:Prop. (A)  Prop

Syntax:

KindDeq

has structure:

Kind-deq

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