### Nuprl Lemma : nth-stream-zip

`∀[f:Top]. ∀[n:ℕ]. ∀[as,bs:stream(Top)].  (s-nth(n;stream-zip(f;as;bs)) ~ f s-nth(n;as) s-nth(n;bs))`

Proof

Definitions occuring in Statement :  stream-zip: `stream-zip(f;as;bs)` s-nth: `s-nth(n;s)` stream: `stream(A)` nat: `ℕ` uall: `∀[x:A]. B[x]` top: `Top` apply: `f a` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` nat: `ℕ` implies: `P `` Q` false: `False` ge: `i ≥ j ` guard: `{T}` uimplies: `b supposing a` prop: `ℙ` s-nth: `s-nth(n;s)` stream-zip: `stream-zip(f;as;bs)` eq_int: `(i =z j)` all: `∀x:A. B[x]` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` and: `P ∧ Q` ifthenelse: `if b then t else f fi ` subtype_rel: `A ⊆r B` bfalse: `ff` exists: `∃x:A. B[x]` or: `P ∨ Q` sq_type: `SQType(T)` bnot: `¬bb` assert: `↑b` subtract: `n - m` nequal: `a ≠ b ∈ T ` not: `¬A` decidable: `Dec(P)` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` top: `Top` le: `A ≤ B` less_than': `less_than'(a;b)` true: `True` has-value: `(a)↓`
Lemmas referenced :  nat_properties less_than_transitivity1 less_than_irreflexivity ge_wf less_than_wf stream_wf top_wf btrue_wf bool_wf eqtt_to_assert assert_of_eq_int stream-ext subtype_rel_weakening equal_wf eqff_to_assert eq_int_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int decidable__le subtract_wf false_wf not-ge-2 less-iff-le condition-implies-le minus-one-mul zero-add minus-one-mul-top minus-add minus-minus add-associates add-swap add-commutes add_functionality_wrt_le add-zero le-add-cancel le_weakening nat_wf value-type-has-value int-value-type
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setElimination rename intWeakElimination lambdaFormation natural_numberEquality independent_isectElimination independent_functionElimination voidElimination sqequalRule lambdaEquality dependent_functionElimination isect_memberEquality sqequalAxiom unionElimination equalityElimination equalityTransitivity equalitySymmetry productElimination because_Cache applyEquality productEquality dependent_pairFormation promote_hyp instantiate cumulativity callbyvalueReduce sqleReflexivity independent_pairFormation addEquality voidEquality intEquality minusEquality

Latex:
\mforall{}[f:Top].  \mforall{}[n:\mBbbN{}].  \mforall{}[as,bs:stream(Top)].    (s-nth(n;stream-zip(f;as;bs))  \msim{}  f  s-nth(n;as)  s-nth(n;bs))

Date html generated: 2017_04_14-AM-07_47_44
Last ObjectModification: 2017_02_27-PM-03_17_46

Theory : co-recursion

Home Index