Quelle OutBoxes_adt.pvs Sprache: PVS

%%% ADT file generated from OutBoxes

OutBoxes_adt[n: posnat]: THEORY
BEGIN

  OutBoxes: TYPE

  IMPORTING boxes_def

  unknown_box?, full_box?, empty_box?, boxes?: [OutBoxes -> boolean]

  boxes: [(boxes?) -> Boxes(n)]

  UnknownBox: (unknown_box?)

  FullBox: (full_box?)

  EmptyBox: (empty_box?)

  Output: [Boxes(n) -> (boxes?)]

  OutBoxes_ord: [OutBoxes -> upto(3)]

  OutBoxes_ord_defaxiom: AXIOM
    OutBoxes_ord(UnknownBox) = 0 AND
     OutBoxes_ord(FullBox) = 1 AND
      OutBoxes_ord(EmptyBox) = 2 AND
       (FORALL (boxes: Boxes(n)): OutBoxes_ord(Output(boxes)) = 3);

  ord(x: OutBoxes): [OutBoxes -> upto(3)] =
      CASES x
        OF UnknownBox: 0, FullBox: 1, EmptyBox: 2, Output(Output1_var): 3
        ENDCASES

  OutBoxes_UnknownBox_extensionality: AXIOM
    FORALL (unknown_box?_var: (unknown_box?),
            unknown_box?_var2: (unknown_box?)):
      unknown_box?_var = unknown_box?_var2;

  OutBoxes_FullBox_extensionality: AXIOM
    FORALL (full_box?_var: (full_box?), full_box?_var2: (full_box?)):
      full_box?_var = full_box?_var2;

  OutBoxes_EmptyBox_extensionality: AXIOM
    FORALL (empty_box?_var: (empty_box?), empty_box?_var2: (empty_box?)):
      empty_box?_var = empty_box?_var2;

  OutBoxes_Output_extensionality: AXIOM
    FORALL (boxes?_var: (boxes?), boxes?_var2: (boxes?)):
      boxes(boxes?_var) = boxes(boxes?_var2) IMPLIES
       boxes?_var = boxes?_var2;

  OutBoxes_Output_eta: AXIOM
    FORALL (boxes?_var: (boxes?)): Output(boxes(boxes?_var)) = boxes?_var;

  OutBoxes_boxes_Output: AXIOM
    FORALL (Output1_var: Boxes(n)):
      boxes(Output(Output1_var)) = Output1_var;

  OutBoxes_inclusive: AXIOM
    FORALL (OutBoxes_var: OutBoxes):
      unknown_box?(OutBoxes_var) OR
       full_box?(OutBoxes_var) OR
        empty_box?(OutBoxes_var) OR boxes?(OutBoxes_var);

  OutBoxes_induction: AXIOM
    FORALL (p: [OutBoxes -> boolean]):
      (p(UnknownBox) AND
        p(FullBox) AND
         p(EmptyBox) AND
          (FORALL (Output1_var: Boxes(n)): p(Output(Output1_var))))
       IMPLIES (FORALL (OutBoxes_var: OutBoxes): p(OutBoxes_var));

  subterm(x: OutBoxes, y: OutBoxes):  boolean = x = y;

  <<:  (strict_well_founded?[OutBoxes]) = LAMBDA (x, y: OutBoxes): FALSE;

  OutBoxes_well_founded: AXIOM strict_well_founded?[OutBoxes](<<);

  reduce_nat(unknown_box?_fun: nat, full_box?_fun: nat,
             empty_box?_fun: nat, boxes?_fun: [Boxes(n) -> nat]):
        [OutBoxes -> nat] =
      LAMBDA (OutBoxes_adtvar: OutBoxes):
        LET red: [OutBoxes -> nat] =
              reduce_nat(unknown_box?_fun, full_box?_fun, empty_box?_fun,
                         boxes?_fun)
          IN
          CASES OutBoxes_adtvar
            OF UnknownBox: unknown_box?_fun,
               FullBox: full_box?_fun,
               EmptyBox: empty_box?_fun,
               Output(Output1_var): boxes?_fun(Output1_var)
            ENDCASES;

  REDUCE_nat(unknown_box?_fun: [OutBoxes -> nat],
             full_box?_fun: [OutBoxes -> nat],
             empty_box?_fun: [OutBoxes -> nat],
             boxes?_fun: [[Boxes(n), OutBoxes] -> nat]):
        [OutBoxes -> nat] =
      LAMBDA (OutBoxes_adtvar: OutBoxes):
        LET red: [OutBoxes -> nat] =
              REDUCE_nat(unknown_box?_fun, full_box?_fun, empty_box?_fun,
                         boxes?_fun)
          IN
          CASES OutBoxes_adtvar
            OF UnknownBox: unknown_box?_fun(OutBoxes_adtvar),
               FullBox: full_box?_fun(OutBoxes_adtvar),
               EmptyBox: empty_box?_fun(OutBoxes_adtvar),
               Output(Output1_var):
                 boxes?_fun(Output1_var, OutBoxes_adtvar)
            ENDCASES;

  reduce_ordinal(unknown_box?_fun: ordinal, full_box?_fun: ordinal,
                 empty_box?_fun: ordinal,
                 boxes?_fun: [Boxes(n) -> ordinal]):
        [OutBoxes -> ordinal] =
      LAMBDA (OutBoxes_adtvar: OutBoxes):
        LET red: [OutBoxes -> ordinal] =
              reduce_ordinal(unknown_box?_fun, full_box?_fun,
                             empty_box?_fun, boxes?_fun)
          IN
          CASES OutBoxes_adtvar
            OF UnknownBox: unknown_box?_fun,
               FullBox: full_box?_fun,
               EmptyBox: empty_box?_fun,
               Output(Output1_var): boxes?_fun(Output1_var)
            ENDCASES;

  REDUCE_ordinal(unknown_box?_fun: [OutBoxes -> ordinal],
                 full_box?_fun: [OutBoxes -> ordinal],
                 empty_box?_fun: [OutBoxes -> ordinal],
                 boxes?_fun: [[Boxes(n), OutBoxes] -> ordinal]):
        [OutBoxes -> ordinal] =
      LAMBDA (OutBoxes_adtvar: OutBoxes):
        LET red: [OutBoxes -> ordinal] =
              REDUCE_ordinal(unknown_box?_fun, full_box?_fun,
                             empty_box?_fun, boxes?_fun)
          IN
          CASES OutBoxes_adtvar
            OF UnknownBox: unknown_box?_fun(OutBoxes_adtvar),
               FullBox: full_box?_fun(OutBoxes_adtvar),
               EmptyBox: empty_box?_fun(OutBoxes_adtvar),
               Output(Output1_var):
                 boxes?_fun(Output1_var, OutBoxes_adtvar)
            ENDCASES;
END OutBoxes_adt

OutBoxes_adt_reduce[n: posnat, range: TYPE]: THEORY
BEGIN

  IMPORTING OutBoxes_adt[n]

  IMPORTING boxes_def

  reduce(unknown_box?_fun: range, full_box?_fun: range,
         empty_box?_fun: range, boxes?_fun: [Boxes(n) -> range]):
        [OutBoxes[n] -> range] =
      LAMBDA (OutBoxes_adtvar: OutBoxes[n]):
        LET red: [OutBoxes[n] -> range] =
              reduce(unknown_box?_fun, full_box?_fun, empty_box?_fun,
                     boxes?_fun)
          IN
          CASES OutBoxes_adtvar
            OF UnknownBox: unknown_box?_fun,
               FullBox: full_box?_fun,
               EmptyBox: empty_box?_fun,
               Output(Output1_var): boxes?_fun(Output1_var)
            ENDCASES;

  REDUCE(unknown_box?_fun: [OutBoxes[n] -> range],
         full_box?_fun: [OutBoxes[n] -> range],
         empty_box?_fun: [OutBoxes[n] -> range],
         boxes?_fun: [[Boxes(n), OutBoxes[n]] -> range]):
        [OutBoxes[n] -> range] =
      LAMBDA (OutBoxes_adtvar: OutBoxes[n]):
        LET red: [OutBoxes[n] -> range] =
              REDUCE(unknown_box?_fun, full_box?_fun, empty_box?_fun,
                     boxes?_fun)
          IN
          CASES OutBoxes_adtvar
            OF UnknownBox: unknown_box?_fun(OutBoxes_adtvar),
               FullBox: full_box?_fun(OutBoxes_adtvar),
               EmptyBox: empty_box?_fun(OutBoxes_adtvar),
               Output(Output1_var):
                 boxes?_fun(Output1_var, OutBoxes_adtvar)
            ENDCASES;
END OutBoxes_adt_reduce

quality63%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.