Nuprl Lemma : fibs-equal-map

fibs() stream-map(λn.fib(n);nats()) ∈ stream(ℕ)


Proof




Definitions occuring in Statement :  fibs: fibs() fib: fib(n) nats: nats() stream-map: stream-map(f;s) stream: stream(A) nat: lambda: λx.A[x] equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] uimplies: supposing a member: t ∈ T uall: [x:A]. B[x] label: ...$L... t nat: ge: i ≥  decidable: Dec(P) or: P ∨ Q not: ¬A implies:  Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False top: Top and: P ∧ Q prop: guard: {T} subtype_rel: A ⊆B true: True squash: T iff: ⇐⇒ Q rev_implies:  Q
Lemmas referenced :  nat_wf nat_properties decidable__equal_int full-omega-unsat intformand_wf intformnot_wf intformeq_wf itermVar_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_formula_prop_wf decidable__le fib_wf intformle_wf itermConstant_wf int_formula_prop_le_lemma int_term_value_constant_lemma istype-le s-nth_wf fibs_wf nats_wf stream-subtype top_wf istype-nat equal_wf squash_wf true_wf istype-universe nth-fibs nth-stream-map nth-nats subtype_rel_self iff_weakening_equal stream-extensionality stream-map_wf
Rules used in proof :  because_Cache lambdaFormation independent_isectElimination hypothesisEquality lambdaEquality hypothesis thin isectElimination sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution sqequalHypSubstitution lemma_by_obid cut introduction extract_by_obid setElimination rename dependent_functionElimination equalityTransitivity equalitySymmetry unionElimination natural_numberEquality approximateComputation independent_functionElimination Error :dependent_pairFormation_alt,  Error :lambdaEquality_alt,  int_eqEquality Error :isect_memberEquality_alt,  voidElimination sqequalRule independent_pairFormation Error :universeIsType,  Error :dependent_set_memberEquality_alt,  applyLambdaEquality applyEquality imageElimination Error :inhabitedIsType,  instantiate universeEquality imageMemberEquality baseClosed productElimination

Latex:
fibs()  =  stream-map(\mlambda{}n.fib(n);nats())



Date html generated: 2019_06_20-PM-02_28_09
Last ObjectModification: 2019_01_15-PM-03_33_57

Theory : num_thy_1


Home Index