---

Step * 1 of Lemma has-valueall-apply


1. a : Base
2. g : Base
3. has-valueall(g a)
4. (g a)↓
5. (g)↓
⊢ has-valueall(g)
BY
{ TACTIC:((Assert ¬(⊥)↓ BY
                 Auto)
          THEN (D 0 THEN Auto)
          THEN (CallByValueReduce 0 THENA Auto)
          THEN Repeat (HVimplies  0 [1])
          THEN RW (SweepUpC StuckApplyC) 4
          THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  Base
2.  g  :  Base
3.  has-valueall(g  a)
4.  (g  a)\mdownarrow{}
5.  (g)\mdownarrow{}
\mvdash{}  has-valueall(g)


By

---

Latex:
TACTIC:((Assert  \mneg{}(\mbot{})\mdownarrow{}  BY
                              Auto)
                THEN  (D  0  THEN  Auto)
                THEN  (CallByValueReduce  0  THENA  Auto)
                THEN  Repeat  (HVimplies    0  [1])
                THEN  RW  (SweepUpC  StuckApplyC)  4
                THEN  Auto)

---

Home Index