---

Step * of Lemma not-has-value-bottom

¬(⊥)↓
BY
{ (RepUR ``has-value`` 0
   THEN skip{both uses of strictness for are for callbyvalue:}
   THEN Strictness
   THEN (D 0 THENA Auto)
   THEN (Assert ⌜0 ~ ⊥⌝⋅ THENA (SqequalSqle THEN Auto))
   THEN (Assert ⌜eval x = 0 in 1 ~ eval x = 0 in 2⌝⋅ THENA (HypSubst (-1) 0 THEN Strictness THEN Auto))
   THEN Reduce (-1)
   THEN Auto
   THEN Assert ⌜1 = 2 ∈ ℤ⌝⋅
   THEN Auto
   THEN HypSubst (-1) 0
   THEN Auto) }

---

Latex:

---

Latex:
\mneg{}(\mbot{})\mdownarrow{}


By

---

Latex:
(RepUR  ``has-value``  0
  THEN  skip\{both  uses  of  strictness  for  are  for  callbyvalue:\}
  THEN  Strictness
  THEN  (D  0  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}0  \msim{}  \mbot{}\mkleeneclose{}\mcdot{}  THENA  (SqequalSqle  THEN  Auto))
  THEN  (Assert  \mkleeneopen{}eval  x  =  0  in  1  \msim{}  eval  x  =  0  in  2\mkleeneclose{}\mcdot{}  THENA  (HypSubst  (-1)  0  THEN  Strictness  THEN  Auto)\000C)
  THEN  Reduce  (-1)
  THEN  Auto
  THEN  Assert  \mkleeneopen{}1  =  2\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  HypSubst  (-1)  0
  THEN  Auto)

---

Home Index