104

1 
\idx{refl_type} A type ==> A = A),


2 
\idx{refl_elem} a : A ==> a = a : A


3 


4 
\idx{sym_type} A = B ==> B = A


5 
\idx{sym_elem} a = b : A ==> b = a : A


6 


7 
\idx{trans_type} [ A = B; B = C ] ==> A = C


8 
\idx{trans_elem} [ a = b : A; b = c : A ] ==> a = c : A


9 


10 
\idx{equal_types} [ a : A; A = B ] ==> a : B


11 
\idx{equal_typesL} [ a = b : A; A = B ] ==> a = b : B


12 


13 
\idx{subst_type} [ a : A; !!z. z:A ==> B(z) type ] ==> B(a) type


14 


15 
\idx{subst_typeL} [ a = c : A; !!z. z:A ==> B(z) = D(z)


16 
] ==> B(a) = D(c)


17 
\idx{subst_elem} [ a : A; !!z. z:A ==> b(z):B(z) ] ==> b(a):B(a)


18 


19 
\idx{subst_elemL} [ a = c : A; !!z. z:A ==> b(z) = d(z) : B(z)


20 
] ==> b(a) = d(c) : B(a)


21 


22 
\idx{refl_red} Reduce(a,a)


23 
\idx{red_if_equal} a = b : A ==> Reduce(a,b)


24 
\idx{trans_red} [ a = b : A; Reduce(b,c) ] ==> a = c : A


25 


26 


27 
\idx{NF} N type


28 


29 
\idx{NI0} 0 : N


30 
\idx{NI_succ} a : N ==> succ(a) : N


31 
\idx{NI_succL} a = b : N ==> succ(a) = succ(b) : N


32 


33 
\idx{NE} [ p: N; a: C(0);


34 
!!u v. [ u: N; v: C(u) ] ==> b(u,v): C(succ(u))


35 
] ==> rec(p, a, %u v.b(u,v)) : C(p)


36 


37 
\idx{NEL} [ p = q : N; a = c : C(0);


38 
!!u v. [ u: N; v: C(u) ] ==> b(u,v) = d(u,v): C(succ(u))


39 
] ==> rec(p, a, %u v.b(u,v)) = rec(q,c,d) : C(p)


40 


41 
\idx{NC0} [ a: C(0);


42 
!!u v. [ u: N; v: C(u) ] ==> b(u,v): C(succ(u))


43 
] ==> rec(0, a, %u v.b(u,v)) = a : C(0)


44 


45 
\idx{NC_succ} [ p: N; a: C(0);


46 
!!u v. [ u: N; v: C(u) ] ==> b(u,v): C(succ(u))


47 
] ==> rec(succ(p), a, %u v.b(u,v)) =


48 
b(p, rec(p, a, %u v.b(u,v))) : C(succ(p))


49 


50 
\idx{zero_ne_succ} [ a: N; 0 = succ(a) : N ] ==> 0: F


51 


52 


53 
\idx{ProdF} [ A type; !!x. x:A ==> B(x) type ] ==> PROD x:A.B(x) type


54 
\idx{ProdFL} [ A = C; !!x. x:A ==> B(x) = D(x) ] ==>


55 
PROD x:A.B(x) = PROD x:C.D(x)


56 


57 
\idx{ProdI} [ A type; !!x. x:A ==> b(x):B(x)


58 
] ==> lam x.b(x) : PROD x:A.B(x)


59 
\idx{ProdIL} [ A type; !!x. x:A ==> b(x) = c(x) : B(x)


60 
] ==> lam x.b(x) = lam x.c(x) : PROD x:A.B(x)


61 


62 
\idx{ProdE} [ p : PROD x:A.B(x); a : A ] ==> p`a : B(a)


63 
\idx{ProdEL} [ p=q: PROD x:A.B(x); a=b : A ] ==> p`a = q`b : B(a)


64 


65 
\idx{ProdC} [ a : A; !!x. x:A ==> b(x) : B(x)


66 
] ==> (lam x.b(x)) ` a = b(a) : B(a)


67 


68 
\idx{ProdC2} p : PROD x:A.B(x) ==> (lam x. p`x) = p : PROD x:A.B(x)


69 


70 


71 
\idx{SumF} [ A type; !!x. x:A ==> B(x) type ] ==> SUM x:A.B(x) type


72 
\idx{SumFL} [ A = C; !!x. x:A ==> B(x) = D(x)


73 
] ==> SUM x:A.B(x) = SUM x:C.D(x)


74 


75 
\idx{SumI} [ a : A; b : B(a) ] ==> <a,b> : SUM x:A.B(x)


76 
\idx{SumIL} [ a=c:A; b=d:B(a) ] ==> <a,b> = <c,d> : SUM x:A.B(x)


77 


78 
\idx{SumE} [ p: SUM x:A.B(x);


79 
!!x y. [ x:A; y:B(x) ] ==> c(x,y): C(<x,y>)


80 
] ==> split(p, %x y.c(x,y)) : C(p)


81 


82 
\idx{SumEL} [ p=q : SUM x:A.B(x);


83 
!!x y. [ x:A; y:B(x) ] ==> c(x,y)=d(x,y): C(<x,y>)


84 
] ==> split(p, %x y.c(x,y)) = split(q, % x y.d(x,y)) : C(p)


85 


86 
\idx{SumC} [ a: A; b: B(a);


87 
!!x y. [ x:A; y:B(x) ] ==> c(x,y): C(<x,y>)


88 
] ==> split(<a,b>, %x y.c(x,y)) = c(a,b) : C(<a,b>)


89 


90 
\idx{fst_def} fst(a) == split(a, %x y.x)


91 
\idx{snd_def} snd(a) == split(a, %x y.y)


92 


93 


94 
\idx{PlusF} [ A type; B type ] ==> A+B type


95 
\idx{PlusFL} [ A = C; B = D ] ==> A+B = C+D


96 


97 
\idx{PlusI_inl} [ a : A; B type ] ==> inl(a) : A+B


98 
\idx{PlusI_inlL} [ a = c : A; B type ] ==> inl(a) = inl(c) : A+B


99 


100 
\idx{PlusI_inr} [ A type; b : B ] ==> inr(b) : A+B


101 
\idx{PlusI_inrL} [ A type; b = d : B ] ==> inr(b) = inr(d) : A+B


102 


103 
\idx{PlusE} [ p: A+B;


104 
!!x. x:A ==> c(x): C(inl(x));


105 
!!y. y:B ==> d(y): C(inr(y))


106 
] ==> when(p, %x.c(x), %y.d(y)) : C(p)


107 


108 
\idx{PlusEL} [ p = q : A+B;


109 
!!x. x: A ==> c(x) = e(x) : C(inl(x));


110 
!!y. y: B ==> d(y) = f(y) : C(inr(y))


111 
] ==> when(p, %x.c(x), %y.d(y)) = when(q, %x.e(x), %y.f(y)) : C(p)


112 


113 
\idx{PlusC_inl} [ a: A;


114 
!!x. x:A ==> c(x): C(inl(x));


115 
!!y. y:B ==> d(y): C(inr(y))


116 
] ==> when(inl(a), %x.c(x), %y.d(y)) = c(a) : C(inl(a))


117 


118 
\idx{PlusC_inr} [ b: B;


119 
!!x. x:A ==> c(x): C(inl(x));


120 
!!y. y:B ==> d(y): C(inr(y))


121 
] ==> when(inr(b), %x.c(x), %y.d(y)) = d(b) : C(inr(b))


122 


123 
\idx{EqF} [ A type; a : A; b : A ] ==> Eq(A,a,b) type


124 
\idx{EqFL} [ A=B; a=c: A; b=d : A ] ==> Eq(A,a,b) = Eq(B,c,d)


125 
\idx{EqI} a = b : A ==> eq : Eq(A,a,b)


126 
\idx{EqE} p : Eq(A,a,b) ==> a = b : A


127 
\idx{EqC} p : Eq(A,a,b) ==> p = eq : Eq(A,a,b)


128 


129 
\idx{FF} F type


130 
\idx{FE} [ p: F; C type ] ==> contr(p) : C


131 
\idx{FEL} [ p = q : F; C type ] ==> contr(p) = contr(q) : C


132 


133 
\idx{TF} T type


134 
\idx{TI} tt : T


135 
\idx{TE} [ p : T; c : C(tt) ] ==> c : C(p)


136 
\idx{TEL} [ p = q : T; c = d : C(tt) ] ==> c = d : C(p)


137 
\idx{TC} p : T ==> p = tt : T)


138 


139 


140 
\idx{replace_type} [ B = A; a : A ] ==> a : B


141 
\idx{subst_eqtyparg} [ a=c : A; !!z. z:A ==> B(z) type ] ==> B(a)=B(c)


142 


143 
\idx{subst_prodE} [ p: Prod(A,B); a: A; !!z. z: B(a) ==> c(z): C(z)


144 
] ==> c(p`a): C(p`a)


145 


146 
\idx{SumIL2} [ c=a : A; d=b : B(a) ] ==> <c,d> = <a,b> : Sum(A,B)


147 


148 
\idx{SumE_fst} p : Sum(A,B) ==> fst(p) : A


149 


150 
\idx{SumE_snd} [ p: Sum(A,B); A type; !!x. x:A ==> B(x) type


151 
] ==> snd(p) : B(fst(p))


152 


153 


154 


155 
\idx{add_def} a#+b == rec(a, b, %u v.succ(v))


156 
\idx{diff_def} ab == rec(b, a, %u v.rec(v, 0, %x y.x))


157 
\idx{absdiff_def} ab == (ab) #+ (ba)


158 
\idx{mult_def} a#*b == rec(a, 0, %u v. b #+ v)


159 


160 
\idx{mod_def} a//b == rec(a, 0, %u v.


161 
rec(succ(v)  b, 0, %x y.succ(v)))


162 


163 
\idx{quo_def} a/b == rec(a, 0, %u v.


164 
rec(succ(u) // b, succ(v), %x y.v))


165 


166 


167 
\idx{add_typing} [ a:N; b:N ] ==> a #+ b : N


168 
\idx{add_typingL} [ a=c:N; b=d:N ] ==> a #+ b = c #+ d : N


169 
\idx{addC0} b:N ==> 0 #+ b = b : N


170 
\idx{addC_succ} [ a:N; b:N ] ==> succ(a) #+ b = succ(a #+ b) : N


171 
\idx{mult_typing} [ a:N; b:N ] ==> a #* b : N


172 
\idx{mult_typingL} [ a=c:N; b=d:N ] ==> a #* b = c #* d : N


173 
\idx{multC0} b:N ==> 0 #* b = 0 : N


174 
\idx{multC_succ} [ a:N; b:N ] ==> succ(a) #* b = b #+ (a #* b) : N


175 
\idx{diff_typing} [ a:N; b:N ] ==> a  b : N


176 
\idx{diff_typingL} [ a=c:N; b=d:N ] ==> a  b = c  d : N


177 
\idx{diffC0} a:N ==> a  0 = a : N


178 
\idx{diff_0_eq_0} b:N ==> 0  b = 0 : N


179 


180 
\idx{diff_succ_succ} [ a:N; b:N ] ==> succ(a)  succ(b) = a  b : N


181 


182 
\idx{add_assoc} [ a:N; b:N; c:N ] ==> (a #+ b) #+ c = a #+ (b #+ c) : N


183 


184 
\idx{add_commute} [ a:N; b:N ] ==> a #+ b = b #+ a : N


185 


186 
\idx{mult_right0} a:N ==> a #* 0 = 0 : N


187 


188 
\idx{mult_right_succ} [ a:N; b:N ] ==> a #* succ(b) = a #+ (a #* b) : N


189 


190 
\idx{mult_commute} [ a:N; b:N ] ==> a #* b = b #* a : N


191 


192 
\idx{add_mult_dist} [ a:N; b:N; c:N ] ==> (a #+ b) #* c = (a #* c) #+ (b #* c) : N


193 


194 
\idx{mult_assoc} [ a:N; b:N; c:N ] ==> (a #* b) #* c = a #* (b #* c) : N


195 


196 
\idx{diff_self_eq_0} a:N ==> a  a = 0 : N


197 


198 
\idx{add_inverse_diff_lemma}


199 
b:N ==> ?a : PROD x:N. Eq(N, bx, 0) > Eq(N, b #+ (xb), x)


200 


201 
\idx{add_inverse_diff} [ a:N; b:N; ba = 0 : N ] ==> b #+ (ab) = a : N


202 


203 
\idx{absdiff_typing} [ a:N; b:N ] ==> a  b : N


204 
\idx{absdiff_typingL} [ a=c:N; b=d:N ] ==> a  b = c  d : N


205 
\idx{absdiff_self_eq_0} a:N ==> a  a = 0 : N


206 
\idx{absdiffC0} a:N ==> 0  a = a : N


207 


208 
\idx{absdiff_succ_succ} [ a:N; b:N ] ==> succ(a)  succ(b) = a  b : N


209 
\idx{absdiff_commute} [ a:N; b:N ] ==> a  b = b  a : N


210 


211 
\idx{add_eq0_lemma} [ a:N; b:N ] ==> ?c : PROD u: Eq(N,a#+b,0) . Eq(N,a,0)


212 


213 
\idx{add_eq0} [ a:N; b:N; a #+ b = 0 : N ] ==> a = 0 : N


214 


215 
\idx{absdiff_eq0_lem}


216 
[ a:N; b:N; a  b = 0 : N ] ==>


217 
?a : SUM v: Eq(N, ab, 0) . Eq(N, ba, 0)


218 


219 
\idx{absdiff_eq0} [ a  b = 0 : N; a:N; b:N ] ==> a = b : N


220 


221 
\idx{mod_typing} [ a:N; b:N ] ==> a//b : N


222 
\idx{mod_typingL} [ a=c:N; b=d:N ] ==> a//b = c//d : N


223 
\idx{modC0} b:N ==> 0//b = 0 : N


224 
\idx{modC_succ}


225 
[ a:N; b:N ] ==> succ(a)//b = rec(succ(a//b)  b, 0, %x y.succ(a//b)) : N


226 


227 
\idx{quo_typing} [ a:N; b:N ] ==> a / b : N


228 
\idx{quo_typingL} [ a=c:N; b=d:N ] ==> a / b = c / d : N


229 
\idx{quoC0} b:N ==> 0 / b = 0 : N


230 
[ a:N; b:N ] ==> succ(a) / b =


231 
rec(succ(a)//b, succ(a / b), %x y. a / b) : N


232 
\idx{quoC_succ2} [ a:N; b:N ] ==>


233 
succ(a) / b =rec(succ(a//b)  b, succ(a / b), %x y. a / b) : N


234 


235 
\idx{iszero_decidable}


236 
a:N ==> rec(a, inl(eq), %ka kb.inr(<ka, eq>)) :


237 
Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))


238 


239 
\idx{mod_quo_equality} [ a:N; b:N ] ==> a//b #+ (a/b) #* b = a : N


240 


241 
