Nuprl Lemma : comb_for_ge_wf

λi,j,z. (i ≥ ) ∈ i:ℤ ⟶ j:ℤ ⟶ (↓True) ⟶ ℙ


Proof




Definitions occuring in Statement :  prop: ge: i ≥  squash: T true: True member: t ∈ T lambda: λx.A[x] function: x:A ⟶ B[x] int:
Definitions unfolded in proof :  member: t ∈ T uall: [x:A]. B[x] prop:
Lemmas referenced :  ge_wf squash_wf true_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaEquality cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis intEquality

Latex:
\mlambda{}i,j,z.  (i  \mgeq{}  j  )  \mmember{}  i:\mBbbZ{}  {}\mrightarrow{}  j:\mBbbZ{}  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  \mBbbP{}



Date html generated: 2016_05_13-PM-04_01_50
Last ObjectModification: 2015_12_26-AM-10_56_57

Theory : int_1


Home Index