Definition: dl-Spec
dl-Spec() ==
[<"prog", [<"aprog", [inr ℕ ]>; <"comp", [inl inl "prog"; inl inl "prog"]>; <"choose", [inl inl "prog"; inl inl "prog"\000C]>; <"iterate", [inl inl "prog"]>; <"test", [inl inl "prop"]>]>;
<"prop", [<"aprop", [inr ℕ ]>; <"false", [inr Unit ]>; <"implies", [inl inl "prop"; inl inl "prop"]>; <"and", [inl in\000Cl "prop"; inl inl "prop"]>; <"or", [inl inl "prop"; inl inl "prop"]>; <"box", [inl inl "prog"; inl inl "prop"]>; <"diamo\000Cnd", [inl inl "prog"; inl inl "prop"]>]>]
Lemma: dl-Spec_wf
dl-Spec() ∈ MutualRectypeSpec
Definition: dl-Obj
dl-Obj() == mobj(dl-Spec())
Lemma: dl-Obj_wf
dl-Obj() ∈ Type
Definition: dl-prog
Prog == mrec(dl-Spec();"prog")
Lemma: dl-prog_wf
Prog ∈ Type
Definition: dl-prop
Prop == mrec(dl-Spec();"prop")
Lemma: dl-prop_wf
Prop ∈ Type
Definition: dl-prog-obj
prog(x) == <"prog", x>
Lemma: dl-prog-obj_wf
∀x:Prog. (prog(x) ∈ dl-Obj())
Definition: dl-prop-obj
prop(x) == <"prop", x>
Lemma: dl-prop-obj_wf
∀x:Prop. (prop(x) ∈ dl-Obj())
Definition: dl-aprog
atm(x) == mk-prec("aprog";x)
Lemma: dl-aprog_wf
∀[x:ℕ]. (atm(x) ∈ Prog)
Definition: dl-comp
(x1;x) == mk-prec("comp";<x1, x>)
Lemma: dl-comp_wf
∀[x1,x:Prog]. ((x1;x) ∈ Prog)
Definition: dl-choose
x1 ⋃ x == mk-prec("choose";<x1, x>)
Lemma: dl-choose_wf
∀[x1,x:Prog]. (x1 ⋃ x ∈ Prog)
Definition: dl-iterate
(x)* == mk-prec("iterate";x)
Lemma: dl-iterate_wf
∀[x:Prog]. ((x)* ∈ Prog)
Definition: dl-test
(x)? == mk-prec("test";x)
Lemma: dl-test_wf
∀[x:Prop]. ((x)? ∈ Prog)
Definition: dl-aprop
atm(x) == mk-prec("aprop";x)
Lemma: dl-aprop_wf
∀[x:ℕ]. (atm(x) ∈ Prop)
Definition: dl-false
0 == mk-prec("false";Ax)
Lemma: dl-false_wf
0 ∈ Prop
Definition: dl-implies
x1 ⇒ x == mk-prec("implies";<x1, x>)
Lemma: dl-implies_wf
∀[x1,x:Prop]. (x1 ⇒ x ∈ Prop)
Definition: dl-and
x1 ∧ x == mk-prec("and";<x1, x>)
Lemma: dl-and_wf
∀[x1,x:Prop]. (x1 ∧ x ∈ Prop)
Definition: dl-or
x1 ∨ x == mk-prec("or";<x1, x>)
Lemma: dl-or_wf
∀[x1,x:Prop]. (x1 ∨ x ∈ Prop)
Definition: dl-box
[x1] x == mk-prec("box";<x1, x>)
Lemma: dl-box_wf
∀[x1:Prog]. ∀[x:Prop]. ([x1] x ∈ Prop)
Definition: dl-diamond
<x1> x == mk-prec("diamond";<x1, x>)
Lemma: dl-diamond_wf
∀[x1:Prog]. ∀[x:Prop]. (<x1> x ∈ Prop)
Definition: dl-kind
dl-kind(d) == mobj-kind(d)
Lemma: dl-kind_wf
∀[d:dl-Obj()]. (dl-kind(d) ∈ {a:Atom| (a ∈ ``prog prop``)} )
Definition: dl-label
dl-label(d) == mobj-label(d)
Lemma: dl-label_wf
∀[d:dl-Obj()]. (dl-label(d) ∈ Atom)
Definition: dl-aprog?
dl-aprog?(x) == dl-label(prog(x)) =a "aprog"
Lemma: dl-aprog?_wf
∀[x:Prog]. (dl-aprog?(x) ∈ 𝔹)
Definition: dl-comp?
dl-comp?(x) == dl-label(prog(x)) =a "comp"
Lemma: dl-comp?_wf
∀[x:Prog]. (dl-comp?(x) ∈ 𝔹)
Definition: dl-choose?
dl-choose?(x) == dl-label(prog(x)) =a "choose"
Lemma: dl-choose?_wf
∀[x:Prog]. (dl-choose?(x) ∈ 𝔹)
Definition: dl-iterate?
dl-iterate?(x) == dl-label(prog(x)) =a "iterate"
Lemma: dl-iterate?_wf
∀[x:Prog]. (dl-iterate?(x) ∈ 𝔹)
Definition: dl-test?
dl-test?(x) == dl-label(prog(x)) =a "test"
Lemma: dl-test?_wf
∀[x:Prog]. (dl-test?(x) ∈ 𝔹)
Definition: dl-aprop?
dl-aprop?(x) == dl-label(prop(x)) =a "aprop"
Lemma: dl-aprop?_wf
∀[x:Prop]. (dl-aprop?(x) ∈ 𝔹)
Definition: dl-false?
dl-false?(x) == dl-label(prop(x)) =a "false"
Lemma: dl-false?_wf
∀[x:Prop]. (dl-false?(x) ∈ 𝔹)
Definition: dl-implies?
dl-implies?(x) == dl-label(prop(x)) =a "implies"
Lemma: dl-implies?_wf
∀[x:Prop]. (dl-implies?(x) ∈ 𝔹)
Definition: dl-and?
dl-and?(x) == dl-label(prop(x)) =a "and"
Lemma: dl-and?_wf
∀[x:Prop]. (dl-and?(x) ∈ 𝔹)
Definition: dl-or?
dl-or?(x) == dl-label(prop(x)) =a "or"
Lemma: dl-or?_wf
∀[x:Prop]. (dl-or?(x) ∈ 𝔹)
Definition: dl-box?
dl-box?(x) == dl-label(prop(x)) =a "box"
Lemma: dl-box?_wf
∀[x:Prop]. (dl-box?(x) ∈ 𝔹)
Definition: dl-diamond?
dl-diamond?(x) == dl-label(prop(x)) =a "diamond"
Lemma: dl-diamond?_wf
∀[x:Prop]. (dl-diamond?(x) ∈ 𝔹)
Definition: dl-aprog-1
dl-aprog-1(x) == snd(x).0
Lemma: dl-aprog-1_wf
∀[x:Prog]. dl-aprog-1(x) ∈ ℕ supposing ↑dl-aprog?(x)
Definition: dl-comp-1
dl-comp-1(x) == snd(x).0
Lemma: dl-comp-1_wf
∀[x:Prog]. dl-comp-1(x) ∈ Prog supposing ↑dl-comp?(x)
Definition: dl-comp-2
dl-comp-2(x) == snd(x).1
Lemma: dl-comp-2_wf
∀[x:Prog]. dl-comp-2(x) ∈ Prog supposing ↑dl-comp?(x)
Definition: dl-choose-1
dl-choose-1(x) == snd(x).0
Lemma: dl-choose-1_wf
∀[x:Prog]. dl-choose-1(x) ∈ Prog supposing ↑dl-choose?(x)
Definition: dl-choose-2
dl-choose-2(x) == snd(x).1
Lemma: dl-choose-2_wf
∀[x:Prog]. dl-choose-2(x) ∈ Prog supposing ↑dl-choose?(x)
Definition: dl-iterate-1
dl-iterate-1(x) == snd(x).0
Lemma: dl-iterate-1_wf
∀[x:Prog]. dl-iterate-1(x) ∈ Prog supposing ↑dl-iterate?(x)
Definition: dl-test-1
dl-test-1(x) == snd(x).0
Lemma: dl-test-1_wf
∀[x:Prog]. dl-test-1(x) ∈ Prop supposing ↑dl-test?(x)
Definition: dl-aprop-1
dl-aprop-1(x) == snd(x).0
Lemma: dl-aprop-1_wf
∀[x:Prop]. dl-aprop-1(x) ∈ ℕ supposing ↑dl-aprop?(x)
Definition: dl-implies-1
dl-implies-1(x) == snd(x).0
Lemma: dl-implies-1_wf
∀[x:Prop]. dl-implies-1(x) ∈ Prop supposing ↑dl-implies?(x)
Definition: dl-implies-2
dl-implies-2(x) == snd(x).1
Lemma: dl-implies-2_wf
∀[x:Prop]. dl-implies-2(x) ∈ Prop supposing ↑dl-implies?(x)
Definition: dl-and-1
dl-and-1(x) == snd(x).0
Lemma: dl-and-1_wf
∀[x:Prop]. dl-and-1(x) ∈ Prop supposing ↑dl-and?(x)
Definition: dl-and-2
dl-and-2(x) == snd(x).1
Lemma: dl-and-2_wf
∀[x:Prop]. dl-and-2(x) ∈ Prop supposing ↑dl-and?(x)
Definition: dl-or-1
dl-or-1(x) == snd(x).0
Lemma: dl-or-1_wf
∀[x:Prop]. dl-or-1(x) ∈ Prop supposing ↑dl-or?(x)
Definition: dl-or-2
dl-or-2(x) == snd(x).1
Lemma: dl-or-2_wf
∀[x:Prop]. dl-or-2(x) ∈ Prop supposing ↑dl-or?(x)
Definition: dl-box-1
dl-box-1(x) == snd(x).0
Lemma: dl-box-1_wf
∀[x:Prop]. dl-box-1(x) ∈ Prog supposing ↑dl-box?(x)
Definition: dl-box-2
dl-box-2(x) == snd(x).1
Lemma: dl-box-2_wf
∀[x:Prop]. dl-box-2(x) ∈ Prop supposing ↑dl-box?(x)
Definition: dl-diamond-1
dl-diamond-1(x) == snd(x).0
Lemma: dl-diamond-1_wf
∀[x:Prop]. dl-diamond-1(x) ∈ Prog supposing ↑dl-diamond?(x)
Definition: dl-diamond-2
dl-diamond-2(x) == snd(x).1
Lemma: dl-diamond-2_wf
∀[x:Prop]. dl-diamond-2(x) ∈ Prop supposing ↑dl-diamond?(x)
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]))
Definition: dl-ind
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]) ==
TERMOF{dl-induction:o, 1:l} (λx0.aprog[x0])
(λx1,x2,x3,x4. comp[x1;
x2;
x3;
x4])
(λx5,x6,x7,x8. choose[x5;
x6;
x7;
x8])
(λx9,x10. iterate[x9; x10])
(λx11,x12. test[x11; x12])
(λx13.aprop[x13])
false
(λx14,x15,x16,x17. implies[x14;
x15;
x16;
x17])
(λx18,x19,x20,x21. and[x18;
x19;
x20;
x21])
(λx22,x23,x24,x25. or[x22;
x23;
x24;
x25])
(λx26,x27,x28,x29. box[x26;
x27;
x28;
x29])
(λx30,x31,x32,x33. diamond[x30;
x31;
x32;
x33])
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])
Lemma: dl-ind_wf_definition
∀[A,B:TYPE]. ∀[aprog:x:ℕ ⟶ A]. ∀[comp,choose:x:Prog ⟶ x1:Prog ⟶ A ⟶ A ⟶ A]. ∀[iterate:x:Prog ⟶ A ⟶ A].
∀[test:x:Prop ⟶ B ⟶ A]. ∀[aprop:x:ℕ ⟶ B]. ∀[false:B]. ∀[implies,and,or:x:Prop ⟶ x1:Prop ⟶ B ⟶ B ⟶ B].
∀[box,diamond:x:Prog ⟶ x1:Prop ⟶ A ⟶ B ⟶ B].
(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]) ∈ d:dl-Obj() ⟶ if dl-kind(d) =a "prog"
then A
else B
fi )
Lemma: dl-ind-dl-aprog
∀[aprog,comp,choose,iterate,test,aprop,false,implies,and,or,box,diamond,x:Top].
(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])
prog(atm(x)) ~ aprog[x])
Lemma: dl-ind-dl-comp
∀[aprog,comp,choose,iterate,test,aprop,false,implies,and,or,box,diamond,x,x1:Top].
(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])
prog((x;x1)) ~ comp[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])
prog(x);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])
prog(x1)])
Lemma: dl-ind-dl-choose
∀[aprog,comp,choose,iterate,test,aprop,false,implies,and,or,box,diamond,x,x1:Top].
(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])
prog(x ⋃ x1) ~ choose[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])
prog(x);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])
prog(x1)])
Lemma: dl-ind-dl-iterate
∀[aprog,comp,choose,iterate,test,aprop,false,implies,and,or,box,diamond,x:Top].
(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])
prog((x)*) ~ iterate[x;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])
prog(x)])
Lemma: dl-ind-dl-test
∀[aprog,comp,choose,iterate,test,aprop,false,implies,and,or,box,diamond,x:Top].
(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])
prog((x)?) ~ test[x;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])
prop(x)])
Lemma: dl-ind-dl-aprop
∀[aprog,comp,choose,iterate,test,aprop,false,implies,and,or,box,diamond,x:Top].
(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])
prop(atm(x)) ~ aprop[x])
Lemma: dl-ind-dl-false
∀[aprog,comp,choose,iterate,test,aprop,false,implies,and,or,box,diamond:Top].
(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])
prop(0) ~ false)
Lemma: dl-ind-dl-implies
∀[aprog,comp,choose,iterate,test,aprop,false,implies,and,or,box,diamond,x,x1:Top].
(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])
prop(x ⇒ x1) ~ implies[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])
prop(x);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])
prop(x1)])
Lemma: dl-ind-dl-and
∀[aprog,comp,choose,iterate,test,aprop,false,implies,and,or,box,diamond,x,x1:Top].
(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])
prop(x ∧ x1) ~ and[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])
prop(x);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])
prop(x1)])
Lemma: dl-ind-dl-or
∀[aprog,comp,choose,iterate,test,aprop,false,implies,and,or,box,diamond,x,x1:Top].
(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])
prop(x ∨ x1) ~ or[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])
prop(x);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])
prop(x1)])
Lemma: dl-ind-dl-box
∀[aprog,comp,choose,iterate,test,aprop,false,implies,and,or,box,diamond,x,x1:Top].
(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])
prop([x] x1) ~ box[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])
prog(x);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])
prop(x1)])
Lemma: dl-ind-dl-diamond
∀[aprog,comp,choose,iterate,test,aprop,false,implies,and,or,box,diamond,x,x1:Top].
(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])
prop(<x> x1) ~ diamond[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])
prog(x);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])
prop(x1)])
Definition: dl-obj-prog
dl-obj-prog(x) == snd(x)
Lemma: dl-obj-prog_wf
∀[x:dl-Obj()]. dl-obj-prog(x) ∈ Prog supposing dl-kind(x) = "prog" ∈ Atom
Definition: dl-obj-prop
dl-obj-prop(x) == snd(x)
Lemma: dl-obj-prop_wf
∀[x:dl-Obj()]. dl-obj-prop(x) ∈ Prop supposing dl-kind(x) = "prop" ∈ Atom
Definition: dlo-eq
dlo-eq() ==
dl-ind(
dl-aprog(x)⇒ λa.(dl-kind(a) =a "prog" ∧b dl-aprog?(dl-obj-prog(a)) ∧b (dl-aprog-1(dl-obj-prog(a)) =z x));
dl-comp(b1,b2)⇒ l1,l2.λa.(dl-kind(a) =a "prog"
∧b dl-comp?(dl-obj-prog(a))
∧b (l1 prog(dl-comp-1(dl-obj-prog(a))))
∧b (l2 prog(dl-comp-2(dl-obj-prog(a)))));
dl-choose(b1,b2)⇒ l1,l2.λa.(dl-kind(a) =a "prog"
∧b dl-choose?(dl-obj-prog(a))
∧b (l1 prog(dl-choose-1(dl-obj-prog(a))))
∧b (l2 prog(dl-choose-2(dl-obj-prog(a)))));
dl-iterate(b1)⇒ l1.λa.(dl-kind(a) =a "prog"
∧b dl-iterate?(dl-obj-prog(a))
∧b (l1 prog(dl-iterate-1(dl-obj-prog(a)))));
dl-test(phi)⇒ l1.λa.(dl-kind(a) =a "prog"
∧b dl-test?(dl-obj-prog(a))
∧b (l1 prop(dl-test-1(dl-obj-prog(a)))));
dl-aprop(x)⇒ λa.(dl-kind(a) =a "prop" ∧b dl-aprop?(dl-obj-prop(a)) ∧b (dl-aprop-1(dl-obj-prop(a)) =z x));
dl-false⇒ λa.(dl-kind(a) =a "prop" ∧b dl-false?(dl-obj-prop(a)));
dl-implies(p,q)⇒ l1,l2.λa.(dl-kind(a) =a "prop"
∧b dl-implies?(dl-obj-prop(a))
∧b (l1 prop(dl-implies-1(dl-obj-prop(a))))
∧b (l2 prop(dl-implies-2(dl-obj-prop(a)))));
dl-and(p,q)⇒ l1,l2.λa.(dl-kind(a) =a "prop"
∧b dl-and?(dl-obj-prop(a))
∧b (l1 prop(dl-and-1(dl-obj-prop(a))))
∧b (l2 prop(dl-and-2(dl-obj-prop(a)))));
dl-or(p,q)⇒ l1,l2.λa.(dl-kind(a) =a "prop"
∧b dl-or?(dl-obj-prop(a))
∧b (l1 prop(dl-or-1(dl-obj-prop(a))))
∧b (l2 prop(dl-or-2(dl-obj-prop(a)))));
dl-box(alpha,phi)⇒ l1,l2.λa.(dl-kind(a) =a "prop"
∧b dl-box?(dl-obj-prop(a))
∧b (l1 prog(dl-box-1(dl-obj-prop(a))))
∧b (l2 prop(dl-box-2(dl-obj-prop(a)))));
dl-diamond(alpha,phi)⇒ l1,l2.λa.(dl-kind(a) =a "prop"
∧b dl-diamond?(dl-obj-prop(a))
∧b (l1 prog(dl-diamond-1(dl-obj-prop(a))))
∧b (l2 prop(dl-diamond-2(dl-obj-prop(a))))))
Lemma: dlo-eq_wf
dlo-eq() ∈ dl-Obj() ⟶ dl-Obj() ⟶ 𝔹
Definition: dlo_eq
dlo_eq(a;b) == dlo-eq() a b
Lemma: dlo_eq_wf
∀[a,b:dl-Obj()]. (dlo_eq(a;b) ∈ 𝔹)
Lemma: assert-dlo_eq
∀a,b:dl-Obj(). (↑dlo_eq(a;b) ⇐⇒ a = b ∈ dl-Obj())
Definition: dl-prop-deq
dl-prop-deq() == λa,b. dlo_eq(prop(a);prop(b))
Lemma: dl-prop-deq_wf
dl-prop-deq() ∈ EqDecider(Prop)
Definition: dlo-le
dlo-le() ==
dl-ind(
dl-aprog(x)⇒ λa.dlo_eq(prog(atm(x));a);
dl-comp(b1,b2)⇒ l1,l2.λa.(((l1 a) ∨b(l2 a)) ∨bdlo_eq(prog((b1;b2));a));
dl-choose(b1,b2)⇒ l1,l2.λa.(((l1 a) ∨b(l2 a)) ∨bdlo_eq(prog(b1 ⋃ b2);a));
dl-iterate(b1)⇒ l1.λa.((l1 a) ∨bdlo_eq(prog((b1)*);a));
dl-test(b1)⇒ l1.λa.((l1 a) ∨bdlo_eq(prog((b1)?);a));
dl-aprop(x)⇒ λa.dlo_eq(prop(atm(x));a);
dl-false⇒ λa.dlo_eq(prop(0);a);
dl-implies(b1,b2)⇒ l1,l2.λa.(((l1 a) ∨b(l2 a)) ∨bdlo_eq(prop(b1 ⇒ b2);a));
dl-and(b1,b2)⇒ l1,l2.λa.(((l1 a) ∨b(l2 a)) ∨bdlo_eq(prop(b1 ∧ b2);a));
dl-or(b1,b2)⇒ l1,l2.λa.(((l1 a) ∨b(l2 a)) ∨bdlo_eq(prop(b1 ∨ b2);a));
dl-box(b1,b2)⇒ l1,l2.λa.(((l1 a) ∨b(l2 a)) ∨bdlo_eq(prop([b1] b2);a));
dl-diamond(b1,b2)⇒ l1,l2.λa.(((l1 a) ∨b(l2 a)) ∨bdlo_eq(prop(<b1> b2);a)))
Lemma: dlo-le_wf
dlo-le() ∈ dl-Obj() ⟶ dl-Obj() ⟶ 𝔹
Definition: dlo_le
a ≤ b == dlo-le() b a
Lemma: dlo_le_wf
∀[a,b:dl-Obj()]. (a ≤ b ∈ 𝔹)
Lemma: dlo-refl
∀a:dl-Obj(). (↑a ≤ a)
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]))
Definition: dl-sem
dl-sem(K;n.R[n];m.P[m]) ==
dl-ind(
dl-aprog(n)⇒ R[n];
dl-comp(alpha,beta)⇒ r1,r2.λk1,k3. ∃k2:K. ((r1 k1 k2) ∧ (r2 k2 k3));
dl-choose(alpha,beta)⇒ r1,r2.λk1,k2. ((r1 k1 k2) ∨ (r2 k1 k2));
dl-iterate(alpha)⇒ r.r^*;
dl-test(phi)⇒ p.λk1,k2. ((p k1) ∧ (k2 = k1 ∈ K));
dl-aprop(m)⇒ P[m];
dl-false⇒ λk.False;
dl-implies(phi,psi)⇒ p,q.λk.((p k) ⇒ (q k));
dl-and(phi,psi)⇒ p,q.λk.((p k) ∧ (q k));
dl-or(phi,psi)⇒ p,q.λk.((p k) ∨ (q k));
dl-box(alpha,phi)⇒ r,p.λk.∀k':K. ((r k k') ⇒ (p k'));
dl-diamond(alpha,phi)⇒ r,p.λk.∃k':K. ((r k k') ∧ (p k')))
Lemma: dl-sem_wf
∀[K:Type]. ∀[R:ℕ ⟶ K ⟶ K ⟶ ℙ]. ∀[P:ℕ ⟶ K ⟶ ℙ].
(dl-sem(K;n.R[n];m.P[m]) ∈ d:dl-Obj() ⟶ if dl-kind(d) =a "prog" then K ⟶ K ⟶ ℙ else K ⟶ ℙ fi )
Definition: dl-same-sem
dl-same-sem(x;K;r;s) ==
((dl-kind(x) = "prog" ∈ Atom) ⇒ (∀k,k':K. (r k k' ⇐⇒ s k k')))
∧ ((dl-kind(x) = "prop" ∈ Atom) ⇒ (∀k:K. (r k ⇐⇒ s k)))
Lemma: dl-same-sem_wf
∀[x:dl-Obj()]. ∀[K:Type]. ∀[r,s:if dl-kind(x) =a "prog" then K ⟶ K ⟶ ℙ else K ⟶ ℙ fi ]. (dl-same-sem(x;K;r;s) ∈ ℙ)
Definition: dl-prop-sem
[|phi|] == dl-sem(K;n.R[n];m.P[m]) prop(phi)
Lemma: dl-prop-sem_wf
∀[K:Type]. ∀[R:ℕ ⟶ K ⟶ K ⟶ ℙ]. ∀[P:ℕ ⟶ K ⟶ ℙ]. ∀[phi:Prop]. ([|phi|] ∈ K ⟶ ℙ)
Definition: dl-prog-sem
[|alpha|] == dl-sem(K;n.R[n];m.P[m]) prog(alpha)
Lemma: dl-prog-sem_wf
∀[K:Type]. ∀[R:ℕ ⟶ K ⟶ K ⟶ ℙ]. ∀[P:ℕ ⟶ K ⟶ ℙ]. ∀[alpha:Prog]. ([|alpha|] ∈ K ⟶ K ⟶ ℙ)
Definition: dl-prop-atoms
dl-prop-atoms() ==
dl-ind(
dl-aprog(a)⇒ [];
dl-comp(alpha,beta)⇒ L1,L2.L1 @ L2;
dl-choose(alpha,beta)⇒ L1,L2.L1 @ L2;
dl-iterate(a)⇒ L.L;
dl-test(phi)⇒ L.L;
dl-aprop(a)⇒ [a];
dl-false⇒ [];
dl-implies(phi,psi)⇒ L1,L2.L1 @ L2;
dl-and(phi,psi)⇒ L1,L2.L1 @ L2;
dl-or(phi,psi)⇒ L1,L2.L1 @ L2;
dl-box(alpha,phi)⇒ L1,L2.L1 @ L2;
dl-diamond(alpha,phi)⇒ L1,L2.L1 @ L2)
Lemma: dl-prop-atoms_wf
dl-prop-atoms() ∈ ∀x:dl-Obj(). (ℕ List)
Lemma: dl-sem_functionality1
∀x:dl-Obj()
∀[K:Type]. ∀[R:ℕ ⟶ K ⟶ K ⟶ ℙ]. ∀[P,P':ℕ ⟶ K ⟶ ℙ].
((∀n∈dl-prop-atoms() x.∀k:K. (P[n] k ⇐⇒ P'[n] k))
⇒ dl-same-sem(x;K;dl-sem(K;n.R[n];m.P[m]) x;dl-sem(K;n.R[n];m.P'[m]) x))
Lemma: dl-prog-sem_functionality
∀alpha:Prog
∀[K:Type]. ∀[R:ℕ ⟶ K ⟶ K ⟶ ℙ]. ∀[P,P':ℕ ⟶ K ⟶ ℙ].
((∀n∈dl-prop-atoms() prog(alpha).∀k:K. (P[n] k ⇐⇒ P'[n] k)) ⇒ (∀k,k':K. ([|alpha|] k k' ⇐⇒ [|alpha|] k k')))
Lemma: dl-lt_functionality
∀x,y,x',y':dl-Obj(). ((↑dlo_eq(x;x')) ⇒ (↑dlo_eq(y;y')) ⇒ x ≤ y = x' ≤ y')
Definition: dl-valid
|= phi == ∀K:Type. ∀R:ℕ ⟶ K ⟶ K ⟶ ℙ. ∀P:ℕ ⟶ K ⟶ ℙ. ∀k:K. ([|phi|] k)
Lemma: dl-valid_wf
∀[phi:Prop]. (|= phi ∈ ℙ')
Definition: dl-equiv
(phi ⇐⇒ psi) == |= phi ⇒ psi ∧ |= psi ⇒ phi
Lemma: dl-equiv_wf
∀[phi,psi:Prop]. ((phi ⇐⇒ psi) ∈ ℙ')
Lemma: dl-valid-trivial
∀phi:Prop. |= phi ⇒ phi
Lemma: dl-valid-box-choose
∀a,b:Prog. ∀phi:Prop. |= [a] phi ⇒ [b] phi ⇒ [a ⋃ b] phi
Lemma: dl-valid-diamond-choose
∀a,b:Prog. ∀phi:Prop. |= <a> phi ⇒ <b> phi ⇒ <a ⋃ b> phi
Lemma: dl-valid-box-comp
∀a,b:Prog. ∀phi,psi:Prop. (|= phi ⇒ [b] psi ⇒ |= [a] phi ⇒ [(a;b)] psi)
Lemma: dl-valid-box-comp2
∀a,b:Prog. ∀phi,psi:Prop. |= phi ⇒ [b] psi ⇒ [a] phi ⇒ [(a;b)] psi
Lemma: dl-diamond-comp
∀a,b:Prog. ∀phi:Prop. (<(a;b)> phi ⇐⇒ <a> <b> phi)
Lemma: dl-box-comp
∀a,b:Prog. ∀phi:Prop. ([(a;b)] phi ⇐⇒ [a] [b] phi)
Lemma: dl-diamond-choose
∀a,b:Prog. ∀phi:Prop. (<a ⋃ b> phi ⇐⇒ <a> phi ∨ <b> phi)
Lemma: dl-box-choose
∀a,b:Prog. ∀phi:Prop. ([a ⋃ b] phi ⇐⇒ [a] phi ∧ [b] phi)
Lemma: dl-diamond-iterate
∀a:Prog. ∀phi:Prop. (<(a)*> phi ⇐⇒ phi ∨ <a> <(a)*> phi)
Lemma: dl-box-iterate
∀a:Prog. ∀phi:Prop. ([(a)*] phi ⇐⇒ phi ∧ [a] [(a)*] phi)
Lemma: dl-valid-diamond-dist-or
∀a:Prog. ∀phi,psi:Prop. (|= <a> phi ∨ psi ⇒ |= <a> phi ∨ <a> psi)
Lemma: dl-valid-diamond-dist-or2
∀a:Prog. ∀phi,psi:Prop. (|= <a> phi ∨ <a> psi ⇒ |= <a> phi ∨ psi)
Lemma: dl-valid-box-dist-and
∀a:Prog. ∀phi,psi:Prop. (|= [a] phi ∧ psi ⇒ |= [a] phi ∧ [a] psi)
Lemma: dl-valid-box-dist-and2
∀a:Prog. ∀phi,psi:Prop. (|= [a] phi ∧ [a] psi ⇒ |= [a] phi ∧ psi)
Lemma: dl-valid-diamond-box-distibute
∀a:Prog. ∀phi,psi:Prop. (|= <a> phi ∧ [a] psi ⇒ |= <a> phi ∧ psi)
Lemma: dl-valid-box-distibute-implies
∀a:Prog. ∀phi,psi:Prop. (|= [a] phi ⇒ psi ⇒ |= [a] phi ⇒ [a] psi)
Lemma: dl-valid-box-choose-dist-and
∀a,b:Prog. ∀phi:Prop. (|= [a ⋃ b] phi ⇒ |= [a] phi ∧ [b] phi)
Lemma: dl-valid-box-choose-dist-and-2
∀a,b:Prog. ∀phi:Prop. (|= [a] phi ∧ [b] phi ⇒ |= [a ⋃ b] phi)
Lemma: dl-valid-box-comp-double-box
∀a,b:Prog. ∀phi:Prop. (|= [(a;b)] phi ⇒ |= [a] [b] phi)
Lemma: dl-valid-box-comp-double-box2
∀a,b:Prog. ∀phi:Prop. (|= [a] [b] phi ⇒ |= [(a;b)] phi)
Lemma: dl-valid-box-test-implies
∀phi,psi:Prop. (|= [(psi)?] phi ⇒ |= psi ⇒ phi)
Lemma: dl-valid-box-test-implies2
∀a:Prog. ∀phi,psi:Prop. (|= [psi] a ⇒ |= [(psi)?] phi)
Lemma: dl-valid-box-test-implies21
∀phi,psi:Prop. |= (psi ⇒ phi) ⇒ [(psi)?] phi
Lemma: dl-valid-induction-ax
∀a:Prog. ∀phi:Prop. (|= phi ∧ [(a)*] phi ⇒ [a] phi ⇒ |= [(a)*] phi)
Definition: dl-true
dl-true() == 0 ⇒ 0
Lemma: dl-true_wf
dl-true() ∈ Prop
Definition: dl-conj
dl-conj(L) == reduce(λx,y. (x ∧ y);dl-true();L)
Lemma: dl-conj_wf
∀[L:Prop List]. (dl-conj(L) ∈ Prop)
Definition: dl-sem-eq
a ≡ b == ∀K:Type. ∀R:ℕ ⟶ K ⟶ K ⟶ ℙ. ∀P:ℕ ⟶ K ⟶ ℙ. ∀k1,k2:K. ([|a|] k1 k2 ⇐⇒ [|b|] k1 k2)
Lemma: dl-sem-eq_wf
∀[a,b:Prog]. (a ≡ b ∈ ℙ')
Definition: dl-logical-eq-weak
(a ⇐⇒w b) ==
∃p:ℕ
((¬(p ∈ dl-prop-atoms() prog(a)))
∧ (¬(p ∈ dl-prop-atoms() prog(b)))
∧ |= <a> atm(p) ⇒ <b> atm(p)
∧ |= <b> atm(p) ⇒ <a> atm(p))
Lemma: dl-logical-eq-weak_wf
∀[a,b:Prog]. ((a ⇐⇒w b) ∈ ℙ')
Definition: dl-logical-eq-atomic
(a ⇐⇒a b) == ∀p:ℕ. (|= <a> atm(p) ⇒ <b> atm(p) ∧ |= <b> atm(p) ⇒ <a> atm(p))
Lemma: dl-logical-eq-atomic_wf
∀[a,b:Prog]. ((a ⇐⇒a b) ∈ ℙ')
Definition: dl-logical-eq
(a ⇐⇒ b) == ∀phi:Prop. (|= <a> phi ⇒ <b> phi ∧ |= <b> phi ⇒ <a> phi)
Lemma: dl-logical-eq_wf
∀[a,b:Prog]. ((a ⇐⇒ b) ∈ ℙ')
Lemma: dl-program-eq-equiv
∀a,b:Prog. equiv-props([(a ⇐⇒ b); (a ⇐⇒a b); (a ⇐⇒w b); a ≡ b])
Lemma: dl-diamond-unwind-1
∀a:Prog. ∀phi:Prop. |= <(a)*> phi ⇒ (phi ∨ <a> (phi ⇒ 0) ∨ <(a)*> phi)
Definition: worlds
worlds(k) == k."w"
Definition: KrRel
sRt == k."mAR" s t
Definition: iPO
iPO(k;s;t) == k."iPO" s t
Definition: atmFrc_prop
atmFrc_prop(k;a;s) == k."F" a s
Definition: atmFrc_prog
atmFrc_prog(k;a;r;s) == k."G" a r s
Definition: dl_KripkeStructure
dl_KripkeStructure ==
"w":Type
"iPO":worlds(self) ⟶ worlds(self) ⟶ ℙ
"mAR":worlds(self) ⟶ worlds(self) ⟶ ℙ
"F":ℕ ⟶ worlds(self) ⟶ ℙ
"G":ℕ ⟶ worlds(self) ⟶ worlds(self) ⟶ ℙ
Lemma: dl_KripkeStructure_wf
dl_KripkeStructure ∈ 𝕌'
Lemma: worlds_wf
∀[k:dl_KripkeStructure]. (worlds(k) ∈ Type)
Lemma: iPO_wf
∀[K:dl_KripkeStructure]. ∀[s,t:worlds(K)]. (iPO(K;s;t) ∈ ℙ)
Lemma: KrRel_wf
∀[K:dl_KripkeStructure]. ∀[s,t:worlds(K)]. (sRt ∈ ℙ)
Lemma: atmFrc_prop_wf
∀[K:dl_KripkeStructure]. ∀[t:worlds(K)]. ∀[a:ℕ]. (atmFrc_prop(K;a;t) ∈ ℙ)
Lemma: atmFrc_prog_wf
∀[K:dl_KripkeStructure]. ∀[s,t:worlds(K)]. ∀[a:ℕ]. (atmFrc_prog(K;a;s;t) ∈ ℙ)
Definition: dl_KS
dl_KS ==
dl_KripkeStructure
"Rref":∀i:worlds(self). iRi
"Rtrans":∀r,s,t:worlds(self). (rRs ⇒ sRt ⇒ rRt)
"FP":∀i:worlds(self). ∀a:ℕ. (atmFrc_prop(self;a;i) ⇒ (∀j:worlds(self). (iRj ⇒ atmFrc_prop(self;a;j))))
Lemma: dl_KS_wf
dl_KS ∈ 𝕌'
Lemma: dl_KS_subtype
dl_KS ⊆r dl_KripkeStructure
Definition: Rref
Rref(k;i) == k."Rref" i
Lemma: Rref_wf
∀[K:dl_KS]. ∀i:worlds(K). (Rref(K;i) ∈ iRi)
Definition: Rtrans
Rtrans(k;r;s;t) == k."Rtrans" r s t
Lemma: Rtrans_wf
∀K:dl_KS. ∀r,s,t:worlds(K). (Rtrans(K;r;s;t) ∈ rRs ⇒ sRt ⇒ rRt)
Definition: atmFrcPersistent
atmFrcPersistent(k;i;a) == k."FP" i a
Lemma: atmFrcPersistent_wf
∀K:dl_KS. ∀i:worlds(K). ∀a:ℕ.
(atmFrcPersistent(K;i;a) ∈ atmFrc_prop(K;a;i) ⇒ (∀j:worlds(K). (iRj ⇒ atmFrc_prop(K;a;j))))
Lemma: dl-R_refl
∀K:dl_KS. ∀i:worlds(K). iRi
Lemma: dl-R_trans
∀K:dl_KS. ∀i,j,k:worlds(K). (iRj ⇒ jRk ⇒ iRk)
Lemma: aFPersistent
∀K:dl_KS. ∀i:worlds(K). ∀a:ℕ. (atmFrc_prop(K;a;i) ⇒ (∀j:worlds(K). (iRj ⇒ atmFrc_prop(K;a;j))))
Definition: dl_forces
dl_forces(K;pos;a;s) ==
dl-ind(
dl-aprog(n)⇒ λk1,k2. (k1Rk2 ∧ atmFrc_prog(K;n;k1;k2));
dl-comp(alpha,beta)⇒ r1,r2.λk1,k3. ∃k2:worlds(K). ((r1 k1 k2) ∧ (r2 k2 k3));
dl-choose(alpha,beta)⇒ r1,r2.λk1,k2. ((r1 k1 k2) ∨ (r2 k1 k2));
dl-iterate(alpha)⇒ r.r^*;
dl-test(phi)⇒ p.λk1,k2. ((p tt k1) ∧ (k2 = k1 ∈ worlds(K)));
dl-aprop(m)⇒ λpos,k. atmFrc_prop(K;m;k);
dl-false⇒ λpos,k. if pos then False else True fi ;
dl-implies(phi,psi)⇒ p,q.λpos,k. if pos
then ∀k':worlds(K). (kRk' ⇒ (p tt k') ⇒ (q tt k'))
else ∃t:worlds(K). (kRt ∧ (p tt t) ∧ (q ff t))
fi ;
dl-and(phi,psi)⇒ p,q.λpos,k. if pos then (p tt k) ∧ (q tt k) else (p ff k) ∨ (q ff k) fi ;
dl-or(phi,psi)⇒ p,q.λpos,k. if pos then (p tt k) ∨ (q tt k) else (p ff k) ∧ (q ff k) fi ;
dl-box(alpha,phi)⇒ r,p.λpos,k. if pos
then ∀k':worlds(K). (kRk' ⇒ (r k k') ⇒ (p tt k))
else ∃t:worlds(K). ((kRt ∧ (r k t)) ∧ (p ff k))
fi ;
dl-diamond(alpha,phi)⇒ r,p.λpos,k. if pos
then ∃k':worlds(K). (kRk' ∧ (r k k') ∧ (p tt k'))
else ∀t:worlds(K). (kRt ⇒ (r k t) ⇒ (p ff k))
fi )
prop(a)
pos
s
Lemma: dl_forces_wf
∀[K:dl_KS]. ∀[a:Prop]. ∀[s:worlds(K)]. ∀[pos:𝔹]. (dl_forces(K;pos;a;s) ∈ ℙ)
Lemma: dl-forces-trivial
∀K:dl_KS. ∀phi:Prop. ∀s:worlds(K). dl_forces(K;tt;phi ⇒ phi;s)
Definition: node
node == Prop List × (Prop List)
Lemma: node_wf
node ∈ Type
Definition: System
System == node List
Lemma: System_wf
System ∈ Type
Definition: dl-localT
localT ==
dl-ind(
dl-aprog(a)⇒ [];
dl-comp(alpha,beta)⇒ L1,L2.[];
dl-choose(alpha,beta)⇒ L1,L2.[];
dl-iterate(a)⇒ L.[];
dl-test(phi)⇒ L.[];
dl-aprop(a)⇒ [];
dl-false⇒ [0];
dl-implies(phi,psi)⇒ l1,l2.[];
dl-and(phi,psi)⇒ l1,l2.l1 @ l2;
dl-or(phi,psi)⇒ l1,l2.[];
dl-box(alpha,phi)⇒ L1,L2.[];
dl-diamond(alpha,phi)⇒ L1,L2.[])
Lemma: dl-localT_wf
localT ∈ dl-Obj() ⟶ (Prop List)
Definition: dl-localF
localF ==
dl-ind(
dl-aprog(a)⇒ [];
dl-comp(alpha,beta)⇒ L1,L2.[];
dl-choose(alpha,beta)⇒ L1,L2.[];
dl-iterate(a)⇒ L.[];
dl-test(phi)⇒ L.[];
dl-aprop(a)⇒ [atm(a)];
dl-false⇒ [0];
dl-implies(phi,psi)⇒ l1,l2.[];
dl-and(phi,psi)⇒ l1,l2.[phi] @ [psi];
dl-or(phi,psi)⇒ l1,l2.[phi] @ [psi];
dl-box(alpha,phi)⇒ L1,L2.[];
dl-diamond(alpha,phi)⇒ L1,L2.[])
Lemma: dl-localF_wf
localF ∈ ∀x:dl-Obj(). (Prop List)
Definition: node_complete
node_complete{i:l}(n) ==
(∀f∈fst(n).(∀f1∈localT prop(f).(f1 ∈ fst(n)))) ∧ (∀f∈snd(n).(∀f1∈localF prop(f).(f1 ∈ snd(n))))
Lemma: node_complete_wf
∀n:node. (node_complete{i:l}(n) ∈ ℙ)
Lemma: decidable__node_complete
∀n:node. ((∀x,y:Prop. Dec(x = y ∈ Prop)) ⇒ Dec(node_complete{i:l}(n)))
Lemma: decidable__node_complete2
∀n:node. ∀d:EqDecider(Prop). Dec(node_complete{i:l}(n))
Lemma: ncomplete-test
((∀a:Prop. (localT prop(a) ∈ Prop List)) ∧ (∀n:node. (fst(n) ∈ Prop List)))
∧ (∀n:node. (∀f∈fst(n).f ∈ Prop))
∧ (∀n:node. (∀f1∈fst(n).(∀f∈localT prop(f1).f ∈ Prop)))
∧ (∀n:node. (∀f∈fst(n).(∀f1∈localT prop(f).(∃f1'∈fst(n). dlo_eq(prop(f1);prop(f1')) ∈ 𝔹))))
Definition: sys-subformulas
sys-subformulas(S) == {phi:Prop| True}
Lemma: sys-subformulas_wf
∀[S:Top]. (sys-subformulas(S) ∈ Type)
Definition: complete
complete{i:l}(S) ==
(∀n∈S.(∃y∈snd(n). |= dl-conj(fst(n)) ⇒ y))
∨ (∃K:dl_KS
∃f:node ⟶ worlds(K). (∀n∈S.(∀phi∈fst(n).dl_forces(K;tt;phi;f n)) ∧ (∀phi∈snd(n).dl_forces(K;ff;phi;f n))))
Lemma: complete_wf
∀[S:System]. (complete{i:l}(S) ∈ ℙ')
Home
Index