COM	bar_primitives	The four basic primitives of the partial type library are: bar(T) the type containing elements of T and all divergent terms t in! T the assertion that t halts and t is in bar(T) T admissible the assertion that fixpoint induction may be performed over T T total the assertion that every element of T halts
DISP	bar	bar( < T:type:* > )== bar( < T > )
DISP	halt	Parens ::Prec(atomrel)::Index 0 :: {[SOFT} < e:term:L > {\\ }in! {- > 0} < T:type:L > { < -}{]} == < e > in! < T > Parens ::Prec(postop):: < e:term:E > halts== < e > halts
DISP	admiss	Parens ::Prec(postop):: < T:type:E > admissible== < T > admissible
DISP	total	Parens ::Prec(postop):: < T:Type:E > total== < T > total
COM	bar_com	We want to be able to form halting assertions t in! T whenever t is in bar(T). For this to be sound, T must not equate any convergent and divergent elements. We instead require the stronger condition that T contains only convergent elements. This seems to make things work out more nicely in practice.
RULE	barEquality	H bar(A) = bar(B) BY barEquality () H A = B H A total
RULE	barInclusion	H a = a' BY barInclusion level{i} H a = a' H bar(A) = bar(A)
RULE	bar_memberEquality	H a = a' BY bar_memberEquality level{i} z B C H a in! B a' in! C H, z:a in! B a = a' H bar(A)
COM	halt_com	We use a typed halting assertion t in! T rather than a simpler untyped halting condition for the following reason: For t in! T to be well-formed in a sequent, we need it to be functional over the hypotheses. With typed halting, we can simply require that t is in bar(T) and bar(T) is functional over the hypotheses. With untyped halting, we would have to show that t's halting behavior is functional over all the hypotheses, which would be impossible to ever prove.
RULE	haltEquality	H (a in! A) = (b in! B) BY haltEquality () H a = b H bar(A) = bar(B)
RULE	halt_axiomEquality	H, Ax = Ax BY halt_axiomEquality () H a in! A
RULE	haltUniversal	H a in! A BY haltUniversal B H a in! B H a = a
RULE	termination	H a = b BY termination () H a in! A H a = b
RULE	member_termination	H a = a BY member_termination () H a in! A
COM	bottom_com	Introducing special rules for bottom are just for convenience. It would have been possible to prove the existence of a divergent term (say, the fixpoint of the flip function), which by bar_memberEquality would have been divergent in every bar type.
RULE	bottomEquality	H Y (x.x) = Y (x.x) BY bottomEquality level{i} H bar(A) = bar(A)
RULE	bottomDivergent	H Void BY bottomDivergent x A H Y (x.x) in! A
COM	total_com	Totality has to be primitive. If we tried to define it as T total iff x:bar(T). x in! T well-formedness would depend upon bar(T) being well-formed, which is only the case if T is total. This would make totality non-negatable.
RULE	totalEquality	H, A total = B total BY totalEquality () H A = B
RULE	total_axiomEquality	H, Ax = Ax BY total_axiomEquality () H A total
RULE	totality	H a in! A BY totality () H A total H a = a
COM	admiss_com	The admissibility assertion, T admissible, is true whenever fixpoint induction can be performed on T.
RULE	admissEquality	H, A admissible = B admissible BY admissEquality () H A = B
RULE	admiss_axiomEquality	H, Ax = Ax BY admiss_axiomEquality () H A admissible
COM	fixpoint_com	This is the critical rule to the theory of partial types, but semantically speaking it says nothing, since admissibility means that fixpoint induction may be performed. So this is just the elimination form for admissibility.
RULE	fixpoint_induction	H Y f = Y f BY fixpoint_induction () H f = f H A admissible
COM	totality_com	Most types are total. In particular, unions, products and functions are total since the intro forms are canonical and halt computation. This specifies that this is a lazy computation system. In an eager system computation would continue within product and union intros at least. Set and quotient types are total when their underlying types are.
RULE	voidTotal	H, Void total BY voidTotal () No Subgoals
RULE	intTotal	H, total BY intTotal () No Subgoals
RULE	atomTotal	H, Atom total BY atomTotal () No Subgoals
RULE	equalityTotal	H, (a1 = a2) total BY equalityTotal level{i} H (a1 = a2) = (a1 = a2)
RULE	unionTotal	H, (A + B) total BY unionTotal level{i} H A + B = A + B
RULE	productTotal	H, (x:A B) total BY productTotal level{i} H x:A B = x:A B
RULE	functionTotal	H, (x:A B) total BY functionTotal level{i} H x:A B = x:A B
RULE	setTotal	H, {x:A| B} total BY setTotal level{i} H A total H {x:A| B} = {x:A| B}
RULE	quotientTotal	H, x,y:A//B total BY quotientTotal level{i} H A total H x,y:A//B = x,y:A//B
COM	admissibility_com	At present there are no rules showing admissibility for dependent products, sets or quotients, but we want some. The present situation is particularly unsatisfying since it makes it impossible to perform t he usual predicate fixpoint induction.
RULE	intAdmissible	H, admissible BY intAdmissible () No Subgoals
RULE	atomAdmissible	H, Atom admissible BY atomAdmissible () No Subgoals
RULE	equalityAdmissible	H, (a1 = a2) admissible BY equalityAdmissible level{i} H (a1 = a2) = (a1 = a2)
RULE	unionAdmissible	H, (A + B) admissible BY unionAdmissible () H A admissible H B admissible
RULE	functionAdmissible	H, (x:A B) admissible BY functionAdmissible () H A admissible H, x:A B admissible
RULE	prodAdmissible	H, (A B) admissible BY prodAdmissible () H A admissible H B admissible
ML	bar_basic_tactics	loadt `~crary/kml/prl/bar-basic-tactics` ;;
THM	total_wf	A:. A total
THM	bar_wf	A:. A total bar(A)
THM	halt_wf	A:. A total (a:bar(A). (a in! A) )
THM	admiss_wf	A:. A admissible
DISP	bottom_df	Bot== Bot
ABS	bottom	Bot == Y (x.x)
THM	bottom_wf	A:. A total Bot bar(A)
THM	bottom_diverge	A:. A total (Bot in! A)
THM	nat_total	total
COM	partial_term_com	For any strict n-place operator there will need to be n+2 partial term rules: 1) a rule for membership in the bar type op(t1, ..., tn) in bar(T) if for each i, ti in bar(Si) 2) a rule for halting op(t1, ..., tn) in! T if for each i, ti in! Si 3) n rules for inducement ti in! Si if op(t1, ..., tn) in! T None of these rules are derivable from the original typing rule op(t1, ..., tn) in T if for each i, ti in Si but the original typing rule is derivable from the halting rule and the totality and member_termination rules, so long as each Si is total. If op is nonstrict in position k, the kth subgoal of the halting rule would be dropped, as well as the kth inducement rule. At present, partial term rules are only in place for subtraction. They need to be put in for every operator.
RULE	subtract_barEquality	H, m1 - n1 = m2 - n2 BY subtract_barEquality () H m1 = m2 H n1 = n2
RULE	subtractHalt	H (e1 - e2) halts BY subHalt () H e1 halts H e2 halts
RULE	subtractInduceLeft	H e1 halts BY subInduceLeft e2 H (e1 - e2) halts H e1 = e1
RULE	subtractInduceRight	H e2 halts BY subInduceRight e1 H (e1 - e2) halts
COM	seq_com	One more primitive operator is the sequencing operator: the term " t1;  t2 " is equivalent to t2 if t1 halts. This allows us to embed eager progra mming systems in this one, and also is critical to deriving results in recur sion theory.
DISP	seq	EdAlias seq ::Parens :: < e1:term:L > ; < e2:term:E > == < e1 > ; < e2 >
RULE	seqEquality	H (e1; e2) = (e1'; e2') BY seqEquality B H e1 = e1' H e2 = e2'
RULE	seqReduce	H (e1; e2) = e2 BY seqReduce B H e1 in! B H e2 = e2
RULE	seqHalt	H (e1; e2) in! A BY seqHalt B H e1 in! B H e2 in! A
RULE	seqInduceLeft	H e1 in! A BY seqInduceLeft e2 B H (e1; e2) in! B H e1 = e1
RULE	seqInduceRight	H e2 in! A BY seqInduceRight e1 H (e1; e2) in! A
ML	bar_tactics	loadt `~crary/kml/prl/bar-tactics` ;;

the other theories