Nuprl Lemma : half-cubes-listable-ext
∀k:ℕ. ∀c:{c:ℚCube(k)| ↑Inhabited(c)} .
(∃L:ℚCube(k) List [(no_repeats(ℚCube(k);L) ∧ (∀h:ℚCube(k). ((h ∈ L) ⇐⇒ ↑is-half-cube(k;h;c))))])
Proof
Definitions occuring in Statement :
inhabited-rat-cube: Inhabited(c),
is-half-cube: is-half-cube(k;h;c),
rational-cube: ℚCube(k),
no_repeats: no_repeats(T;l),
l_member: (x ∈ l),
list: T List,
nat: ℕ,
assert: ↑b,
all: ∀x:A. B[x],
sq_exists: ∃x:A [B[x]],
iff: P ⇐⇒ Q,
and: P ∧ Q,
set: {x:A| B[x]}
Definitions unfolded in proof :
has-value: (a)↓,
implies: P ⇒ Q,
all: ∀x:A. B[x],
so_apply: x[s1;s2],
so_lambda: λ2x y.t[x; y],
uimplies: b supposing a,
so_apply: x[s],
top: Top,
so_lambda: λ2x.t[x],
so_apply: x[s1;s2;s3;s4],
so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]),
uall: ∀[x:A]. B[x],
decidable__int_equal,
any: any x,
bool_cases_sqequal,
decidable__equal_int,
half-cubes-listable,
half-cubes: half-cubes(k),
ifthenelse: if b then t else f fi ,
subtract: n - m,
cons: [a / b],
it: ⋅,
nil: [],
member: t ∈ T
Lemmas referenced :
is-exception_wf,
has-value_wf_base,
lifting-strict-decide,
strict4-apply,
lifting-strict-spread,
strict4-decide,
istype-void,
lifting-strict-int_eq,
half-cubes-listable,
decidable__int_equal,
bool_cases_sqequal,
decidable__equal_int
Rules used in proof :
closedConclusion,
baseApply,
exceptionSqequal,
axiomSqleEquality,
decideExceptionCases,
independent_functionElimination,
dependent_functionElimination,
equalityIstype,
sqleReflexivity,
unionElimination,
hypothesisEquality,
callbyvalueDecide,
divergentSqle,
sqequalSqle,
lambdaFormation_alt,
inhabitedIsType,
independent_isectElimination,
voidElimination,
isect_memberEquality_alt,
baseClosed,
isectElimination,
equalitySymmetry,
equalityTransitivity,
sqequalHypSubstitution,
thin,
sqequalRule,
hypothesis,
extract_by_obid,
instantiate,
cut,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
introduction
Latex:
\mforall{}k:\mBbbN{}. \mforall{}c:\{c:\mBbbQ{}Cube(k)| \muparrow{}Inhabited(c)\} .
(\mexists{}L:\mBbbQ{}Cube(k) List [(no\_repeats(\mBbbQ{}Cube(k);L) \mwedge{} (\mforall{}h:\mBbbQ{}Cube(k). ((h \mmember{} L) \mLeftarrow{}{}\mRightarrow{} \muparrow{}is-half-cube(k;h;c))))])
Date html generated:
2019_10_29-AM-07_53_08
Last ObjectModification:
2019_10_21-PM-02_59_10
Theory : rationals
Home
Index