---

Step * 1 2 1 1 2 2 1 of Lemma no-excluded-middle-using-partial


1. ∀P:ℙ. (P ∨ (¬P))
2. h : n:partial(ℤ) ⟶ {b:𝔹| ↑b ⇐⇒ (n)↓} 
3. value-type(ℤ)
4. fix((λx.if h x then ⊥ else 0 fi )) ∈ partial(ℤ)
⊢ (fix((λx.if h x then ⊥ else 0 fi )))↓
BY
{ TACTIC:( Decide ⌜↑(h fix((λx.if h x then ⊥ else 0 fi )))⌝⋅ THENA Auto) }

1
1. ∀P:ℙ. (P ∨ (¬P))
2. h : n:partial(ℤ) ⟶ {b:𝔹| ↑b ⇐⇒ (n)↓} 
3. value-type(ℤ)
4. fix((λx.if h x then ⊥ else 0 fi )) ∈ partial(ℤ)
5. ↑(h fix((λx.if h x then ⊥ else 0 fi )))
⊢ (fix((λx.if h x then ⊥ else 0 fi )))↓

2
1. ∀P:ℙ. (P ∨ (¬P))
2. h : n:partial(ℤ) ⟶ {b:𝔹| ↑b ⇐⇒ (n)↓} 
3. value-type(ℤ)
4. fix((λx.if h x then ⊥ else 0 fi )) ∈ partial(ℤ)
5. ¬↑(h fix((λx.if h x then ⊥ else 0 fi )))
⊢ (fix((λx.if h x then ⊥ else 0 fi )))↓

---

Latex:

---

Latex:

1.  \mforall{}P:\mBbbP{}.  (P  \mvee{}  (\mneg{}P))
2.  h  :  n:partial(\mBbbZ{})  {}\mrightarrow{}  \{b:\mBbbB{}|  \muparrow{}b  \mLeftarrow{}{}\mRightarrow{}  (n)\mdownarrow{}\} 
3.  value-type(\mBbbZ{})
4.  fix((\mlambda{}x.if  h  x  then  \mbot{}  else  0  fi  ))  \mmember{}  partial(\mBbbZ{})
\mvdash{}  (fix((\mlambda{}x.if  h  x  then  \mbot{}  else  0  fi  )))\mdownarrow{}


By

---

Latex:
TACTIC:(  Decide  \mkleeneopen{}\muparrow{}(h  fix((\mlambda{}x.if  h  x  then  \mbot{}  else  0  fi  )))\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index