Step
*
1
of Lemma
fun-path-cons
1. T : Type
2. f : T ⟶ T
3. x : T
4. y : T
5. z : T
⊢ uiff(z=f*(x) via [y];{(z = y ∈ T)
∧ ((y = (f hd([])) ∈ T) ∧ (¬(y = hd([]) ∈ T))) ∧ hd([])=f*(x) via [] supposing 0 < ||[]||
∧ x = y ∈ T supposing ¬0 < ||[]||})
BY
{ (RepUR ``guard fun-path last`` 0 THEN Auto) }
Latex:
Latex:
1. T : Type
2. f : T {}\mrightarrow{} T
3. x : T
4. y : T
5. z : T
\mvdash{} uiff(z=f*(x) via [y];\{(z = y)
\mwedge{} ((y = (f hd([]))) \mwedge{} (\mneg{}(y = hd([])))) \mwedge{} hd([])=f*(x) via [] supposing 0 < ||[]||
\mwedge{} x = y supposing \mneg{}0 < ||[]||\})
By
Latex:
(RepUR ``guard fun-path last`` 0 THEN Auto)
Home
Index