Nuprl Lemma : dl-complete-induction
∀[T:dl-Obj() ⟶ Type]
((∀x:ℕ. T[prog(atm(x))])
⇒ (∀x,x1:Prog.
((∀y:dl-Obj(). ((↑y ≤ prog(x)) ⇒ T[y])) ⇒ (∀y:dl-Obj(). ((↑y ≤ prog(x1)) ⇒ T[y])) ⇒ T[prog((x;x1))]))
⇒ (∀x,x1:Prog.
((∀y:dl-Obj(). ((↑y ≤ prog(x)) ⇒ T[y])) ⇒ (∀y:dl-Obj(). ((↑y ≤ prog(x1)) ⇒ T[y])) ⇒ T[prog(x ⋃ x1)]))
⇒ (∀x:Prog. ((∀y:dl-Obj(). ((↑y ≤ prog(x)) ⇒ T[y])) ⇒ T[prog((x)*)]))
⇒ (∀x:Prop. ((∀y:dl-Obj(). ((↑y ≤ prop(x)) ⇒ T[y])) ⇒ T[prog((x)?)]))
⇒ (∀x:ℕ. T[prop(atm(x))])
⇒ T[prop(0)]
⇒ (∀x,x1:Prop.
((∀y:dl-Obj(). ((↑y ≤ prop(x)) ⇒ T[y])) ⇒ (∀y:dl-Obj(). ((↑y ≤ prop(x1)) ⇒ T[y])) ⇒ T[prop(x ⇒ x1)]))
⇒ (∀x,x1:Prop.
((∀y:dl-Obj(). ((↑y ≤ prop(x)) ⇒ T[y])) ⇒ (∀y:dl-Obj(). ((↑y ≤ prop(x1)) ⇒ T[y])) ⇒ T[prop(x ∧ x1)]))
⇒ (∀x,x1:Prop.
((∀y:dl-Obj(). ((↑y ≤ prop(x)) ⇒ T[y])) ⇒ (∀y:dl-Obj(). ((↑y ≤ prop(x1)) ⇒ T[y])) ⇒ T[prop(x ∨ x1)]))
⇒ (∀x:Prog. ∀x1:Prop.
((∀y:dl-Obj(). ((↑y ≤ prog(x)) ⇒ T[y])) ⇒ (∀y:dl-Obj(). ((↑y ≤ prop(x1)) ⇒ T[y])) ⇒ T[prop([x] x1)]))
⇒ (∀x:Prog. ∀x1:Prop.
((∀y:dl-Obj(). ((↑y ≤ prog(x)) ⇒ T[y])) ⇒ (∀y:dl-Obj(). ((↑y ≤ prop(x1)) ⇒ T[y])) ⇒ T[prop(<x> x1)]))
⇒ (∀x:dl-Obj(). T[x]))
Proof
Definitions occuring in Statement :
dlo_le: a ≤ b,
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: ℕ,
assert: ↑b,
uall: ∀[x:A]. B[x],
so_apply: x[s],
all: ∀x:A. B[x],
implies: P ⇒ Q,
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
all: ∀x:A. B[x],
member: t ∈ T,
so_apply: x[s],
so_lambda: λ2x.t[x],
prop: ℙ,
subtype_rel: A ⊆r B,
dlo_le: a ≤ b,
dlo-le: dlo-le(),
top: Top,
so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]),
so_apply: x[s1;s2;s3;s4],
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
iff: P ⇐⇒ Q,
and: P ∧ Q,
uiff: uiff(P;Q),
uimplies: b supposing a,
or: P ∨ Q,
guard: {T},
rev_implies: P ⇐ Q
Lemmas referenced :
dl-Obj_wf,
dl-prog_wf,
dl-prop_wf,
istype-assert,
dlo_le_wf,
dl-prog-obj_wf,
dl-prop-obj_wf,
dl-diamond_wf,
dl-box_wf,
dl-or_wf,
dl-and_wf,
dl-implies_wf,
dl-false_wf,
istype-nat,
dl-aprop_wf,
dl-test_wf,
dl-iterate_wf,
dl-choose_wf,
dl-comp_wf,
dl-aprog_wf,
istype-universe,
dl-induction,
all_wf,
assert_wf,
subtype_rel_self,
subtype-TYPE,
dl-ind-dl-aprog,
istype-void,
assert-dlo_eq,
dl-ind-dl-comp,
dl-ind-dl-choose,
dl-ind-dl-iterate,
assert_of_bor,
dlo_eq_wf,
dl-ind-dl-test,
dl-ind-dl-aprop,
dl-ind-dl-false,
iff_weakening_equal,
dl-ind-dl-implies,
dl-ind-dl-and,
dl-ind-dl-or,
dl-ind-dl-box,
dl-ind-dl-diamond,
bor_wf,
iff_transitivity,
iff_weakening_uiff,
dlo-refl
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
lambdaFormation_alt,
universeIsType,
cut,
introduction,
extract_by_obid,
hypothesis,
sqequalRule,
functionIsType,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
dependent_functionElimination,
applyEquality,
because_Cache,
instantiate,
universeEquality,
lambdaEquality_alt,
functionEquality,
inhabitedIsType,
independent_functionElimination,
isect_memberEquality_alt,
voidElimination,
productElimination,
independent_isectElimination,
unionElimination,
inlFormation_alt,
equalityIstype,
inrFormation_alt,
equalitySymmetry,
equalityTransitivity,
unionEquality,
unionIsType,
hyp_replacement,
independent_pairFormation
Latex:
\mforall{}[T:dl-Obj() {}\mrightarrow{} Type]
((\mforall{}x:\mBbbN{}. T[prog(atm(x))])
{}\mRightarrow{} (\mforall{}x,x1:Prog.
((\mforall{}y:dl-Obj(). ((\muparrow{}y \mleq{} prog(x)) {}\mRightarrow{} T[y]))
{}\mRightarrow{} (\mforall{}y:dl-Obj(). ((\muparrow{}y \mleq{} prog(x1)) {}\mRightarrow{} T[y]))
{}\mRightarrow{} T[prog((x;x1))]))
{}\mRightarrow{} (\mforall{}x,x1:Prog.
((\mforall{}y:dl-Obj(). ((\muparrow{}y \mleq{} prog(x)) {}\mRightarrow{} T[y]))
{}\mRightarrow{} (\mforall{}y:dl-Obj(). ((\muparrow{}y \mleq{} prog(x1)) {}\mRightarrow{} T[y]))
{}\mRightarrow{} T[prog(x \mcup{} x1)]))
{}\mRightarrow{} (\mforall{}x:Prog. ((\mforall{}y:dl-Obj(). ((\muparrow{}y \mleq{} prog(x)) {}\mRightarrow{} T[y])) {}\mRightarrow{} T[prog((x)*)]))
{}\mRightarrow{} (\mforall{}x:Prop. ((\mforall{}y:dl-Obj(). ((\muparrow{}y \mleq{} prop(x)) {}\mRightarrow{} T[y])) {}\mRightarrow{} T[prog((x)?)]))
{}\mRightarrow{} (\mforall{}x:\mBbbN{}. T[prop(atm(x))])
{}\mRightarrow{} T[prop(0)]
{}\mRightarrow{} (\mforall{}x,x1:Prop.
((\mforall{}y:dl-Obj(). ((\muparrow{}y \mleq{} prop(x)) {}\mRightarrow{} T[y]))
{}\mRightarrow{} (\mforall{}y:dl-Obj(). ((\muparrow{}y \mleq{} prop(x1)) {}\mRightarrow{} T[y]))
{}\mRightarrow{} T[prop(x {}\mRightarrow{} x1)]))
{}\mRightarrow{} (\mforall{}x,x1:Prop.
((\mforall{}y:dl-Obj(). ((\muparrow{}y \mleq{} prop(x)) {}\mRightarrow{} T[y]))
{}\mRightarrow{} (\mforall{}y:dl-Obj(). ((\muparrow{}y \mleq{} prop(x1)) {}\mRightarrow{} T[y]))
{}\mRightarrow{} T[prop(x \mwedge{} x1)]))
{}\mRightarrow{} (\mforall{}x,x1:Prop.
((\mforall{}y:dl-Obj(). ((\muparrow{}y \mleq{} prop(x)) {}\mRightarrow{} T[y]))
{}\mRightarrow{} (\mforall{}y:dl-Obj(). ((\muparrow{}y \mleq{} prop(x1)) {}\mRightarrow{} T[y]))
{}\mRightarrow{} T[prop(x \mvee{} x1)]))
{}\mRightarrow{} (\mforall{}x:Prog. \mforall{}x1:Prop.
((\mforall{}y:dl-Obj(). ((\muparrow{}y \mleq{} prog(x)) {}\mRightarrow{} T[y]))
{}\mRightarrow{} (\mforall{}y:dl-Obj(). ((\muparrow{}y \mleq{} prop(x1)) {}\mRightarrow{} T[y]))
{}\mRightarrow{} T[prop([x] x1)]))
{}\mRightarrow{} (\mforall{}x:Prog. \mforall{}x1:Prop.
((\mforall{}y:dl-Obj(). ((\muparrow{}y \mleq{} prog(x)) {}\mRightarrow{} T[y]))
{}\mRightarrow{} (\mforall{}y:dl-Obj(). ((\muparrow{}y \mleq{} prop(x1)) {}\mRightarrow{} T[y]))
{}\mRightarrow{} T[prop(<x> x1)]))
{}\mRightarrow{} (\mforall{}x:dl-Obj(). T[x]))
Date html generated:
2019_10_15-AM-11_43_28
Last ObjectModification:
2019_04_12-PM-05_35_45
Theory : dynamic!logic
Home
Index