1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "sandwich_corollary.ma".
19 λR.λml:mlattice R.λxn:sequence ml.λx:ml.
20 increasing ? xn → upper_bound ? xn x ∧ xn ⇝ x.
23 λR.λml:mlattice R.λxn:sequence ml.λx:ml.
24 decreasing ? xn → lower_bound ? xn x ∧ xn ⇝ x.
28 ∀R.∀ml:mlattice R.∀xn:sequence ml.increasing ? xn → (* BUG again the wrong coercion is chosen *)
29 ∀x,y:apart_of_metric_space ? ml.supremum ?? xn x → supremum ?? xn y → x ≈ y.
30 intros (R ml xn Hxn x y Sx Sy);
31 elim (Sx Hxn) (_ Hx); elim (Sy Hxn) (_ Hy);
32 apply (tends_uniq ?? xn ?? Hx Hy);
35 definition shift : ∀R.∀ml:mlattice R.∀xn:sequence ml.nat → sequence ml ≝
36 λR.λml:mlattice R.λxn:sequence ml.λm:nat.λn.xn (n+m).
39 λR.λml:mlattice R.λxn:sequence ml.λk:nat.
40 let rec ank_aux (i : nat) ≝
42 [ O ⇒ (shift ?? xn k) O
43 | S n1 ⇒ (shift ?? xn k) (S n1) ∧ ank_aux n1]
47 λR.λml:mlattice R.λxn:sequence ml.λk:nat.
48 let rec bnk_aux (i : nat) ≝
50 [ O ⇒ (shift ?? xn k) O
51 | S n1 ⇒ (shift ?? xn k) (S n1) ∨ bnk_aux n1]
55 ∀R.∀ml:mlattice R.∀xn:sequence ml.∀m.decreasing ? (ank ?? xn m).
56 intros (R ml xn m); unfold; intro n; simplify; apply lem;
61 ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k,n:nat.
62 ((ank ?? xn k) (S n)) ≈ (xn k ∧ ank ?? xn (S k) n).
63 intros (R ml xn k n); elim n; simplify; [apply meet_comm]
64 simplify in H; apply (Eq≈ ? (feq_ml ???? (H))); clear H;
65 apply (Eq≈ ? (meet_assoc ????));
66 apply (Eq≈ ?? (eq_sym ??? (meet_assoc ????)));
67 apply feq_mr; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));
68 simplify; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));