---

Step * 1 of Lemma fun-path-member-connected

.....assertion..... 
1. [T] : Type
2. f : T ⟶ T
⊢ ∀L:T List. ∀x,y:T.  (x ∈ L) ∧ (∀a:T. ((a ∈ L) ⇒ {x is f*(a) ∧ a is f*(y)})) supposing x=f*(y) via L
BY
{ xxx(BLemma `fun-path-induction`
      THEN Auto
      THEN (Try ((RWO "member_singleton" (-1))) THENM Try ((RWO "cons_member" (-1))) THENM SplitOrHyps)
      THEN Auto
      THEN UnfoldTopAb 0
      THEN Auto
      THEN (Assert f y = f+(y) BY
                  (Auto THEN OnSomeHyp ParallelOp)))xxx }

1
1. [T] : Type
2. f : T ⟶ T
3. L : T List
4. x : T
5. y : T
6. z : T
7. x = (f y) ∈ T
8. ¬(x = y ∈ T)
9. (y ∈ [y / L])
10. ∀a:T. ((a ∈ [y / L]) ⇒ {y is f*(a) ∧ a is f*(z)})
11. (x ∈ [x; [y / L]])
12. a : T
13. a = x ∈ T
14. x is f*(a)
15. f y = f+(y)
⊢ a is f*(z)

2
1. [T] : Type
2. f : T ⟶ T
3. L : T List
4. x : T
5. y : T
6. z : T
7. x = (f y) ∈ T
8. ¬(x = y ∈ T)
9. (y ∈ [y / L])
10. ∀a:T. ((a ∈ [y / L]) ⇒ {y is f*(a) ∧ a is f*(z)})
11. (x ∈ [x; [y / L]])
12. a : T
13. (a ∈ [y / L])
14. f y = f+(y)
⊢ x is f*(a)

---

Latex:

---

Latex:
.....assertion..... 
1.  [T]  :  Type
2.  f  :  T  {}\mrightarrow{}  T
\mvdash{}  \mforall{}L:T  List.  \mforall{}x,y:T.
        (x  \mmember{}  L)  \mwedge{}  (\mforall{}a:T.  ((a  \mmember{}  L)  {}\mRightarrow{}  \{x  is  f*(a)  \mwedge{}  a  is  f*(y)\}))  supposing  x=f*(y)  via  L


By

---

Latex:
xxx(BLemma  `fun-path-induction`
        THEN  Auto
        THEN  (Try  ((RWO  "member\_singleton"  (-1)))
                    THENM  Try  ((RWO  "cons\_member"  (-1)))
                    THENM  SplitOrHyps)
        THEN  Auto
        THEN  UnfoldTopAb  0
        THEN  Auto
        THEN  (Assert  f  y  =  f+(y)  BY
                                (Auto  THEN  OnSomeHyp  ParallelOp)))xxx

---

Home Index