---

Step * of Lemma is-above-pair

∀[A:Type]. ∀[B:A ⟶ Type]. ∀[a:A]. ∀[b:B[a]].
  ∀z:Base. (is-above(a:A × B[a];<a, b>;z) ⇒ (∃c,d:Base. ((z ~ <c, d>) ∧ is-above(A;a;c) ∧ is-above(B[a];b;d))))
BY
{ (Auto
   THEN (InstConcl [⌜fst(z)⌝;⌜snd(z)⌝]⋅ THENA Auto)
   THEN RepeatFor 2 (D (-1))
   THEN (InstLemma `pair-eta` [⌜y⌝]⋅ THENA Auto)⋅
   THEN HypSubst' -1 -2
   THEN HypSubst' -1 -3
   THEN Thin (-1)
   THEN (EqHD (-2) THENA Auto)
   THEN All Reduce
   THEN ((FLemma `has-value-monotonic` [-1] THENA (Reduce 0 THEN Auto))
         THEN ((FLemma `has-value-implies-dec-ispair-2` [-1]⋅ THENM D -1) THENA Auto)
         )⋅) }

1
1. [A] : Type
2. [B] : A ⟶ Type
3. [a] : A
4. [b] : B[a]
5. z : Base
6. y : Base
7. (fst(y)) = a ∈ A
8. (snd(y)) = b ∈ B[fst(y)]
9. <fst(y), snd(y)> ≤ z
10. (z)↓
11. z ~ <fst(z), snd(z)>
⊢ (z ~ <fst(z), snd(z)>) ∧ is-above(A;a;fst(z)) ∧ is-above(B[a];b;snd(z))

2
1. [A] : Type
2. [B] : A ⟶ Type
3. [a] : A
4. [b] : B[a]
5. z : Base
6. y : Base
7. (fst(y)) = a ∈ A
8. (snd(y)) = b ∈ B[fst(y)]
9. <fst(y), snd(y)> ≤ z
10. (z)↓
11. ∀a,b:Base.  (if z is a pair then a otherwise b ~ b)
⊢ (z ~ <fst(z), snd(z)>) ∧ is-above(A;a;fst(z)) ∧ is-above(B[a];b;snd(z))

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[a:A].  \mforall{}[b:B[a]].
    \mforall{}z:Base.  (is-above(a:A  \mtimes{}  B[a];<a,  b>z)  {}\mRightarrow{}  (\mexists{}c,d:Base.  ((z  \msim{}  <c,  d>)  \mwedge{}  is-above(A;a;c)  \mwedge{}  is-above(\000CB[a];b;d))))


By

---

Latex:
(Auto
  THEN  (InstConcl  [\mkleeneopen{}fst(z)\mkleeneclose{};\mkleeneopen{}snd(z)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (D  (-1))
  THEN  (InstLemma  `pair-eta`  [\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THENA  Auto)\mcdot{}
  THEN  HypSubst'  -1  -2
  THEN  HypSubst'  -1  -3
  THEN  Thin  (-1)
  THEN  (EqHD  (-2)  THENA  Auto)
  THEN  All  Reduce
  THEN  ((FLemma  `has-value-monotonic`  [-1]  THENA  (Reduce  0  THEN  Auto))
              THEN  ((FLemma  `has-value-implies-dec-ispair-2`  [-1]\mcdot{}  THENM  D  -1)  THENA  Auto)
              )\mcdot{})

---

Home Index