Nuprl Lemma : int_lower_ind
∀i:ℤ. ∀[E:{...i} ⟶ ℙ{u}]. (E[i] ⇒ (∀k:{...i - 1}. (E[k + 1] ⇒ E[k])) ⇒ {∀k:{...i}. E[k]})
Proof
Definitions occuring in Statement :
int_lower: {...i},
uall: ∀[x:A]. B[x],
prop: ℙ,
guard: {T},
so_apply: x[s],
all: ∀x:A. B[x],
implies: P ⇒ Q,
function: x:A ⟶ B[x],
subtract: n - m,
add: n + m,
natural_number: $n,
int: ℤ
Definitions unfolded in proof :
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
guard: {T},
member: t ∈ T,
prop: ℙ,
subtype_rel: A ⊆r B,
so_lambda: λ2x.t[x],
so_apply: x[s],
int_lower: {...i},
decidable: Dec(P),
or: P ∨ Q,
iff: P ⇐⇒ Q,
and: P ∧ Q,
not: ¬A,
rev_implies: P ⇐ Q,
false: False,
uiff: uiff(P;Q),
uimplies: b supposing a,
subtract: n - m,
top: Top,
le: A ≤ B,
less_than': less_than'(a;b),
true: True,
wellfounded: WellFnd{i}(A;x,y.R[x; y]),
gt: i > j,
sq_type: SQType(T),
sq_stable: SqStable(P),
squash: ↓T
Lemmas referenced :
add-zero,
zero-mul,
add-mul-special,
not-gt-2,
decidable__lt,
sq_stable__le,
minus-minus,
not-equal-2,
int_subtype_base,
subtype_base_sq,
decidable__int_equal,
gt_wf,
int_lower_well_founded,
le_reflexive,
le-add-cancel2,
subtype_rel_sets,
le_wf,
le-add-cancel,
add_functionality_wrt_le,
zero-add,
add-commutes,
minus-add,
minus-one-mul-top,
add-swap,
minus-one-mul,
add-associates,
condition-implies-le,
not-le-2,
false_wf,
decidable__le,
subtract_wf,
int_lower_wf,
all_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
isect_memberFormation,
cut,
thin,
instantiate,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
hypothesisEquality,
natural_numberEquality,
hypothesis,
applyEquality,
lambdaEquality,
cumulativity,
universeEquality,
sqequalRule,
functionEquality,
dependent_set_memberEquality,
addEquality,
setElimination,
rename,
dependent_functionElimination,
unionElimination,
independent_pairFormation,
voidElimination,
productElimination,
independent_functionElimination,
independent_isectElimination,
minusEquality,
isect_memberEquality,
voidEquality,
intEquality,
because_Cache,
setEquality,
equalityTransitivity,
equalitySymmetry,
introduction,
imageMemberEquality,
baseClosed,
imageElimination,
multiplyEquality
Latex:
\mforall{}i:\mBbbZ{}. \mforall{}[E:\{...i\} {}\mrightarrow{} \mBbbP{}\{u\}]. (E[i] {}\mRightarrow{} (\mforall{}k:\{...i - 1\}. (E[k + 1] {}\mRightarrow{} E[k])) {}\mRightarrow{} \{\mforall{}k:\{...i\}. E[k]\})
Date html generated:
2016_05_13-PM-03_47_32
Last ObjectModification:
2016_01_14-PM-07_11_34
Theory : call!by!value_2
Home
Index