---

Step * of 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 )
BY
{ MrecIndDef }

---

Latex:

---

Latex:
\mforall{}[A,B:TYPE].  \mforall{}[aprog:x:\mBbbN{}  {}\mrightarrow{}  A].  \mforall{}[comp,choose:x:Prog  {}\mrightarrow{}  x1:Prog  {}\mrightarrow{}  A  {}\mrightarrow{}  A  {}\mrightarrow{}  A].  \mforall{}[iterate:x:Prog
                                                                                                                                                                                      {}\mrightarrow{}  A
                                                                                                                                                                                      {}\mrightarrow{}  A].
\mforall{}[test:x:Prop  {}\mrightarrow{}  B  {}\mrightarrow{}  A].  \mforall{}[aprop:x:\mBbbN{}  {}\mrightarrow{}  B].  \mforall{}[false:B].  \mforall{}[implies,and,or:x:Prop
                                                                                                                                                    {}\mrightarrow{}  x1:Prop
                                                                                                                                                    {}\mrightarrow{}  B
                                                                                                                                                    {}\mrightarrow{}  B
                                                                                                                                                    {}\mrightarrow{}  B].
\mforall{}[box,diamond:x:Prog  {}\mrightarrow{}  x1:Prop  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B].
    (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{}  d:dl-Obj()
      {}\mrightarrow{}  if  dl-kind(d)  =a  "prog"  then  A  else  B  fi  )


By

---

Latex:
MrecIndDef

---

Home Index