order.elf revision c6506aa7090643badb5a6dca5df0ca6617558f5e
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%read "../../logics/first-order/proof_theory/derived.elf".
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig OrderInf = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct ord : PartialOrder %open rel %as leq.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder inf : i -> i -> i.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder is_infimum_of : i -> i -> i -> o = [x][y][i] ((i leq x) and (i leq y)) and forall ([z] ((z leq x and z leq y) => z leq i)).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ax_inf : ded forall [x] forall [y] is_infimum_of x y (inf x y).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig OrderSup = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct ord : PartialOrder %open rel %as leq.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder sup: i -> i -> i.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder is_supremum_of: i -> i -> i -> o = [x][y][s] ((x leq s ) and (y leq s)) and forall ( [z] ((x leq z and y leq z) => s leq z)).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ax_sup: ded forall [x] forall [y] is_supremum_of x y (sup x y).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view OppInf : OrderInf -> OrderSup = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct ord := OppPartialOrder ord.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ax_inf := ax_sup.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view OppSup : OrderSup -> OrderInf = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct ord := OppPartialOrder ord.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ax_sup := ax_inf.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig OrderTop = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct ord : PartialOrder %open rel %as leq.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ax_top : ded forall [x] x leq top.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig OrderBot = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct ord : PartialOrder %open rel %as leq.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ax_bot : ded forall [x] bot leq x.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view OppTop : OrderTop -> OrderBot = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct ord := OppPartialOrder ord.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ax_top := ax_bot.