Nuprl Lemma : gcd_p_eq_args

a:ℤGCD(a;a;a)


Proof




Definitions occuring in Statement :  gcd_p: GCD(a;b;y) all: x:A. B[x] int:
Definitions unfolded in proof :  gcd_p: GCD(a;b;y) all: x:A. B[x] and: P ∧ Q cand: c∧ B member: t ∈ T implies:  Q uall: [x:A]. B[x] prop:
Lemmas referenced :  divides_reflexivity divides_wf istype-int
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep Error :lambdaFormation_alt,  cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality hypothesis independent_pairFormation productElimination Error :productIsType,  Error :universeIsType,  isectElimination Error :inhabitedIsType

Latex:
\mforall{}a:\mBbbZ{}.  GCD(a;a;a)



Date html generated: 2019_06_20-PM-02_21_26
Last ObjectModification: 2018_10_02-PM-11_35_11

Theory : num_thy_1


Home Index