---

Step * of Lemma rec-value-list-is-rec-value

∀[x:rec-value() List]. (x ∈ rec-value())
BY
{ (((D 0 THENA Auto) THEN ListInd (-1))
   THEN SubsumeC ⌜atomic-values() ⋃ (rec-value() × rec-value()) ⋃ (rec-value() + rec-value())⌝⋅
   THEN Try ((InstLemma `rec-value-ext` [] THEN D -1 THEN Trivial))) }

1
[] ∈ atomic-values() ⋃ (rec-value() × rec-value()) ⋃ (rec-value() + rec-value())

2
1. u : rec-value()
2. v : rec-value() List
3. v ∈ rec-value()
⊢ [u / v] ∈ atomic-values() ⋃ (rec-value() × rec-value()) ⋃ (rec-value() + rec-value())

---

Latex:

---

Latex:
\mforall{}[x:rec-value()  List].  (x  \mmember{}  rec-value())


By

---

Latex:
(((D  0  THENA  Auto)  THEN  ListInd  (-1))
  THEN  SubsumeC  \mkleeneopen{}atomic-values()  \mcup{}  (rec-value()  \mtimes{}  rec-value())  \mcup{}  (rec-value()  +  rec-value())\mkleeneclose{}\mcdot{}
  THEN  Try  ((InstLemma  `rec-value-ext`  []  THEN  D  -1  THEN  Trivial)))

---

Home Index