Nuprl Lemma : dl-ind_wf
∀[T:dl-Obj() ⟶ TYPE]. ∀[aprog:x:ℕ ⟶ T[prog(atm(x))]]. ∀[comp:x:Prog
⟶ x1:Prog
⟶ T[prog(x)]
⟶ T[prog(x1)]
⟶ T[prog((x;x1))]]. ∀[choose:x:Prog
⟶ x1:Prog
⟶ T[prog(x)]
⟶ T[prog(x1)]
⟶ T[prog(x ⋃ x1)]].
∀[iterate:x:Prog ⟶ T[prog(x)] ⟶ T[prog((x)*)]]. ∀[test:x:Prop ⟶ T[prop(x)] ⟶ T[prog((x)?)]].
∀[aprop:x:ℕ ⟶ T[prop(atm(x))]]. ∀[false:T[prop(0)]]. ∀[implies:x:Prop
⟶ x1:Prop
⟶ T[prop(x)]
⟶ T[prop(x1)]
⟶ T[prop(x ⇒ x1)]]. ∀[and:x:Prop
⟶ x1:Prop
⟶ T[prop(x)]
⟶ T[prop(x1)]
⟶ T[prop(x ∧ x1)]].
∀[or:x:Prop ⟶ x1:Prop ⟶ T[prop(x)] ⟶ T[prop(x1)] ⟶ T[prop(x ∨ x1)]]. ∀[box:x:Prog
⟶ x1:Prop
⟶ T[prog(x)]
⟶ T[prop(x1)]
⟶ T[prop([x] x1)]].
∀[diamond:x:Prog ⟶ x1:Prop ⟶ T[prog(x)] ⟶ T[prop(x1)] ⟶ T[prop(<x> x1)]].
(dl-ind(
dl-aprog(x0)⇒ aprog[x0];
dl-comp(x1,x2)⇒ x3,x4.comp[x1;x2;x3;x4];
dl-choose(x5,x6)⇒ x7,x8.choose[x5;x6;x7;x8];
dl-iterate(x9)⇒ x10.iterate[x9;x10];
dl-test(x11)⇒ x12.test[x11;x12];
dl-aprop(x13)⇒ aprop[x13];
dl-false⇒ false;
dl-implies(x14,x15)⇒ x16,x17.implies[x14;x15;x16;x17];
dl-and(x18,x19)⇒ x20,x21.and[x18;x19;x20;x21];
dl-or(x22,x23)⇒ x24,x25.or[x22;x23;x24;x25];
dl-box(x26,x27)⇒ x28,x29.box[x26;x27;x28;x29];
dl-diamond(x30,x31)⇒ x32,x33.diamond[x30;x31;x32;x33]) ∈ ∀x:dl-Obj(). T[x])
Proof
Definitions occuring in Statement :
dl-ind: dl-ind,
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[s1;s2;s3;s4],
so_apply: x[s1;s2],
so_apply: x[s],
all: ∀x:A. B[x],
member: t ∈ T,
function: x:A ⟶ B[x]
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
dl-ind: dl-ind,
all: ∀x:A. B[x],
implies: P ⇒ Q,
so_apply: x[s],
subtype_rel: A ⊆r B,
so_apply: x[s1;s2;s3;s4],
so_apply: x[s1;s2]
Lemmas referenced :
istype-nat,
dl-prog-obj_wf,
dl-aprog_wf,
dl-prog_wf,
dl-comp_wf,
dl-choose_wf,
dl-iterate_wf,
dl-prop_wf,
dl-prop-obj_wf,
dl-test_wf,
dl-aprop_wf,
dl-false_wf,
dl-implies_wf,
dl-and_wf,
dl-or_wf,
dl-box_wf,
dl-diamond_wf,
dl-Obj_wf,
dl-induction
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
cut,
sqequalRule,
lambdaEquality_alt,
isectElimination,
hypothesisEquality,
equalityTransitivity,
equalitySymmetry,
hypothesis,
isectIsType,
inhabitedIsType,
functionIsType,
introduction,
extract_by_obid,
TYPEMemberIsType,
applyEquality,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
universeIsType,
because_Cache,
instantiate,
TYPEIsType
Latex:
\mforall{}[T:dl-Obj() {}\mrightarrow{} TYPE]. \mforall{}[aprog:x:\mBbbN{} {}\mrightarrow{} T[prog(atm(x))]]. \mforall{}[comp:x:Prog
{}\mrightarrow{} x1:Prog
{}\mrightarrow{} T[prog(x)]
{}\mrightarrow{} T[prog(x1)]
{}\mrightarrow{} T[prog((x;x1))]].
\mforall{}[choose:x:Prog {}\mrightarrow{} x1:Prog {}\mrightarrow{} T[prog(x)] {}\mrightarrow{} T[prog(x1)] {}\mrightarrow{} T[prog(x \mcup{} x1)]].
\mforall{}[iterate:x:Prog {}\mrightarrow{} T[prog(x)] {}\mrightarrow{} T[prog((x)*)]]. \mforall{}[test:x:Prop {}\mrightarrow{} T[prop(x)] {}\mrightarrow{} T[prog((x)?)]].
\mforall{}[aprop:x:\mBbbN{} {}\mrightarrow{} T[prop(atm(x))]]. \mforall{}[false:T[prop(0)]]. \mforall{}[implies:x:Prop
{}\mrightarrow{} x1:Prop
{}\mrightarrow{} T[prop(x)]
{}\mrightarrow{} T[prop(x1)]
{}\mrightarrow{} T[prop(x {}\mRightarrow{} x1)]].
\mforall{}[and:x:Prop {}\mrightarrow{} x1:Prop {}\mrightarrow{} T[prop(x)] {}\mrightarrow{} T[prop(x1)] {}\mrightarrow{} T[prop(x \mwedge{} x1)]]. \mforall{}[or:x:Prop
{}\mrightarrow{} x1:Prop
{}\mrightarrow{} T[prop(x)]
{}\mrightarrow{} T[prop(x1)]
{}\mrightarrow{} T[prop(x \mvee{} x1)]].
\mforall{}[box:x:Prog {}\mrightarrow{} x1:Prop {}\mrightarrow{} T[prog(x)] {}\mrightarrow{} T[prop(x1)] {}\mrightarrow{} T[prop([x] x1)]].
\mforall{}[diamond:x:Prog {}\mrightarrow{} x1:Prop {}\mrightarrow{} T[prog(x)] {}\mrightarrow{} T[prop(x1)] {}\mrightarrow{} T[prop(<x> x1)]].
(dl-ind(
dl-aprog(x0){}\mRightarrow{} aprog[x0];
dl-comp(x1,x2){}\mRightarrow{} x3,x4.comp[x1;x2;x3;x4];
dl-choose(x5,x6){}\mRightarrow{} x7,x8.choose[x5;x6;x7;x8];
dl-iterate(x9){}\mRightarrow{} x10.iterate[x9;x10];
dl-test(x11){}\mRightarrow{} x12.test[x11;x12];
dl-aprop(x13){}\mRightarrow{} aprop[x13];
dl-false{}\mRightarrow{} false;
dl-implies(x14,x15){}\mRightarrow{} x16,x17.implies[x14;x15;x16;x17];
dl-and(x18,x19){}\mRightarrow{} x20,x21.and[x18;x19;x20;x21];
dl-or(x22,x23){}\mRightarrow{} x24,x25.or[x22;x23;x24;x25];
dl-box(x26,x27){}\mRightarrow{} x28,x29.box[x26;x27;x28;x29];
dl-diamond(x30,x31){}\mRightarrow{} x32,x33.diamond[x30;x31;x32;x33]) \mmember{} \mforall{}x:dl-Obj(). T[x])
Date html generated:
2019_10_15-AM-11_41_56
Last ObjectModification:
2019_03_26-AM-11_25_08
Theory : dynamic!logic
Home
Index