The value of a term exists and is unique

Proof

1. 1
   By strong induction on : assume every term of length has a value existing uniquely (the induction hypothesis, "IH"); show the same for of length .
2. 2
   By T32 (ii), is either for a unique , or for a unique - never both.
3. 3
   Variable case. If : the var clause of D089 forces , a specific element of since is a function (D087); by mutual exclusivity the func clause imposes no competing constraint, and by uniqueness of (T32 (ii)) this is the only value consistent with the var clause. Existence and uniqueness hold.
4. 4
   Function case, length bound. If with unique and : each for , by the same length bookkeeping as in the proof of T31 (each partial application there is obtained from by appending , so ).
5. 5
   By the IH, exists uniquely for every , so is a genuine function , i.e. a member of (D018, D085). The func clause of D089 then forces , a specific element of since is a function (D086); by mutual exclusivity and uniqueness of , this is the only value consistent with D089.
6. 6
   T08 concludes: exists and is unique for every .

Used by