-- I) Base case

open INV
  red inv190(init,tag1,tag2,tag3,bfifo1,bfifo2) .
close

-- II) Inductive ceses

--> 1) send1(s)
open ISTEP
-- arbitrary objects
-- assumptions
-- successor state
  eq s' = send1(s) .
-- check if the predicate is true.
  red istep190(tag1,tag2,tag3,bfifo1,bfifo2) .
close

--> 2) rec1(s)
-- 2.1) c-rec1(s)
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-rec1(s) = true .
  eq empty?(fifo2(s)) = false .
--
  eq (get(fifo2(s)) = bfifo1 @ (tag1 | tag2 | bfifo2)) = false .
-- successor state
  eq s' = rec1(s) .
-- check if the predicate is true.
  red istep190(tag1,tag2,tag3,bfifo1,bfifo2) .
close
--
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-rec1(s) = true .
  eq empty?(fifo2(s)) = false .
--
  eq get(fifo2(s)) = bfifo1 @ (tag1 | tag2 | bfifo2) .
-- facts
  eq (fifo2(s) = top(fifo2(s)) | (bfifo1 @ (tag1 | tag2 | bfifo2))) = true .
-- successor state
  eq s' = rec1(s) .
-- check if the predicate is true.
  red inv190(s,tag1,tag2,tag3,(top(fifo2(s)) | bfifo1),bfifo2)
      implies istep190(tag1,tag2,tag3,bfifo1,bfifo2) .
close
--
-- 2.2) not c-rec1(s)
open ISTEP
-- arbitrary objects
-- assumptions
  eq c-rec1(s) = false .
-- successor state
  eq s' = rec1(s) .
-- check if the predicate is true.
  red istep190(tag1,tag2,tag3,bfifo1,bfifo2) .
close

--> 3) send2(s)
open ISTEP
-- arbitrary objects
-- assumptions
  eq (put(fifo2(s),tag2(s)) = bfifo1 @ (tag1 | tag2 | bfifo2)) = false .
-- successor state
  eq s' = send2(s) .
-- check if the predicate is true.
  red istep190(tag1,tag2,tag3,bfifo1,bfifo2) .
close
--
open ISTEP
-- arbitrary objects
-- assumptions
  eq put(fifo2(s),tag2(s)) = bfifo1 @ (tag1 | tag2 | bfifo2) .
  eq bfifo2 = empty .
-- facts
  eq (tag2(s) = tag2) = true .
-- successor state
  eq s' = send2(s) .
-- check if the predicate is true.
  red istep190(tag1,tag2,tag3,bfifo1,bfifo2) .
close
--
open ISTEP
-- arbitrary objects
  op tag10 : -> Tagvalue .
  op bfifo10 : -> BFifo .
-- assumptions
  eq put(fifo2(s),tag2(s)) = bfifo1 @ (tag1 | tag2 | bfifo2) .
  eq bfifo2 = tag10 | bfifo10 .
  eq tag3 \in del(tag10 | bfifo10) = true .
-- facts
  eq fifo2(s) = del(bfifo1 @ (tag1 | tag2 | bfifo2)) .
-- successor state
  eq s' = send2(s) .
-- check if the predicate is true.
  red inv190(s,tag1,tag2,tag3,bfifo1,del(tag10 | bfifo10)) 
      implies istep190(tag1,tag2,tag3,bfifo1,bfifo2) .
close
--
open ISTEP
-- arbitrary objects
  op tag10 : -> Tagvalue .
  op bfifo10 : -> BFifo .
-- assumptions
  eq put(fifo2(s),tag2(s)) = bfifo1 @ (tag1 | tag2 | bfifo2) .
  eq bfifo2 = tag10 | bfifo10 .
  eq tag3 \in del(tag10 | bfifo10) = false .
  eq tag3 \in tag10 | bfifo10 = false .
-- facts
  eq fifo2(s) = del(bfifo1 @ (tag1 | tag2 | bfifo2)) .
-- successor state
  eq s' = send2(s) .
-- check if the predicate is true.
  red inv190(s,tag1,tag2,tag3,bfifo1,del(tag10 | bfifo10)) 
      implies istep190(tag1,tag2,tag3,bfifo1,bfifo2) .
close
--
open ISTEP
-- arbitrary objects
  op tag10 : -> Tagvalue .
  op bfifo10 : -> BFifo .
-- assumptions
  eq put(fifo2(s),tag2(s)) = bfifo1 @ (tag1 | tag2 | bfifo2) .
  eq bfifo2 = tag10 | bfifo10 .
  eq tag3 \in del(tag10 | bfifo10) = false . -- (1)
  eq tag3 \in tag10 | bfifo10 = true .       -- (2)
-- facts
  eq fifo2(s) = del(bfifo1 @ (tag1 | tag2 | bfifo2)) .
  eq tag2(s) = tag3 . -- from (1) and (2)
-- successor state
  eq s' = send2(s) .
-- check if the predicate is true.
  red inv190(s,tag1,tag2,tag3,bfifo1,del(tag10 | bfifo10)) 
      implies istep190(tag1,tag2,tag3,bfifo1,bfifo2) .
close

--> 4) rec2(s)
-- 4.1) c-rec2(s)
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-rec2(s) = true .
  eq empty?(fifo1(s)) = false .
--
  eq (tag2(s) = 1st(top(fifo1(s)))) = false .
-- successor state
  eq s' = rec2(s) .
-- check if the predicate is true.
  red istep190(tag1,tag2,tag3,bfifo1,bfifo2) .
close
--
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-rec2(s) = true .
  eq empty?(fifo1(s)) = false .
--
  eq tag2(s) = 1st(top(fifo1(s))) .
  eq (fifo2(s) = bfifo1 @ (tag1 | tag2 | bfifo2)) = false .
-- successor state
  eq s' = rec2(s) .
-- check if the predicate is true.
  red istep190(tag1,tag2,tag3,bfifo1,bfifo2) .
close
--
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-rec2(s) = true .
  eq empty?(fifo1(s)) = false .
--
  eq tag2(s) = 1st(top(fifo1(s))) .
  eq fifo2(s) = bfifo1 @ (tag1 | tag2 | bfifo2) .
  eq (tag1 = 1st(top(fifo1(s)))) = false .
-- facts 
  eq tag1 \in (bfifo1 @ (tag1 | (tag2 | bfifo2))) = true .
-- successor state
  eq s' = rec2(s) .
-- check if the predicate is true.
  red inv210(s,tag1) implies istep190(tag1,tag2,tag3,bfifo1,bfifo2) .
close
--
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-rec2(s) = true .
  eq empty?(fifo1(s)) = false .
--
  eq tag2(s) = 1st(top(fifo1(s))) .
  eq fifo2(s) = bfifo1 @ (tag1 | tag2 | bfifo2) .
  eq (tag2 = 1st(top(fifo1(s)))) = false .
-- facts 
  eq tag2 \in (bfifo1 @ (tag1 | (tag2 | bfifo2))) = true .
-- successor state
  eq s' = rec2(s) .
-- check if the predicate is true.
  red inv210(s,tag2) implies istep190(tag1,tag2,tag3,bfifo1,bfifo2) .
close
--
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-rec2(s) = true .
  eq empty?(fifo1(s)) = false .
--
  eq tag2(s) = 1st(top(fifo1(s))) .
  eq fifo2(s) = bfifo1 @ (tag1 | tag2 | bfifo2) .
  eq tag1 = 1st(top(fifo1(s))) .
  eq tag2 = 1st(top(fifo1(s))) .
-- successor state
  eq s' = rec2(s) .
-- check if the predicate is true.
  red istep190(tag1,tag2,tag3,bfifo1,bfifo2) .
close
--
-- 4.2) c-rec2(s)
open ISTEP
-- arbitrary objects
-- assumptions
  eq c-rec2(s) = false .
-- successor state
  eq s' = rec2(s) .
-- check if the predicate is true.
  red istep190(tag1,tag2,tag3,bfifo1,bfifo2) .
close

--> 5) drop1(s)
-- 5.1) c-drop1(s)
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-drop1(s) = true .
  eq empty?(fifo1(s)) = false .
-- successor state
  eq s' = drop1(s) .
-- check if the predicate is true.
  red istep190(tag1,tag2,tag3,bfifo1,bfifo2) .
close
--
-- 5.2) not c-drop1(s)
open ISTEP
-- arbitrary objects
-- assumptions
  eq c-drop1(s) = false .
-- successor state
  eq s' = drop1(s) .
-- check if the predicate is true.
  red istep190(tag1,tag2,tag3,bfifo1,bfifo2) .
close

--> 6) dup1(s)
-- 6.1) c-dup1(s)
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-dup1(s) = true .
  eq empty?(fifo1(s)) = false .
-- successor state
  eq s' = dup1(s) .
-- check if the predicate is true.
  red istep190(tag1,tag2,tag3,bfifo1,bfifo2) .
close
--
-- 6.2) not c-dup1(s)
open ISTEP
-- arbitrary objects
-- assumptions
  eq c-dup1(s) = false .
-- successor state
  eq s' = dup1(s) .
-- check if the predicate is true.
  red istep190(tag1,tag2,tag3,bfifo1,bfifo2) .
close

--> 7) drop2(s)
-- 7.1) c-drop2(s)
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-drop2(s) = true .
  eq empty?(fifo2(s)) = false .
--
  eq (get(fifo2(s)) = bfifo1 @ (tag1 | tag2 | bfifo2)) = false .
-- successor state
  eq s' = drop2(s) .
-- check if the predicate is true.
  red istep190(tag1,tag2,tag3,bfifo1,bfifo2) .
close
--
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-drop2(s) = true .
  eq empty?(fifo2(s)) = false .
--
  eq get(fifo2(s)) = bfifo1 @ (tag1 | tag2 | bfifo2) .
-- facts
  eq (fifo2(s) = top(fifo2(s)) | (bfifo1 @ (tag1 | tag2 | bfifo2))) = true .
-- successor state
  eq s' = drop2(s) .
-- check if the predicate is true.
  red inv190(s,tag1,tag2,tag3,(top(fifo2(s)) | bfifo1),bfifo2)
      implies istep190(tag1,tag2,tag3,bfifo1,bfifo2) .
close
--
-- 7.2) not c-drop2(s)
open ISTEP
-- arbitrary objects
-- assumptions
  eq c-drop2(s) = false .
-- successor state
  eq s' = drop2(s) .
-- check if the predicate is true.
  red istep190(tag1,tag2,tag3,bfifo1,bfifo2) .
close

--> 8) dup2(s)
-- 8.1) c-dup2(s)
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-dup2(s) = true .
  eq empty?(fifo2(s)) = false .
--
  eq (top(fifo2(s)) | fifo2(s) = bfifo1 @ (tag1 | tag2 | bfifo2)) = false .
-- successor state
  eq s' = dup2(s) .
-- check if the predicate is true.
  red istep190(tag1,tag2,tag3,bfifo1,bfifo2) .
close
--
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-dup2(s) = true .
  eq empty?(fifo2(s)) = false .
--
  eq top(fifo2(s)) | fifo2(s) = bfifo1 @ (tag1 | tag2 | bfifo2) .
  eq bfifo1 = empty .
-- facts
  eq tag1 = tag2 .
-- successor state
  eq s' = dup2(s) .
-- check if the predicate is true.
  red istep190(tag1,tag2,tag3,bfifo1,bfifo2) .
close
--
open ISTEP
-- arbitrary objects
  op tag10 : -> Tagvalue .
  op bfifo10 : -> BFifo .
-- assumptions
  -- eq c-dup2(s) = true .
  eq empty?(fifo2(s)) = false .
--
  eq top(fifo2(s)) | fifo2(s) = bfifo1 @ (tag1 | tag2 | bfifo2) .
  eq bfifo1 = tag10 | bfifo10 .
-- facts 
  eq fifo2(s) = bfifo10 @ (tag1 | (tag2 | bfifo2)) .
-- successor state
  eq s' = dup2(s) .
-- check if the predicate is true.
  red inv190(s,tag1,tag2,tag3,bfifo10,bfifo2) 
      implies istep190(tag1,tag2,tag3,bfifo1,bfifo2) .
close
--
-- 8.2) not c-dup2(s)
open ISTEP
-- arbitrary objects
-- assumptions
  eq c-dup2(s) = false .
-- successor state
  eq s' = dup2(s) .
-- check if the predicate is true.
  red istep190(tag1,tag2,tag3,bfifo1,bfifo2) .
close

--> Q.E.D.