Step
*
of Lemma
Wcmp_transitivity
∀[A:Type]. ∀[B:A ⟶ Type].
∀w1,w2,w3:W(A;a.B[a]).
((((w1 < w2) ⇒ (w2 ≤ w3) ⇒ (w1 < w3)) ∧ ((w1 ≤ w2) ⇒ (w2 < w3) ⇒ (w1 < w3)))
∧ ((w1 ≤ w2) ⇒ (w2 ≤ w3) ⇒ (w1 ≤ w3)))
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN RepeatFor 3 (UseWInductionLemma) THEN Auto) }
1
1. [A] : Type
2. [B] : A ⟶ Type
3. a : A@i
4. f : B[a] ⟶ W(A;a.B[a])@i
5. ∀b:B[a]. ∀w2,w3:W(A;a.B[a]).
(((((f b) < w2) ⇒ (w2 ≤ w3) ⇒ ((f b) < w3)) ∧ (((f b) ≤ w2) ⇒ (w2 < w3) ⇒ ((f b) < w3)))
∧ (((f b) ≤ w2) ⇒ (w2 ≤ w3) ⇒ ((f b) ≤ w3)))@i
6. a@0 : A@i
7. f@0 : B[a@0] ⟶ W(A;a.B[a])@i
8. ∀b:B[a@0]. ∀w3:W(A;a.B[a]).
((((Wsup(a;f) < (f@0 b)) ⇒ ((f@0 b) ≤ w3) ⇒ (Wsup(a;f) < w3))
∧ ((Wsup(a;f) ≤ (f@0 b)) ⇒ ((f@0 b) < w3) ⇒ (Wsup(a;f) < w3)))
∧ ((Wsup(a;f) ≤ (f@0 b)) ⇒ ((f@0 b) ≤ w3) ⇒ (Wsup(a;f) ≤ w3)))@i
9. a@1 : A@i
10. f@1 : B[a@1] ⟶ W(A;a.B[a])@i
11. ∀b:B[a@1]
((((Wsup(a;f) < Wsup(a@0;f@0)) ⇒ (Wsup(a@0;f@0) ≤ (f@1 b)) ⇒ (Wsup(a;f) < (f@1 b)))
∧ ((Wsup(a;f) ≤ Wsup(a@0;f@0)) ⇒ (Wsup(a@0;f@0) < (f@1 b)) ⇒ (Wsup(a;f) < (f@1 b))))
∧ ((Wsup(a;f) ≤ Wsup(a@0;f@0)) ⇒ (Wsup(a@0;f@0) ≤ (f@1 b)) ⇒ (Wsup(a;f) ≤ (f@1 b))))@i
12. Wsup(a;f) < Wsup(a@0;f@0)@i
13. Wsup(a@0;f@0) ≤ Wsup(a@1;f@1)@i
⊢ Wsup(a;f) < Wsup(a@1;f@1)
2
1. [A] : Type
2. [B] : A ⟶ Type
3. a : A@i
4. f : B[a] ⟶ W(A;a.B[a])@i
5. ∀b:B[a]. ∀w2,w3:W(A;a.B[a]).
(((((f b) < w2) ⇒ (w2 ≤ w3) ⇒ ((f b) < w3)) ∧ (((f b) ≤ w2) ⇒ (w2 < w3) ⇒ ((f b) < w3)))
∧ (((f b) ≤ w2) ⇒ (w2 ≤ w3) ⇒ ((f b) ≤ w3)))@i
6. a@0 : A@i
7. f@0 : B[a@0] ⟶ W(A;a.B[a])@i
8. ∀b:B[a@0]. ∀w3:W(A;a.B[a]).
((((Wsup(a;f) < (f@0 b)) ⇒ ((f@0 b) ≤ w3) ⇒ (Wsup(a;f) < w3))
∧ ((Wsup(a;f) ≤ (f@0 b)) ⇒ ((f@0 b) < w3) ⇒ (Wsup(a;f) < w3)))
∧ ((Wsup(a;f) ≤ (f@0 b)) ⇒ ((f@0 b) ≤ w3) ⇒ (Wsup(a;f) ≤ w3)))@i
9. a@1 : A@i
10. f@1 : B[a@1] ⟶ W(A;a.B[a])@i
11. ∀b:B[a@1]
((((Wsup(a;f) < Wsup(a@0;f@0)) ⇒ (Wsup(a@0;f@0) ≤ (f@1 b)) ⇒ (Wsup(a;f) < (f@1 b)))
∧ ((Wsup(a;f) ≤ Wsup(a@0;f@0)) ⇒ (Wsup(a@0;f@0) < (f@1 b)) ⇒ (Wsup(a;f) < (f@1 b))))
∧ ((Wsup(a;f) ≤ Wsup(a@0;f@0)) ⇒ (Wsup(a@0;f@0) ≤ (f@1 b)) ⇒ (Wsup(a;f) ≤ (f@1 b))))@i
12. (Wsup(a;f) < Wsup(a@0;f@0)) ⇒ (Wsup(a@0;f@0) ≤ Wsup(a@1;f@1)) ⇒ (Wsup(a;f) < Wsup(a@1;f@1))
13. Wsup(a;f) ≤ Wsup(a@0;f@0)@i
14. Wsup(a@0;f@0) < Wsup(a@1;f@1)@i
⊢ Wsup(a;f) < Wsup(a@1;f@1)
3
1. [A] : Type
2. [B] : A ⟶ Type
3. a : A@i
4. f : B[a] ⟶ W(A;a.B[a])@i
5. ∀b:B[a]. ∀w2,w3:W(A;a.B[a]).
(((((f b) < w2) ⇒ (w2 ≤ w3) ⇒ ((f b) < w3)) ∧ (((f b) ≤ w2) ⇒ (w2 < w3) ⇒ ((f b) < w3)))
∧ (((f b) ≤ w2) ⇒ (w2 ≤ w3) ⇒ ((f b) ≤ w3)))@i
6. a@0 : A@i
7. f@0 : B[a@0] ⟶ W(A;a.B[a])@i
8. ∀b:B[a@0]. ∀w3:W(A;a.B[a]).
((((Wsup(a;f) < (f@0 b)) ⇒ ((f@0 b) ≤ w3) ⇒ (Wsup(a;f) < w3))
∧ ((Wsup(a;f) ≤ (f@0 b)) ⇒ ((f@0 b) < w3) ⇒ (Wsup(a;f) < w3)))
∧ ((Wsup(a;f) ≤ (f@0 b)) ⇒ ((f@0 b) ≤ w3) ⇒ (Wsup(a;f) ≤ w3)))@i
9. a@1 : A@i
10. f@1 : B[a@1] ⟶ W(A;a.B[a])@i
11. ∀b:B[a@1]
((((Wsup(a;f) < Wsup(a@0;f@0)) ⇒ (Wsup(a@0;f@0) ≤ (f@1 b)) ⇒ (Wsup(a;f) < (f@1 b)))
∧ ((Wsup(a;f) ≤ Wsup(a@0;f@0)) ⇒ (Wsup(a@0;f@0) < (f@1 b)) ⇒ (Wsup(a;f) < (f@1 b))))
∧ ((Wsup(a;f) ≤ Wsup(a@0;f@0)) ⇒ (Wsup(a@0;f@0) ≤ (f@1 b)) ⇒ (Wsup(a;f) ≤ (f@1 b))))@i
12. (Wsup(a;f) < Wsup(a@0;f@0)) ⇒ (Wsup(a@0;f@0) ≤ Wsup(a@1;f@1)) ⇒ (Wsup(a;f) < Wsup(a@1;f@1))
13. Wsup(a;f) ≤ Wsup(a@0;f@0)@i
14. Wsup(a@0;f@0) ≤ Wsup(a@1;f@1)@i
15. (Wsup(a@0;f@0) < Wsup(a@1;f@1)) ⇒ (Wsup(a;f) < Wsup(a@1;f@1))
⊢ Wsup(a;f) ≤ Wsup(a@1;f@1)
Latex:
Latex:
\mforall{}[A:Type]. \mforall{}[B:A {}\mrightarrow{} Type].
\mforall{}w1,w2,w3:W(A;a.B[a]).
((((w1 < w2) {}\mRightarrow{} (w2 \mleq{} w3) {}\mRightarrow{} (w1 < w3)) \mwedge{} ((w1 \mleq{} w2) {}\mRightarrow{} (w2 < w3) {}\mRightarrow{} (w1 < w3)))
\mwedge{} ((w1 \mleq{} w2) {}\mRightarrow{} (w2 \mleq{} w3) {}\mRightarrow{} (w1 \mleq{} w3)))
By
Latex:
(RepeatFor 2 ((D 0 THENA Auto)) THEN RepeatFor 3 (UseWInductionLemma) THEN Auto)
Home
Index