=========================================================================
Theory CPO

Definitions --
  REFL  |- !r. REFL r = (!x. r x x)
  TRANS  |- !r. TRANS r = (!x y z. r x y /\ r y z ==> r x z)
  ANTISYM  |- !r. ANTISYM r = (!x y. r x y /\ r y x ==> (x = y))
  PO  |- !r. PO r = REFL r /\ TRANS r /\ ANTISYM r
  IS_UB  |- !r X b. IS_UB r X b = (!a. a IN X ==> r a b)
  IS_LB  |- !r X a. IS_LB r X a = (!b. b IN X ==> r a b)
  isCUP
    |- !r X b. isCUP r X b = IS_UB r X b /\ (!c. IS_UB r X c ==> r b c)
  isCAP
    |- !r X c. isCAP r X c = IS_LB r X c /\ (!b. IS_LB r X b ==> r b c)
  CUP  |- !r X. (?a. isCUP r X a) ==> isCUP r X(CUP r X)
  CAP  |- !r X. (?a. isCAP r X a) ==> isCAP r X(CAP r X)
  Cup  |- !r a b. Cup r a b = CUP r{a,b}
  Cap  |- !r a b. Cap r a b = CAP r{a,b}
  Bot  |- !r. Bot r = CUP r{}
  Top  |- !r. Top r = CAP r{}
  Directed
    |- !r X.
        Directed r X = (!a b. a IN X /\ b IN X ==> (?c. isCUP r{a,b}c))
  CPO
    |- !r.
        CPO r =
        PO r /\
        (?a. isCUP r{}a) /\
        (!X. Directed r X ==> (?a. isCUP r X a))
  isLFP
    |- !r fun x.
        isLFP r fun x = (fun x = x) /\ (!y. (fun y = y) ==> r x y)
  LFP  |- !r f. (?x. isLFP r f x) ==> isLFP r f(LFP r f)
  ITER
    |- (!f x. ITER 0 f x = x) /\
       (!n f x. ITER(SUC n)f x = f(ITER n f x))
  Mono  |- !r s f. Mono r s f = (!x y. r x y ==> s(f x)(f y))
  Cont
    |- !r s f.
        Cont r s f =
        (!X.
          ~(X = {}) /\ Directed r X ==>
          Directed s(IMAGE f X) /\ (f(CUP r X) = CUP s(IMAGE f X)))
  
Theorems --
  Low_EXTENSION
    |- !r x y. REFL r /\ ANTISYM r ==> ((x = y) = (!z. r z x = r z y))
  High_EXTENSION
    |- !r x y. REFL r /\ ANTISYM r ==> ((x = y) = (!z. r x z = r y z))
  Bot_THM  |- !a. isCUP r{}a ==> (!x. r(Bot r)x)
  Top_THM  |- !a. isCAP r{}a ==> (!x. r x(Top r))
  UNIQUE_CUP
    |- !r X x y. ANTISYM r /\ isCUP r X x /\ isCUP r X y ==> (y = x)
  UNIQUE_CAP
    |- !r X x y. ANTISYM r /\ isCAP r X x /\ isCAP r X y ==> (y = x)
  isCUP_CUP  |- !r X a. ANTISYM r /\ isCUP r X a ==> (CUP r X = a)
  isCAP_CAP  |- !r X a. ANTISYM r /\ isCAP r X a ==> (CAP r X = a)
  CUP_greater  |- !r X a x. isCUP r X a /\ x IN X ==> r x(CUP r X)
  CUP_less
    |- !r X a x. PO r /\ isCUP r X a ==> (IS_UB r X x = r(CUP r X)x)
  CAP_less  |- !r X a x. isCAP r X a /\ x IN X ==> r(CAP r X)x
  CAP_greater
    |- !r X a x. PO r /\ isCAP r X a ==> (IS_LB r X x = r x(CAP r X))
  isCUP_ORDER  |- !r a b. REFL r ==> (r a b = isCUP r{a,b}b)
  isCAP_ORDER  |- !r a b. REFL r ==> (r a b = isCAP r{a,b}a)
  CUP_SINGLETON  |- !r a. REFL r ==> isCUP r{a}a
  CAP_SINGLETON  |- !r a. REFL r ==> isCAP r{a}a
  EMPTY_Directed  |- !r. Directed r{}
  CPO_Bot  |- !r x. CPO r ==> r(Bot r)x
  CPO_CUP  |- !r X. CPO r /\ Directed r X ==> isCUP r X(CUP r X)
  UNIQUE_LFP
    |- !r f x y. ANTISYM r /\ isLFP r f x /\ isLFP r f y ==> (x = y)
  Mono_o  |- !r s t f g. Mono r s f /\ Mono s t g ==> Mono r t(g o f)
  Cont_o  |- !r s t f g. Cont r s f /\ Cont s t g ==> Cont r t(g o f)
  Cont_IMP_Mono  |- !r s f. CPO r /\ CPO s /\ Cont r s f ==> Mono r s f
  TARSKI_CPO
    |- !r f.
        CPO r /\ Cont r r f ==>
        isLFP r f(CUP r{x | ?n. x = ITER n f(Bot r)})


=========================================================================
Theory Cla

Definitions --
  CLa
    |- !r.
        CLa r =
        (!X. ~(X = {}) ==> (?a. isCUP r X a) /\ (?b. isCAP r X b))
  DLa  |- !r. DLa r = (!X. (?a. isCUP r X a) /\ (?b. isCAP r X b))
  CUP_Distr
    |- !r s f. CUP_Distr r s f = (!X. f(CUP r X) = CUP s(IMAGE f X))
  CAP_Distr
    |- !r s f. CAP_Distr r s f = (!X. f(CAP r X) = CAP s(IMAGE f X))
  CUP_Junct
    |- !r s f.
        CUP_Junct r s f =
        (!X. ~(X = {}) ==> (f(CUP r X) = CUP s(IMAGE f X)))
  CAP_Junct
    |- !r s f.
        CAP_Junct r s f =
        (!X. ~(X = {}) ==> (f(CAP r X) = CAP s(IMAGE f X)))
  
Theorems --
  DLa_IMP_CLa  |- !r. DLa r ==> CLa r
  CLa_CUP  |- !r X. CLa r /\ ~(X = {}) ==> isCUP r X(CUP r X)
  CLa_CAP  |- !r X. CLa r /\ ~(X = {}) ==> isCAP r X(CAP r X)
  DLa_Bot_THM  |- !r x. DLa r ==> r(Bot r)x
  DLa_Top_THM  |- !r x. DLa r ==> r x(Top r)
  CLa_CUP_less
    |- !r X x.
        CLa r /\ PO r /\ ~(X = {}) ==> (IS_UB r X x = r(CUP r X)x)
  DLa_CUP_less  |- !r X x. DLa r /\ PO r ==> (IS_UB r X x = r(CUP r X)x)
  CLa_CUP_greater  |- !r X x. CLa r /\ x IN X ==> r x(CUP r X)
  CLa_CAP_greater
    |- !r X x.
        CLa r /\ PO r /\ ~(X = {}) ==> (IS_LB r X x = r x(CAP r X))
  DLa_CAP_greater
    |- !r X x. DLa r /\ PO r ==> (IS_LB r X x = r x(CAP r X))
  CLa_CAP_less  |- !r X x. CLa r /\ x IN X ==> r(CAP r X)x
  CLa_IMP_CPO  |- !r. PO r /\ CLa r /\ (?a. isCUP r{}a) ==> CPO r
  CUP_Distr_IMP_Junct  |- !r s f. CUP_Distr r s f ==> CUP_Junct r s f
  CAP_Distr_IMP_Junct  |- !r s f. CAP_Distr r s f ==> CAP_Junct r s f
  CUP_Distr_Bot  |- !r s f. CUP_Distr r s f ==> (f(Bot r) = Bot s)
  CAP_Distr_Top  |- !r s f. CAP_Distr r s f ==> (f(Top r) = Top s)
  CUP_Junct_IMP_Cont  |- !r s f. CLa s /\ CUP_Junct r s f ==> Cont r s f
  TARSKI_MONO_isLFP
    |- !r f.
        DLa r /\ PO r /\ Mono r r f ==> isLFP r f(CAP r{x | r(f x)x})
  TARSKI_MONO_LFP
    |- !r f.
        DLa r /\ PO r /\ Mono r r f ==> (LFP r f = CAP r{x | r(f x)x})
  TARSKI_MONO_equ
    |- !r f. DLa r /\ PO r /\ Mono r r f ==> (f(LFP r f) = LFP r f)
  TARSKI_MONO_less
    |- !r f x. DLa r /\ PO r /\ Mono r r f /\ r(f x)x ==> r(LFP r f)x
  ROLING_THM
    |- !r s f g.
        DLa r /\ PO r /\ Mono r s f /\ DLa s /\ PO s /\ Mono s r g ==>
        (f(LFP r(g o f)) = LFP s(f o g))
  FP_lower_FUSION
    |- !r s f g h.
        DLa r /\
        PO r /\
        Mono r r g /\
        DLa s /\
        PO s /\
        Mono s s h /\
        (!x. s((h o f)x)((f o g)x)) ==>
        s(LFP s h)(f(LFP r g))

=========================================================================
Theory galois

Definitions --
  GalCon  |- !r s f g. GalCon r s f g = (!a b. r(f a)b = s a(g b))     
Theorems --
  GC_lower_CANCEL
    |- !r s f g a. PO s /\ GalCon r s f g ==> r((f o g)a)a
  GC_upper_CANCEL
    |- !r s f g a. PO r /\ GalCon r s f g ==> s a((g o f)a)
  GC_DISTR_CUP
    |- !r s f g.
        DLa r /\ DLa s /\ PO r /\ PO s /\ GalCon r s f g ==>
        CUP_Distr s r f
  GC_DISTR_CAP
    |- !r s f g.
        DLa r /\ DLa s /\ PO r /\ PO s /\ GalCon r s f g ==>
        CAP_Distr r s g
  FP_upper_FUSION
    |- !r s f g h.
        DLa r /\
        PO r /\
        Mono r r g /\
        DLa s /\
        PO s /\
        Mono s s h /\
        (?fu. GalCon s r f fu) /\
        (!x. s((f o g)x)((h o f)x)) ==>
        s(f(LFP r g))(LFP s h)
  FP_FUSION
    |- !r s f g h.
        DLa r /\
        PO r /\
        Mono r r g /\
        DLa s /\
        PO s /\
        Mono s s h /\
        (?fu. GalCon s r f fu) /\
        (f o g = h o f) ==>
        (f(LFP r g) = LFP s h)
==============================================================================