#!python
module PRIORITY
{
  imports
  {
    pr(ENTITY)
    ex(OBSERVER2NUMBER)
  }
  signature
  {
    op priority : Entity -> Observer2Number
  }
}

#!python
module PRIOR
{
  imports
  {
    pr(INEQUALITY)
    pr(PRIORITY)
    ex(OBSERVER2RELATION/ENTITY)
  }
  signature
  {
    op prior : -> Observer2Relation/Entity
  }
  axioms
  {
    vars S : System
    vars X Y : Entity
--  (X prior(S) Y) = (priority(X)(S) > priority(Y)(S)) .
    eq deducible((X prior(S) Y) |- (priority(X)(S) > priority(Y)(S))) = true .
    eq deducible((priority(X)(S) > priority(Y)(S)) |- (X prior(S) Y)) = true .
  }
}

#!python
module CLAIM1/PRIOR
{
  imports
  {
    pr(LK)
    pr(PRIOR)
  }
  signature
  {
    op s : -> System
    ops x y z : -> Entity
    ops claim1 claim2 claim3 : -> Prop
  }
  axioms
  {
    eq claim1 = deducible((x prior(s) x) |- nil) . 
    eq claim2 = deducible((x prior(s) y),(y prior(s) x) |- nil) . 
    eq claim3 = deducible((x prior(s) y),(y prior(s) z) |- (x prior(s) z)) . 
  }
}

#!python
-- confirm irreflexivity
open CLAIM1/PRIOR .
ops i : -> Inference .
ops q1 q2 : -> Sequent .
eq q1 = ((priority(x)(s) > priority(x)(s)) |- nil) .
eq q2 = ((x prior(s) x) |- (priority(x)(s) > priority(x)(s))) .
eq antecedent(i) = (q1,q2) .
eq ((x prior(s) x) |- nil) = consequent(i) .
red claim1 .
close

-- confirm asymmetricity
open CLAIM1/PRIOR .
ops i : -> Inference .
ops q1 q2 q3 : -> Sequent .
eq q1 = ((priority(x)(s) > priority(y)(s)),(priority(y)(s) > priority(x)(s)) |- nil) .
eq q2 = ((x prior(s) y) |- (priority(x)(s) > priority(y)(s))) .
eq q3 = ((y prior(s) x) |- (priority(y)(s) > priority(x)(s))) .
eq antecedent(i) = (q1,q2,q3) .
eq ((x prior(s) y),(y prior(s) x) |- nil) = consequent(i) .
red claim2 .
close

-- confirm transitivity
open CLAIM1/PRIOR .
ops i1 i2 : -> Inference .
ops q1 q2 q3 q4 : -> Sequent .
eq q1 = ((priority(x)(s) > priority(y)(s)),(priority(y)(s) > priority(z)(s))
         |- (priority(x)(s) > priority(z)(s))) .
eq q2 = ((x prior(s) y) |- (priority(x)(s) > priority(y)(s))) .
eq q3 = ((y prior(s) z) |- (priority(y)(s) > priority(z)(s))) .
eq q4 = ((priority(x)(s) > priority(z)(s)) |- (x prior(s) z)) .
eq antecedent(i1) = (q1,q2,q3) .
trans ((x prior(s) y),(y prior(s) z) |- (priority(x)(s) > priority(z)(s))) => consequent(i1) .
trans consequent(i1) => ((x prior(s) y),(y prior(s) z) |- (priority(x)(s) > priority(z)(s))) .
eq antecedent(i2) = (consequent(i1),q4) .
eq ((x prior(s) y),(y prior(s) z) |- (x prior(s) z)) = consequent(i2) .
red claim3 .
close

#!python

#!python
make LEMMA5/COMPLEMENT/NUMBER
(
  LEMMA5/COMPLEMENT(
    NUMBER { sort Elt -> Number },
    RELATION/NUMBER { sort Relation -> Relation/Number },
    IRREFLEXIVE/NUMBER { sort Irreflexive -> Irreflexive/Number },
    ASYMMETRIC/NUMBER { sort Asymmetric -> Asymmetric/Number },
    TRANSITIVE/NUMBER { sort Transitive -> Transitive/Number },
    PARTIALORDER/NUMBER { sort PartialOrder -> PartialOrder/Number },
    TOTALORDER/NUMBER { sort TotalOrder -> TotalOrder/Number },
    COMPLEMENT/NUMBER
  )
)

#!python
module CLAIM2/PRIOR
{
  imports
  {
    pr(PRIOR)
    pr(LEMMA5/COMPLEMENT/NUMBER)
    pr(COMPLEMENT/ENTITY)
  }
  signature
  {
    op s : -> System
    ops x y z : -> Entity
    ops claim1 claim2 claim3 : -> Prop
  }
  axioms
  {
    eq claim1 = deducible((x [prior(s)] y),(y prior(s) z) |- (x prior(s) z)) .
    eq claim2 = deducible((x prior(s) y),(y [prior(s)] z) |- (x prior(s) z)) .
    eq claim3 = deducible((x [prior(s)] y),(y [prior(s)] z) |- (x [prior(s)] z)) .
  }
}

#!python
-- proof that the partialorder prior satisfies axioms of PartialOrder'
-- proof of claim1
open CLAIM2/PRIOR .
ops i1 : -> Inference .
ops q1 q2 q3 : -> Sequent .
eq q1 = (nil |- (priority(x)(s) [>] priority(y)(s)),(priority(y)(s) > priority(x)(s))) .
eq q2 = ((priority(y)(s) > priority(x)(s)) |- (y prior(s) x)) .
eq q3 = ((x [prior(s)] y),(y prior(s) x) |- nil) .
eq antecedent(i1) = (q1,q2,q3) .
trans ((x [prior(s)] y) |- (priority(x)(s) [>] priority(y)(s))) => consequent(i1) .
trans consequent(i1) => ((x [prior(s)] y) |- (priority(x)(s) [>] priority(y)(s))) .
ops i2 : -> Inference .
ops q4 q5 q6 : -> Sequent .
eq q4 = ((priority(x)(s) [>] priority(y)(s)),
         (priority(y)(s) > priority(z)(s))
         |- (priority(x)(s) > priority(z)(s))) .
eq q5 = ((y prior(s) z) |- (priority(y)(s) > priority(z)(s))) .
eq q6 = ((priority(x)(s) > priority(z)(s)) |- (x prior(s) z)) .
eq antecedent(i2) = (q4,q5,q6) .
trans ((priority(x)(s) [>] priority(y)(s)),(y prior(s) z) |- (x prior(s) z)) => consequent(i2) .
trans consequent(i2) => ((priority(x)(s) [>] priority(y)(s)),(y prior(s) z) |- (x prior(s) z)) .
ops i3 : -> Inference .
eq antecedent(i3) = (consequent(i1),consequent(i2)) .
eq ((x [prior(s)] y),(y prior(s) z) |- (x prior(s) z)) = consequent(i3) .
red claim1 .
close

-- proof of claim2
open CLAIM2/PRIOR .
ops i1 : -> Inference .
ops q1 q2 q3 : -> Sequent .
eq q1 = (nil |- (priority(y)(s) [>] priority(z)(s)),(priority(z)(s) > priority(y)(s))) .
eq q2 = ((priority(z)(s) > priority(y)(s)) |- (z prior(s) y)) .
eq q3 = ((y [prior(s)] z),(z prior(s) y) |- nil) .
eq antecedent(i1) = (q1,q2,q3) .
trans ((y [prior(s)] z) |- (priority(y)(s) [>] priority(z)(s))) => consequent(i1) .
trans consequent(i1) => ((y [prior(s)] z) |- (priority(y)(s) [>] priority(z)(s))) .
ops i2 : -> Inference .
ops q4 q5 q6 : -> Sequent .
eq q4 = ((priority(x)(s) > priority(y)(s)),
         (priority(y)(s) [>] priority(z)(s))
         |- (priority(x)(s) > priority(z)(s))) .
eq q5 = ((x prior(s) y) |- (priority(x)(s) > priority(y)(s))) .
eq q6 = ((priority(x)(s) > priority(z)(s)) |- (x prior(s) z)) .
eq antecedent(i2) = (q4,q5,q6) .
trans ((x prior(s) y),(priority(y)(s) [>] priority(z)(s)) |- (x prior(s) z)) => consequent(i2) .
trans consequent(i2) => ((x prior(s) y),(priority(y)(s) [>] priority(z)(s)) |- (x prior(s) z)) .
ops i3 : -> Inference .
eq antecedent(i3) = (consequent(i1),consequent(i2)) .
eq ((x prior(s) y),(y [prior(s)] z) |- (x prior(s) z)) = consequent(i3) .
red claim2 .
close

-- proof of claim3
open CLAIM2/PRIOR .
ops i1 : -> Inference .
ops q1 q2 q3 : -> Sequent .
eq q1 = (nil |- (priority(x)(s) [>] priority(y)(s)),(priority(y)(s) > priority(x)(s))) .
eq q2 = ((priority(y)(s) > priority(x)(s)) |- (y prior(s) x)) .
eq q3 = ((x [prior(s)] y),(y prior(s) x) |- nil) .
eq antecedent(i1) = (q1,q2,q3) .
trans ((x [prior(s)] y) |- (priority(x)(s) [>] priority(y)(s))) => consequent(i1) .
trans consequent(i1) => ((x [prior(s)] y) |- (priority(x)(s) [>] priority(y)(s))) .
ops i2 : -> Inference .
ops q4 q5 q6 : -> Sequent .
eq q4 = (nil |- (priority(y)(s) [>] priority(z)(s)),(priority(z)(s) > priority(y)(s))) .
eq q5 = ((priority(z)(s) > priority(y)(s)) |- (z prior(s) y)) .
eq q6 = ((y [prior(s)] z),(z prior(s) y) |- nil) .
eq antecedent(i2) = (q4,q5,q6) .
trans ((y [prior(s)] z) |- (priority(y)(s) [>] priority(z)(s))) => consequent(i2) .
trans consequent(i2) => ((y [prior(s)] z) |- (priority(y)(s) [>] priority(z)(s))) .
ops i3 : -> Inference .
ops q7 q8 q9 : -> Sequent .
eq q7 = ((priority(x)(s) [>] priority(z)(s)),(priority(z)(s) > priority(x)(s)) |- nil) .
eq q8 = ((z prior(s) x) |- (priority(z)(s) > priority(x)(s))) .
eq q9 = (nil |- (x [prior(s)] z),(z prior(s) x)) .
eq antecedent(i3) = (q7,q8,q9) .
trans ((priority(x)(s) [>] priority(z)(s)) |- (x [prior(s)] z)) => consequent(i3) .
trans consequent(i3) => ((priority(x)(s) [>] priority(z)(s)) |- (x [prior(s)] z)) .
ops i4 : -> Inference .
ops q10 : -> Sequent .
eq q10 = ((priority(x)(s) [>] priority(y)(s)),(priority(y)(s) [>] priority(z)(s)) |- (priority(x)(s) [>] priority(z)(s))) .
eq antecedent(i4) = (q10,consequent(i1),consequent(i2)) .
trans ((x [prior(s)] y),(y [prior(s)] z) |- (priority(x)(s) [>] priority(z)(s))) => consequent(i4) .
trans consequent(i4) => ((x [prior(s)] y),(y [prior(s)] z) |- (priority(x)(s) [>] priority(z)(s))) .
ops i5 : -> Inference .
eq antecedent(i5) = (consequent(i3),consequent(i4)) .
eq ((x [prior(s)] y),(y [prior(s)] z) |- (x [prior(s)] z)) = consequent(i5) .
red claim3 .
close

#!python

#!python
module PRIOR
{
  imports
  {
    pr(INEQUALITY)
    pr(PRIORITY)
    ex(OBSERVER2PARTIALORDER'/ENTITY)
  }
  signature
  {
    op prior : -> Observer2PartialOrder'/Entity
  }
  axioms
  {
    vars S : System
    vars X Y : Entity
--  (X prior(S) Y) = (priority(X)(S) > priority(Y)(S)) .
    eq deducible((X prior(S) Y) |- (priority(X)(S) > priority(Y)(S))) = true .
    eq deducible((priority(X)(S) > priority(Y)(S)) |- (X prior(S) Y)) = true .
  }
}

#!python
module ENTRY
{
  imports
  {
    pr(OBSERVER2LIST/ENTITY)
  }
  signature
  {
    op entry : -> Observer2List/Entity
  }
}

#!python
module AHEAD
{
  imports
  {
    pr(FORMER/ENTITY)
    pr(ENTRY)
    ex(OBSERVER2RELATION/ENTITY)
  }
  signature
  {
    op ahead : -> Observer2Relation/Entity
  }
  axioms
  {
    vars S : System
    vars X Y : Entity
    eq (X ahead(S) Y) = (X former(entry(S)) Y) .
  }
}

#!python
open AHEAD .
ops s : -> System .
ops x y z : -> Entity .
red deducible((x ahead(s) x) |- nil) .
red deducible((x ahead(s) y),(y ahead(s) x) |- nil) .
red deducible((x ahead(s) y),(y ahead(s) z) |- (x ahead(s) z)) .
close

#!python
module AHEAD
{
  imports
  {
    pr(FORMER/ENTITY)
    pr(ENTRY)
    ex(OBSERVER2PARTIALORDER/ENTITY)
  }
  signature
  {
    op ahead : -> Observer2PartialOrder/Entity
  }
  axioms
  {
    vars S : System
    vars X Y : Entity
--  (X ahead(S) Y) = (X former(entry(S)) Y) .
    eq deducible((X former(entry(S)) Y) |- (X ahead(S) Y)) = true .
    eq deducible((X ahead(S) Y) |- (X former(entry(S)) Y)) = true .
    eq deducible((X @ entry(S)),(Y @ entry(S)) |- (X ahead(S) Y),(X = Y),(Y ahead(S) X)) = true .
    eq deducible((X ahead(S) Y) |- (X @ entry(S))) = true .
    eq deducible((X ahead(S) Y) |- (Y @ entry(S))) = true .
  }
}

#!python
module PRECEDE
{
  imports
  {
    pr(PRIOR)
    pr(AHEAD)
    pr(OVERRIDE/ENTITY)
  }
  signature
  {
    op precede : -> Observer2PartialOrder/Entity
  }
  axioms
  {
    vars S : System
    vars X Y : Entity
    eq precede(S) = [prior(S);ahead(S)] .
  }
}

#!python
module NEXT
{
  imports
  {
    pr(ROOT/ENTITY)
    pr(PRECEDE)
    ex(RUNNABLE)
  }
  signature
  {
    op next : -> Observer2Set/Entity
  }
  axioms
  {
    vars S : System
    vars X : Entity
    eq next(S) = root(runnable(S),precede(S)) .
  }
}

#!python
module CURRENT
{
  imports
  {
    ex(OBSERVER2SET/ENTITY)
  }
  signature
  {
    op current : -> Observer2Set/Entity
  }
}

#!python
module BLOCK
{
  imports
  {
    ex(OBSERVER2RELATION/ENTITY)
  }
  signature
  {
    op block : -> Observer2Relation/Entity
  }
}

#!python
module BASESTATE
{
  imports
  {
    pr(ASSIGN)
    pr(CURRENT)
    pr(PRECEDE)
    pr(BLOCK)
  }
}

#!python
module CLAIM1/BASESTATE
{
  imports
  {
    pr(BASESTATE)
    pr(LK)
  }
  signature
  {
    op s : -> System
    ops x y : -> Entity
    op claim : -> Prop
  }
  axioms
  {
    vars X Y : Entity
    eq deducible((X block(s) X) |- nil) = true .
    eq deducible((X block(s) Y),(X ahead(s) Y) |- (priority(Y)(s) = assign(Y))) = true .
    eq deducible((X block(s) Y),(Y ahead(s) X) |- (X [prior(s);ahead(s)] Y)) = true .
    eq deducible((X block(s) Y),(assign(Y) > priority(X)(s)) |- nil) = true .
    eq claim = deducible((x @ entry(s)),(y @ entry(s)),(x block(s) y) |- (x precede(s) y)) .
  }
}

#!python
open CLAIM1/BASESTATE .
ops i1 : -> Inference .
ops q11 q12 q13 : -> Sequent .
eq q11 = ((x block(s) y),(assign(y) > priority(x)(s)) |- nil) .
eq q12 = ((priority(y)(s) = assign(y)),(priority(y)(s) > priority(x)(s)) |- (assign(y) > priority(x)(s))) .
eq q13 = ((y prior(s) x) |- (priority(y)(s) > priority(x)(s))) .
eq antecedent(i1) = (q11,q12,q13) .
trans ((x block(s) y),(priority(y)(s) = assign(y)),(y prior(s) x) |- nil) => consequent(i1) .
trans consequent(i1) => ((x block(s) y),(priority(y)(s) = assign(y)),(y prior(s) x) |- nil) .
ops i2 : -> Inference .
ops q21 : -> Sequent .
eq q21 = ((x block(s) y),(x ahead(s) y) |- (priority(y)(s) = assign(y))) .
eq antecedent(i2) = (consequent(i1),q21) .
trans ((x block(s) y),(x ahead(s) y),(y prior(s) x) |- nil) => consequent(i2) .
trans consequent(i2) => ((x block(s) y),(x ahead(s) y),(y prior(s) x) |- nil) .
ops i3 : -> Inference .
ops q31 q32 : -> Sequent .
eq q31 = ((x ahead(s) y),(x [prior(s)] y) |- (x precede(s) y)) .
eq q32 = (nil |- (x [prior(s)] y),(y prior(s) x)) .
eq antecedent(i3) = (consequent(i2),q31,q32) .
trans ((x block(s) y),(x ahead(s) y) |- (x [prior(s);ahead(s)] y)) => consequent(i3) .
trans consequent(i3) => ((x block(s) y),(x ahead(s) y) |- (x [prior(s);ahead(s)] y)) .
ops i4 : -> Inference .
ops q41 q42 : -> Sequent .
eq q41 = ((x block(s) x) |- nil) .
eq q42 = ((x = y),(x block(s) y) |- (x block(s) x)) .
eq antecedent(i4) = (q41,q42) .
trans ((x = y),(x block(s) y) |- nil) => consequent(i4) .
trans consequent(i4) => ((x = y),(x block(s) y) |- nil) .
ops i5 : -> Inference .
ops q51 : -> Sequent .
eq q51 = ((x @ entry(s)),(y @ entry(s)) |- (x ahead(s) y),(x = y),(y ahead(s) x)) .
eq antecedent(i5) = (consequent(i4),q51) .
trans ((x @ entry(s)),(y @ entry(s)),(x block(s) y) |- (x ahead(s) y),(y ahead(s) x)) => consequent(i5) .
trans consequent(i5) => ((x @ entry(s)),(y @ entry(s)),(x block(s) y) |- (x ahead(s) y),(y ahead(s) x)) .
ops i6 : -> Inference .
ops q61 : -> Sequent .
eq q61 = ((x block(s) y),(y ahead(s) x) |- (x [prior(s);ahead(s)] y)) .
eq antecedent(i6) = (consequent(i3),consequent(i5),q61) .
eq ((x @ entry(s)),(y @ entry(s)),(x block(s) y) |- (x [prior(s);ahead(s)] y)) = consequent(i6) .
red claim .
close

#!python
module THEOREM1/BASESTATE
{
  imports
  {
    pr(BASESTATE)
    pr(LK)
  }
  axioms
  {
    vars S : System
    vars X Y : Entity
    cq deducible((X @ entry(S)),(Y @ entry(S)),(X block(S) Y) |- (X [prior(S);ahead(S)] Y)) = true
       if  (deducible((X block(S) X) |- nil) = true)
       and (deducible((X block(S) Y),(X ahead(S) Y) |- (priority(Y)(S) = assign(Y))) = true)
       and (deducible((X block(S) Y),(Y ahead(S) X) |- (X [prior(S);ahead(S)] Y)) = true)
       and (deducible((X block(S) Y),(assign(Y) > priority(X)(S)) |- nil) = true) .
  }
}