---

Step * 1 1 2 1 2 of Lemma partial-int-not-discrete


1. ∀k:ℕ. (λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) k) ∈ ℝ ⟶ partial(ℤ))
2. ⊥ = 1 ∈ partial(ℤ)
⊢ False
BY
{ ((InstLemma `termination-equality` [⌜ℤ⌝;⌜1⌝;⌜⊥⌝]⋅ THENA Auto)
   THEN (InstLemma `value-type-has-value` [⌜ℤ⌝;⌜⊥⌝]⋅ THENA Auto)
   ) }

1
1. ∀k:ℕ. (λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) k) ∈ ℝ ⟶ partial(ℤ))
2. ⊥ = 1 ∈ partial(ℤ)
3. 1 = ⊥ ∈ ℤ
4. (⊥)↓
⊢ False

---

Latex:

---

Latex:

1.  \mforall{}k:\mBbbN{}.  (\mlambda{}x.(fix((\mlambda{}f,n.  if  4  <z  |x  (n  +  1)|  then  1  else  f  (n  +  1)  fi  ))  k)  \mmember{}  \mBbbR{}  {}\mrightarrow{}  partial(\mBbbZ{}))
2.  \mbot{}  =  1
\mvdash{}  False


By

---

Latex:
((InstLemma  `termination-equality`  [\mkleeneopen{}\mBbbZ{}\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}\mbot{}\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `value-type-has-value`  [\mkleeneopen{}\mBbbZ{}\mkleeneclose{};\mkleeneopen{}\mbot{}\mkleeneclose{}]\mcdot{}  THENA  Auto)
  )

---

Home Index