Nuprl Lemma : comb_for_gt_wf

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


Proof




Definitions occuring in Statement :  prop: gt: i > j 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 :  gt_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  >  j)  \mmember{}  i:\mBbbZ{}  {}\mrightarrow{}  j:\mBbbZ{}  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  \mBbbP{}



Date html generated: 2016_05_13-PM-04_01_49
Last ObjectModification: 2015_12_26-AM-10_56_58

Theory : int_1


Home Index