Nuprl 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]\000C)

  (λ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])

Definitions occuring in Statement : apply: f a, lambda: λx.A[x]
Definitions occuring in definition : apply: f a, dl-induction, lambda: λx.A[x]
TermOfs occuring in Definition : dl-induction
FDL editor aliases : dl-ind

Latex:
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]) == TERMOF\{dl-induction:o, 1:l\} (\mlambda{}x0.aprog[x0]) (\mlambda{}x1,x2,x3,x4. comp[x1; x2; x3; x4]) (\mlambda{}x5,x6,x7,x8. choose[x5; x6; x7; x8]) (\mlambda{}x9,x10. iterate[x9; x10]) (\mlambda{}x11,x12. test[x11; x12]) (\mlambda{}x13.aprop[x13]) false (\mlambda{}x14,x15,x16,x17. implies[x14; x15; x16; x17]) (\mlambda{}x18,x19,x20,x21. and[x18; x19; x20; x21]) (\mlambda{}x22,x23,x24,x25. or[x22; x23; x24; x25]) (\mlambda{}x26,x27,x28,x29. box[x26; x27; x28; x29]) (\mlambda{}x30,x31,x32,x33. diamond[x30; x31; x32; x33]) Date html generated: 2019_10_15-AM-11_41_53 Last ObjectModification: 2019_03_26-AM-11_18_35 Theory : dynamic!logic Home Index