in citp
in abp

*** ***********************************************************************
*** PROOF of inv5 ***
*** ***********************************************************************

th INV5 is inc ABP .
 vars B B' : Bit . 
 vars P P' : Packet .
 vars C1 C2 C3 : Channel1 .
 vars D1 D2 D3 : Channel2 .
 var S : Sys .
 crl B  => bit1(S)     if C1,< B,P >,C2 := channel1(S) /\  bit2(S) = bit1(S)[nonexec metadata "inv2"].
 ceq bit2(S) = bit1(S) if D1,B,D2 := channel2(S) /\ B = bit1(S) [metadata "inv3"].
 crl true => false if not bit1(S) => bit1(S) [nonexec metadata "inc"].
endth

select #CITP# .
loop init .

(goal INV5 |- crl P:Packet => pac(next(S:Sys)) if C1:Channel1,< B:Bit,P:Packet >,C2:Channel1 := channel1(S:Sys) /\ B:Bit = bit1(S:Sys);)
(ind on S:Sys)

(ca  red cs pair tc  pair  imp  red)

---> rec1
(init inv3 by S:Sys <- x#1 ;)
(init inv2 by S:Sys <- x#1 ;)
(init inc  by S:Sys <- x#1 ;)