---

Step * of Lemma fun-not-int

∀[f:ℕ+ ⟶ ℤ]. (isint(f) ~ ff)
BY
{ (Auto THEN (InstLemma `function-not-int` [⌜ℕ+⌝;⌜λ2a.ℤ⌝;⌜f⌝]⋅ THENA Auto)) }

1
.....antecedent..... 
1. f : ℕ+ ⟶ ℤ
⊢ ↓∃a:ℕ+. value-type(ℤ)

2
1. f : ℕ+ ⟶ ℤ
2. isint(f) ~ ff
⊢ isint(f) = ff

---

Latex:

---

Latex:
\mforall{}[f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}].  (isint(f)  \msim{}  ff)


By

---

Latex:
(Auto  THEN  (InstLemma  `function-not-int`  [\mkleeneopen{}\mBbbN{}\msupplus{}\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}a.\mBbbZ{}\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index