Nuprl Lemma : imax-wf-bar-nat


[x,y:bar(ℕ)].  (imax(x;y) ∈ bar(ℕ))


Proof




Definitions occuring in Statement :  bar: bar(T) imax: imax(a;b) nat: uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  bar: bar(T)
Lemmas referenced :  imax-wf-partial-nat
Rules used in proof :  cut lemma_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity hypothesis

Latex:
\mforall{}[x,y:bar(\mBbbN{})].    (imax(x;y)  \mmember{}  bar(\mBbbN{}))



Date html generated: 2016_07_08-PM-05_19_02
Last ObjectModification: 2016_01_06-AM-00_35_16

Theory : bar!type


Home Index