order.elf revision 239352d9aec4bc3823511873533fa812cbe259c7
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova%read "../../logics/first-order/proof_theory/derived.elf".
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova%sig OrderInf = {
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova %include FOLEQPFExt %open.
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova %struct ord : PartialOrder %open rel %as leq.
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova inf : i -> i -> i.
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova 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)).
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova ax_inf : ded forall [x] forall [y] is_infimum_of x y (inf x y).
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova%sig OrderSup = {
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova %include FOLEQPFExt %open.
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova %struct ord : PartialOrder %open rel %as leq.
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova sup: i -> i -> i.
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova 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)).
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova ax_sup: ded forall [x] forall [y] is_supremum_of x y (sup x y).
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova%view OppInf : OrderInf -> OrderSup = {
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova %struct ord := OppPartialOrder ord.
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova ax_inf := ax_sup.
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova%view OppSup : OrderSup -> OrderInf = {
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova %struct ord := OppPartialOrder ord.
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova ax_sup := ax_inf.
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova%sig OrderTop = {
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova %include FOLEQPFExt %open.
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova %struct ord : PartialOrder %open rel %as leq.
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova ax_top : ded forall [x] x leq top.
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova%sig OrderBot = {
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova %include FOLEQPFExt %open.
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova %struct ord : PartialOrder %open rel %as leq.
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova ax_bot : ded forall [x] bot leq x.
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova%view OppTop : OrderTop -> OrderBot = {
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova %struct ord := OppPartialOrder ord.
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova ax_top := ax_bot.