Nuprl Lemma : member-gcd-reduce-constraints
∀n:ℕ+. ∀eqs,sat:{L:ℤ List| ||L|| = n ∈ ℤ} List. ∀cc:{L:ℤ List| ||L|| = n ∈ ℤ} .
((↑isl(gcd-reduce-eq-constraints(sat;eqs))) ⇒ (cc ∈ sat) ⇒ (cc ∈ outl(gcd-reduce-eq-constraints(sat;eqs))))
Proof
Definitions occuring in Statement :
gcd-reduce-eq-constraints: gcd-reduce-eq-constraints(sat;LL),
l_member: (x ∈ l),
listp: A List+,
length: ||as||,
list: T List,
nat_plus: ℕ+,
outl: outl(x),
assert: ↑b,
isl: isl(x),
all: ∀x:A. B[x],
implies: P ⇒ Q,
set: {x:A| B[x]} ,
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
member: t ∈ T,
prop: ℙ,
so_lambda: λ2x.t[x],
subtype_rel: A ⊆r B,
uimplies: b supposing a,
nat_plus: ℕ+,
so_apply: x[s],
implies: P ⇒ Q,
listp: A List+,
and: P ∧ Q,
less_than: a < b,
squash: ↓T,
cand: A c∧ B,
guard: {T},
isl: isl(x),
outl: outl(x),
not: ¬A,
false: False,
gcd-reduce-eq-constraints: gcd-reduce-eq-constraints(sat;LL),
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
assert: ↑b,
ifthenelse: if b then t else f fi ,
btrue: tt,
or: P ∨ Q,
cons: [a / b],
decidable: Dec(P),
nil: [],
it: ⋅,
bfalse: ff,
eager-map: eager-map(f;as),
list_ind: list_ind,
true: True,
top: Top,
outr: outr(x),
evalall: evalall(t),
callbyvalueall: callbyvalueall,
less_than': less_than'(a;b),
le: A ≤ B,
uiff: uiff(P;Q),
rev_implies: P ⇐ Q,
iff: P ⇐⇒ Q,
has-value: (a)↓,
has-valueall: has-valueall(a),
nat: ℕ,
subtract: n - m,
int_nzero: ℤ-o,
nequal: a ≠ b ∈ T ,
rev_uimplies: rev_uimplies(P;Q)
Lemmas referenced :
list_induction,
list_wf,
equal-wf-base,
all_wf,
list_subtype_base,
int_subtype_base,
set_subtype_base,
less_than_wf,
istype-int,
assert_wf,
gcd-reduce-eq-constraints_wf,
subtype_rel_list,
listp_wf,
subtype_rel_sets_simple,
length_wf,
less_than_transitivity1,
le_weakening,
btrue_wf,
bfalse_wf,
l_member_wf,
istype-less_than,
assert_elim,
btrue_neq_bfalse,
accumulate_abort_nil_lemma,
istype-true,
istype-assert,
nat_plus_wf,
accumulate_abort_cons_lemma,
list-cases,
product_subtype_list,
less_than_irreflexivity,
length_of_nil_lemma,
spread_cons_lemma,
eager_map_cons_lemma,
decidable__assert,
null_wf,
null_cons_lemma,
null_nil_lemma,
istype-void,
eager_map_nil_lemma,
length_of_cons_lemma,
decidable__equal_int,
cons-listp,
le-add-cancel,
zero-add,
add-commutes,
add-swap,
add-associates,
add_functionality_wrt_le,
le_antisymmetry_iff,
not-lt-2,
istype-false,
decidable__lt,
cons_member,
length-singleton,
nil_wf,
cons_wf,
void-valueall-type,
int-valueall-type,
list-valueall-type,
union-valueall-type,
valueall-type-has-valueall,
evalall-reduce,
top_wf,
it_wf,
accumulate_abort-aborted,
absval_wf,
gcd-list_wf,
length_wf_nat,
condition-implies-le,
minus-add,
minus-one-mul,
minus-one-mul-top,
add-zero,
value-type-has-value,
int-value-type,
istype-top,
remainder_wfa,
not-equal-2,
decidable__le,
istype-le,
not-le-2,
less-iff-le,
le-add-cancel2,
nequal_wf,
divide_wfa,
list-value-type,
eager-map_wf,
map-length,
map_wf,
eager-map-is-map
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
cut,
thin,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
setEquality,
intEquality,
hypothesis,
because_Cache,
sqequalRule,
lambdaEquality_alt,
closedConclusion,
baseApply,
baseClosed,
hypothesisEquality,
applyEquality,
independent_isectElimination,
natural_numberEquality,
universeIsType,
setElimination,
rename,
functionEquality,
inhabitedIsType,
equalityTransitivity,
equalitySymmetry,
independent_pairFormation,
imageElimination,
productElimination,
dependent_functionElimination,
equalityIstype,
sqequalBase,
unionElimination,
independent_functionElimination,
dependent_set_memberEquality_alt,
productIsType,
applyLambdaEquality,
voidElimination,
setIsType,
Error :memTop,
functionIsType,
promote_hyp,
hypothesis_subsumption,
callbyvalueReduce,
sqleReflexivity,
isect_memberEquality_alt,
int_eqReduceFalseSq,
int_eqReduceTrueSq,
inrFormation_alt,
addEquality,
inlEquality_alt,
voidEquality,
unionEquality,
minusEquality,
lessCases,
isect_memberFormation_alt,
axiomSqEquality,
isectIsTypeImplies,
imageMemberEquality,
inlFormation_alt
Latex:
\mforall{}n:\mBbbN{}\msupplus{}. \mforall{}eqs,sat:\{L:\mBbbZ{} List| ||L|| = n\} List. \mforall{}cc:\{L:\mBbbZ{} List| ||L|| = n\} .
((\muparrow{}isl(gcd-reduce-eq-constraints(sat;eqs)))
{}\mRightarrow{} (cc \mmember{} sat)
{}\mRightarrow{} (cc \mmember{} outl(gcd-reduce-eq-constraints(sat;eqs))))
Date html generated:
2020_05_19-PM-09_38_29
Last ObjectModification:
2020_01_01-AM-10_05_31
Theory : omega
Home
Index