Nuprl Lemma : comb_for_gcd_p_wf

λa,b,y,z. GCD(a;b;y) ∈ a:ℤ ⟶ b:ℤ ⟶ y:ℤ ⟶ (↓True) ⟶ ℙ


Proof




Definitions occuring in Statement :  gcd_p: GCD(a;b;y) prop: squash: T true: True member: t ∈ T lambda: λx.A[x] function: x:A ⟶ B[x] int:
Definitions unfolded in proof :  member: t ∈ T squash: T uall: [x:A]. B[x] prop:
Lemmas referenced :  gcd_p_wf squash_wf true_wf istype-int
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaEquality_alt,  sqequalHypSubstitution imageElimination cut introduction extract_by_obid isectElimination thin hypothesisEquality equalityTransitivity hypothesis equalitySymmetry Error :universeIsType,  Error :inhabitedIsType

Latex:
\mlambda{}a,b,y,z.  GCD(a;b;y)  \mmember{}  a:\mBbbZ{}  {}\mrightarrow{}  b:\mBbbZ{}  {}\mrightarrow{}  y:\mBbbZ{}  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  \mBbbP{}



Date html generated: 2019_06_20-PM-02_21_22
Last ObjectModification: 2018_10_02-PM-11_35_10

Theory : num_thy_1


Home Index