---

Step * 1 of Lemma assert-is_int


1. T : Type
2. value-type(T)
3. T ⊆r Base
4. x : T
5. x ∈ ℤ
6. ∀[u,v:Top].  (if x is an integer then u else v ~ v)
⊢ False
BY
{ ((InstHyp [⌜0⌝;⌜1⌝] (-1)⋅ THENA Auto) THEN Reduce -1 THEN Auto) }

1
1. T : Type
2. value-type(T)
3. T ⊆r Base
4. x : T
5. x ∈ ℤ
6. ∀[u,v:Top].  (if x is an integer then u else v ~ v)
7. 0 ~ 1
⊢ False

---

Latex:

---

Latex:

1.  T  :  Type
2.  value-type(T)
3.  T  \msubseteq{}r  Base
4.  x  :  T
5.  x  \mmember{}  \mBbbZ{}
6.  \mforall{}[u,v:Top].    (if  x  is  an  integer  then  u  else  v  \msim{}  v)
\mvdash{}  False


By

---

Latex:
((InstHyp  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)  THEN  Reduce  -1  THEN  Auto)

---

Home Index