|
%%% 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
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
¤
|
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.
|
