Step
*
of Lemma
fun-path-member-connected
∀[T:Type]. ∀f:T ⟶ T. ∀L:T List. ∀x,y:T. ∀a:T. ((a ∈ L)
⇒ {x is f*(a) ∧ a is f*(y)}) supposing x=f*(y) via L
BY
{ xxx(RepeatFor 2 ((D 0 THENA Auto))
THEN Assert ⌜∀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⌝
⋅
)xxx }
1
.....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
2
1. [T] : Type
2. f : T ⟶ T
3. ∀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
⊢ ∀L:T List. ∀x,y:T. ∀a:T. ((a ∈ L)
⇒ {x is f*(a) ∧ a is f*(y)}) supposing x=f*(y) via L
Latex:
Latex:
\mforall{}[T:Type]
\mforall{}f:T {}\mrightarrow{} T. \mforall{}L:T List. \mforall{}x,y:T.
\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(RepeatFor 2 ((D 0 THENA Auto))
THEN Assert \mkleeneopen{}\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\mkleeneclose{}
\mcdot{}
)xxx
Home
Index