Nuprl Lemma : comb_for_divides_wf
λa,b,z. (a | b) ∈ a:ℤ ⟶ b:ℤ ⟶ (↓True) ⟶ ℙ
Proof
Definitions occuring in Statement : 
divides: b | a
, 
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 : 
divides_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,z.  (a  |  b)  \mmember{}  a:\mBbbZ{}  {}\mrightarrow{}  b:\mBbbZ{}  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  \mBbbP{}
Date html generated:
2019_06_20-PM-02_19_53
Last ObjectModification:
2018_10_03-AM-00_35_38
Theory : num_thy_1
Home
Index