PVS‎ > ‎exercises‎ > ‎Euclid‎ > ‎

### quotient_remainder_TCC2

 An explanationWhy does PVS generate quotient_remainder_TCC2 subtype TCC quotient_remainder_TCC2: OBLIGATION  FORALL (d: nat1, n: nat,          v: [d11: {z: [nat, nat1] | m(z) < m(n, d)} -> (qr?(d11`1, d11`2))]):    NOT n < d IMPLIES     qr?(n, d)(LET (q: nat, r: nat) = v(n - d, d) IN (1 + q, r)) when type checking quotient_remainder recursive function quotient_remainder(n: nat, d: nat1): RECURSIVE (qr?(n, d))  = IF n (qr?(n1, d1))]):    NOT n < d IMPLIES     qr?(n, d)(LET (q: nat, r: nat) = v(n - d, d) IN (1 + q, r)) where the type assumed for v clearly resembles that of quotient_remainder. We actually have: quotient_remainder: [                       n1: nat, d1: nat1 -> (qr?(n1, d1))]                 v: [{n1: nat, d1: nat1 | m(n1, d1) < m(n, d) -> (qr?(n1, d1))] The only difference is that the domain of v is smaller than the domain of quotient_remainder for two reasons: v type is specified in the context of n and d, and thus depends on these two parameters, v is defined only on the pairs (n1, d1) whose measure m is smaller than that of (n, d) input: this is reasonable, since the recursive call precisely applies to (n-d, d) whose measure m is smaller than that of (n, d). Finally, the meaning of the TCC is the following: assuming that the result (q, r) of the recursive call satisfies the output type specification (qr?(n-d, d)), then prove that the LET form itself yields a result of the desired type (qr?(n, d)). In other words, the TCC is essentially equivalent to: quotient_remainder_TCC2'': OBLIGATION  FORALL (d: nat1, n: nat,          qr: (qr?(n-d, d))):     NOT n < d IMPLIES      qr?(n, d)(LET (q, r) = qr IN (1 + q, r)) Indeed, when we look at the actual proof of the TCC, we see that the reference to v is soon replaced with a (q, r) pair.