Step * 2 of Lemma fun-path-append


1. Type
2. T ⟶ T
3. T
4. List
5. ∀[L2:T List]. ∀[x,y,z:T].  uiff(z=f*(x) via [y L2];{y=f*(x) via [y L2] ∧ z=f*(y) via [y]})
⊢ ∀[L2:T List]. ∀[x,y,z:T].  uiff(z=f*(x) via [u v] [y L2];{y=f*(x) via [y L2] ∧ z=f*(y) via [u v] [y]})
BY
TACTIC:ParallelLast }

1
1. Type
2. T ⟶ T
3. T
4. List
5. ∀[L2:T List]. ∀[x,y,z:T].  uiff(z=f*(x) via [y L2];{y=f*(x) via [y L2] ∧ z=f*(y) via [y]})
6. [L2] List
7. ∀[x,y,z:T].  uiff(z=f*(x) via [y L2];{y=f*(x) via [y L2] ∧ z=f*(y) via [y]})
⊢ ∀[x,y,z:T].  uiff(z=f*(x) via [u v] [y L2];{y=f*(x) via [y L2] ∧ z=f*(y) via [u v] [y]})


Latex:


Latex:

1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  T
3.  u  :  T
4.  v  :  T  List
5.  \mforall{}[L2:T  List].  \mforall{}[x,y,z:T].
          uiff(z=f*(x)  via  v  @  [y  /  L2];\{y=f*(x)  via  [y  /  L2]  \mwedge{}  z=f*(y)  via  v  @  [y]\})
\mvdash{}  \mforall{}[L2:T  List].  \mforall{}[x,y,z:T].
        uiff(z=f*(x)  via  [u  /  v]  @  [y  /  L2];\{y=f*(x)  via  [y  /  L2]  \mwedge{}  z=f*(y)  via  [u  /  v]  @  [y]\})


By


Latex:
TACTIC:ParallelLast




Home Index