Nuprl Lemma : nth-stream-map

[f:Top]. ∀[n:ℕ]. ∀[as:stream(Top)].  (s-nth(n;stream-map(f;as)) s-nth(n;as))


Proof




Definitions occuring in Statement :  stream-map: stream-map(f;s) s-nth: s-nth(n;s) stream: stream(A) nat: uall: [x:A]. B[x] top: Top apply: a sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T nat: implies:  Q false: False ge: i ≥  guard: {T} uimplies: supposing a prop: s-nth: s-nth(n;s) stream-map: stream-map(f;s) 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 then else fi  subtype_rel: A ⊆B bfalse: ff exists: x:A. B[x] or: P ∨ Q sq_type: SQType(T) bnot: ¬bb assert: b subtract: m nequal: a ≠ b ∈  not: ¬A decidable: Dec(P) iff: ⇐⇒ Q rev_implies:  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:stream(Top)].    (s-nth(n;stream-map(f;as))  \msim{}  f  s-nth(n;as))



Date html generated: 2017_04_14-AM-07_47_53
Last ObjectModification: 2017_02_27-PM-03_18_21

Theory : co-recursion


Home Index