---

Step * of Lemma last-decomp2

No Annotations
∀[l:Top List]. (l ~ if (||l|| =z 0) then [] else firstn(||l|| - 1;l) @ [last(l)] fi )
BY
{ (Auto THEN AutoSplit) }

1
1. l : Top List
2. ||l|| = 0 ∈ ℤ
⊢ l ~ []

2
1. l : Top List
2. ||l|| ≠ 0
⊢ l ~ firstn(||l|| - 1;l) @ [last(l)]

---

Latex:

---

Latex:
No  Annotations
\mforall{}[l:Top  List].  (l  \msim{}  if  (||l||  =\msubz{}  0)  then  []  else  firstn(||l||  -  1;l)  @  [last(l)]  fi  )


By

---

Latex:
(Auto  THEN  AutoSplit)

---

Home Index