Nuprl Lemma : rel-path-between-cons

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  ∀L:T List. ∀x,y,z:T.
    (rel-path-between(T;R;x;y;[z / L])
    ⇐⇒

 (x = z ∈ T) ∧ y = z ∈ T supposing ↑null(L) ∧ (x R hd(L)) ∧ rel-path-between(T;R;hd(L);y;L) supposing ¬↑null(L))

Proof

Error : references

Latex:
\mforall{}[T:Type]. \mforall{}[R:T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}]. \mforall{}L:T List. \mforall{}x,y,z:T. (rel-path-between(T;R;x;y;[z / L]) \mLeftarrow{}{}\mRightarrow{} (x = z) \mwedge{} y = z supposing \muparrow{}null(L) \mwedge{} (x R hd(L)) \mwedge{} rel-path-between(T;R;hd(L);y;L) supposing \mneg{}\muparrow{}null(L)) Date html generated: 2020_05_19-PM-09_52_49 Last ObjectModification: 2020_02_07-AM-10_07_46 Theory : relations2 Home Index