Quelle Unit_adt.pvs Sprache: PVS

%%% ADT file generated from Unit

Unit_adt: THEORY
BEGIN

  Unit: TYPE

  unit?: [Unit -> boolean]

  unit: (unit?)

  Unit_ord: [Unit -> upto(0)]

  Unit_ord_defaxiom: AXIOM Unit_ord(unit) = 0;

  ord(x: Unit): [Unit -> upto(0)] = CASES x OF unit: 0 ENDCASES

  Unit_inclusive: AXIOM FORALL (Unit_var: Unit): unit?(Unit_var);

  Unit_induction: AXIOM
    FORALL (p: [Unit -> boolean]):
      p(unit) IMPLIES (FORALL (Unit_var: Unit): p(Unit_var));

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

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

  Unit_well_founded: AXIOM strict_well_founded?[Unit](<<);
END Unit_adt

Unit_adt_reduce[range: TYPE]: THEORY
BEGIN

  IMPORTING Unit_adt

  reduce(unit?_fun: range):  [Unit -> range] =
      LAMBDA (Unit_adtvar: Unit):
        LET red: [Unit -> range] = reduce(unit?_fun) IN
          CASES Unit_adtvar OF unit: unit?_fun ENDCASES;

  REDUCE(unit?_fun: [Unit -> range]):  [Unit -> range] =
      LAMBDA (Unit_adtvar: Unit):
        LET red: [Unit -> range] = REDUCE(unit?_fun) IN
          CASES Unit_adtvar OF unit: unit?_fun(Unit_adtvar) ENDCASES;
END Unit_adt_reduce

quality65%

¤ 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.