-- I) Base case

open INV
  red inv160(init,pair) .
close

-- II) Inductive ceses

--> 1) send1(s)
open ISTEP
-- arbitrary objects
-- assumptions
  eq fifo1(s) = empty .
  eq pair = < tag1(s) , next(s) > .
-- successor state
  eq s' = send1(s) .
-- check if the predicate is true.
  red istep160(pair) .
close
--
open ISTEP
-- arbitrary objects
-- assumptions
  eq fifo1(s) = empty .
  eq (pair = < tag1(s) , next(s) >) = false .
-- successor state
  eq s' = send1(s) .
-- check if the predicate is true.
  red istep160(pair) .
close
--
open ISTEP
-- arbitrary objects
  op pair10 : -> Pair .
  op pfifo10 : -> PFifo .
-- assumptions
  eq fifo1(s) = pair10 | pfifo10 .
  eq pair10 = pair .
-- successor state
  eq s' = send1(s) .
-- check if the predicate is true.
  red istep160(pair) .
close
--
open ISTEP
-- arbitrary objects
  op pair10 : -> Pair .
  op pfifo10 : -> PFifo .
-- assumptions
  eq fifo1(s) = pair10 | pfifo10 .
  eq (pair10 = pair) = false .
  eq pair \in pfifo10 = true .
-- successor state
  eq s' = send1(s) .
-- check if the predicate is true.
  red istep160(pair) .
close
--
open ISTEP
-- arbitrary objects
  op pair10 : -> Pair .
  op pfifo10 : -> PFifo .
-- assumptions
  eq fifo1(s) = pair10 | pfifo10 .
  eq (pair10 = pair) = false .                                   -- (1)
  eq pair \in pfifo10 = false .
  eq tag2(s) = 1st(pair10) .
  eq (tag1(s) = 1st(pair10) and next(s) = 2nd(pair10)) = true .  -- (2)
-- facts
  -- from (1) and (2)
  eq (1st(pair) = tag1(s) and 2nd(pair) = next(s)) = false .
-- successor state
  eq s' = send1(s) .
-- check if the predicate is true.
  red istep160(pair) .
close
--
open ISTEP
-- arbitrary objects
  op pair10 : -> Pair .
  op pfifo10 : -> PFifo .
-- assumptions
  eq fifo1(s) = pair10 | pfifo10 .
  eq (pair10 = pair) = false .
  eq pair \in pfifo10 = false .
  eq tag2(s) = 1st(pair10) .
  eq (tag1(s) = 1st(pair10) and next(s) = 2nd(pair10)) = false .
-- successor state
  eq s' = send1(s) .
-- check if the predicate is true.
  red inv120(s) implies istep160(pair) .
close
--
open ISTEP
-- arbitrary objects
  op pair10 : -> Pair .
  op pfifo10 : -> PFifo .
-- assumptions
  eq fifo1(s) = pair10 | pfifo10 .
  eq (pair10 = pair) = false .                                  
  eq pair \in pfifo10 = false .
  eq (tag2(s) = 1st(pair10)) = false .
  eq (1st(pair) = tag1(s) and 2nd(pair) = next(s)) = true .
-- successor state
  eq s' = send1(s) .
-- check if the predicate is true.
  red istep160(pair) .
close
--
open ISTEP
-- arbitrary objects
  op pair10 : -> Pair .
  op pfifo10 : -> PFifo .
-- assumptions
  eq fifo1(s) = pair10 | pfifo10 .
  eq (pair10 = pair) = false .                                  
  eq pair \in pfifo10 = false .
  eq (tag2(s) = 1st(pair10)) = false .
  eq (1st(pair) = tag1(s) and 2nd(pair) = next(s)) = false .
-- successor state
  eq s' = send1(s) .
-- check if the predicate is true.
  red istep160(pair) .
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 tag1(s) = top(fifo2(s)) .
-- successor state
  eq s' = rec1(s) .
-- check if the predicate is true.
  red istep160(pair) .
close
--
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-rec1(s) = true .
  eq empty?(fifo2(s)) = false .
--
  eq (tag1(s) = top(fifo2(s))) = false .
  eq pair = < top(fifo2(s)) , s(next(s)) > .
-- successor state
  eq s' = rec1(s) .
-- check if the predicate is true.
  red istep160(pair) .
close
--
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-rec1(s) = true .
  eq empty?(fifo2(s)) = false .
--
  eq (tag1(s) = top(fifo2(s))) = false .
  -- eq (pair = < top(fifo2(s)) , s(next(s)) >) = false .
  eq (1st(pair) = top(fifo2(s)) and 2nd(pair) = s(next(s))) = false .
  --
  eq pair \in fifo1(s) = false .
-- successor state
  eq s' = rec1(s) .
-- check if the predicate is true.
  red istep160(pair) .
close
--
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-rec1(s) = true .
  eq empty?(fifo2(s)) = false .
--
  eq (tag1(s) = top(fifo2(s))) = false .
  -- eq (pair = < top(fifo2(s)) , s(next(s)) >) = false .
  eq (1st(pair) = top(fifo2(s)) and 2nd(pair) = s(next(s))) = false .
  --
  eq pair \in fifo1(s) = true .
  eq (tag2(s) = 1st(pair)) = false .
-- successor state
  eq s' = rec1(s) .
-- check if the predicate is true.
  red istep160(pair) .
close
--
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-rec1(s) = true .
  eq empty?(fifo2(s)) = false .
--
  eq (tag1(s) = top(fifo2(s))) = false .
  -- eq (pair = < top(fifo2(s)) , s(next(s)) >) = false .
  eq (1st(pair) = top(fifo2(s)) and 2nd(pair) = s(next(s))) = false .
  --
  eq pair \in fifo1(s) = true .
  eq tag2(s) = 1st(pair) .
  eq (tag1(s) = 1st(pair)) = false .
-- successor state
  eq s' = rec1(s) .
-- check if the predicate is true.
  red istep160(pair) .
close
--
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-rec1(s) = true .
  eq empty?(fifo2(s)) = false .
--
  -- eq (tag1(s) = top(fifo2(s))) = false .
  eq (1st(pair) = top(fifo2(s))) = false .
  -- eq (pair = < top(fifo2(s)) , s(next(s)) >) = false .
  eq (1st(pair) = top(fifo2(s)) and 2nd(pair) = s(next(s))) = false .
  --
  eq pair \in fifo1(s) = true .
  eq tag2(s) = 1st(pair) .
  eq tag1(s) = 1st(pair) .
-- successor state
  eq s' = rec1(s) .
-- check if the predicate is true.
  red inv110(s) implies istep160(pair) .
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 istep160(pair) .
close

--> 3) send2(s)
open ISTEP
-- arbitrary objects
-- assumptions
-- successor state
  eq s' = send2(s) .
-- check if the predicate is true.
  red istep160(pair) .
close

--> 4) rec2(s)
-- 4.1) c-rec2(s)
open ISTEP
-- arbitrary objects
  op pair10 : -> Pair .
-- assumptions
  -- eq c-rec2(s) = true .
  -- eq empty?(fifo1(s)) = false .
  eq fifo1(s) = pair10 | empty .
-- successor state
  eq s' = rec2(s) .
-- check if the predicate is true.
  red istep160(pair) .
close
--
open ISTEP
-- arbitrary objects
  ops pair10 pair20 : -> Pair .
  op pfifo10 : -> PFifo .
-- assumptions
  -- eq c-rec2(s) = true .
  -- eq empty?(fifo1(s)) = false .
  eq fifo1(s) = pair10 | pair20 | pfifo10 .
--
  eq pair10 = pair20 .
  eq tag2(s) = 1st(pair20) .
  eq pair = pair20 .
-- successor state
  eq s' = rec2(s) .
-- check if the predicate is true.
  red istep160(pair) .
close
--
open ISTEP
-- arbitrary objects
  ops pair10 pair20 : -> Pair .
  op pfifo10 : -> PFifo .
-- assumptions
  -- eq c-rec2(s) = true .
  -- eq empty?(fifo1(s)) = false .
  eq fifo1(s) = pair10 | pair20 | pfifo10 .
--
  eq pair10 = pair20 .
  eq tag2(s) = 1st(pair20) .
  eq (pair = pair20) = false .
-- successor state
  eq s' = rec2(s) .
-- check if the predicate is true.
  red inv150(s,pair) implies istep160(pair) .
close
--
open ISTEP
-- arbitrary objects
  ops pair10 pair20 : -> Pair .
  op pfifo10 : -> PFifo .
-- assumptions
  -- eq c-rec2(s) = true .
  -- eq empty?(fifo1(s)) = false .
  eq fifo1(s) = pair10 | pair20 | pfifo10 .
--
  eq pair10 = pair20 .
  eq (tag2(s) = 1st(pair20)) = false .
  eq pair = pair20 .
-- successor state
  eq s' = rec2(s) .
-- check if the predicate is true.
  red istep160(pair) .
close
--
open ISTEP
-- arbitrary objects
  ops pair10 pair20 : -> Pair .
  op pfifo10 : -> PFifo .
-- assumptions
  -- eq c-rec2(s) = true .
  -- eq empty?(fifo1(s)) = false .
  eq fifo1(s) = pair10 | pair20 | pfifo10 .
--
  eq pair10 = pair20 .
  eq (tag2(s) = 1st(pair20)) = false .
  eq (pair = pair20) = false .
-- successor state
  eq s' = rec2(s) .
-- check if the predicate is true.
  red istep160(pair) .
close
--
open ISTEP
-- arbitrary objects
  ops pair10 pair20 : -> Pair .
  op pfifo10 : -> PFifo .
-- assumptions
  -- eq c-rec2(s) = true .
  -- eq empty?(fifo1(s)) = false .
  eq fifo1(s) = pair10 | pair20 | pfifo10 .
--
  eq (pair10 = pair20) = false .
  eq tag2(s) = 1st(pair20) .
  eq pair = pair20 .
-- successor state
  eq s' = rec2(s) .
-- check if the predicate is true.
  red istep160(pair) .
close
--
open ISTEP
-- arbitrary objects
  ops pair10 pair20 : -> Pair .
  op pfifo10 : -> PFifo .
-- assumptions
  -- eq c-rec2(s) = true .
  -- eq empty?(fifo1(s)) = false .
  eq fifo1(s) = pair10 | pair20 | pfifo10 .
--
  eq (pair10 = pair20) = false .
  eq tag2(s) = 1st(pair20) .
  eq (pair = pair20) = false .
  eq pair \in pfifo10 = true .
-- successor state
  eq s' = rec2(s) .
-- check if the predicate is true.
  red inv180(s,pair10,pair20,pair,pfifo10) implies istep160(pair) .
close
--
open ISTEP
-- arbitrary objects
  ops pair10 pair20 : -> Pair .
  op pfifo10 : -> PFifo .
-- assumptions
  -- eq c-rec2(s) = true .
  -- eq empty?(fifo1(s)) = false .
  eq fifo1(s) = pair10 | pair20 | pfifo10 .
--
  eq (pair10 = pair20) = false .
  eq tag2(s) = 1st(pair20) .
  eq (pair = pair20) = false .
  eq pair \in pfifo10 = false .
-- successor state
  eq s' = rec2(s) .
-- check if the predicate is true.
  red istep160(pair) .
close
--
open ISTEP
-- arbitrary objects
  ops pair10 pair20 : -> Pair .
  op pfifo10 : -> PFifo .
-- assumptions
  -- eq c-rec2(s) = true .
  -- eq empty?(fifo1(s)) = false .
  eq fifo1(s) = pair10 | pair20 | pfifo10 .
--
  eq (pair10 = pair20) = false .
  eq (tag2(s) = 1st(pair20)) = false .
  eq pair = pair20 .
  eq pair20 \in pfifo10 = true .
-- successor state
  eq s' = rec2(s) .
-- check if the predicate is true.
  red inv180(s,pair10,pair20,pair,pfifo10) implies istep160(pair) .
close
--
open ISTEP
-- arbitrary objects
  ops pair10 pair20 : -> Pair .
  op pfifo10 : -> PFifo .
-- assumptions
  -- eq c-rec2(s) = true .
  -- eq empty?(fifo1(s)) = false .
  eq fifo1(s) = pair10 | pair20 | pfifo10 .
--
  eq (pair10 = pair20) = false .
  eq (tag2(s) = 1st(pair20)) = false . 
  eq pair = pair20 .
  eq pair20 \in pfifo10 = false .
  eq (tag2(s) = 1st(pair10)) = true .  
-- successor state
  eq s' = rec2(s) .
-- check if the predicate is true.
  red inv150(s,pair) implies istep160(pair) .
close
--
open ISTEP
-- arbitrary objects
  ops pair10 pair20 : -> Pair .
  op pfifo10 : -> PFifo .
-- assumptions
  -- eq c-rec2(s) = true .
  -- eq empty?(fifo1(s)) = false .
  eq fifo1(s) = pair10 | pair20 | pfifo10 .
--
  eq (pair10 = pair20) = false .
  eq (tag2(s) = 1st(pair20)) = false . 
  eq pair = pair20 .
  eq pair20 \in pfifo10 = false .
  eq (tag2(s) = 1st(pair10)) = false .  
-- successor state
  eq s' = rec2(s) .
-- check if the predicate is true.
  red istep160(pair) .
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 istep160(pair) .
close

--> 5) drop1(s)
-- 5.1) c-drop1(s)
open ISTEP
-- arbitrary objects
  op pair10 : -> Pair .
-- assumptions
  -- eq c-drop1(s) = true .
  -- eq empty?(fifo1(s)) = false .
  eq fifo1(s) = pair10 | empty .
-- successor state
  eq s' = drop1(s) .
-- check if the predicate is true.
  red istep160(pair) .
close
--
open ISTEP
-- arbitrary objects
  ops pair10 pair20 : -> Pair .
  op pfifo10 : -> PFifo .
-- assumptions
  -- eq c-drop1(s) = true .
  -- eq empty?(fifo1(s)) = false .
  eq fifo1(s) = pair10 | pair20 | pfifo10 .
--
  eq pair10 = pair20 .
  eq pair = pair20 .
-- successor state
  eq s' = drop1(s) .
-- check if the predicate is true.
  red istep160(pair) .
close
--
open ISTEP
-- arbitrary objects
  ops pair10 pair20 : -> Pair .
  op pfifo10 : -> PFifo .
-- assumptions
  -- eq c-drop1(s) = true .
  -- eq empty?(fifo1(s)) = false .
  eq fifo1(s) = pair10 | pair20 | pfifo10 .
--
  eq pair10 = pair20 .
  eq (pair = pair20) = false .
-- successor state
  eq s' = drop1(s) .
-- check if the predicate is true.
  red istep160(pair) .
close
--
open ISTEP
-- arbitrary objects
  ops pair10 pair20 : -> Pair .
  op pfifo10 : -> PFifo .
-- assumptions
  -- eq c-drop1(s) = true .
  -- eq empty?(fifo1(s)) = false .
  eq fifo1(s) = pair10 | pair20 | pfifo10 .
--
  eq (pair10 = pair20) = false .
  eq pair = pair20 .
-- successor state
  eq s' = drop1(s) .
-- check if the predicate is true.
  red istep160(pair) .
close
--
open ISTEP
-- arbitrary objects
  ops pair10 pair20 : -> Pair .
  op pfifo10 : -> PFifo .
-- assumptions
  -- eq c-drop1(s) = true .
  -- eq empty?(fifo1(s)) = false .
  eq fifo1(s) = pair10 | pair20 | pfifo10 .
--
  eq (pair10 = pair20) = false .
  eq (pair = pair20) = false .
  eq pair = pair10 .
-- successor state
  eq s' = drop1(s) .
-- check if the predicate is true.
  red istep160(pair) .
close
--
open ISTEP
-- arbitrary objects
  ops pair10 pair20 : -> Pair .
  op pfifo10 : -> PFifo .
-- assumptions
  -- eq c-drop1(s) = true .
  -- eq empty?(fifo1(s)) = false .
  eq fifo1(s) = pair10 | pair20 | pfifo10 .
--
  eq (pair10 = pair20) = false .
  eq (pair = pair20) = false .
  eq (pair = pair10) = false .
-- successor state
  eq s' = drop1(s) .
-- check if the predicate is true.
  red istep160(pair) .
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 istep160(pair) .
close

--> 6) dup1(s)
-- 6.1) c-dup1(s)
open ISTEP
-- arbitrary objects
  op pair10 : -> Pair .
  op pfifo10 : -> PFifo .
-- assumptions
  -- eq c-dup1(s) = true .
  -- eq empty?(fifo1(s)) = false .
  eq fifo1(s) = pair10 | pfifo10 .
--
  eq pair = pair10 .
-- successor state
  eq s' = dup1(s) .
-- check if the predicate is true.
  red istep160(pair) .
close
--
open ISTEP
-- arbitrary objects
  op pair10 : -> Pair .
  op pfifo10 : -> PFifo .
-- assumptions
  -- eq c-dup1(s) = true .
  -- eq empty?(fifo1(s)) = false .
  eq fifo1(s) = pair10 | pfifo10 .
--
  eq (pair = pair10) = false .
-- successor state
  eq s' = dup1(s) .
-- check if the predicate is true.
  red istep160(pair) .
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 istep160(pair) .
close

--> 7) drop2(s)
-- 7.1) c-drop2(s)
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-drop2(s) = true .
  eq empty?(fifo2(s)) = false .
-- successor state
  eq s' = drop2(s) .
-- check if the predicate is true.
  red istep160(pair) .
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 istep160(pair) .
close

--> 8) dup2(s)
-- 8.1) c-dup2(s)
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-dup2(s) = true .
  eq empty?(fifo2(s)) = false .
-- successor state
  eq s' = dup2(s) .
-- check if the predicate is true.
  red istep160(pair) .
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 istep160(pair) .
close

--> Q.E.D.