---

Step * 1 of Lemma split-gap_wf

.....equality..... 
1. T : Type
2. f : T ⟶ ℤ
3. L : T List
⊢ split-gap(f;L) ~ TERMOF{split-at-first-gap-ext:o, \\v:l, i:l} f L
BY
{ xxx(RW (SubC (TagC (mk_tag_term 15))) 0 THEN Auto)xxx }

---

Latex:

---

Latex:
.....equality..... 
1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  \mBbbZ{}
3.  L  :  T  List
\mvdash{}  split-gap(f;L)  \msim{}  TERMOF\{split-at-first-gap-ext:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}  f  L


By

---

Latex:
xxx(RW  (SubC  (TagC  (mk\_tag\_term  15)))  0  THEN  Auto)xxx

---

Home Index