Nuprl Lemma : gcd_sq_exists_anne
n,m:
. (
g:{| GCD(m;n;g)})
Proof
Definitions occuring in Statement :
gcd_p: GCD(a;b;y),
nat: ,
all: x:A. B[x],
sq_exists: x:{A| B[x]}
Definitions :
all: x:A. B[x],
member: t 
T,
implies: P 
Q,
so_lambda: 
x.t[x],
sq_exists: x:{A| B[x]},
so_lambda: x y.t[x; y],
so_apply: x[s1;s2],
subtype_rel: A 
r B,
nat: ,
le: A 
B,
not: 
A,
false: False,
int_seg: {i..j
},
lelt: i j < k,
and: P 
Q,
nat_plus: 
,
int_nzero: 
,
nequal: a 
b T ,
prop: 
,
uall: [x:A]. B[x],
so_apply: x[s],
decidable: Dec(P),
or: P 
Q,
uimplies: b supposing a,
guard: {T},
sq_type: SQType(T),
iff: P 
Q,
rev_implies: P Q
Lemmas :
nat_wf,
all_wf,
int_seg_wf,
sq_exists_wf,
gcd_p_wf,
natrec_wf,
decidable__equal_nat,
le_wf,
subtype_base_sq,
set_subtype_base,
int_subtype_base,
gcd_p_zero,
zero-le-nat,
remainder_wf,
lelt_wf,
rem_bounds_1,
div_rem_gcd_anne,
nequal_wf
\mforall{}n,m:\mBbbN{}. (\mexists{}g:\{\mBbbN{}| GCD(m;n;g)\})
Date html generated:
2013_09_05-AM-11_15_44
Last ObjectModification:
2013_08_22-PM-00_15_20
Home
Index