c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%read "../../logics/first-order/proof_theory/derived.elf".
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig BinRel = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder rel : i -> i -> o. %infix none 100 rel.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view OppRel : BinRel -> BinRel = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder rel := [x][y] y rel x.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct br : BinRel %open rel.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder refl : ded forall [x] x rel x.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view OppRefl : Refl -> Refl = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct br := OppRel br.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder refl := refl.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig Irrefl = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct br : BinRel %open rel.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder irrefl : ded forall [x] not x rel x.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view OppIrrefl : Irrefl -> Irrefl = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct br := OppRel br.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder irrefl := irrefl.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct br : BinRel %open rel.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder sym : ded forall [x] forall [y] x rel y imp y rel x.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view OppSym : Sym -> Sym = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct br := OppRel br.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder sym := forallI [x] forallI [y] impI [p] impE (forallE (forallE sym y) x) p.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig Antisym = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct br : BinRel %open rel.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder antisym : ded forall [x] forall [y] x rel y and y rel x imp x eq y.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view OppAntisym : Antisym -> Antisym = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct br := OppRel br.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder antisym := forallI [x] forallI [y] impI [p] sym (impE (forallE (forallE antisym y) x) p).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig Trans = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct br : BinRel %open rel.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder trans : ded forall [x] forall [y] forall [z] x rel y and y rel z imp x rel z.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view OppTrans : Trans -> Trans = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct br := OppRel br.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder trans := forallI [x] forallI [y] forallI [z] impI [p] impE
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder (forallE (forallE (forallE trans z) y) x) (andI (andEr p) (andEl p)).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig Serial = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct br : BinRel %open rel.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder serial : ded forall [x] exists [y] x rel y.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig TrichAx = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct br : BinRel %open rel.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder trich : ded forall [x] forall [y] x eq y or x rel y or y rel x.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig Total = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct r : Refl %open rel.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct ta : TrichAx = {%struct br := r.br.} %open trich.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig Trich = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct ir : Irrefl %open rel.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct as : Antisym = {%struct br := ir.br.} %open antisym.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct ta : TrichAx = {%struct br := ir.br.} %open trich.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig Preorder = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct r : Refl %open rel.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct t : Trans = {%struct br := r.br.} %open trans.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig PartialOrder = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct r : Refl %open rel.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct as : Antisym = {%struct br := r.br.} %open antisym.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct t : Trans = {%struct br := r.br.} %open trans.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view OppPartialOrder : PartialOrder -> PartialOrder = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct r := OppRefl r.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct as := OppAntisym as.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct t := OppTrans t.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view Preorder-Partial : Preorder -> PartialOrder = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct r := r.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct t := t.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig TotalOrder = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct po : PartialOrder %open rel.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct ta : TrichAx = {%struct br := po.r.br.} %open trich.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig StrictPartialOrder = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct ir : Irrefl %open rel.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct as : Antisym = {%struct br := ir.br.} %open antisym.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct t : Trans = {%struct br := ir.br.} %open trans.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view OppStrictPartialOrder : StrictPartialOrder -> StrictPartialOrder = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct ir := OppIrrefl ir.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct as := OppAntisym as.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct t := OppTrans t.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig StrictTotalOrder = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct spo : StrictPartialOrder %open rel.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct ta : TrichAx = {%struct br := spo.ir.br.} %open trich.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig EquivRel = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct r : Refl %open rel.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct s : Sym = {%struct br := r.br.} %open sym.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct t : Trans = {%struct br := r.br.} %open trans.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view Preorder-Equiv : Preorder -> EquivRel = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct r := r.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct t := t.