Nuprl Definition : test-ind

test-ind(
         test-aprog(x0)⇒ aprog[x0];
         test-iterate(x1)⇒ x2.iterate[x1; x2];
         test-test(x3)⇒ x4.test[x3; x4];
         test-afoo(x5)⇒ afoo[x5];
         test-bar(x6)⇒ x7.bar[x6; x7];
         test-xx(x8,x9)⇒ x10,x11.xx[x8; x9; x10; x11];
         test-aprop(x12)⇒ aprop[x12];
         test-false⇒ false;
         test-implies(x13,x14)⇒ x15,x16.implies[x13; x14; x15; x16];
         test-box(x17,x18)⇒ x19,x20.box[x17; x18; x19; x20];
         test-diamond(x21,x22)⇒ x23,x24.diamond[x21; x22; x23; x24])  ==
  TERMOF{test-induction:o, 1:l} (λx0.aprog[x0]) (λx1,x2. iterate[x1; x2]) (λx3,x4. test[x3; x4]) (λx5.afoo[x5]) (λx6,x7.\000C bar[x6; x7]) 
  (λx8,x9,x10,x11. xx[x8; x9; x10; x11]) 
  (λx12.aprop[x12]) 
  false 
  (λx13,x14,x15,x16. implies[x13; x14; x15; x16]) 
  (λx17,x18,x19,x20. box[x17; x18; x19; x20]) 
  (λx21,x22,x23,x24. diamond[x21; x22; x23; x24])


Definitions occuring in Statement :  apply: f a,  lambda: λx.A[x]
Definitions occuring in definition :  apply: f a,  test-induction,  lambda: λx.A[x]
TermOfs occuring in Definition :  test-induction
FDL editor aliases :  test-ind
Latex:
test-ind(
                  test-aprog(x0){}\mRightarrow{}  aprog[x0];
                  test-iterate(x1){}\mRightarrow{}  x2.iterate[x1;  x2];
                  test-test(x3){}\mRightarrow{}  x4.test[x3;  x4];
                  test-afoo(x5){}\mRightarrow{}  afoo[x5];
                  test-bar(x6){}\mRightarrow{}  x7.bar[x6;  x7];
                  test-xx(x8,x9){}\mRightarrow{}  x10,x11.xx[x8;  x9;  x10;  x11];
                  test-aprop(x12){}\mRightarrow{}  aprop[x12];
                  test-false{}\mRightarrow{}  false;
                  test-implies(x13,x14){}\mRightarrow{}  x15,x16.implies[x13;  x14;  x15;  x16];
                  test-box(x17,x18){}\mRightarrow{}  x19,x20.box[x17;  x18;  x19;  x20];
                  test-diamond(x21,x22){}\mRightarrow{}  x23,x24.diamond[x21;  x22;  x23;  x24])    ==
    TERMOF\{test-induction:o,  1:l\}  (\mlambda{}x0.aprog[x0])  (\mlambda{}x1,x2.  iterate[x1;  x2])  (\mlambda{}x3,x4.  test[x3;  x4])  (\mlambda{}x\000C5.afoo[x5]) 
    (\mlambda{}x6,x7.  bar[x6;  x7]) 
    (\mlambda{}x8,x9,x10,x11.  xx[x8;  x9;  x10;  x11]) 
    (\mlambda{}x12.aprop[x12]) 
    false 
    (\mlambda{}x13,x14,x15,x16.  implies[x13;  x14;  x15;  x16]) 
    (\mlambda{}x17,x18,x19,x20.  box[x17;  x18;  x19;  x20]) 
    (\mlambda{}x21,x22,x23,x24.  diamond[x21;  x22;  x23;  x24])


Date html generated: 2019_10_15-AM-10_51_26
Last ObjectModification: 2019_03_25-PM-01_46_34

Theory : tree_1


Home Index