---

Step * 1 1 of Lemma is-above-inr


1. [A] : Type
2. [B] : Type
3. [a] : B
4. z : Base
5. y : Base
6. y = (inr a ) ∈ (A + B)
7. y ≤ z
8. c : Base
9. y ~ inr c 
10. (inr c ) = (inr a ) ∈ (A + B)
11. inr c  ≤ z
⊢ (z ~ inr outr(z) ) ∧ is-above(B;a;outr(z))
BY
{ ((FLemma `has-value-monotonic` [-1] THENA (Reduce 0 THEN Auto))
   THEN ((FLemma `has-value-implies-dec-isinr-2` [-1]⋅ THENM D -1) THENA Auto)
   )⋅ }

1
1. [A] : Type
2. [B] : Type
3. [a] : B
4. z : Base
5. y : Base
6. y = (inr a ) ∈ (A + B)
7. y ≤ z
8. c : Base
9. y ~ inr c 
10. (inr c ) = (inr a ) ∈ (A + B)
11. inr c  ≤ z
12. (z)↓
13. z ~ inr outr(z) 
⊢ (z ~ inr outr(z) ) ∧ is-above(B;a;outr(z))

2
1. [A] : Type
2. [B] : Type
3. [a] : B
4. z : Base
5. y : Base
6. y = (inr a ) ∈ (A + B)
7. y ≤ z
8. c : Base
9. y ~ inr c 
10. (inr c ) = (inr a ) ∈ (A + B)
11. inr c  ≤ z
12. (z)↓
13. ∀a,b:Base.  (if z is inr then a else b ~ b)
⊢ (z ~ inr outr(z) ) ∧ is-above(B;a;outr(z))

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  [a]  :  B
4.  z  :  Base
5.  y  :  Base
6.  y  =  (inr  a  )
7.  y  \mleq{}  z
8.  c  :  Base
9.  y  \msim{}  inr  c 
10.  (inr  c  )  =  (inr  a  )
11.  inr  c    \mleq{}  z
\mvdash{}  (z  \msim{}  inr  outr(z)  )  \mwedge{}  is-above(B;a;outr(z))


By

---

Latex:
((FLemma  `has-value-monotonic`  [-1]  THENA  (Reduce  0  THEN  Auto))
  THEN  ((FLemma  `has-value-implies-dec-isinr-2`  [-1]\mcdot{}  THENM  D  -1)  THENA  Auto)
  )\mcdot{}

---

Home Index