Proof of Nuprl Lemma : dl-ind-dl-diamond

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

Latex:

Latex:
\mforall{}[aprog,comp,choose,iterate,test,aprop,false,implies,and,or,box,diamond,x,x1:Top]. (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]) prop(<x> x1) \msim{} diamond[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]) prog(x);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]) prop(x1)]) By Latex: MrecIndReduce Home Index