Goal of exercise on euclidian division

See how

• types can be used to specify program correction;
• proof obligations stem from specification;
• PVS pre-compiles well founded induction, from the type specification of a recursive function.

Step by step

• Restore euclid theory and proofs as usual from ~gloess/pvs/5.0.euclid.26oct2011.euclid.dmp.txt into your new ~login/pvs/euclid/ context;
• then follow indications given in comments:
• look at definitions present in euclid theory (nat1, m, qr?, quotient_remainder, quotient_remainder2) and quotient_remainder2_correct theorem (whose proof is given);
• analyze each proof obligation (TCC): where does it come from?
• DO NOT IMMEDIATELY LOOK at explanation for quotient_remainder_TCC2 (most interesting) subtype TCC for PVS 5.0!
• DO NOT IMMEDIATELY LOOK at quotient_remainder_TCC2 proof given in PVS 5.0 solution dump:
• ~gloess/pvs/5.0/euclid/5.0.euclid.26oct2011.euclid.proved_complete.dmp.txt;