### Nuprl Lemma : is-list-approx-step

`∀j:ℕ+. ∀[x:Top]. (is-list-approx(j) x ~ is-list-fun() is-list-approx(j - 1) x)`

Proof

Definitions occuring in Statement :  is-list-approx: `is-list-approx(j)` is-list-fun: `is-list-fun()` nat_plus: `ℕ+` uall: `∀[x:A]. B[x]` top: `Top` all: `∀x:A. B[x]` apply: `f a` subtract: `n - m` natural_number: `\$n` sqequal: `s ~ t`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` member: `t ∈ T` is-list-approx: `is-list-approx(j)` top: `Top`
Lemmas referenced :  fun_exp_unroll_1 top_wf nat_plus_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality isect_memberEquality voidElimination voidEquality hypothesis sqequalAxiom

Latex:
\mforall{}j:\mBbbN{}\msupplus{}.  \mforall{}[x:Top].  (is-list-approx(j)  x  \msim{}  is-list-fun()  is-list-approx(j  -  1)  x)

Date html generated: 2016_05_15-PM-10_09_55
Last ObjectModification: 2015_12_27-PM-05_59_08

Theory : eval!all

Home Index