An explanation

Why 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<d
     THEN (0, n)
     ELSE LET (q, r)= quotient_remainder(n-d, d)
            IN (1+q, r)
    ENDIF
  MEASURE m   ?

The answer is that the LET resulting form, in the case where n≥d, must have the expected (qr?(n, d)) type. Since the LET form refers to quotient_remainder function, which is under definition, the proof obligation (which is generated before) cannot refer to quotient_remainder function (not yet defined): hence the use of v template, which mimics quotient_remainder, in the expression of the TCC.

The TCC can be rewritten into the more understandable form:

quotient_remainder_TCC2': OBLIGATION
  FORALL (d: nat1, n: nat,
          v: [{n1: nat, d1: nat1 | m(n1, d1) < m(n, d)} -> (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.