## The Base Structure for Deadlock Free Task Scheduling in the OSEK OS ##

The followings are 
transitions which preserve values specified observers return.

### ΞCURRENT ###
Transitions which preserve a value the observer current returns.
```
#!python
module ΞCURRENT
{
  imports
  {
    ex(TRANSITION)
    pr(CURRENT)
    pr(DEDUCIBLE)
  }
  signature
  {
    [ Ξcurrent < Transition ]
  }
  axioms
  {
    vars S : System
    vars F : Ξcurrent
    vars X : Entity
    crl current(F(S)) => current(S)
        if complete(F(S)) .
--  current(F(S)) = current(S)
--  current(S) ⊆ current(F(S))
    cq deducible((X @ current(S)) |- (X @ current(F(S)))) = true
       if complete(F(S)) .
--  current(F(S)) ⊆ current(S)
    cq deducible((X @ current(F(S))) |- (X @ current(S))) = true
       if complete(F(S)) .
  }
}
```
### ΞENTRY ###
Transitions which preserve values the observers entry and runnable return.
```
#!python
module ΞENTRY
{
  imports
  {
    ex(TRANSITION)
    pr(RUNNABLE)
    pr(ENTRY)
    pr(DEDUCIBLE)
  }
  signature
  {
    [ Ξentry < Transition ]
  }
  axioms
  {
    vars S : System
    vars F : Ξentry
    vars X : Entity
    crl runnable(F(S)) => runnable(S)
        if complete(F(S)) .
--  runnable(F(S)) = runnable(S)
--  runnable(S) ⊆ runnable(F(S))
    cq deducible((X @ runnable(S)) |- (X @ runnable(F(S)))) = true
       if complete(F(S)) .
--  runnable(F(S)) ⊆ runnable(S)
    cq deducible((X @ runnable(F(S))) |- (X @ runnable(S))) = true
       if complete(F(S)) .
    crl entry(F(S)) => entry(S)
        if complete(F(S)) .
--  entry(F(S)) = entry(S)
--  entry(S) ⊆ entry(F(S))
    cq deducible((X ? entry(S)) |- (X ? entry(F(S)))) = true
        if complete(F(S)) .
--  entry(F(S)) ⊆ entry(S)
    cq deducible((X ? entry(F(S))) |- (X ? entry(S))) = true
       if complete(F(S)) .
  }
}
```

Transitions included in Ξentry 
preserve also a value returned by the observer ahead
```
#!python
open AHEAD + ΞENTRY + LK .
ops s : -> System .
ops f : -> Ξentry .
ops x y : -> Entity .
ops claim : -> Prop .
eq complete(f(s)) = true .
eq claim = deducible((x ahead(f(s)) y) |- (x ahead(s) y)) .
ops i : -> Inference .
ops q1 q2 : -> Sequent .
eq q1 = ((x ahead(f(s)) y) |- (x former(entry(f(s))) y)) .
eq q2 = ((x former(entry(s)) y) |- (x ahead(s) y)) .
eq antecedent(i) = (q1,q2) .
eq ((x ahead(f(s)) y) |- (x ahead(s) y)) = consequent(i) .
red claim .
close
```
```
#!python
%ΞENTRY + LK + AHEAD> *
-- reduce in %ΞENTRY + LK + AHEAD : (claim):Prop

** Found [state 62] (consequent(i)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 205 rewrites(0.110 sec), 3433 matches, 49 memo hits)
```
```
#!python
open AHEAD + ΞENTRY + LK .
ops s : -> System .
ops f : -> Ξentry .
ops x y : -> Entity .
ops claim : -> Prop .
eq complete(f(s)) = true .
eq claim = deducible((x ahead(s) y) |- (x ahead(f(s)) y)) .
ops i : -> Inference .
ops q1 q2 : -> Sequent .
eq q1 = ((x ahead(s) y) |- (x former(entry(s)) y)) .
eq q2 = ((x former(entry(f(s))) y) |- (x ahead(f(s)) y)) .
eq antecedent(i) = (q1,q2) .
eq ((x ahead(s) y) |- (x ahead(f(s)) y)) = consequent(i) .
red claim .
close
```
```
#!python
%ΞENTRY + LK + AHEAD> *
-- reduce in %ΞENTRY + LK + AHEAD : (claim):Prop

** Found [state 75] (consequent(i)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 215 rewrites(0.130 sec), 3669 matches, 49 memo hits)
```

### ΞENTRY (redefined) ###
We would be able to add some axioms to the module ΞENTRY.
```
#!python
module ΞENTRY
{
  imports
  {
    ex(TRANSITION)
    pr(RUNNABLE)
    pr(ENTRY)
    pr(AHEAD)
    pr(DEDUCIBLE)
  }
  signature
  {
    [ Ξentry < Transition ]
  }
  axioms
  {
    vars S : System
    vars F : Ξentry
    vars X Y : Entity
    crl runnable(F(S)) => runnable(S)
        if complete(F(S)) .
--  runnable(F(S)) = runnable(S)
--  runnable(S) ⊆ runnable(F(S))
    cq deducible((X @ runnable(S)) |- (X @ runnable(F(S)))) = true
       if complete(F(S)) .
--  runnable(F(S)) ⊆ runnable(S)
    cq deducible((X @ runnable(F(S))) |- (X @ runnable(S))) = true
       if complete(F(S)) .
    crl entry(F(S)) => entry(S)
        if complete(F(S)) .
--  entry(F(S)) = entry(S)
--  entry(S) ⊆ entry(F(S))
    cq deducible((X ? entry(S)) |- (X ? entry(F(S)))) = true
        if complete(F(S)) .
--  entry(F(S)) ⊆ entry(S)
    cq deducible((X ? entry(F(S))) |- (X ? entry(S))) = true
       if complete(F(S)) .
--  added axioms
--  X ahead(S) Y ⇔ X ahead(F(S)) Y
--  X ahead(F(S)) Y ⇒ X ahead(S) Y
    cq deducible((X ahead(F(S)) Y) |- (X ahead(S) Y)) = true
       if complete(F(S)) .
--  X ahead(S) Y ⇒ X ahead(F(S)) Y
    cq deducible((X ahead(S) Y) |- (X ahead(F(S)) Y)) = true
       if complete(F(S)) .
--  cq ahead(F(S)) = ahead(S)
--     if complete(F(S)) .
  }
}
```

### ΞEXECUTED ###
Transitions which preserve a value the observer executed returns.
```
#!python
module ΞEXECUTED
{
  imports
  {
    ex(TRANSITION)
    pr(EXECUTED)
    pr(DEDUCIBLE)
  }
  signature
  {
    [ Ξexecuted < Transition ]
  }
  axioms
  {
    vars S : System
    vars F : Ξexecuted
    vars X : Entity
    crl executed(F(S)) => executed(S)
        if complete(F(S)) .
--  executed(F(S)) = executed(S)
--  executed(S) ⊆ executed(F(S))
    cq deducible((X @ executed(S)) |- (X @ executed(F(S)))) = true
       if complete(F(S)) .
--  executed(F(S)) ⊆ executed(S)
    cq deducible((X @ executed(F(S))) |- (X @ executed(S))) = true
       if complete(F(S)) .
  }
}
```
### ΞPRIORITY ###
Transitions which preserve a value the observer priority returns.
```
#!python
module ΞPRIORITY
{
  imports
  {
    ex(TRANSITION)
    pr(PRIORITY)
    pr(DEDUCIBLE)
  }
  signature
  {
    [ Ξpriority < Transition ]
  }
  axioms
  {
    vars S : System
    vars F : Ξpriority
    vars X : Entity
    crl priority(X)(F(S)) => priority(X)(S)
        if complete(F(S)) .
--  priority(X)(S) = priority(X)(F(S))
    cq deducible(nil |- (priority(X)(S) = priority(X)(F(S)))) = true
       if complete(F(S)) .
  }
}
```
Transitions contained in Ξpriority also preserve 
a value returen by the observer prior.
```
#!python
open PRIOR + ΞPRIORITY + LK .
ops s : -> System .
ops f : -> Ξpriority .
ops x y : -> Entity .
ops claim : -> Prop .
eq complete(f(s)) = true .
eq claim = deducible((x prior(f(s)) y) |- (x prior(s) y)) .
ops i : -> Inference .
ops q1 q2 : -> Sequent .
eq q1 = ((x prior(f(s)) y) |- (priority(x)(f(s)) > priority(y)(f(s)))) .
eq q2 = ((priority(x)(s) > priority(y)(s)) |- (x prior(s) y)) .
eq antecedent(i) = (q1,q2) .
eq ((x prior(f(s)) y) |- (x prior(s) y)) = consequent(i) .
red claim .
close
```
```
#!python
%ΞPRIORITY + PRIOR + LK> *
-- reduce in %ΞPRIORITY + PRIOR + LK : (claim):Prop

** Found [state 330] (consequent(i)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 1459 rewrites(0.570 sec), 22777 matches, 471 memo hits)
```

```
#!python
open PRIOR + ΞPRIORITY + LK .
ops s : -> System .
ops f : -> Ξpriority .
ops x y : -> Entity .
ops claim : -> Prop .
eq complete(f(s)) = true .
eq claim = deducible((x prior(s) y) |- (x prior(f(s)) y)) .
ops i : -> Inference .
ops q1 q2 : -> Sequent .
eq q1 = ((x prior(s) y) |- (priority(x)(s) > priority(y)(s))) .
eq q2 = ((priority(x)(f(s)) > priority(y)(f(s))) |- (x prior(f(s)) y)) .
eq antecedent(i) = (q1,q2) .
eq ((x prior(s) y) |- (x prior(f(s)) y)) = consequent(i) .
red claim .
close
```
```
#!python
%ΞPRIORITY + PRIOR + LK> *
-- reduce in %ΞPRIORITY + PRIOR + LK : (claim):Prop

** Found [state 386] (consequent(i)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 1545 rewrites(0.630 sec), 23663 matches, 471 memo hits)
```
### ΞPRIORITY (redefined) ###
We would be able to add some axioms proved in the above to ΞPRIORITY.
```
#!python
module ΞPRIORITY
{
  imports
  {
    ex(TRANSITION)
    pr(PRIOR)
    pr(DEDUCIBLE)
  }
  signature
  {
    [ Ξpriority < Transition ]
  }
  axioms
  {
    vars S : System
    vars F : Ξpriority
    vars X Y : Entity
    crl priority(X)(F(S)) => priority(X)(S)
        if complete(F(S)) .
--  priority(X)(S) = priority(X)(F(S))
    cq deducible(nil |- (priority(X)(S) = priority(X)(F(S)))) = true
       if complete(F(S)) .
--  added axioms
--  X prior(S) Y ⇔ X prior(F(S)) Y
--  X prior(F(S)) Y ⇒ X prior(S) Y
    cq deducible((X prior(F(S)) Y) |- (X prior(S) Y)) = true
       if complete(F(S)) .
--  X prior(S) Y ⇒ X prior(F(S)) Y
    cq deducible((X prior(S) Y) |- (X prior(F(S)) Y)) = true
       if complete(F(S)) .
--  cq prior(F(S)) = prior(S)
--     if complete(F(S)) .
  }
}
```
We would be able to verify that 
any transition contained in Ξpriority 
also preserves the value x [prior(s)] y 
for any x and y : Entity.
```
#!python
open ΞPRIORITY + LK .
ops s : -> System .
ops f : -> Ξpriority .
ops x y : -> Entity .
eq complete(f(s)) = true .
ops claim : -> Prop .
eq claim = deducible((x [prior(f(s))] y) |- (x [prior(s)] y)) .
ops i : -> Inference .
ops q1 q2 q3 : -> Sequent .
eq q1 = ((y prior(f(s)) x),(x [prior(f(s))] y) |- nil) .
eq q2 = ((y prior(s) x) |- (y prior(f(s)) x)) .
eq q3 = (nil |- (x [prior(s)] y),(y prior(s) x)) .
eq antecedent(i) = (q1,q2,q3) .
eq ((x [prior(f(s))] y) |- (x [prior(s)] y)) = consequent(i) .
red claim .
close
```
```
#!python
%ΞPRIORITY + LK> *
-- reduce in %ΞPRIORITY + PRIOR + LK : (claim):Prop

** Found [state 159] (consequent(i)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 446 rewrites(0.520 sec), 15074 matches, 184 memo hits)
```
```
#!python
open ΞPRIORITY + LK .
ops s : -> System .
ops f : -> Ξpriority .
ops x y : -> Entity .
eq complete(f(s)) = true .
ops claim : -> Prop .
eq claim = deducible((x [prior(s)] y) |- (x [prior(f(s))] y)) .
ops i : -> Inference .
ops q1 q2 q3 : -> Sequent .
eq q1 = ((y prior(s) x),(x [prior(s)] y) |- nil) .
eq q2 = ((y prior(f(s)) x) |- (y prior(s) x)) .
eq q3 = (nil |- (x [prior(f(s))] y),(y prior(f(s)) x)) .
eq antecedent(i) = (q1,q2,q3) .
eq ((x [prior(s)] y) |- (x [prior(f(s))] y)) = consequent(i) .
red claim .
close
```
```
#!python
%ΞPRIORITY + LK> *
-- reduce in %ΞPRIORITY + LK : (claim):Prop

** Found [state 159] (consequent(i)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 446 rewrites(0.510 sec), 15075 matches, 184 memo hits)
```
### ΞPRIORITY furthermore redefined) ###
```
#!python
module ΞPRIORITY
{
  imports
  {
    ex(TRANSITION)
    pr(PRIOR)
    pr(DEDUCIBLE)
  }
  signature
  {
    [ Ξpriority < Transition ]
  }
  axioms
  {
    vars S : System
    vars F : Ξpriority
    vars X Y : Entity
    crl priority(X)(F(S)) => priority(X)(S)
        if complete(F(S)) .
--  priority(X)(S) = priority(X)(F(S))
    cq deducible(nil |- (priority(X)(S) = priority(X)(F(S)))) = true
       if complete(F(S)) .
--  added axioms
--  X prior(S) Y ⇔ X prior(F(S)) Y
--  X prior(F(S)) Y ⇒ X prior(S) Y
    cq deducible((X prior(F(S)) Y) |- (X prior(S) Y)) = true
       if complete(F(S)) .
--  X prior(S) Y ⇒ X prior(F(S)) Y
    cq deducible((X prior(S) Y) |- (X prior(F(S)) Y)) = true
       if complete(F(S)) .
--  furthermore added axioms
--  X [prior(S)] Y ⇔ X [prior(F(S))] Y
--  X [prior(F(S))] Y ⇒ X [prior(S)] Y
    cq deducible((X [prior(F(S))] Y) |- (X [prior(S)] Y)) = true
       if complete(F(S)) .
--  X [prior(S)] Y ⇒ X [prior(F(S))] Y
    cq deducible((X [prior(S)] Y) |- (X [prior(F(S))] Y)) = true
       if complete(F(S)) .
--  cq prior(F(S)) = prior(S)
--     if complete(F(S)) .
  }
}
```

### ΞBLOCK ###
Transitions which preserve a value the observer block returns.
```
#!python
module ΞBLOCK
{
  imports
  {
    ex(TRANSITION)
    pr(BLOCK)
    pr(DEDUCIBLE)
  }
  signature
  {
    [ Ξblock < Transition ]
  }
  axioms
  {
    vars S : System
    vars F : Ξblock
    vars X Y : Entity
    crl block(F(S)) => block(S)
        if complete(F(S)) .
--  X block(S) Y ⇔ X block(F(S)) Y
--  X block(F(S)) Y ⇒ X block(S) Y
    cq deducible((X block(S) Y) |-  (X block(F(S)) Y)) = true
       if complete(F(S)) .
--  X block(S) Y ⇒ X block(F(S)) Y
    cq deducible((X block(F(S)) Y) |-  (X block(S) Y)) = true
       if complete(F(S)) .
  }
}
```

```
#!python
open PRECEDE + ΞENTRY + ΞPRIORITY + LK .
[ T < Ξentry Ξpriority ]
ops s : -> System .
ops f : -> T .
ops x y : -> Entity .
ops claim : -> Prop .
eq complete(f(s)) = true .
eq claim = deducible((x precede(f(s)) y) |- (x precede(s) y)) .
ops i1 : -> Inference .
ops q1 q2 : -> Sequent .
eq q1 = ((x [prior(f(s));ahead(f(s))] y) |- (x [prior(f(s))] y)) .
eq q2 = ((x [prior(f(s))] y) |- (x [prior(s)] y)) .
eq antecedent(i1) = (q1,q2) .
trans ((x [prior(f(s));ahead(f(s))] y) |- (x [prior(s)] y)) => consequent(i1) .
trans consequent(i1) => ((x [prior(f(s));ahead(f(s))] y) |- (x [prior(s)] y)) .
ops i2 : -> Inference .
ops q3 q4 q5 : -> Sequent .
eq q3 = ((x [prior(f(s));ahead(f(s))] y) |- (x prior(f(s)) y),(x ahead(f(s)) y)) .
eq q4 = ((x ahead(f(s)) y) |- (x ahead(s) y)) .
eq q5 = ((x prior(f(s)) y) |- (x prior(s) y)) .
eq antecedent(i2) = (q3,q4,q5) .
trans ((x [prior(f(s));ahead(f(s))] y) |- (x prior(s) y),(x ahead(s) y)) => consequent(i2) .
trans consequent(i2) => ((x [prior(f(s));ahead(f(s))] y) |- (x prior(s) y),(x ahead(s) y)) .
ops i3 : -> Inference .
ops q6 : -> Sequent .
eq q6 = ((x ahead(s) y),(x [prior(s)] y) |- (x [prior(s);ahead(s)] y)) .
eq antecedent(i3) = (consequent(i1),consequent(i2),q6) .
trans ((x [prior(f(s));ahead(f(s))] y) |- (x prior(s) y),(x [prior(s);ahead(s)] y))
   => consequent(i3) .
trans consequent(i3)
   => ((x [prior(f(s));ahead(f(s))] y) |- (x prior(s) y),(x [prior(s);ahead(s)] y)) .
ops i4 : -> Inference .
ops q7 : -> Sequent .
eq q7 = ((x prior(s) y) |- (x [prior(s);ahead(s)] y)) .
eq antecedent(i4) = (consequent(i3),q7) .
eq ((x [prior(f(s));ahead(f(s))] y) |- (x [prior(s);ahead(s)] y)) = consequent(i4) .
red claim .
close
```

Any transition contained in both Ξentry and Ξpriority
preserves the value x precede(x) y for any x,y : Entity.
```
#!python
%ΞPRIORITY + ΞENTRY + PRECEDE + LK> *
-- reduce in %ΞPRIORITY + ΞENTRY + PRECEDE + LK : 
    (claim):Prop

** Found [state 11] (consequent(i4)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 5319] (consequent(i3)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 2620] (consequent(i2)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 34] (consequent(i1)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 97834 rewrites(80.950 sec), 4487093 matches, 54662 memo hits)
```
```
#!python
open PRECEDE + ΞENTRY + ΞPRIORITY + LK .
[ T < Ξentry Ξpriority ]
ops s : -> System .
ops f : -> T .
ops x y : -> Entity .
ops claim : -> Prop .
eq complete(f(s)) = true .
eq claim = deducible((x precede(s) y) |- (x precede(f(s)) y)) .
ops i1 : -> Inference .
ops q1 q2 : -> Sequent .
eq q1 = ((x [prior(s);ahead(s)] y) |- (x [prior(s)] y)) .
eq q2 = ((x [prior(s)] y) |- (x [prior(f(s))] y)) .
eq antecedent(i1) = (q1,q2) .
trans ((x [prior(s);ahead(s)] y) |- (x [prior(f(s))] y)) => consequent(i1) .
trans consequent(i1) => ((x [prior(s);ahead(s)] y) |- (x [prior(f(s))] y)) .
ops i2 : -> Inference .
ops q3 q4 q5 : -> Sequent .
eq q3 = ((x [prior(s);ahead(s)] y) |- (x prior(s) y),(x ahead(s) y)) .
eq q4 = ((x ahead(s) y) |- (x ahead(f(s)) y)) .
eq q5 = ((x prior(s) y) |- (x prior(f(s)) y)) .
eq antecedent(i2) = (q3,q4,q5) .
trans ((x [prior(s);ahead(s)] y) |- (x prior(f(s)) y),(x ahead(f(s)) y)) => consequent(i2) .
trans consequent(i2) => ((x [prior(s);ahead(s)] y) |- (x prior(f(s)) y),(x ahead(f(s)) y)) .
ops i3 : -> Inference .
ops q6 : -> Sequent .
eq q6 = ((x ahead(f(s)) y),(x [prior(f(s))] y) |- (x [prior(f(s));ahead(f(s))] y)) .
eq antecedent(i3) = (consequent(i1),consequent(i2),q6) .
trans ((x [prior(s);ahead(s)] y) |- (x prior(f(s)) y),(x [prior(f(s));ahead(f(s))] y))
   => consequent(i3) .
trans consequent(i3)
   => ((x [prior(s);ahead(s)] y) |- (x prior(f(s)) y),(x [prior(f(s));ahead(f(s))] y)) .
ops i4 : -> Inference .
ops q7 : -> Sequent .
eq q7 = ((x prior(f(s)) y) |- (x [prior(f(s));ahead(f(s))] y)) .
eq antecedent(i4) = (consequent(i3),q7) .
eq ((x [prior(s);ahead(s)] y) |- (x [prior(f(s));ahead(f(s))] y)) = consequent(i4) .
red claim .
close
```
```
#!python
%ΞPRIORITY + ΞENTRY + PRECEDE + LK> red claim .
-- reduce in %ΞPRIORITY + ΞENTRY + PRECEDE + LK : 
    (claim):Prop

** Found [state 11] (consequent(i4)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 5319] (consequent(i3)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 2620] (consequent(i2)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 34] (consequent(i1)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 97834 rewrites(77.200 sec), 4487161 matches, 54662 memo hits)
```

So, we would be able to define the following module:
### ΞPRECEDE ###
```
#!python
module ΞPRECEDE
{
  imports
  {
    ex(ΞENTRY)
    ex(ΞPRIORITY)
    ex(PRECEDE)
  }
  signature
  {
    [ Ξprecede < Ξentry Ξpriority ]
  }
  axioms
  {
    vars S : System
    vars F : Ξprecede
    vars X Y : Entity
--  ((X precede(F(S)) Y) ⇔ (X precede(S) Y))
--  X precede(F(S)) Y ⇒ X precede(S) Y
    cq deducible((X [prior(F(S));ahead(F(S))] Y) |- (X [prior(S);ahead(S)] Y)) = true
       if complete(F(S)) .
--  X precede(S) Y ⇒ X precede(F(S)) Y
    cq deducible((X [prior(S);ahead(S)] Y) |- (X [prior(F(S));ahead(F(S))] Y)) = true
       if complete(F(S)) .
--  cq [prior(F(S));ahead(F(S))] = [prior(S);ahead(S)]
--     if complete(F(S)) .
  }
}
```

### RUN ###
```
#!python
module RUN
{
  imports
  {
    pr(NEXT)
    pr(CURRENT)
    pr(EXECUTED)
    ex(ΞPRECEDE)
    ex(ΞBLOCK)
  }
  signature
  {
    [ Run < Ξprecede Ξblock ]
    op run : Run -> Entity
  }
  axioms
  {
    vars S : System
    vars F : Run
    vars X : Entity
--  (current(F(S)) = {run(F))}
--  current(F(S)) ⊆ {run(F)}
    cq deducible((X @ current(F(S))) |- (X = run(F))) = true
       if complete(F(S)) .
--  {run(F)} ⊆　current(F(S)) ⊆ run(F)
    cq deducible((X = run(F)) |- (X @ current(F(S)))) = true
       if complete(F(S)) .
    cq deducible(nil |- (run(F) @ current(F(S)))) = true
       if complete(F(S)) .
--  executed(F(S)) = ((executed(S)),run(F))
--  executed(F(S)) ⊆ ((executed(S)),run(F))
    cq deducible((X @ executed(F(S))) |- (X @ executed(S)),(X = run(F))) = true
       if complete(F(S)) .
--  ((executed(S)),run(F)) ⊆ executed(F(S))
    cq deducible((X @ executed(S)) |- (X @ executed(F(S)))) = true
       if complete(F(S)) .
    cq deducible((X = run(F)) |- (X @ executed(F(S)))) = true
       if complete(F(S)) .
--  (run(F) @ next(S))
    cq deducible((X = run(F)) |- (X @ root(runnable(S),[prior(S);ahead(S)]))) = true
       if complete(F(S)) .
    cq deducible(nil |- (run(F) @ root(runnable(S),[prior(S);ahead(S)]))) = true
       if complete(F(S)) .
  }
}
```

### STOP ###
```
#!python
module STOP
{
  imports
  {
    ex(ΞPRIORITY)
    ex(ΞBLOCK)
    pr(CURRENT)
  }
  signature
  {
    [ Stop < Ξpriority Ξblock ]
  }
  axioms
  {
    vars S : System
    vars F : Stop
    vars X : Entity
    cq current(F(S)) = nil
       if complete(F(S)) .
  }
}
```

### ENTER ###
```
#!python
module ENTER
{
  imports
  {
    ex(ΞCURRENT)
    ex(ΞEXECUTED)
    ex(ΞPRIORITY)
    ex(ΞBLOCK)
    pr(AHEAD)
    pr(RUNNABLE)
  }
  signature
  {
    [ Enter < Ξcurrent Ξexecuted Ξpriority Ξblock ]
    op enter : Enter -> Entity
  }
  axioms
  {
    vars S : System
    vars F : Enter
    vars X Y : Entity
--  runnable(F(S)) = (runnable(S) ∪ {enter(F)})
--  runnable(F(S)) ⊆ (runnable(S) ∪ {enter(F)})
    cq deducible((X @ runnable(F(S))) |- (X @ runnable(S)),(X = enter(F))) = true
       if complete(F(S)) .
--  (runnable(S) ∪ {enter(F)}) ⊆ runnable(F(S))
    cq deducible((X @ runnable(S)) |- (X @ runnable(F(S)))) = true
       if complete(F(S)) .
    cq deducible((X = enter(F)) |- (X @ runnable(F(S)))) = true
       if complete(F(S)) .
--  entry(F(S)) = ((entry(S));enter(F))
--  entry(F(S)) ⊆ ((entry(S));enter(F))
    cq deducible((X ? entry(F(S))) |- (X ? entry(S)),(X = enter(F))) = true
       if complete(F(S)) .
--  ((entry(S));enter(F)) ⊆ entry(F(S))
    cq deducible((X ? entry(S)) |- (X ? entry(F(S)))) = true
       if complete(F(S)) .
    cq deducible((X = enter(F)) |- (X ? entry(F(S)))) = true
       if complete(F(S)) .
    cq deducible((X ? entry(S)) |- (position(entry(S),X) = position(entry(F(S)),X))) = true
       if complete(F(S)) .
--  (X ahead(F(S)) Y) ⇔ ((X ahead(S) Y) ∨ ((X ? entry(S)) ∧ ¬(Y ? entry(S)) ∧ (Y = enter(F)))
--  (X ahead(F(S)) Y) ⇒ ((X ahead(S) Y) ∨ ((X ? entry(S)) ∧ ¬(Y ? entry(S)) ∧ (Y = enter(F))))
    cq deducible((X ahead(F(S)) Y) |- (X ahead(S) Y),(X ? entry(S))) = true
       if complete(F(S)) .
    cq deducible((X ahead(F(S)) Y),(Y ? entry(S)) |- (X ahead(S) Y)) = true
       if complete(F(S)) .
    cq deducible((X ahead(F(S)) Y) |- (X ahead(S) Y),(Y = enter(F))) = true
       if complete(F(S)) .
--  ((X ahead(S) Y) ∨ ((X ? entry(S)) ∧ ¬(Y ? entry(S)) ∧ (Y = enter(F)))) ⇒ (X ahead(F(S)) Y)
    cq deducible((X ahead(S) Y) |- (X ahead(F(S)) Y)) = true
       if complete(F(S)) .
    cq deducible((X ? entry(S)),(Y = enter(F)) |- (Y ? entry(S)),(X ahead(F(S)) Y)) = true
       if complete(F(S)) .
  }
}
```

### RELATIONAL IMAGE ###

The following module declares an operation to take an image of a relation.

```
#!python
module IMAGE
(
  X :: TRIV,
  R :: RELATION(X),
  S :: SET(X)
)
{
  imports
  {
    pr(DEDUCIBLE)
  }
  signature
  {
    op _[_] : Relation Elt -> Set
  }
  axioms
  {
    vars R : Relation
    vars X Y : Elt
    eq deducible((X R Y) |- (Y @ R[X])) = true .
    eq deducible((Y @ R[X]) |- (X R Y)) = true .
  }
}
```
For all x : Elt and R : Relation, 
the expression R[x] represents a set such that 
(y @ R[x]) is equivalent to (x R y), for all y : Elt.

The following module is an instantiation of the above module.

```
#!python
make IMAGE/ENTITY
(
  IMAGE(
    ENTITY { sort Elt -> Entity },
    RELATION/ENTITY { sort Relation -> Relation/Entity },
    SET/ENTITY { sort Set -> Set/Entity }
  )
)
```

### EXIT ###
```
#!python
module EXIT
{
  imports
  {
    ex(STOP)
    pr(EXECUTED)
    pr(AHEAD)
    pr(RUNNABLE)
    pr(IMAGE/ENTITY)
  }
  signature
  {
    [ Exit < Stop ]
    op exit : Exit -> Entity
  }
  axioms
  {
    vars S : System
    vars F : Exit
    vars X Y : Entity
--  executed(F(S)) = (executed(S) \ {exit(F)})
--  executed(F(S)) ⊆ (executed(S) \ {exit(F)})
    cq deducible((X @ executed(F(S))) |- (X @ executed(S))) = true
       if complete(F(S)) .
    cq deducible((X @ executed(F(S))),(X = exit(F)) |- nil) = true
       if complete(F(S)) .
--  (executed(S) \ exit(F)) ⊆ executed(F(S))
    cq deducible((X @ executed(S)) |- (X @ executed(F(S))),(X = exit(F))) = true
       if complete(F(S)) .
--  exit(F) ∈ entry(S)
    cq deducible((X = exit(F)) |- X ? entry(S)) = true
       if complete(F(S)) .
    cq deducible(nil |- exit(F) ? entry(S)) = true
       if complete(F(S)) .
--  entry(F(S)) = ((entry(S)) - exit(F))
--  (X ≠ exit(F)) ⇒ ((X ? entry(S)) ⇔ (X ? entry(F(S))))
--  (X ≠ exit(F)) ⇒ ((X ? entry(S)) ⇒ (X ? entry(F(S))))
    cq deducible((X ? entry(S)) |- (X = exit(F)),(X ? entry(F(S)))) = true
       if complete(F(S)) .
--  (X ≠ exit(F)) ⇒ ((X ? entry(F(S))) ⇒ (X ? entry(S)))
    cq deducible((X ? entry(F(S))) |- (X = exit(F)),(X ? entry(S))) = true
       if complete(F(S)) .
--  (exit(F) ∈ entry(F(S))) ⇒ (X ∈ entry(S) ⇔ X ∈ entry(F(S)))
--  (exit(F) ∈ entry(F(S))) ⇒ (X ∈ entry(S) ⇒ X ∈ entry(F(S)))
    cq deducible((exit(F) ? entry(F(S))),(X ? entry(S)) |- (X ? entry(F(S)))) = true
       if complete(F(S)) .
--  (exit(F) ∈ entry(F(S))) ⇒ (X ∈ entry(F(S)) ⇒ X ∈ entry(S))
    cq deducible((exit(F) ? entry(F(S))),(X ? entry(F(S))) |- (X ? entry(S))) = true
       if complete(F(S)) .
    cq deducible((X ahead(S) exit(F)) |- (position(entry(F(S)),X) = position(entry(S),X))) = true
       if complete(F(S)) .
    cq deducible((exit(F) ahead(S) X) |- (s(position(entry(F(S)),X)) = position(entry(S),X))) = true
       if complete(F(S)) .
    cq deducible((X ahead(S) Y) |- (X = exit(F)),(Y = exit(F)),(X ahead(F(S)) Y)) = true
       if complete(F(S)) .
    cq deducible((X ahead(F(S)) Y) |- (X ahead(S) Y)) = true
       if complete(F(S)) .
--  (exit(F) ∈ entry(F(S))) ⇒ (runnable(F(S)) = runnable(S))
    cq deducible((exit(F) ? entry(F(S))) |- (runnable(F(S)) = runnable(S))) = true
       if complete(F(S)) .
-- ¬(exit(F) ∈ entry(F(S)) ⇒ (runnable(F(S)) = runnable(S) \ {exit(F)})
-- ¬(exit(F) ∈ entry(F(S)) ⇒ (runnable(F(S)) ⊆ (runnable(S) \ {exit(F)}))
    cq deducible((X @ runnable(F(S))) |- (X @ runnable(S)),(exit(F) ? entry(F(S)))) = true
       if complete(F(S)) .
    cq deducible((X @ runnable(F(S))),(X = exit(F)) |- (exit(F) ? entry(F(S)))) = true
       if complete(F(S)) .
-- ¬(exit(F) ∈ entry(F(S))) ⇒ (runnable(S) \ {exit(F)}) ⊆ runnable(F(S))
    cq deducible((X @ runnable(S)) |- (X = exit(F)),(X @ runnable(F(S))),(exit(F) ? entry(F(S)))) = true
       if complete(F(S)) .
--  runnable(F(S)) ⊆ runnable(S)
    cq deducible((X @ runnable(F(S))) |- (X @ runnable(S))) = true
       if complete(F(S)) .
--  (runnable(S) \ {exit(F)}) ⊆ runnable(F(S))
    cq deducible((X @ runnable(S)) |- (X = exit(F)),(X @ runnable(F(S)))) = true
       if complete(F(S)) .
--  ¬(exit(F) ∈ domain(block(S)))
    cq deducible((X = exit(F)),(X block(S) Y) |- nil) = true
       if complete(F(S)) .
    cq deducible((X = exit(F)) |- (block(S)[X] = nil)) = true
       if complete(F(S)) .
--  {exit(F)} = current(S)
--  current(S) ⊆ {exit(F)}
    cq deducible((X @ current(S)) |- (X = exit(F))) = true
       if complete(F(S)) .
--  {exit(F)} ⊆ current(S)
    cq deducible((X = exit(F)) |- (X @ current(S))) = true
       if complete(F(S)) .
    cq deducible(nil |- (exit(F) @ current(S))) = true
       if complete(F(S)) .
  }
}
```

### LEAVE ###
```
#!python
module LEAVE
{
  imports
  {
    ex(STOP)
    ex(ΞEXECUTED)
    ex(ΞPRECEDE)
  }
  signature
  {
    [ Leave < Stop Ξexecuted Ξprecede ]
  }
}
```
### PRIORITY CEILING ###

The following module declares 
necessary properties of the priority ceiling protocol
to prove its dead-lock freeness.
```
#!python
module PRIORITY-CEILING
{
  imports
  {
    pr(BLOCK)
    pr(PRIORITY)
    pr(ASSIGN)
    pr(CURRENT)
    pr(COMPARISON)
    pr(IMAGE/ENTITY)
    pr(DEDUCIBLE)
    pr(TRANSITION)
  }
  axioms
  {
    vars S : System
    vars F : Transition
    vars X Y : Entity
--  (X block(S) Y) ⇒ (priority(X)(S) ≧ assign(Y))
    cq deducible((X block(S) Y),(assign(Y) > priority(X)(S)) |- nil) = true
       if complete(S) .
--  (∀Y : Entity・¬(X block(S) Y)) ⇒ (priority(X)(S) = assign(Y))
    cq deducible((block(S)[X] = nil) |- (priority(X)(S) = assign(X))) = true
       if complete(S) .
--  ¬(X ∈ current(S)) ⇒ ((priority(X)(F(S)) = priority(X)(S))
    cq deducible(nil |- (X @ current(S)),(priority(X)(S) = priority(X)(F(S)))) = true
       if complete(F(S)) .
  }
}
```

### ADJUST ###
```
#!python
module ADJUST
{
  imports
  {
    ex(ΞCURRENT)
    ex(ΞEXECUTED)
    ex(ΞENTRY)
    pr(PRIORITY-CEILING)
  }
  signature
  {
    [ Adjust < Ξcurrent Ξexecuted Ξentry ]
  }
}
```

### PREVENT ###
```
#!python
module PREVENT
{
  imports
  {
    ex(ADJUST)
  }
  signature
  {
    [ Prevent < Adjust ]
    op blocked : Prevent -> Set/Entity
  }
  axioms
  {
    vars S : System
    vars F : Prevent
    vars X Y : Entity
--  (X ∈ current(S)) ⇒ ((priority(X)(F(S)) ≧ priority(X)(S))
    cq deducible((X @ current(S)),(priority(X)(S) > priority(X)(F(S))) |- nil) = true
       if complete(F(S)) .
--  (X block(F(S)) Y) ⇔ ((X block(S) Y) ∨ ((X ∈ current(S)) ∧ (Y ∈ blocked(F))))
    cq deducible((X @ current(S)) |- (block(F(S))[X] = ((block(S)[X]),(blocked(F))))) = true
       if complete(F(S)) .
--  ((X block(S) Y) ∨ ((X ∈ current(S)) ∧ (Y ∈ blocked(F)))) ⇒ (X block(F(S)) Y)
    cq deducible((X block(S) Y) |- (X block(F(S)) Y)) = true
       if complete(F(S)) .
    cq deducible((X @ current(S)),(Y @ blocked(F)) |- (X block(F(S)) Y)) = true
       if complete(F(S)) .
--  (X block(F(S)) Y) ⇒ ((X block(S) Y) ∨ ((X ∈ current(S)) ∧ (Y ∈ blocked(F))))
    cq deducible((X block(F(S)) Y) |- (X block(S) Y),(X @ current(S))) = true
       if complete(F(S)) .
    cq deducible((X block(F(S)) Y) |- (X block(S) Y),(Y @ blocked(F))) = true
       if complete(F(S)) .
--  (current(S) ∩ blocked(F)) = ∅
    cq deducible((X @ current(S)),(X @ blocked(F)) |- nil) = true
       if (complete(F(S))) = true .
  }
}
```

### FREE ###
```
#!python
module FREE
{
  imports
  {
    ex(ADJUST)
  }
  signature
  {
    [ Free < Adjust ]
    op freed : Free -> Set/Entity
  }
  axioms
  {
    vars S : System
    vars F : Free
    vars X Y : Entity
--  (X block(F(S)) Y) ⇔ ((X block(S) Y) ∧ ¬((X ∈ current(S)) ∧ (Y ∈ freed(F))))
--  ((X block(S) Y) ∧ ¬((X ∈ current(S)) ∧ (Y ∈ freed(F)))) ⇒ (X block(F(S)) Y)
    cq deducible((X block(S) Y) |- (X block(F(S)) Y),(X @ current(S))) = true
       if complete(F(S)) .
    cq deducible((X block(S) Y) |- (X block(F(S)) Y),(Y @ freed(F))) = true
       if complete(F(S)) .
--  (X block(F(S)) Y) ⇒ ((X block(S) Y) ∧ ¬((X ∈ current(S)) ∧ (Y ∈ freed(F))))
    cq deducible((X block(F(S)) Y) |- (X block(S) Y)) = true
       if complete(F(S)) .
    cq deducible((X block(F(S)) Y),(X @ current(S)),(Y @ freed(F)) |- nil) = true
       if complete(F(S)) .
  }
}
```

```
#!python
make EXTEND/ENTITY
(
  EXTEND(
    ENTITY { sort Elt -> Entity },
    SET/ENTITY { sort Set -> Set/Entity },
    RELATION/ENTITY { sort Relation -> Relation/Entity }
  )
)
```
```
#!python
module EQUALITY/SET
(
  X :: TRIV,
  X :: SET(X)
)
{
  imports
  {
    pr(DEDUCIBLE)
  }
  axioms
  {
    vars X Y : Elt
    vars S T : Set
    eq deducible((X = Y),(X @ S) |- (Y @ S)) = true .
    eq deducible((S = T),(X @ S) |- (X @ T)) = true .
  }
}
```
```
#!python
make EQUALITY/SET/ENTITY
(
  EQUALITY/SET(
    ENTITY { sort Elt -> Entity },
    SET/ENTITY { sort Set -> Set/Entity }
  )
)
```
```
#!python
module EQUALITY/EQUALITY
(
  X :: TRIV
)
{
  imports
  {
    pr(DEDUCIBLE)
  }
  axioms
  {
    vars X Y Z : Elt
    eq deducible((X = Y),(Y = Z) |- (X = Z)) = true .
  }
}
```
```
#!python
make EQUALITY/EQUALITY/NUMBER
(
  EQUALITY/EQUALITY(
    NUMBER { sort Elt -> Number }
  )
)
```

Just after the transition Run,
any runnable entity does not precede the executed entity by the transition. 
```
#!python
open RUN + LK .
ops s : -> System .
ops f : -> Run .
eq complete(f(s)) = true .
ops x y : -> Entity .
ops claim : -> Prop .
eq claim = deducible((x @ runnable(f(s))),(y @ current(f(s))),(x precede(f(s)) y) |- nil) .
ops i1 : -> Inference .
ops q1 q2 : -> Sequent .
eq q1 = (nil |- (run(f) @ root(runnable(s),[prior(s);ahead(s)]))) .
eq q2 = ((run(f) @ root(runnable(s),[prior(s);ahead(s)])),
         (x @ runnable(s)),
         (x [prior(s);ahead(s)] run(f)) |- nil) .
eq antecedent(i1) = (q1,q2) .
trans ((x @ runnable(s)),(x [prior(s);ahead(s)] run(f)) |- nil) => consequent(i1) .
trans consequent(i1) => ((x @ runnable(s)),(x [prior(s);ahead(s)] run(f)) |- nil) .
ops i2 : -> Inference .
ops q3 : -> Sequent .
eq q3 = ((x [prior(f(s));ahead(f(s))] run(f)) |- (x [prior(s);ahead(s)] run(f))) .
eq antecedent(i2) = (consequent(i1),q3) .
trans ((x @ runnable(s)),(x [prior(f(s));ahead(f(s))] run(f)) |- nil) => consequent(i2) .
trans consequent(i2) => ((x @ runnable(s)),(x [prior(f(s));ahead(f(s))] run(f)) |- nil) .
ops i3 : -> Inference .
ops q4 q5 : -> Sequent .
eq q4 = ((y @ current(f(s))) |- (y = run(f))) .
eq q5 = ((y = run(f)),(x [prior(f(s));ahead(f(s))] y) |- (x [prior(f(s));ahead(f(s))] run(f))) .
eq antecedent(i3) = (consequent(i2),q4,q5) .
trans ((x @ runnable(s)),(y @ current(f(s))),(x [prior(f(s));ahead(f(s))] y) |- nil) => consequent(i3) .
trans consequent(i3) => ((x @ runnable(s)),(y @ current(f(s))),(x [prior(f(s));ahead(f(s))] y) |- nil) .
ops i4 : -> Inference .
ops q6 : -> Sequent .
eq q6 = ((x @ runnable(f(s))) |- (x @ runnable(s))) . 
eq antecedent(i4) = (consequent(i3),q6) .
eq ((x @ runnable(f(s))),(y @ current(f(s))),(x [prior(f(s));ahead(f(s))] y) |- nil) = consequent(i4) .
red claim .
close
```
```
#!python
%RUN + LK> red claim .
-- reduce in %RUN + LK : (claim):Prop

** Found [state 12] (consequent(i4)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 3409] (consequent(i3)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 42] (consequent(i2)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 28] (consequent(i1)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 18965 rewrites(18.420 sec), 1172200 matches, 10859 memo hits)
```
Just after any transition F contained in Run, 
the following sequents can be deducible.

### A BASE STRUCTURE FOR DEADLOCK FREE SCHEDULING ###
```
#!python
module BASE
{
  imports
  {
    pr(RUN)
    pr(LEAVE)
    pr(ENTER)
    pr(EXIT)
    pr(PREVENT)
    pr(FREE)
  }
}

```

### THEOREM ###
The above structure satisfies the following properties:

For any s : System and x,y : Entity, 
the following sequents can be deduced.

* ((x @ current(s)) |- (x @ executed(s)))

* ((x @ executed(s)) |- (x @ runnable(s)))

* ((x @ runnable(s)) |- (x ? entry(s)))

* ((x block(s) x) |- nil)

* ((x block(s) y) |- (x @ executed(s)))

* ((x @ executed(s)),(y ahead(s) x) |- (x prior(s) y))

* ((x block(s) y),(x ahead(s) y),(y @ executed(s)) |- nil)

* (nil |- (x @ executed(s)),(priority(x)(s) = assign(x)))

* ((x block(s) y),(assign(y) > priority(x)(s)) |- nil)

* ((X @ executed(F(S))),(Y ahead(F(S)) X) |- (X prior(F(S)) Y))


### PROOF OF THE THEOREM ###
With structurral induction, 
we indicate that each sequent listed above can be deduced.

* ((x @ current(s)) |- (x @ executed(s)))

```
#!python
open BASE + LK .
[ T < Ξcurrent Ξexecuted ]
-- Prevent, Free, Enter ⊆ T
ops s : -> System .
ops f : -> T .
ops x : -> Entity .
ops claim : -> Prop .
eq claim = deducible((x @ current(f(s))) |- (x @ executed(f(s)))) .
eq deducible((x @ current(s)) |- (x @ executed(s))) = true .
eq complete(f(s)) = true .

ops i : -> Inference .
ops q1 q2 q3 : -> Sequent .
eq q1 = ((x @ current(s)) |- (x @ executed(s))) .
eq q2 = ((x @ current(f(s))) |- (x @ current(s))) .
eq q3 = ((x @ executed(s)) |- (x @ executed(f(s)))) .
eq antecedent(i) = (q1,q2,q3) .
eq ((x @ current(f(s))) |- (x @ executed(f(s)))) = consequent(i) .
red claim .
close
```
```
#!python
%LK + BASE> *
-- reduce in %LK + BASE : (claim):Prop

** Found [state 317] (consequent(i)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 3547 rewrites(1.900 sec), 218673 matches, 1465 memo hits)
```
```
#!python
open BASE + LK .
ops s : -> System .
ops f : -> Run .
ops x : -> Entity .
ops claim : -> Prop .
eq claim = deducible((x @ current(f(s))) |- (x @ executed(f(s)))) .
eq complete(f(s)) = true .

ops i : -> Inference .
ops q1 q2 : -> Sequent .
eq q1 = ((x @ current(f(s))) |- (x = run(f))) .
eq q2 = ((x = run(f)) |- (x @ executed(f(s)))) .
eq antecedent(i) = (q1,q2) .
eq ((x @ current(f(s))) |- (x @ executed(f(s)))) = consequent(i) .
red claim .
close
```
```
#!python
%LK + BASE> *
-- reduce in %LK + BASE : (claim):Prop

** Found [state 5] (consequent(i)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 37 rewrites(0.010 sec), 1074 matches, 2 memo hits)
```
```
#!python
open BASE + LK .
ops s : -> System .
ops f : -> Stop .
-- Leave, Exit ⊆ Stop
ops x : -> Entity .
ops claim : -> Prop .
eq claim = deducible((x @ current(f(s))) |- (x @ executed(f(s)))) .
eq complete(f(s)) = true .
red claim .
close
```
```
#!python
%LK + BASE> *
-- reduce in %LK + BASE : (claim):Prop
(true):Bool
(0.000 sec for parse, 11 rewrites(0.000 sec), 625 matches)
```
```
#!python
module STRUCTURE
{
  imports
  {
    pr(BASE)
  }
  axioms
  {
    vars S : System
    vars X : Entity
    cq deducible((X @ current(S)) |- (X @ executed(S))) = true
       if complete(S) .
  }
}
```

* ((x @ executed(s)) |- (x @ runnable(s)))

```
#!python
open BASE + LK .
[ T < Ξentry Ξexecuted ]
-- Prevent, Free, Leave ⊆ T
ops s : -> System .
ops f : -> T .
ops x : -> Entity .
ops claim : -> Prop .
eq claim = deducible((x @ executed(f(s))) |- (x @ runnable(f(s)))) .
eq deducible((x @ executed(s)) |- (x @ runnable(s))) = true .
eq complete(f(s)) = true .

ops i : -> Inference .
ops q1 q2 q3 : -> Sequent .
eq q1 = ((x @ executed(s)) |- (x @ runnable(s))) .
eq q2 = ((x @ executed(f(s))) |- (x @ executed(s))) .
eq q3 = ((x @ runnable(s)) |- (x @ runnable(f(s)))) .
eq antecedent(i) = (q1,q2,q3) .
eq ((x @ executed(f(s))) |- (x @ runnable(f(s)))) = consequent(i) .
red claim .
close
```
```
#!python
%LK + BASE> *
-- reduce in %LK + BASE : (claim):Prop

** Found [state 317] (consequent(i)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 3547 rewrites(1.500 sec), 218686 matches, 1465 memo hits)
```
```
#!python
open BASE + LK .
ops s : -> System .
ops f : -> Run .
ops x : -> Entity .
ops claim : -> Prop .
eq claim = deducible((x @ executed(f(s))) |- (x @ runnable(f(s)))) .
eq deducible((x @ executed(s)) |- (x @ runnable(s))) = true .
eq complete(f(s)) = true .

ops i1 : -> Inference .
ops q11 q12 q13 : -> Sequent .
eq q11 = ((x @ executed(s)) |- (x @ runnable(s))) .
eq q12 = ((x @ executed(f(s))) |- (x @ executed(s)),(x = run(f))) .
eq q13 = ((x @ runnable(s)) |- (x @ runnable(f(s)))) .
eq antecedent(i1) = (q11,q12,q13) .
trans ((x @ executed(f(s))) |- (x @ runnable(f(s))),(x = run(f))) => consequent(i1) .
trans consequent(i1) => ((x @ executed(f(s))) |- (x @ runnable(f(s))),(x = run(f))) .

ops i2 : -> Inference .
ops q21 : -> Sequent .
eq q21 = ((x = run(f)) |- (x @ runnable(f(s)))) .
eq antecedent(i2) = (consequent(i1),q21) .
eq ((x @ executed(f(s))) |- (x @ runnable(f(s)))) = consequent(i2) .
red claim .
close
```
```
#!python
%LK + BASE> red claim .
-- reduce in %LK + BASE : (claim):Prop

** Found [state 12] (consequent(i2)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 6462] (consequent(i1)):Set/Sequent
   {}
-- found required number of solutions 1.
(deducible(consequent(i2))):Prop
(0.000 sec for parse, 66937 rewrites(56.440 sec), 5227362 matches, 33516 memo hits)
```
```
#!python
open BASE + LK .
ops s : -> System .
ops f : -> Enter .
ops x : -> Entity .
ops claim : -> Prop .
eq claim = deducible((x @ executed(f(s))) |- (x @ runnable(f(s)))) .
eq deducible((x @ executed(s)) |- (x @ runnable(s))) = true .
eq complete(f(s)) = true .

ops i : -> Inference .
ops q1 q2 q3 : -> Sequent .
eq q1 = ((x @ executed(s)) |- (x @ runnable(s))) .
eq q2 = ((x @ executed(f(s))) |- (x @ executed(s))) .
eq q3 = ((x @ runnable(s)) |- (x @ runnable(f(s)))) .
eq antecedent(i) = (q1,q2,q3) .
eq ((x @ executed(f(s))) |- (x @ runnable(f(s)))) = consequent(i) .
red claim .
close
```
```
#!python
%LK + BASE> *
-- reduce in %LK + BASE : (claim):Prop

** Found [state 288] (consequent(i)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 2793 rewrites(1.340 sec), 188530 matches, 1224 memo hits)
```
```
#!python
open BASE + LK .
ops s : -> System .
ops f : -> Exit .
ops x : -> Entity .
ops claim : -> Prop .
eq claim = deducible((x @ executed(f(s))) |- (x @ runnable(f(s)))) .
eq deducible((x @ executed(s)) |- (x @ runnable(s))) = true .
eq complete(f(s)) = true .

ops i : -> Inference .
ops q1 q2 q3 q4 : -> Sequent .
eq q1 = ((x @ executed(s)) |- (x @ runnable(s))) .
eq q2 = ((x @ executed(f(s))) |- (x @ executed(s))) .
eq q3 = ((x @ runnable(s)) |- (x @ runnable(f(s))),(x = exit(f))) .
eq q4 = ((x @ executed(f(s))),(x = exit(f)) |- nil) .
eq antecedent(i) = (q1,q2,q3,q4) .
eq ((x @ executed(f(s))) |- (x @ runnable(f(s)))) = consequent(i) .
red claim .
close
```
```
#!python
%LK + BASE> *
-- reduce in %LK + BASE : (claim):Prop

** Found [state 530] (consequent(i)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 17314 rewrites(9.380 sec), 1732119 matches, 9748 memo hits)
```
```
#!python
module STRUCTURE
{
  imports
  {
    pr(BASE)
  }
  axioms
  {
    vars S : System
    vars X : Entity
    cq deducible((X @ current(S)) |- (X @ executed(S))) = true
       if complete(S) .
    cq deducible((X @ executed(S)) |- (X @ runnable(S))) = true
       if complete(S) .
  }
}
```


* ((x @ runnable(s)) |- (x ? entry(s)))

```
#!python
open BASE + LK .
ops s : -> System .
ops f : -> Ξentry .
-- Run, Leave, Prevent, Free ⊆ Ξentry
ops x : -> Entity .
ops claim : -> Prop .
eq claim = deducible((x @ runnable(f(s))) |- (x ? entry(f(s)))) .
eq deducible((x @ runnable(s)) |- (x ? entry(s))) = true .
eq complete(f(s)) = true .

ops i : -> Inference .
ops q1 q2 q3 : -> Sequent .
eq q1 = ((x @ runnable(s)) |- (x ? entry(s))) .
eq q2 = ((x ? entry(s)) |- (x ? entry(f(s)))) .
eq q3 = ((x @ runnable(f(s))) |- (x @ runnable(s))) .
eq antecedent(i) = (q1,q2,q3) .
eq ((x @ runnable(f(s))) |- (x ? entry(f(s)))) = consequent(i) .
red claim .
close
```
```
#!python
%LK + BASE> *
-- reduce in %LK + BASE : (claim):Prop

** Found [state 328] (consequent(i)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 3567 rewrites(2.030 sec), 265416 matches, 1465 memo hits)
```

```
#!python
open BASE + LK .
ops s : -> System .
ops f : -> Enter .
ops x : -> Entity .
ops claim : -> Prop .
eq claim = deducible((x @ runnable(f(s))) |- (x ? entry(f(s)))) .
eq deducible((x @ runnable(s)) |- (x ? entry(s))) = true .
eq complete(f(s)) = true .

ops i : -> Inference .
ops q1 q2 q3 q4 : -> Sequent .
eq q1 = ((x @ runnable(s)) |- (x ? entry(s))) .
eq q2 = ((x ? entry(s)) |- (x ? entry(f(s)))) .
eq q3 = ((x = enter(f)) |- (x ? entry(f(s)))) .
eq q4 = ((x @ runnable(f(s))) |- (x @ runnable(s)),(x = enter(f))) .
eq antecedent(i) = (q1,q2,q3,q4) .
eq ((x @ runnable(f(s))) |- (x ? entry(f(s)))) = consequent(i) .
red claim .
close
```
```
#!python
%LK + BASE> *
-- reduce in %LK + BASE : (claim):Prop

** Found [state 2274] (consequent(i)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 13785 rewrites(15.640 sec), 1700183 matches, 7401 memo hits)
```
```
#!python
open BASE + EQUALITY/SET/ENTITY + LK .
ops s : -> System .
ops f : -> Exit .
ops x : -> Entity .
ops claim : -> Prop .
eq claim = deducible((x @ runnable(f(s))) |- (x ? entry(f(s)))) .
eq deducible((x @ runnable(s)) |- (x ? entry(s))) = true .
eq complete(f(s)) = true .

ops i1 : -> Inference .
ops q11 q12 q13 : -> Sequent .
eq q11 = ((x @ runnable(s)) |- (x ? entry(s))) .
eq q12 = ((exit(f) ? entry(f(s))) |- (runnable(s) = runnable(f(s)))) .
eq q13 = ((runnable(s) = runnable(f(s))),(x @ runnable(f(s))) |- (x @ runnable(s))) .
eq antecedent(i1) = (q11,q12,q13) .
trans ((exit(f) ? entry(f(s))),(x @ runnable(f(s))) |- (x ? entry(s))) => consequent(i1) .
trans consequent(i1) => ((exit(f) ? entry(f(s))),(x @ runnable(f(s))) |- (x ? entry(s))) .

ops i2 : -> Inference .
ops q21 : -> Sequent .
eq q21 = ((x ? entry(s)),(exit(f) ? entry(f(s))) |- (x ? entry(f(s)))) .
eq antecedent(i2) = (consequent(i1),q21) .
trans ((exit(f) ? entry(f(s))),(x @ runnable(f(s))) |- (x ? entry(f(s)))) => consequent(i2) .
trans consequent(i2) => ((exit(f) ? entry(f(s))),(x @ runnable(f(s))) |- (x ? entry(f(s)))) .

ops i3 : -> Inference .
ops q31 q32 : -> Sequent .
eq q31 = ((x @ runnable(f(s))) |- (x @ runnable(s))) .
eq q32 = ((x ? entry(s)) |- (x = exit(f)),(x ? entry(f(s)))) .
eq antecedent(i3) = (q11,q31,q32) .
trans ((x @ runnable(f(s))) |- (x = exit(f)),(x ? entry(f(s)))) => consequent(i3) .
trans consequent(i3) => ((x @ runnable(f(s))) |- (x = exit(f)),(x ? entry(f(s)))) .

ops i4 : -> Inference .
ops q41 : -> Sequent .
eq q41 = ((x @ runnable(f(s))),(x = exit(f)) |- (exit(f) ? entry(f(s)))) .
eq antecedent(i4) = (consequent(i3),q41) .
trans ((x @ runnable(f(s))) |- (exit(f) ? entry(f(s))),(x ? entry(f(s)))) => consequent(i4) .
trans consequent(i4) => ((x @ runnable(f(s))) |- (exit(f) ? entry(f(s))),(x ? entry(f(s)))) .

ops i5 : -> Inference .
eq antecedent(i5) = (consequent(i2),consequent(i4)) .
eq ((x @ runnable(f(s))) |- (x ? entry(f(s)))) = consequent(i5) .
red claim .
close
```
```
#!python
%LK + EQUALITY/SET/ENTITY + BASE> *
-- reduce in %LK + EQUALITY/SET/ENTITY + BASE : 
    (claim):Prop

** Found [state 40] (consequent(i5)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 48] (consequent(i4)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 5782] (consequent(i3)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 160] (consequent(i2)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 2089] (consequent(i1)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 59543 rewrites(56.960 sec), 6069577 matches, 31597 memo hits)
```
```
#!python
module STRUCTURE
{
  imports
  {
    pr(BASE)
  }
  axioms
  {
    vars S : System
    vars X : Entity
    cq deducible((X @ current(S)) |- (X @ executed(S))) = true
       if complete(S) .
    cq deducible((X @ executed(S)) |- (X @ runnable(S))) = true
       if complete(S) .
    cq deducible((X @ runnable(S)) |- (X ? entry(S))) = true
       if complete(S) .
  }
}
```

* ((x block(s) x) |- nil)

```
#!python
open BASE + LK .
ops s : -> System .
ops f : -> Ξblock .
-- Run, Leave, Enter, Exit ⊆ Ξblock
ops x : -> Entity .
ops claim : -> Prop .
eq claim = deducible((x block(f(s)) x) |- nil) .
eq deducible((x block(s) x) |- nil) = true .
eq complete(f(s)) = true .

ops i : -> Inference .
ops q1 q2 : -> Sequent .
eq q1 = ((x block(s) x) |- nil) .
eq q2 = ((x block(f(s)) x) |- (x block(s) x)) .
eq antecedent(i) = (q1,q2) .
eq ((x block(f(s)) x) |- nil) = consequent(i) .
red claim .
close
```
```
#!python
%LK + BASE> *
-- reduce in %LK + BASE : (claim):Prop

** Found [state 3] (consequent(i)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 35 rewrites(0.010 sec), 485 matches, 1 memo hits)
```
```
#!python
open BASE + LK .
ops s : -> System .
ops f : -> Prevent .
ops x : -> Entity .
ops claim : -> Prop .
eq claim = deducible((x block(f(s)) x) |- nil) .
eq deducible((x block(s) x) |- nil) = true .
eq complete(f(s)) = true .

ops i1 : -> Inference .
ops q11 q12 : -> Sequent .
eq q11 = ((x block(s) x) |- nil) .
eq q12 = ((x block(f(s)) x) |- (x block(s) x),(x @ current(s))) .
eq antecedent(i1) = (q11,q12) .
trans ((x block(f(s)) x) |- (x @ current(s))) => consequent(i1) .
trans consequent(i1) => ((x block(f(s)) x) |- (x @ current(s))) .

ops i2 : -> Inference .
ops q21 : -> Sequent .
eq q21 = ((x block(f(s)) x) |- (x block(s) x),(x @ blocked(f))) .
eq antecedent(i2) = (q11,q21) .
trans ((x block(f(s)) x) |- (x @ blocked(f))) => consequent(i2) .
trans consequent(i2) => ((x block(f(s)) x) |- (x @ blocked(f))) .

ops i3 : -> Inference .
ops q31 : -> Sequent .
eq q31 = ((x @ current(s)),(x @ blocked(f)) |- nil) .
eq antecedent(i3) = (consequent(i1),consequent(i2),q31) .
eq ((x block(f(s)) x) |- nil) = consequent(i3) .
red claim .
close
```
```
#!python
%LK + BASE> *
-- reduce in %LK + BASE : (claim):Prop

** Found [state 360] (consequent(i3)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 29] (consequent(i2)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 28] (consequent(i1)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 2456 rewrites(1.400 sec), 109459 matches, 1158 memo hits)
```
```
#!python
open BASE + LK .
ops s : -> System .
ops f : -> Free .
ops x : -> Entity .
ops claim : -> Prop .
eq claim = deducible((x block(f(s)) x) |- nil) .
eq deducible((x block(s) x) |- nil) = true .
eq complete(f(s)) = true .

ops i : -> Inference .
ops q1 q2 : -> Sequent .
eq q1 = ((x block(s) x) |- nil) .
eq q2 = ((x block(f(s)) x) |- (x block(s) x)) .
eq antecedent(i) = (q1,q2) .
eq ((x block(f(s)) x) |- nil) = consequent(i) .
red claim .
close
```
```
#!python
%LK + BASE> *
-- reduce in %LK + BASE : (claim):Prop

** Found [state 3] (consequent(i)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 31 rewrites(0.010 sec), 415 matches, 1 memo hits)
```
```
#!python
module STRUCTURE
{
  imports
  {
    pr(BASE)
  }
  axioms
  {
    vars S : System
    vars X : Entity
    cq deducible((X @ current(S)) |- (X @ executed(S))) = true
       if complete(S) .
    cq deducible((X @ executed(S)) |- (X @ runnable(S))) = true
       if complete(S) .
    cq deducible((X @ runnable(S)) |- (X ? entry(S))) = true
       if complete(S) .
    cq deducible((X block(S) X) |- nil) = true
       if complete(S) .
  }
}
```

* ((x block(s) y) |- (x @ executed(s)))

```
#!python
open BASE + LK .
[ T < Ξblock Ξexecuted ]
-- Enter, Leave ⊆ T
ops s : -> System .
ops f : -> T .
ops x y : -> Entity .
ops claim : -> Prop .
eq claim = deducible((x block(f(s)) y) |- (x @ executed(f(s)))) .
eq deducible((x block(s) y) |- (x @ executed(s))) = true .
eq complete(f(s)) = true .

ops i : -> Inference .
ops q1 q2 q3 : -> Sequent .
eq q1 = ((x block(s) y) |- (x @ executed(s))) .
eq q2 = ((x block(f(s)) y) |- (x block(s) y)) .
eq q3 = ((x @ executed(s)) |- (x @ executed(f(s)))) .
eq antecedent(i) = (q1,q2,q3) .
eq ((x block(f(s)) y) |- (x @ executed(f(s)))) = consequent(i) .
red claim .
close
```
```
#!python
%LK + BASE> *
-- reduce in %LK + BASE : (claim):Prop

** Found [state 317] (consequent(i)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 3547 rewrites(1.480 sec), 155336 matches, 1465 memo hits)
```
```
#!python
open BASE + LK .
ops s : -> System .
ops f : -> Run .
ops x y : -> Entity .
ops claim : -> Prop .
eq claim = deducible((x block(f(s)) y) |- (x @ executed(f(s)))) .
eq deducible((x block(s) y) |- (x @ executed(s))) = true .
eq complete(f(s)) = true .

ops i : -> Inference .
ops q1 q2 q3 : -> Sequent .
eq q1 = ((x block(s) y) |- (x @ executed(s))) .
eq q2 = ((x block(f(s)) y) |- (x block(s) y)) .
eq q3 = ((x @ executed(s)) |- (x @ executed(f(s)))) .
eq antecedent(i) = (q1,q2,q3) .
eq ((x block(f(s)) y) |- (x @ executed(f(s)))) = consequent(i) .
red claim .
close
```
```
#!python
%LK + BASE> *
-- reduce in %LK + BASE : (claim):Prop

** Found [state 288] (consequent(i)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 2793 rewrites(1.730 sec), 134278 matches, 1224 memo hits)
```
```
#!python
open BASE + LK .
ops s : -> System .
ops f : -> Exit .
ops x y : -> Entity .
ops claim : -> Prop .
eq claim = deducible((x block(f(s)) y) |- (x @ executed(f(s)))) .
eq deducible((x block(s) y) |- (x @ executed(s))) = true .
eq complete(f(s)) = true .

ops i1 : -> Inference .
ops q11 q12 q13 : -> Sequent .
eq q11 = ((x block(s) y) |- (x @ executed(s))) .
eq q12 = ((x = exit(f)),(x block(s) y) |- nil) . 
eq q13 = ((x @ executed(s)) |- (x = exit(f)),(x @ executed(f(s)))) .
eq antecedent(i1) = (q11,q12,q13) .
trans ((x block(s) y) |- (x @ executed(f(s)))) => consequent(i1) .
trans consequent(i1) => ((x block(s) y) |- (x @ executed(f(s)))) .

ops i2 : -> Inference .
ops q21 : -> Sequent .
eq q21 = ((x block(f(s)) y) |- (x block(s) y)) .
eq antecedent(i2) = (consequent(i1),q21) .
eq ((x block(f(s)) y) |- (x @ executed(f(s)))) = consequent(i2) .
red claim .
close
```
```
#!python
%LK + BASE> *
-- reduce in %LK + BASE : (claim):Prop

** Found [state 10] (consequent(i2)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 315] (consequent(i1)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 6965 rewrites(2.410 sec), 433025 matches, 3497 memo hits)
```
```
#!python
open STRUCTURE + LK .
ops s : -> System .
ops f : -> Prevent .
ops x y : -> Entity .
ops claim : -> Prop .
eq claim = deducible((x block(f(s)) y) |- (x @ executed(f(s)))) .
eq deducible((x block(s) y) |- (x @ executed(s))) = true .
eq complete(s) = true .
eq complete(f(s)) = true .

ops i1 : -> Inference .
ops q11 q12 q13 : -> Sequent .
eq q11 = ((x block(s) y) |- (x @ executed(s))) .
eq q12 = ((x block(f(s)) y) |- (x block(s) y),(x @ current(s))) . 
eq q13 = ((x @ current(s)) |- (x @ executed(s))) . 
eq antecedent(i1) = (q11,q12,q13) .
trans ((x block(f(s)) y) |- (x @ executed(s))) => consequent(i1) .
trans consequent(i1) => ((x block(f(s)) y) |- (x @ executed(s))) .

ops i2 : -> Inference .
ops q21 : -> Sequent .
eq q21 = ((x @ executed(s)) |- (x @ executed(f(s)))) .
eq antecedent(i2) = (consequent(i1),q21) .
eq ((x block(f(s)) y) |- (x @ executed(f(s)))) = consequent(i2) .
red claim .
close
```
```
#!python
%LK + BASE> *
-- reduce in %LK + BASE : (claim):Prop

** Found [state 10] (consequent(i2)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 2016] (consequent(i1)):Set/Sequent
   {}
-- found required number of solutions 1.
(deducible(consequent(i2))):Prop
(0.000 sec for parse, 6337 rewrites(7.860 sec), 418586 matches, 3037 memo hits)
```
```
#!python
open BASE + LK .
ops s : -> System .
ops f : -> Free .
ops x y : -> Entity .
ops claim : -> Prop .
eq claim = deducible((x block(f(s)) y) |- (x @ executed(f(s)))) .
eq deducible((x block(s) y) |- (x @ executed(s))) = true .
eq complete(f(s)) = true .

ops i : -> Inference .
ops q1 q2 q3 : -> Sequent .
eq q1 = ((x block(s) y) |- (x @ executed(s))) .
eq q2 = ((x block(f(s)) y) |- (x block(s) y)) . 
eq q3 = ((x @ executed(s)) |- (x @ executed(f(s)))) .
eq antecedent(i) = (q1,q2,q3) .
eq ((x block(f(s)) y) |- (x @ executed(f(s)))) = consequent(i) .
red claim .
close
```
```
#!python
%LK + BASE> *
-- reduce in %LK + BASE : (claim):Prop

** Found [state 288] (consequent(i)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 2793 rewrites(1.330 sec), 133998 matches, 1224 memo hits)
```
```
#!python
module STRUCTURE
{
  imports
  {
    pr(BASE)
  }
  axioms
  {
    vars S : System
    vars X Y : Entity
    cq deducible((X @ current(S)) |- (X @ executed(S))) = true
       if complete(S) .
    cq deducible((X @ executed(S)) |- (X @ runnable(S))) = true
       if complete(S) .
    cq deducible((X @ runnable(S)) |- (X ? entry(S))) = true
       if complete(S) .
    cq deducible((X block(S) X) |- nil) = true
       if complete(S) .
    cq deducible((X block(S) Y) |- (X @ executed(S))) = true
       if complete(S) .
  }
}
```

* (nil |- (x @ executed(s)),(priority(x)(s) = assign(x)))

```
#!python
open BASE + EQUALITY/EQUALITY/NUMBER + LK .
[ T < Ξexecuted Ξpriority ]
-- Leave, Enter ⊆ T
ops s : -> System .
ops f : -> T .
ops x y : -> Entity .
ops claim : -> Prop .
eq claim = deducible(nil |- (x @ executed(f(s))),(priority(x)(f(s)) = assign(x))) .
eq deducible(nil |- (x @ executed(s)),(priority(x)(s) = assign(x))) = true .
eq complete(f(s)) = true .

ops i1 : -> Inference .
ops q11 q12 q13 : -> Sequent .
eq q11 = (nil |- (x @ executed(s)),(priority(x)(s) = assign(x))) .
eq q12 = (nil |- (priority(x)(s) = priority(x)(f(s)))) . 
eq q13 = ((priority(x)(s) = assign(x)),(priority(x)(s) = priority(x)(f(s))) |- (priority(x)(f(s)) = assign(x))) .
eq antecedent(i1) = (q11,q12,q13) .
trans (nil |- (x @ executed(s)),(priority(x)(f(s)) = assign(x))) => consequent(i1) .
trans consequent(i1) => (nil |- (x @ executed(s)),(priority(x)(f(s)) = assign(x))) .

ops i2 : -> Inference .
ops q21 : -> Sequent .
eq q21 = ((x @ executed(s)) |- (x @ executed(f(s)))) .
eq antecedent(i2) = (consequent(i1),q21) .
eq (nil |- (x @ executed(f(s))),(priority(x)(f(s)) = assign(x))) = consequent(i2) .
red claim .
close
```
```
#!python
%LK + EQUALITY/EQUALITY/NUMBER + BASE> *
-- reduce in %LK + EQUALITY/EQUALITY/NUMBER + BASE : 
    (claim):Prop

** Found [state 10] (consequent(i2)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 277] (consequent(i1)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 6848 rewrites(2.030 sec), 296208 matches, 2853 memo hits)
```
```
#!python
open BASE + EQUALITY/EQUALITY/NUMBER + LK .
ops s : -> System .
ops f : -> Run .
ops x y : -> Entity .
ops claim : -> Prop .
eq claim = deducible(nil |- (x @ executed(f(s))),(priority(x)(f(s)) = assign(x))) .
eq deducible(nil |- (x @ executed(s)),(priority(x)(s) = assign(x))) = true .
eq complete(f(s)) = true .

ops i1 : -> Inference .
ops q11 q12 q13 : -> Sequent .
eq q11 = (nil |- (x @ executed(s)),(priority(x)(s) = assign(x))) .
eq q12 = (nil |- (priority(x)(s) = priority(x)(f(s)))) . 
eq q13 = ((priority(x)(s) = assign(x)),(priority(x)(s) = priority(x)(f(s))) |- (priority(x)(f(s)) = assign(x))) .
eq antecedent(i1) = (q11,q12,q13) .
trans (nil |- (x @ executed(s)),(priority(x)(f(s)) = assign(x))) => consequent(i1) .
trans consequent(i1) => (nil |- (x @ executed(s)),(priority(x)(f(s)) = assign(x))) .

ops i2 : -> Inference .
ops q21 : -> Sequent .
eq q21 = ((x @ executed(s)) |- (x @ executed(f(s)))) .
eq antecedent(i2) = (consequent(i1),q21) .
eq (nil |- (x @ executed(f(s))),(priority(x)(f(s)) = assign(x))) = consequent(i2) .
red claim .
close
```
```
#!python
%LK + EQUALITY/EQUALITY/NUMBER + BASE> *
-- reduce in %LK + EQUALITY/EQUALITY/NUMBER + BASE : 
    (claim):Prop

** Found [state 9] (consequent(i2)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 277] (consequent(i1)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 6828 rewrites(1.990 sec), 295870 matches, 2849 memo hits)
```

```
#!python
open BASE + IMAGE/ENTITY + EQUALITY/EQUALITY/NUMBER + LK .
ops s : -> System .
ops f : -> Exit .
ops x y : -> Entity .
ops claim : -> Prop .
eq claim = deducible(nil |- (x @ executed(f(s))),(priority(x)(f(s)) = assign(x))) .
eq deducible(nil |- (x @ executed(s)),(priority(x)(s) = assign(x))) = true .
eq complete(f(s)) = true .
eq complete(s) = true .

ops i1 : -> Inference .
ops q11 q12 : -> Sequent .
eq q11 = ((x = exit(f)) |- (block(s)[x] = nil)) .
eq q12 = ((block(s)[x] = nil) |- (priority(x)(s) = assign(x))) .
eq antecedent(i1) = (q11,q12) .
trans ((x = exit(f)) |- (priority(x)(s) = assign(x))) => consequent(i1) .
trans consequent(i1) => ((x = exit(f)) |- (priority(x)(s) = assign(x))) .

ops i2 : -> Inference .
ops q21 q22 : -> Sequent .
eq q21 = (nil |- (x @ executed(s)),(priority(x)(s) = assign(x))) .
eq q22 = ((x @ executed(s)) |- (x @ executed(f(s))),(x = exit(f))) .
eq antecedent(i2) = (consequent(i1),q21,q22) .
trans (nil |- (x @ executed(f(s))),(priority(x)(s) = assign(x))) => consequent(i2) .
trans consequent(i2) => (nil |- (x @ executed(f(s))),(priority(x)(s) = assign(x))) .

ops i3 : -> Inference .
ops q31 q32 : -> Sequent .
eq q31 = (nil |- (priority(x)(s) = priority(x)(f(s)))) . 
eq q32 = ((priority(x)(s) = assign(x)),(priority(x)(s) = priority(x)(f(s))) |- (priority(x)(f(s)) = assign(x))) .
eq antecedent(i3) = (consequent(i2),q31,q32) .
eq (nil |- (x @ executed(f(s))),(priority(x)(f(s)) = assign(x))) = consequent(i3) .
red claim .
close
```
```
#!python
%LK + IMAGE/ENTITY + EQUALITY/EQUALITY/NUMBER + BASE> red claim .
*
-- reduce in %LK + IMAGE/ENTITY + EQUALITY/EQUALITY/NUMBER + BASE : 
    (claim):Prop

** Found [state 123] (consequent(i3)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 3467] (consequent(i2)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 34] (consequent(i1)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.010 sec for parse, 18671 rewrites(16.880 sec), 1225860 matches, 10003 memo hits)
```
```
#!python
open STRUCTURE + EQUALITY/EQUALITY/NUMBER + LK .
ops s : -> System .
ops f : -> Adjust .
ops x y : -> Entity .
ops claim : -> Prop .
eq claim = deducible(nil |- (x @ executed(f(s))),(priority(x)(f(s)) = assign(x))) .
eq deducible(nil |- (x @ executed(s)),(priority(x)(s) = assign(x))) = true .
eq complete(f(s)) = true .
eq complete(s) = true .

ops i1 : -> Inference .
ops q11 q12 : -> Sequent .
eq q11 = (nil |- (x @ current(s)),(priority(x)(s) = priority(x)(f(s)))) . 
eq q12 = ((x @ current(s)) |- (x @ executed(s))) .
eq antecedent(i1) = (q11,q12) .
trans (nil |- (x @ executed(s)),(priority(x)(s) = priority(x)(f(s)))) => consequent(i1) .
trans consequent(i1) => (nil |- (x @ executed(s)),(priority(x)(s) = priority(x)(f(s)))) .

ops i2 : -> Inference .
ops q21 q22 : -> Sequent .
eq q21 = (nil |- (x @ executed(s)),(priority(x)(s) = assign(x))) .
eq q22 = ((priority(x)(s) = assign(x)),(priority(x)(s) = priority(x)(f(s))) |- (priority(x)(f(s)) = assign(x))) .
eq antecedent(i2) = (consequent(i1),q21,q22) .
trans (nil |- (x @ executed(s)),(priority(x)(f(s)) = assign(x))) => consequent(i2) .
trans consequent(i2) => (nil |- (x @ executed(s)),(priority(x)(f(s)) = assign(x))) .

ops i3 : -> Inference .
ops q31 : -> Sequent .
eq q31 = ((x @ executed(s)) |- (x @ executed(f(s)))) .
eq antecedent(i3) = (consequent(i2),q31) .
eq (nil |- (x @ executed(f(s))),(priority(x)(f(s)) = assign(x))) = consequent(i3) .
red claim .
close
```
```
#!python
%STRUCTURE + LK + EQUALITY/EQUALITY/NUMBER> red claim .
*
-- reduce in %STRUCTURE + LK + EQUALITY/EQUALITY/NUMBER : 
    (claim):Prop

** Found [state 10] (consequent(i3)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 1223] (consequent(i2)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 34] (consequent(i1)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 21392 rewrites(12.710 sec), 1358869 matches, 12178 memo hits)
```
```
#!python
module STRUCTURE
{
  imports
  {
    pr(BASE)
  }
  axioms
  {
    vars S : System
    vars X Y : Entity
    cq deducible((X @ current(S)) |- (X @ executed(S))) = true
       if complete(S) .
    cq deducible((X @ executed(S)) |- (X @ runnable(S))) = true
       if complete(S) .
    cq deducible((X @ runnable(S)) |- (X ? entry(S))) = true
       if complete(S) .
    cq deducible((X block(S) X) |- nil) = true
       if complete(S) .
    cq deducible((X block(S) Y) |- (X @ executed(S))) = true
       if complete(S) .
    cq deducible(nil |- (X @ executed(S)),(priority(X)(S) = assign(X))) = true
       if complete(S) .
  }
}
```

* ((x block(s) y),(assign(y) > priority(x)(s)) |- nil)

This sequent has been already declared as an axiom in the module PRIORITY-CEILING:
```
#!python
open BASE .
ops s : -> System .
ops x y : -> Entity .
eq complete(s) = true .
red deducible((x block(s) y),(assign(y) > priority(x)(s)) |- nil) .
close
```
```
#!python
%BASE> *
-- reduce in %BASE : (deducible((((x (block s) y) , (assign(y) > (priority(x) s))) |- nil))):Prop
(true):Bool
(0.000 sec for parse, 2 rewrites(0.000 sec), 21 matches)
```

We prove that the following two sequents can be deduced simultaneously 
using structural induction on the base structure.

* ((x @ current(s)),(x ahead(s) y),(y @ executed(s)) |- nil)
* ((x @ executed(s)),(y ahead(s) x) |- (x prior(s) y))


First of all, 
we prove the first sequent can be deducible.
```
#!python
open BASE + LK .
ops s : -> System .
ops f : -> Stop .
-- Leave, Exit ⊆ Stop
ops x y : -> Entity .
eq deducible((x @ current(s)),(x ahead(s) y),(y @ executed(s)) |- nil) = true .
eq complete(f(s)) = true .
ops claim : -> Prop .
eq claim = deducible((x @ current(f(s))),(x ahead(f(s)) y),(y @ executed(f(s))) |- nil) .
red claim .
close
```
```
#!python
%LK + BASE> *
-- reduce in %LK + BASE : (claim):Prop
(true):Bool
(0.000 sec for parse, 5 rewrites(0.000 sec), 152 matches)
```
```
#!python
open BASE + LK .
[ T < Ξcurrent Ξentry Ξexecuted ]
-- Prevent, Free ⊆ T
ops s : -> System .
ops f : -> T .
ops x y : -> Entity .
eq deducible((x @ current(s)),(x ahead(s) y),(y @ executed(s)) |- nil) = true .
eq complete(f(s)) = true .
ops claim : -> Prop .
eq claim = deducible((x @ current(f(s))),(x ahead(f(s)) y),(y @ executed(f(s))) |- nil) .

ops i1 : -> Inference .
ops q11 q12 q13 : -> Sequent .
eq q11 = ((x @ current(s)),(x ahead(s) y),(y @ executed(s)) |- nil) .
eq q12 = ((x @ current(f(s))) |- (x @ current(s))) .
eq q13 = ((y @ executed(f(s))) |- (y @ executed(s))) .
eq antecedent(i1) = (q11,q12,q13) .
trans ((x @ current(f(s))),(x ahead(s) y),(y @ executed(f(s))) |- nil) => consequent(i1) .
trans consequent(i1) => ((x @ current(f(s))),(x ahead(s) y),(y @ executed(f(s))) |- nil) .

ops i2 : -> Inference .
ops q21 : -> Sequent .
eq q21 = ((x ahead(f(s)) y) |- (x ahead(s) y)) .
eq antecedent(i2) = (consequent(i1),q21) .
eq ((x @ current(f(s))),(x ahead(f(s)) y),(y @ executed(f(s))) |- nil) = consequent(i2) .
red claim .
close
```
```
#!python
%LK + BASE> red claim .
-- reduce in %LK + BASE : (claim):Prop

** Found [state 11] (consequent(i2)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 9863] (consequent(i1)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 84702 rewrites(85.100 sec), 5510050 matches, 39192 memo hits)
```
```
#!python
open STRUCTURE + LK .
ops s : -> System .
ops f : -> Enter .
ops x y : -> Entity .
eq deducible((x @ current(s)),(x ahead(s) y),(y @ executed(s)) |- nil) = true .
eq complete(s) = true .
eq complete(f(s)) = true .
ops claim : -> Prop .
eq claim = deducible((x @ current(f(s))),(x ahead(f(s)) y),(y @ executed(f(s))) |- nil) .

ops i1 : -> Inference .
ops q11 q12 q13 : -> Sequent .
eq q11 = ((x ahead(f(s)) y),(y ? entry(s)) |- (x ahead(s) y)) .
eq q12 = ((y @ executed(s)) |- (y @ runnable(s))) .
eq q13 = ((y @ runnable(s)) |- (y ? entry(s))) .
eq antecedent(i1) = (q11,q12,q13) .
trans ((x ahead(f(s)) y),(y @ executed(s)) |- (x ahead(s) y)) => consequent(i1) .
trans consequent(i1) => ((x ahead(f(s)) y),(y @ executed(s)) |- (x ahead(s) y)) .

ops i2 : -> Inference .
ops q21 : -> Sequent .
eq q21 = ((x @ current(s)),(x ahead(s) y),(y @ executed(s)) |- nil) .
eq antecedent(i2) = (consequent(i1),q21) .
trans ((x @ current(s)),(x ahead(f(s)) y),(y @ executed(s)) |- nil) => consequent(i2) .
trans consequent(i2) => ((x @ current(s)),(x ahead(f(s)) y),(y @ executed(s)) |- nil) .

ops i3 : -> Inference .
ops q31 q32 : -> Sequent .
eq q31 = ((x @ current(f(s))) |- (x @ current(s))) .
eq q32 = ((y @ executed(f(s))) |- (y @ executed(s))) .
eq antecedent(i3) = (consequent(i2),q31,q32) .
eq ((x @ current(f(s))),(x ahead(f(s)) y),(y @ executed(f(s))) |- nil) = consequent(i3) .
red claim .
close
```
```
#!python
%STRUCTURE + LK> red claim .
-- reduce in %STRUCTURE + LK : (claim):Prop

** Found [state 1397] (consequent(i3)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 158] (consequent(i2)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 1594] (consequent(i1)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 19721 rewrites(19.440 sec), 1323212 matches, 9448 memo hits)
```
```
#!python
make EQUALITY/EQUALITY/ENTITY
(
  EQUALITY/EQUALITY(
    ENTITY { sort Elt -> Entity }
  )
)
```
```
#!python
open STRUCTURE + EQUALITY/EQUALITY/ENTITY + LK .
ops s : -> System .
ops f : -> Run .
ops x y : -> Entity .
eq deducible((x @ current(s)),(x ahead(s) y),(y @ executed(s)) |- nil) = true .
eq deducible((y @ executed(s)),(x ahead(s) y) |- (y prior(s) x)) = true .
eq complete(f(s)) = true .
eq complete(s) = true .
ops claim : -> Prop .
eq claim = deducible((x @ current(f(s))),(x ahead(f(s)) y),(y @ executed(f(s))) |- nil) .

ops i1 : -> Inference .
ops q11 q12 q13 : -> Sequent .
eq q11 = ((x = run(f)) |- (x @ root(runnable(s),[prior(s);ahead(s)]))) .
eq q12 = ((x @ root(runnable(s),[prior(s);ahead(s)])),(y @ runnable(s)),(y [prior(s);ahead(s)] x) |- nil) .
eq q13 = ((y @ executed(s)) |- (y @ runnable(s))) .
eq antecedent(i1) = (q11,q12,q13) .
trans ((x = run(f)),(y @ executed(s)),(y [prior(s);ahead(s)] x) |- nil) => consequent(i1) .
trans consequent(i1) => ((x = run(f)),(y @ executed(s)),(y [prior(s);ahead(s)] x) |- nil) .

ops i2 : -> Inference .
ops q21 q22 : -> Sequent .
eq q21 = ((y @ executed(s)),(x ahead(s) y) |- (y prior(s) x)) .
eq q22 = ((y prior(s) x) |- (y [prior(s);ahead(s)] x)) .
eq antecedent(i2) = (consequent(i1),q21,q22) .
trans ((x = run(f)),(x ahead(s) y),(y @ executed(s)) |- nil) => consequent(i2) .
trans consequent(i2) => ((x = run(f)),(x ahead(s) y),(y @ executed(s)) |- nil) .

ops i3 : -> Inference .
ops q31 q32 q33 : -> Sequent .
eq q31 = ((x ahead(s) y),(x = y) |- (x ahead(s) x)) .
eq q32 = ((x ahead(s) x) |- nil) .
eq q33 = ((x = run(f)),(y = run(f)) |- (x = y)) .
eq antecedent(i3) = (q31,q32,q33) .
trans ((x = run(f)),(y = run(f)),(x ahead(s) y) |- nil) => consequent(i3) .
trans consequent(i3) => ((x = run(f)),(y = run(f)),(x ahead(s) y) |- nil) .

ops i4 : -> Inference .
ops q41 : -> Sequent .
eq q41 = ((y @ executed(f(s))) |- (y @ executed(s)),(y = run(f))) .
eq antecedent(i4) = (consequent(i2),consequent(i3),q41) .
trans ((x = run(f)),(x ahead(s) y),(y @ executed(f(s))) |- nil) => consequent(i4) .
trans consequent(i4) => ((x = run(f)),(x ahead(s) y),(y @ executed(f(s))) |- nil) .

ops i5 : -> Inference .
ops q51 q52 : -> Sequent .
eq q51 = ((x ahead(f(s)) y) |- (x ahead(s) y)) .
eq q52 = ((x @ current(f(s))) |- (x = run(f))) .
eq antecedent(i5) = (consequent(i4),q51,q52) .
eq ((x @ current(f(s))),(x ahead(f(s)) y),(y @ executed(f(s))) |- nil) = consequent(i5) .
red claim .
close
```
```
#!python
%STRUCTURE + LK + EQUALITY/EQUALITY/ENTITY> red claim .
-- reduce in %STRUCTURE + LK + EQUALITY/EQUALITY/ENTITY : 
    (claim):Prop

** Found [state 1212] (consequent(i5)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 4766] (consequent(i4)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 15094] (consequent(i3)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 6326] (consequent(i2)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 2131] (consequent(i1)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 217880 rewrites(323.210 sec), 14817309 matches, 124380 memo hits)
```

Then, 
we prove that the second sequent can be deducible.

To prove that, we need the following lemma.

For any s : System, x,y : Entity and f : Ξpriority, 
the two propositions (x prior(s) y) and (x prior(f(s)) are equivalent to each other.

* ((x prior(s) y) |- (x prior(f(s)) y))
* ((x prior(s) y) |- (x prior(f(s)) y))

```
#!python
open BASE + LK .
ops s : -> System .
ops f : -> Ξpriority .
ops x y : -> Entity .
ops claim : -> Prop .
eq claim = deducible((x prior(s) y) |- (x prior(f(s)) y)) .
eq complete(f(s)) = true .

ops i1 : -> Inference .
ops q11 q12 q13 q14 : -> Sequent .
eq q11 = (nil |- (priority(x)(s) = priority(x)(f(s)))) .
eq q12 = ((priority(x)(s) = priority(x)(f(s))),(priority(x)(s) > priority(y)(s))
          |- (priority(x)(f(s)) > priority(y)(s))) .
eq antecedent(i1) = (q11,q12) .
trans ((priority(x)(s) > priority(y)(s)) |- (priority(x)(f(s)) > priority(y)(s))) => consequent(i1) .
trans consequent(i1) => ((priority(x)(s) > priority(y)(s)) |- (priority(x)(f(s)) > priority(y)(s))) .

ops i2 : -> Inference .
ops q21 q22 : -> Sequent .
eq q21 = (nil |- (priority(y)(s) = priority(y)(f(s)))) .
eq q22 = ((priority(y)(s) = priority(y)(f(s))),(priority(x)(f(s)) > priority(y)(s))
          |- (priority(x)(f(s)) > priority(y)(f(s)))) .
eq antecedent(i2) = (q21,q22) .
trans ((priority(x)(f(s)) > priority(y)(s)) |- (priority(x)(f(s)) > priority(y)(f(s)))) => consequent(i2) .
trans consequent(i2) => ((priority(x)(f(s)) > priority(y)(s)) |- (priority(x)(f(s)) > priority(y)(f(s)))) .

ops i3 : -> Inference .
eq antecedent(i3) = (consequent(i1),consequent(i2)) .
trans ((priority(x)(s) > priority(y)(s)) |- (priority(x)(f(s)) > priority(y)(f(s)))) => consequent(i3) .
trans consequent(i3) => ((priority(x)(s) > priority(y)(s)) |- (priority(x)(f(s)) > priority(y)(f(s)))) .

ops i4 : -> Inference .
ops q41 q42 : -> Sequent .
eq q41 = ((x prior(s) y) |- (priority(x)(s) > priority(y)(s))) .
eq q42 = ((priority(x)(f(s)) > priority(y)(f(s))) |- (x prior(f(s)) y)) .
eq antecedent(i4) = (consequent(i3),q41,q42) .
eq ((x prior(s) y) |- (x prior(f(s)) y)) = consequent(i4) .
red claim .
close
```
```
#!python
%LK + BASE> red claim .
*
-- reduce in %LK + BASE : (claim):Prop

** Found [state 794] (consequent(i4)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 135] (consequent(i3)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 45] (consequent(i2)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 37] (consequent(i1)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 11536 rewrites(5.220 sec), 257514 matches, 4934 memo hits)
```
```
#!python
module LEMMA/ΞPRIORITY
{
  imports
  {
    pr(ΞPRIORITY)
  }
  axioms
  {
    vars S : System
    vars F : Ξpriority
    vars X Y : Entity
    cq deducible((X prior(S) Y) |- (X prior(F(S)) Y)) = true
       if complete(F(S)) .
    cq deducible((X prior(F(S)) Y) |- (X prior(S) Y)) = true
       if complete(F(S)) .
  }
}
```
```
#!python
open BASE + LK + LEMMA/ΞPRIORITY .
ops s : -> System .
ops f : -> Leave .
ops x y : -> Entity .
eq deducible((x @ executed(s)),(y ahead(s) x) |- (x prior(s) y)) = true .
eq complete(f(s)) = true .
ops claim : -> Prop .
eq claim = deducible((x @ executed(f(s))),(y ahead(f(s)) x) |- (x prior(f(s)) y)) .

ops i1 : -> Inference .
ops q11 q12 q13 : -> Sequent .
eq q11 = ((x @ executed(s)),(y ahead(s) x) |- (x prior(s) y)) .
eq q12 = ((x @ executed(f(s))) |- (x @ executed(s))) .
eq q13 = ((y ahead(f(s)) x) |- (y ahead(s) x)) .
eq antecedent(i1) = (q11,q12,q13) .
trans ((x @ executed(f(s))),(y ahead(f(s)) x) |- (x prior(s) y)) => consequent(i1) .
trans consequent(i1) => ((x @ executed(f(s))),(y ahead(f(s)) x) |- (x prior(s) y)) .

ops i2 : -> Inference .
ops q21 : -> Sequent .
eq q21 = ((x prior(s) y) |- (x prior(f(s)) y)) .
eq antecedent(i2) = (consequent(i1),q21) .
eq ((x @ executed(f(s))),(y ahead(f(s)) x) |- (x prior(f(s)) y)) = consequent(i2) .
red claim .
close
```
```
#!python
%LK + LEMMA/ΞPRIORITY + BASE> red claim .
-- reduce in %LK + LEMMA/ΞPRIORITY + BASE : (claim):Prop

** Found [state 11] (consequent(i2)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 6531] (consequent(i1)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 56687 rewrites(53.110 sec), 3026399 matches, 28104 memo hits)
```
```
#!python
open BASE + LK + LEMMA/ΞPRIORITY .
ops s : -> System .
ops f : -> Run .
ops x y : -> Entity .
eq deducible((x @ executed(s)),(y ahead(s) x) |- (x prior(s) y)) = true .
eq complete(f(s)) = true .
eq deducible(nil |- (x @ runnable(s))) = true .
eq deducible(nil |- (y @ runnable(s))) = true .
ops claim : -> Prop .
eq claim = deducible((x @ executed(f(s))),(y ahead(f(s)) x) |- (x prior(f(s)) y)) .

ops i1 : -> Inference .
ops q11 q12 : -> Sequent .
eq q11 = (nil |- (y @ runnable(s))) .
eq q12 = ((x @ root(runnable(s),[prior(s);ahead(s)])),(y @ runnable(s)),(y [prior(s);ahead(s)] x) |- nil) .
eq antecedent(i1) = (q11,q12) .
trans ((x @ root(runnable(s),[prior(s);ahead(s)])),(y [prior(s);ahead(s)] x) |- nil) => consequent(i1) .
trans consequent(i1) => ((x @ root(runnable(s),[prior(s);ahead(s)])),(y [prior(s);ahead(s)] x) |- nil) .

ops i2 : -> Inference .
ops q21 q22 : -> Sequent .
eq q21 = ((x = run(f)) |- (x @ root(runnable(s),[prior(s);ahead(s)]))) .
eq q22 = ((y ahead(s) x) |- (y [prior(s);ahead(s)] x),(x prior(s) y)) .
eq antecedent(i2) = (consequent(i1),q21,q22) .
trans ((x = run(f)),(y ahead(s) x) |- (x prior(s) y)) => consequent(i2) .
trans consequent(i2) => ((x = run(f)),(y ahead(s) x) |- (x prior(s) y)) .

ops i3 : -> Inference .
ops q31 q32 : -> Sequent .
eq q31 = ((x @ executed(s)),(y ahead(s) x) |- (x prior(s) y)) .
eq q32 = ((x @ executed(f(s))) |- (x = run(f)),(x @ executed(s))) .
eq antecedent(i3) = (consequent(i2),q31,q32) .
trans ((x @ executed(f(s))),(y ahead(s) x) |- (x prior(s) y)) => consequent(i3) .
trans consequent(i3) => ((x @ executed(f(s))),(y ahead(s) x) |- (x prior(s) y)) .

ops i4 : -> Inference .
ops q41 q42 : -> Sequent .
eq q41 = ((y ahead(f(s)) x) |- (y ahead(s) x)) .
eq q42 = ((x prior(s) y) |- (x prior(f(s)) y)) .
eq antecedent(i4) = (consequent(i3),q41,q42) .
eq ((x @ executed(f(s))),(y ahead(f(s)) x) |- (x prior(f(s)) y)) = consequent(i4) .
red claim .
close
```
```
#!python
%LK + LEMMA/ΞPRIORITY + BASE> red claim .
-- reduce in %LK + LEMMA/ΞPRIORITY + BASE : (claim):Prop

** Found [state 1063] (consequent(i4)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 2937] (consequent(i3)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 1185] (consequent(i2)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 28] (consequent(i1)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 104667 rewrites(83.520 sec), 6443250 matches, 57418 memo hits)
```
```
#!python
open STRUCTURE + LK + LEMMA/ΞPRIORITY .
ops s : -> System .
ops f : -> Enter .
ops x y : -> Entity .
eq deducible((x @ executed(s)),(y ahead(s) x) |- (x prior(s) y)) = true .
eq complete(f(s)) = true .
eq complete(s) = true .
ops claim : -> Prop .
eq claim = deducible((x @ executed(f(s))),(y ahead(f(s)) x) |- (x prior(f(s)) y)) .

ops i1 : -> Inference .
ops q11 q12 q13 : -> Sequent .
eq q11 = ((x @ executed(s)) |- (x @ runnable(s))) .
eq q12 = ((x @ runnable(s)) |- (x ? entry(s))) .
eq q13 = ((y ahead(f(s)) x),(x ? entry(s)) |- (y ahead(s) x)) .
eq antecedent(i1) = (q11,q12,q13) .
trans ((x @ executed(s)),(y ahead(f(s)) x) |- (y ahead(s) x)) => consequent(i1) .
trans consequent(i1) => ((x @ executed(s)),(y ahead(f(s)) x) |- (y ahead(s) x)) .

ops i2 : -> Inference .
ops q21 : -> Sequent .
eq q21 = ((x @ executed(s)),(y ahead(s) x) |- (x prior(s) y)) .
eq antecedent(i2) = (consequent(i1),q21) .
trans ((x @ executed(s)),(y ahead(f(s)) x) |- (x prior(s) y)) => consequent(i2) .
trans consequent(i2) => ((x @ executed(s)),(y ahead(f(s)) x) |- (x prior(s) y)) .

ops i3 : -> Inference .
ops q31 q32 : -> Sequent .
eq q31 = ((x @ executed(f(s))) |- (x @ executed(s))) .
eq q32 = ((x prior(s) y) |- (x prior(f(s)) y)) .
eq antecedent(i3) = (consequent(i2),q31,q32) .
eq ((x @ executed(f(s))),(y ahead(f(s)) x) |- (x prior(f(s)) y)) = consequent(i3) .
red claim .
close
```
```
#!python
%STRUCTURE + LK + LEMMA/ΞPRIORITY> red claim .
-- reduce in %STRUCTURE + LK + LEMMA/ΞPRIORITY : (claim):Prop

** Found [state 1312] (consequent(i3)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 160] (consequent(i2)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 2083] (consequent(i1)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 16308 rewrites(20.570 sec), 1013867 matches, 7817 memo hits)
```
```
#!python
open BASE + LK + LEMMA/ΞPRIORITY .
ops s : -> System .
ops f : -> Exit .
ops x y : -> Entity .
eq deducible((x @ executed(s)),(y ahead(s) x) |- (x prior(s) y)) = true .
eq complete(f(s)) = true .
ops claim : -> Prop .
eq claim = deducible((x @ executed(f(s))),(y ahead(f(s)) x) |- (x prior(f(s)) y)) .

ops i1 : -> Inference .
ops q11 q12 q13 : -> Sequent .
eq q11 = ((x @ executed(s)),(y ahead(s) x) |- (x prior(s) y)) .
eq q12 = ((x @ executed(f(s))) |- (x @ executed(s))) .
eq q13 = ((y ahead(f(s)) x) |- (y ahead(s) x)) .
eq antecedent(i1) = (q11,q12,q13) .
trans ((x @ executed(f(s))),(y ahead(f(s)) x) |- (x prior(s) y)) => consequent(i1) .
trans consequent(i1) => ((x @ executed(f(s))),(y ahead(f(s)) x) |- (x prior(s) y)) .

ops i2 : -> Inference .
ops q21 : -> Sequent .
eq q21 = ((x prior(s) y) |- (x prior(f(s)) y)) .
eq antecedent(i2) = (consequent(i1),q21) .
eq ((x @ executed(f(s))),(y ahead(f(s)) x) |- (x prior(f(s)) y)) = consequent(i2) .
red claim .
close
```
```
#!python
%LK + LEMMA/ΞPRIORITY + BASE> *
-- reduce in %LK + LEMMA/ΞPRIORITY + BASE : (claim):Prop

** Found [state 11] (consequent(i2)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 5928] (consequent(i1)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 43254 rewrites(43.310 sec), 2618152 matches, 23605 memo hits)
```
```
#!python
make LEMMA1/TOTALORDER/NUMBER
(
  LEMMA1/TOTALORDER(
    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 }
  )
)
```
```
#!python
open BASE + LEMMA/ΞPRIORITY + LEMMA1/TOTALORDER/NUMBER .
ops s : -> System .
ops f : -> Prevent .
ops x y : -> Entity .
eq deducible((y @ current(s)),(y ahead(s) x),(x @ executed(s)) |- nil) = true .
eq deducible((x @ executed(s)),(y ahead(s) x) |- (x prior(s) y)) = true .
eq complete(f(s)) = true .
ops claim : -> Prop .
eq claim = deducible((x @ executed(f(s))),(y ahead(f(s)) x) |- (x prior(f(s)) y)) .

ops i1 : -> Inference .
ops q11 q12 q13 : -> Sequent .
eq q11 = ((x prior(s) y) |- (priority(x)(s) > priority(y)(s))) .
eq q12 = (nil |- (x @ current(s)),(priority(x)(s) = priority(x)(f(s)))) .
eq q13 = ((priority(x)(s) > priority(y)(s)),(priority(x)(s) = priority(x)(f(s)))
          |- (priority(x)(f(s)) > priority(y)(s))) .
eq antecedent(i1) = (q11,q12,q13) .
trans ((x prior(s) y) |- (x @ current(s)),(priority(x)(f(s)) > priority(y)(s))) => consequent(i1) .
trans consequent(i1) => ((x prior(s) y) |- (x @ current(s)),(priority(x)(f(s)) > priority(y)(s))) .

ops i2 : -> Inference .
ops q21 q22 : -> Sequent .
eq q21 = ((x @ current(s)),(priority(x)(s) > priority(x)(f(s))) |- nil) .
eq q22 = ((priority(x)(s) > priority(y)(s))
          |- (priority(x)(s) > priority(x)(f(s))),(priority(x)(f(s)) > priority(y)(s))) .
eq antecedent(i2) = (q11,q21,q22) .
trans ((x prior(s) y),(x @ current(s)) |- (priority(x)(f(s)) > priority(y)(s))) => consequent(i2) .
trans consequent(i2) => ((x prior(s) y),(x @ current(s)) |- (priority(x)(f(s)) > priority(y)(s))) .

ops i3 : -> Inference .
eq antecedent(i3) = (consequent(i1),consequent(i2)) .
trans ((x prior(s) y) |- (priority(x)(f(s)) > priority(y)(s))) => consequent(i3) .
trans consequent(i3) => ((x prior(s) y) |- (priority(x)(f(s)) > priority(y)(s))) .

ops i4 : -> Inference .
ops q41 : -> Sequent .
eq q41 = ((x @ executed(s)),(y ahead(s) x) |- (x prior(s) y)) .
eq antecedent(i4) = (consequent(i3),q41) .
trans ((x @ executed(s)),(y ahead(s) x) |- (priority(x)(f(s)) > priority(y)(s))) => consequent(i4) .
trans consequent(i4) => ((x @ executed(s)),(y ahead(s) x) |- (priority(x)(f(s)) > priority(y)(s))) .

ops i5 : -> Inference .
ops q51 q52 : -> Sequent .
eq q51 = (nil |- (y @ current(s)),(priority(y)(s) = priority(y)(f(s)))) .
eq q52 = ((y @ current(s)),(y ahead(s) x),(x @ executed(s)) |- nil) .
eq antecedent(i5) = (q51,q52) .
trans ((x @ executed(s)),(y ahead(s) x) |- (priority(y)(s) = priority(y)(f(s)))) => consequent(i5) .
trans consequent(i5) => ((x @ executed(s)),(y ahead(s) x) |- (priority(y)(s) = priority(y)(f(s)))) .

ops i6 : -> Inference .
ops q61 : -> Sequent .
eq q61 = ((priority(x)(f(s)) > priority(y)(s)),(priority(y)(s) = priority(y)(f(s)))
          |- (priority(x)(f(s)) > priority(y)(f(s)))) .
eq antecedent(i6) = (consequent(i4),q61) .
trans ((x @ executed(s)),(y ahead(s) x),(priority(y)(s) = priority(y)(f(s)))
       |- (priority(x)(f(s)) > priority(y)(f(s))))
   => consequent(i6) .
trans consequent(i6)
   => ((x @ executed(s)),(y ahead(s) x),(priority(y)(s) = priority(y)(f(s)))
       |- (priority(x)(f(s)) > priority(y)(f(s)))) .

ops i7 : -> Inference .
eq antecedent(i7) = (consequent(i5),consequent(i6)) .
trans ((x @ executed(s)),(y ahead(s) x) |- (priority(x)(f(s)) > priority(y)(f(s)))) => consequent(i7) .
trans consequent(i7) => ((x @ executed(s)),(y ahead(s) x) |- (priority(x)(f(s)) > priority(y)(f(s)))) .

ops i8 : -> Inference .
ops q81 : -> Sequent .
eq q81 = ((priority(x)(f(s)) > priority(y)(f(s))) |- (x prior(f(s)) y)) .
eq antecedent(i8) = (consequent(i7),q81) .
trans ((x @ executed(s)),(y ahead(s) x) |- (x prior(f(s)) y)) => consequent(i8) .
trans consequent(i8) => ((x @ executed(s)),(y ahead(s) x) |- (x prior(f(s)) y)) .

ops i9 : -> Inference .
ops q91 q92 : -> Sequent .
eq q91 = ((x @ executed(f(s))) |- (x @ executed(s))) .
eq q92 = ((y ahead(f(s)) x) |- (y ahead(s) x)) .
eq antecedent(i9) = (consequent(i8),q91,q92) .
eq ((x @ executed(f(s))),(y ahead(f(s)) x) |- (x prior(f(s)) y)) = consequent(i9) .
red claim .
close
```
```
#!python
%LEMMA1/TOTALORDER/NUMBER + LEMMA/ΞPRIORITY + BASE> red claim .
-- reduce in %LEMMA1/TOTALORDER/NUMBER + LEMMA/ΞPRIORITY + BASE : 
    (claim):Prop

** Found [state 972] (consequent(i9)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 82] (consequent(i8)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 416] (consequent(i7)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 179] (consequent(i6)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 99] (consequent(i4)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 204] (consequent(i3)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 326] (consequent(i2)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 327] (consequent(i1)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 17] (consequent(i5)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 27679 rewrites(14.760 sec), 1293287 matches, 13860 memo hits)
```