proposition: Lemma chain_algo : forall c : Call, conform c -> gencode c.
proof: Proof. refine (well_founded_induction Wf_Call_lt (fun c => conform c -> gencode c) _). intros c; case c; [ intro p | intros p n0 | intros p n0 ]; intros hr hc; simpl in hc. apply (COND3 (fun n => gencode (Call_M n)) p); auto with arith. intros h; rewrite h; apply M3. intros q h; rewrite h; apply M2q. refine (fun q _ _ => C2M p q (hr (Call_C p q) _ _)); auto with arith. constructor 2; auto with arith. simpl in |- *; auto with arith. elim hc; intros hc1 hc2. cut (n0 > 0); [ intro Hn0 | unfold gt in |- *; apply lt_trans with 1; auto with arith ]. elim (eucl_dev n0 Hn0 p); intros q r E1 E2. elim (zerop r); intro Z. rewrite Z in E2; rewrite <- plus_n_O in E2; rewrite E2. cut (0 < q). intro Hq. refine (MMC n0 q (hr (Call_M n0) _ _) (hr (Call_M q) _ _)). constructor 3; auto with arith. simpl in |- *; auto with arith. constructor 3. rewrite E2; rewrite <- mult_comm; apply mult_p_lt_qp; auto with arith. simpl in |- *; auto with arith. apply quotient_positive with p n0; auto with arith. apply le_lt_trans with n0; auto with arith. cut (0 < q). intro Hq; rewrite E2. refine (KMC n0 q r (hr (Call_K n0 r) _ _) (hr (Call_M q) _ _)). constructor 5; auto with arith. simpl in |- *; auto with arith. constructor 3; auto with arith. rewrite E2; auto with arith. simpl in |- *; auto with arith. apply lt_O_q with n0 r; auto; rewrite <- E2; auto. elim hc; intros hc1 hc2. cut (n0 > 0); [ intro Hn0 | unfold gt in |- *; auto with arith ]. elim (eucl_dev n0 Hn0 p); intros q r E1 E2. elim (zerop r); intro Z. rewrite Z in E2; rewrite <- plus_n_O in E2; rewrite E2. cut (0 < q). intro Hq. refine (MMK n0 q (hr (Call_M n0) _ _) (hr (Call_M q) _ _)). constructor 4; auto with arith. simpl in |- *; auto with arith. constructor 4. rewrite E2; apply mult_p_le_pq; auto with arith. simpl in |- *; auto with arith. apply quotient_positive with p n0; auto with arith. apply le_lt_trans with n0; auto with arith. cut (0 < q). intro Hq; rewrite E2. refine (KMK n0 q r (hr (Call_K n0 r) _ _) (hr (Call_M q) _ _)). constructor 6; auto with arith. simpl in |- *; auto with arith. constructor 4; auto with arith. rewrite E2; auto with arith. simpl in |- *; auto with arith. apply lt_O_q with n0 r; auto; rewrite <- E2; auto. Qed.
imports: monoid spec Constants machine Euclid Le_lt_compl euclid shift two_power log2_spec develop Arith Peano_dec Compare_dec strategies Mult_compl Wf_nat Wf_compl