|
Require Import Arith.Compare_dec.
Require Import Unicode.Utf8.
Fixpoint my_nat_iter (n : nat) {A} (f : A → A) (x : A) : A :=
match n with
| O => x
| S n' => f (my_nat_iter n' f x)
end.
Definition gcd_IT_F (f : nat * nat → nat) (mn : nat * nat) : nat :=
match mn with
| (0, 0) => 0
| (0, S n') => S n'
| (S m', 0) => S m'
| (S m', S n') =>
match le_gt_dec (S m') (S n') with
| left _ => f (S m', S n' - S m')
| right _ => f (S m' - S n', S n')
end
end.
Axiom max_correct_l : ∀ m n : nat, m <= max m n.
Axiom max_correct_r : ∀ m n : nat, n <= max m n.
Hint Resolve max_correct_l max_correct_r : arith.
Theorem foo : ∀ p p' p'' : nat, p'' < S (max p (max p' p'')).
Proof.
intros.
Timeout 3 eauto with arith.
Qed.
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
