---

Step * 1 2 1 2 1 of Lemma wfd-subtrees_wf


1. A : Type
2. a : A
3. p : ℕ ⟶ A
4. L : ℕ List
⊢ map(p;L) ~ map(λx.if (x + 1 =z 0) then a else p ((x + 1) - 1) fi ;L)
BY
{ (ListInd (-1) THEN Reduce 0 THEN Try (AutoSplit)) }

1
1. A : Type
2. a : A
3. p : ℕ ⟶ A
⊢ [] ~ []

---

Latex:

---

Latex:

1.  A  :  Type
2.  a  :  A
3.  p  :  \mBbbN{}  {}\mrightarrow{}  A
4.  L  :  \mBbbN{}  List
\mvdash{}  map(p;L)  \msim{}  map(\mlambda{}x.if  (x  +  1  =\msubz{}  0)  then  a  else  p  ((x  +  1)  -  1)  fi  ;L)


By

---

Latex:
(ListInd  (-1)  THEN  Reduce  0  THEN  Try  (AutoSplit))

---

Home Index