Nuprl Lemma : stream-pointwise_wf

[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (stream-pointwise(R) ∈ stream(T) ⟶ stream(T) ⟶ ℙ)


Proof




Definitions occuring in Statement :  stream-pointwise: stream-pointwise(R) stream: stream(A) uall: [x:A]. B[x] prop: member: t ∈ T function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T stream-pointwise: stream-pointwise(R) so_lambda: λ2x.t[x] infix_ap: y prop: so_apply: x[s]
Lemmas referenced :  bigrel_wf stream_wf and_wf s-hd_wf s-tl_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis lambdaEquality applyEquality functionEquality cumulativity universeEquality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    (stream-pointwise(R)  \mmember{}  stream(T)  {}\mrightarrow{}  stream(T)  {}\mrightarrow{}  \mBbbP{})



Date html generated: 2016_05_14-AM-06_24_30
Last ObjectModification: 2015_12_26-AM-11_58_03

Theory : co-recursion


Home Index