Nuprl Lemma : div_rem_gcd_anne
m:
. n:
. g:. (GCD(m;n;g) 
GCD(n;m rem n;g))
Proof
Definitions occuring in Statement :
gcd_p: GCD(a;b;y),
int_nzero: ,
all: x:A. B[x],
iff: P Q,
remainder: n rem m,
int:
Definitions :
iff: P Q,
and: P 
Q,
implies: P Q,
member: t 
T,
gcd_p: GCD(a;b;y),
divides: b | a,
exists: 
x:A. B[x],
nequal: a 
b T ,
not: 
A,
false: False,
all: x:A. B[x],
prop: 
,
rev_implies: P Q,
uall: [x:A]. B[x],
int_nzero: ,
uimplies: b supposing a,
sq_type: SQType(T),
guard: {T}
Lemmas :
gcd_p_wf,
rem_to_div,
subtype_base_sq,
int_subtype_base,
Error :equal-wf-T-base,
divides_wf,
div_rem_sum,
equal-wf-base
\mforall{}m:\mBbbZ{}. \mforall{}n:\mBbbZ{}\msupminus{}\msupzero{}. \mforall{}g:\mBbbZ{}. (GCD(m;n;g) \mLeftarrow{}{}\mRightarrow{} GCD(n;m rem n;g))
Date html generated:
2013_09_05-AM-11_15_33
Last ObjectModification:
2013_08_20-PM-04_00_17
Home
Index