---

Step * 2 1 of Lemma rec-value-evalall


1. v : rec-value()
⊢ (evalall(v))↓
BY
{ ((Assert ⌜∀n:ℕ. ∀v:rec-value().  ((rec-value-height(v) ≤ n) ⇒ (evalall(v))↓)⌝⋅
   THENM (InstHyp [⌜rec-value-height(v)⌝;⌜v⌝] (-1)⋅ THEN Auto)
   )
   THEN Thin 1
   THEN InductionOnNat
   THEN Auto
   THEN SubsumeHyp ⌜atomic-values() ⋃ (rec-value() × rec-value()) ⋃ (rec-value() + rec-value())⌝ (-2)⋅
   THEN Try ((InstLemma `rec-value-ext` [] THEN D -1 THEN Hypothesis))
   THEN Try ((DoSubsume THEN (Declaration ⋅ ORELSE (InstLemma `rec-value-ext` [] THEN D -1 THEN Hypothesis))))
   THEN Repeat (D_b_union (-2)⋅)
   THEN Try ((D -2
              THEN Unfold `rec-value-height` -1
              THEN RecUnfold `co-value-height` (-1)
              THEN Reduce (-1)
              THEN Fold `rec-value-height` (-1)
              THEN Auto'
              THEN RecUnfold `evalall` 0
              THEN Reduce 0
              THEN Repeat ((CallByValueReduce 0 THENA Auto))
              THEN Reduce 0
              THEN Complete (Auto)))) }

1
1. n : ℤ
2. a1 : atomic-values()
3. rec-value-height(a1) ≤ 0
⊢ (evalall(a1))↓

2
1. n : ℤ
2. 0 < n
3. ∀v:rec-value(). ((rec-value-height(v) ≤ (n - 1)) ⇒ (evalall(v))↓)
4. a1 : atomic-values()
5. rec-value-height(a1) ≤ n
⊢ (evalall(a1))↓

---

Latex:

---

Latex:

1.  v  :  rec-value()
\mvdash{}  (evalall(v))\mdownarrow{}


By

---

Latex:
((Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  \mforall{}v:rec-value().    ((rec-value-height(v)  \mleq{}  n)  {}\mRightarrow{}  (evalall(v))\mdownarrow{})\mkleeneclose{}\mcdot{}
  THENM  (InstHyp  [\mkleeneopen{}rec-value-height(v)\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)
  )
  THEN  Thin  1
  THEN  InductionOnNat
  THEN  Auto
  THEN  SubsumeHyp  \mkleeneopen{}atomic-values()  \mcup{}  (rec-value()  \mtimes{}  rec-value())  \mcup{}  (rec-value()  +  rec-value())\mkleeneclose{}  (-2)\mcdot{}
  THEN  Try  ((InstLemma  `rec-value-ext`  []  THEN  D  -1  THEN  Hypothesis))
  THEN  Try  ((DoSubsume
                        THEN  (Declaration  \mcdot{}  ORELSE  (InstLemma  `rec-value-ext`  []  THEN  D  -1  THEN  Hypothesis))
                        ))
  THEN  Repeat  (D\_b\_union  (-2)\mcdot{})
  THEN  Try  ((D  -2
                        THEN  Unfold  `rec-value-height`  -1
                        THEN  RecUnfold  `co-value-height`  (-1)
                        THEN  Reduce  (-1)
                        THEN  Fold  `rec-value-height`  (-1)
                        THEN  Auto'
                        THEN  RecUnfold  `evalall`  0
                        THEN  Reduce  0
                        THEN  Repeat  ((CallByValueReduce  0  THENA  Auto))
                        THEN  Reduce  0
                        THEN  Complete  (Auto))))

---

Home Index