---

Step * 1 of Lemma fun-connected-step-back


1. [T] : Type
2. f : T ⟶ T
3. x : T
4. y : T
5. L : T List
6. x=f*(y) via L
7. ¬(x = y ∈ T)
8. ¬↑null(L)
⊢ x is f*(f y)
BY
{ ((InstLemma `last_lemma` [⌜T⌝;⌜L⌝]⋅ THENA Auto)⋅ THEN UnfoldTopAb 0 THEN ParallelLast) }

1
1. [T] : Type
2. f : T ⟶ T
3. x : T
4. y : T
5. L : T List
6. x=f*(y) via L
7. ¬(x = y ∈ T)
8. ¬↑null(L)
9. L' : T List
10. L = (L' @ [last(L)]) ∈ (T List)
⊢ x=f*(f y) via L'

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  f  :  T  {}\mrightarrow{}  T
3.  x  :  T
4.  y  :  T
5.  L  :  T  List
6.  x=f*(y)  via  L
7.  \mneg{}(x  =  y)
8.  \mneg{}\muparrow{}null(L)
\mvdash{}  x  is  f*(f  y)


By

---

Latex:
((InstLemma  `last\_lemma`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THENA  Auto)\mcdot{}  THEN  UnfoldTopAb  0  THEN  ParallelLast)

---

Home Index