---

Step * of Lemma dl_forces_wf

No Annotations
∀[K:dl_KS]. ∀[a:Prop]. ∀[s:worlds(K)]. ∀[pos:𝔹].  (dl_forces(K;pos;a;s) ∈ ℙ)
BY
{ (Intros
   THEN Unhide
   THEN Unfold `dl_forces` 0
   THEN (InstLemma `dl-ind_wf_definition` [⌜worlds(K) ⟶ worlds(K) ⟶ ℙ⌝;⌜𝔹 ⟶ worlds(K) ⟶ ℙ⌝]⋅ THENA Auto)) }

1
1. K : dl_KS
2. a : Prop
3. s : worlds(K)
4. pos : 𝔹
5. ∀[aprog:x:ℕ ⟶ worlds(K) ⟶ worlds(K) ⟶ ℙ]. ∀[comp,choose:x:Prog
                                                              ⟶ x1:Prog
                                                              ⟶ (worlds(K) ⟶ worlds(K) ⟶ ℙ)
                                                              ⟶ (worlds(K) ⟶ worlds(K) ⟶ ℙ)
                                                              ⟶ worlds(K)
                                                              ⟶ worlds(K)
                                                              ⟶ ℙ]. ∀[iterate:x:Prog
                                                                               ⟶ (worlds(K) ⟶ worlds(K) ⟶ ℙ)
                                                                               ⟶ worlds(K)
                                                                               ⟶ worlds(K)
                                                                               ⟶ ℙ]. ∀[test:x:Prop
                                                                                             ⟶ (𝔹 ⟶ worlds(K) ⟶ ℙ)
                                                                                             ⟶ worlds(K)
                                                                                             ⟶ worlds(K)
                                                                                             ⟶ ℙ]. ∀[aprop:x:ℕ
                                                                                                            ⟶ 𝔹
                                                                                                            ⟶ worlds(K)
                                                                                                            ⟶ ℙ].
   ∀[false:𝔹 ⟶ worlds(K) ⟶ ℙ]. ∀[implies,and,or:x:Prop
                                                  ⟶ x1:Prop
                                                  ⟶ (𝔹 ⟶ worlds(K) ⟶ ℙ)
                                                  ⟶ (𝔹 ⟶ worlds(K) ⟶ ℙ)
                                                  ⟶ 𝔹
                                                  ⟶ worlds(K)
                                                  ⟶ ℙ]. ∀[box,diamond:x:Prog
                                                                       ⟶ x1:Prop
                                                                       ⟶ (worlds(K) ⟶ worlds(K) ⟶ ℙ)
                                                                       ⟶ (𝔹 ⟶ worlds(K) ⟶ ℙ)
                                                                       ⟶ 𝔹
                                                                       ⟶ worlds(K)
                                                                       ⟶ ℙ].
     (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 worlds(K) ⟶ worlds(K) ⟶ ℙ
                                                                                      else 𝔹 ⟶ worlds(K) ⟶ ℙ
                                                                                      fi )
⊢ 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 ∈ ℙ

---

Latex:

---

Latex:
No  Annotations
\mforall{}[K:dl\_KS].  \mforall{}[a:Prop].  \mforall{}[s:worlds(K)].  \mforall{}[pos:\mBbbB{}].    (dl\_forces(K;pos;a;s)  \mmember{}  \mBbbP{})


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  Unfold  `dl\_forces`  0
  THEN  (InstLemma  `dl-ind\_wf\_definition`  [\mkleeneopen{}worlds(K)  {}\mrightarrow{}  worlds(K)  {}\mrightarrow{}  \mBbbP{}\mkleeneclose{};\mkleeneopen{}\mBbbB{}  {}\mrightarrow{}  worlds(K)  {}\mrightarrow{}  \mBbbP{}\mkleeneclose{}]\mcdot{}
              THENA  Auto
              ))

---

Home Index