Nuprl Lemma : dl-induction
∀[T:dl-Obj() ⟶ TYPE]
((∀x:ℕ. T[prog(atm(x))])
⇒ (∀x,x1:Prog. (T[prog(x)] ⇒ T[prog(x1)] ⇒ T[prog((x;x1))]))
⇒ (∀x,x1:Prog. (T[prog(x)] ⇒ T[prog(x1)] ⇒ T[prog(x ⋃ x1)]))
⇒ (∀x:Prog. (T[prog(x)] ⇒ T[prog((x)*)]))
⇒ (∀x:Prop. (T[prop(x)] ⇒ T[prog((x)?)]))
⇒ (∀x:ℕ. T[prop(atm(x))])
⇒ T[prop(0)]
⇒ (∀x,x1:Prop. (T[prop(x)] ⇒ T[prop(x1)] ⇒ T[prop(x ⇒ x1)]))
⇒ (∀x,x1:Prop. (T[prop(x)] ⇒ T[prop(x1)] ⇒ T[prop(x ∧ x1)]))
⇒ (∀x,x1:Prop. (T[prop(x)] ⇒ T[prop(x1)] ⇒ T[prop(x ∨ x1)]))
⇒ (∀x:Prog. ∀x1:Prop. (T[prog(x)] ⇒ T[prop(x1)] ⇒ T[prop([x] x1)]))
⇒ (∀x:Prog. ∀x1:Prop. (T[prog(x)] ⇒ T[prop(x1)] ⇒ T[prop(<x> x1)]))
⇒ (∀x:dl-Obj(). T[x]))
Proof
Definitions occuring in Statement :
dl-diamond: <x1> x,
dl-box: [x1] x,
dl-or: x1 ∨ x,
dl-and: x1 ∧ x,
dl-implies: x1 ⇒ x,
dl-false: 0,
dl-aprop: atm(x),
dl-test: (x)?,
dl-iterate: (x)*,
dl-choose: x1 ⋃ x,
dl-comp: (x1;x),
dl-aprog: atm(x),
dl-prop-obj: prop(x),
dl-prog-obj: prog(x),
dl-prop: Prop,
dl-prog: Prog,
dl-Obj: dl-Obj(),
nat: ℕ,
uall: ∀[x:A]. B[x],
so_apply: x[s],
all: ∀x:A. B[x],
implies: P ⇒ Q,
function: x:A ⟶ B[x]
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
all: ∀x:A. B[x],
mrecind: mrecind(L;x.P[x]),
mkinds: mKinds,
eager-map: eager-map(f;as),
list_ind: list_ind,
dl-Spec: dl-Spec(),
cons: [a / b],
pi1: fst(t),
nil: [],
it: ⋅,
member: t ∈ T,
decidable: Dec(P),
or: P ∨ Q,
uimplies: b supposing a,
sq_type: SQType(T),
guard: {T},
mrec-spec: mrec-spec(L;lbl;p),
apply-alist: apply-alist(eq;L;x),
ifthenelse: if b then t else f fi ,
atom-deq: AtomDeq,
eq_atom: x =a y,
btrue: tt,
pi2: snd(t),
top: Top,
eqof: eqof(d),
bool: 𝔹,
unit: Unit,
uiff: uiff(P;Q),
and: P ∧ Q,
prec-arg-types: prec-arg-types(lbl,p.a[lbl; p];i;lbl),
int_seg: {i..j-},
nat: ℕ,
ge: i ≥ j ,
lelt: i ≤ j < k,
not: ¬A,
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
prop: ℙ,
false: False,
select: L[n],
dl-aprog: atm(x),
dl-prog-obj: prog(x),
le: A ≤ B,
bfalse: ff,
bnot: ¬bb,
assert: ↑b,
mrec: mrec(L;i),
nequal: a ≠ b ∈ T ,
select-tuple: x.n,
eq_int: (i =z j),
subtract: n - m,
dl-prog: Prog,
dl-comp: (x1;x),
so_apply: x[s],
dl-choose: x1 ⋃ x,
dl-iterate: (x)*,
dl-prop-obj: prop(x),
dl-prop: Prop,
dl-test: (x)?,
less_than: a < b,
squash: ↓T,
less_than': less_than'(a;b),
dl-aprop: atm(x),
dl-false: 0,
dl-implies: x1 ⇒ x,
dl-and: x1 ∧ x,
dl-or: x1 ∨ x,
dl-box: [x1] x,
dl-diamond: <x1> x,
iff: P ⇐⇒ Q,
so_lambda: λ2x.t[x],
dl-Obj: dl-Obj()
Lemmas referenced :
decidable__atom_equal,
subtype_base_sq,
atom_subtype_base,
apply_alist_cons_lemma,
istype-void,
eq_atom_wf,
eqtt_to_assert,
assert_of_eq_atom,
length_of_cons_lemma,
length_of_nil_lemma,
atomdeq_reduce_lemma,
map_cons_lemma,
map_nil_lemma,
tupletype_cons_lemma,
null_nil_lemma,
tupletype_nil_lemma,
nat_properties,
decidable__le,
full-omega-unsat,
intformnot_wf,
intformle_wf,
itermConstant_wf,
istype-int,
int_formula_prop_not_lemma,
int_formula_prop_le_lemma,
int_term_value_constant_lemma,
int_formula_prop_wf,
decidable__lt,
intformless_wf,
int_formula_prop_less_lemma,
istype-le,
istype-less_than,
int_seg_wf,
decidable__equal_int,
int_subtype_base,
int_seg_properties,
true_wf,
int_seg_subtype_special,
int_seg_cases,
intformand_wf,
itermVar_wf,
int_formula_prop_and_lemma,
int_term_value_var_lemma,
eqff_to_assert,
bool_cases_sqequal,
bool_wf,
bool_subtype_base,
assert-bnot,
neg_assert_of_eq_atom,
null_cons_lemma,
dl-prog-obj_wf,
mrec_wf,
dl-Spec_wf,
dl-prop-obj_wf,
istype-atom,
length_wf,
mrec-spec_wf,
unit_wf2,
cons_member,
cons_wf,
nil_wf,
member_singleton,
mkinds_wf,
mrec_ind_wf,
mobj_wf,
dl-Obj_wf,
dl-diamond_wf,
dl-box_wf,
dl-or_wf,
dl-and_wf,
dl-implies_wf,
dl-false_wf,
dl-aprop_wf,
dl-prop_wf,
dl-test_wf,
dl-iterate_wf,
dl-choose_wf,
dl-prog_wf,
dl-comp_wf,
istype-nat,
dl-aprog_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
lambdaFormation_alt,
cut,
thin,
sqequalHypSubstitution,
setElimination,
rename,
sqequalRule,
hypothesis,
introduction,
extract_by_obid,
dependent_functionElimination,
hypothesisEquality,
tokenEquality,
unionElimination,
instantiate,
isectElimination,
cumulativity,
atomEquality,
independent_isectElimination,
because_Cache,
independent_functionElimination,
equalityTransitivity,
equalitySymmetry,
isect_memberEquality_alt,
voidElimination,
inhabitedIsType,
equalityElimination,
productElimination,
dependent_set_memberEquality_alt,
natural_numberEquality,
independent_pairFormation,
approximateComputation,
dependent_pairFormation_alt,
lambdaEquality_alt,
universeIsType,
productIsType,
functionIsType,
intEquality,
hypothesis_subsumption,
int_eqEquality,
equalityIstype,
promote_hyp,
TYPEMemberIsType,
applyEquality,
imageElimination,
setIsType,
unionEquality,
universeEquality,
TYPEIsType
Latex:
\mforall{}[T:dl-Obj() {}\mrightarrow{} TYPE]
((\mforall{}x:\mBbbN{}. T[prog(atm(x))])
{}\mRightarrow{} (\mforall{}x,x1:Prog. (T[prog(x)] {}\mRightarrow{} T[prog(x1)] {}\mRightarrow{} T[prog((x;x1))]))
{}\mRightarrow{} (\mforall{}x,x1:Prog. (T[prog(x)] {}\mRightarrow{} T[prog(x1)] {}\mRightarrow{} T[prog(x \mcup{} x1)]))
{}\mRightarrow{} (\mforall{}x:Prog. (T[prog(x)] {}\mRightarrow{} T[prog((x)*)]))
{}\mRightarrow{} (\mforall{}x:Prop. (T[prop(x)] {}\mRightarrow{} T[prog((x)?)]))
{}\mRightarrow{} (\mforall{}x:\mBbbN{}. T[prop(atm(x))])
{}\mRightarrow{} T[prop(0)]
{}\mRightarrow{} (\mforall{}x,x1:Prop. (T[prop(x)] {}\mRightarrow{} T[prop(x1)] {}\mRightarrow{} T[prop(x {}\mRightarrow{} x1)]))
{}\mRightarrow{} (\mforall{}x,x1:Prop. (T[prop(x)] {}\mRightarrow{} T[prop(x1)] {}\mRightarrow{} T[prop(x \mwedge{} x1)]))
{}\mRightarrow{} (\mforall{}x,x1:Prop. (T[prop(x)] {}\mRightarrow{} T[prop(x1)] {}\mRightarrow{} T[prop(x \mvee{} x1)]))
{}\mRightarrow{} (\mforall{}x:Prog. \mforall{}x1:Prop. (T[prog(x)] {}\mRightarrow{} T[prop(x1)] {}\mRightarrow{} T[prop([x] x1)]))
{}\mRightarrow{} (\mforall{}x:Prog. \mforall{}x1:Prop. (T[prog(x)] {}\mRightarrow{} T[prop(x1)] {}\mRightarrow{} T[prop(<x> x1)]))
{}\mRightarrow{} (\mforall{}x:dl-Obj(). T[x]))
Date html generated:
2019_10_15-AM-11_41_52
Last ObjectModification:
2019_03_26-AM-11_18_35
Theory : dynamic!logic
Home
Index