Superior - proofs of reachability

  I1A1B1C1D1E1E2F1G1G2G3H1J1J2K0K1L0L1L2M0M1M2M3N1Y1Z0Z
receive ENROL/rsp-req A1                                                   Y1
receive ENROL/no-rsp-req B1                                                   Z
receive RESIGN/rsp-req Y1   C1 C1 C1       G3 Z G3                         C1 Y1   Y1
receive RESIGN/no-rsp-req Z   Z Z Z       Z Z Z                         Z Z   Z
receive PREPARED Y1   E1   E1 E1   F1 G1 G2                           N1 Y1   Y1
receive PREPARED/cancel Y1   E2   E2   E2 F1 G1 G2                           N1 Y1   Y1
receive CONFIRMED/auto L2   H1   H1 H1   F1 L0 L0   H1         L0 L1 L2         N1 L2   L2
receive CONFIRMED/response               Z0                   L1 L2         Z   Z0 Z
receive CANCELLED Y1   Z   Z J1 J1 K0 J2 Z     J1 J2 K0 K1               Z Y1   Y1
receive HAZARD M0 M0 M0   M0 M0 M0 M1 M2 M2                   M0 M1 M2 M3 Z M0   M0
receive INF_STATE/active/y Y1 A1 B1   D1       G1 G2                           N1 Y1   Y1
receive INF_STATE/active     B1   D1       G1 G2                           N1 Z   Z
receive INF_STATE/unknown     Z Z Z       Z Z Z     Z           M0   M2 M3 Z Z   Z
send ENROLLED   B1                                                  
send RESIGNED       Z                                              
send PREPARE         D1 E1 E2                                        
send REQUEST_CONFIRM     N1     N1 N1                                 N1      
send CONFIRM               F1                                      
send CANCEL                 G2 G2 Z     Z                          
send CONTRADICTION                               Z   Z         Z        
send SUP_STATE/active/y     B1                                                
send SUP_STATE/active     B1                                                
send SUP_STATE/preparedreceived/y           E1 E2                                        
send SUP_STATE/preparedreceived           E1 E2                                        
send SUP_STATE/unknown                                                 Z    
decide to prepare     D1     E1 E2                                        
decide to confirm           F1 F1         F1 K0                            
decide to cancel     G1   G1 G1 Z         L0 J2                            
remove confirm information                                                   Z  
record contradiction                             K1   L1   L1 M3 M3 M3          
disruption 0 I1 A1 B1 C1 D1 E1 E2 F1 G1 G2 G3 H1 J1 J2 K0 K1 L0 L1 L2 M0 M1 M2 M3 N1 Y1 Z0 Z
disruption I Z Z Z Z Z Z Z   Z Z Z Z Z Z F1 Z Z Z Z Z Z Z Z Z      
disruption II           D1 D1         E1 E1 G2     G2       F1 G2          
disruption III           B1 B1         D1 B1 Z                          
disruption IV                       B1 B1                            
Inferior - proofs of reachability
  i1a1b1c1d1e1e2f0f1f2g0g1g2h1h2j1j2j3k1l1m1m2m3n0n1n2n3n4n5y0y1y2y3zz1
send ENROL/rsp-req a1                                                                    
send ENROL/no-rsp-req b1                                                                    
send RESIGN/rsp-req     c1 c1 c1                                                            
send RESIGN/no-rsp-req     z z z                                                            
send PREPARED           e1                                                          
send PREPARED/cancel             e2                                                        
send CONFIRMED/auto                           h1           l1                              
send CONFIRMED/response                   z         z                     z           z      
send CANCELLED     z   z               z     j2 j2 z k1               z           z1    
send HAZARD                                         m1 m2 m3         z z            
send INF_STATE/active/y   a1 b1   d1                                                            
send INF_STATE/active     b1   d1                                                            
send INF_STATE/unknown                                                             z        
receive ENROLLED   b1                                     m1 m2                       z  
receive RESIGNED       z                                                     y1     z  
receive PREPARE   d1 d1 c1 d1 e1 e2             h1   j1 j2       m1 m2 m3               y1   y3 y1 z1
receive REQUEST_CONFIRM   n1 n1 c1   n0 n0             n2   n3 n3       n4 n5 n5 n0 n1 n2 n3 n4 n5   y1   y3 y1 y1
receive CONFIRM           f0 f1 f0 f1 f2       h2 h2 k1 k1   k1   m1 m2 m3                 y2 y3 y2 y3
receive CANCEL   g2 g2 z g2 g0 g1       g0 g1 g2 l1   j3 z j3   l1 m1 m2 m3               y1   z y1 y1
receive CONTRADICTION           z z             z     z   z z z z z     n2   n4 z   z   z z z
receive SUP_STATE/active/y   b1 b1 c1   e1 e2             h1   j1 j2       m1 m2 m3               y1   y3 y1 y3
receive SUP_STATE/active   b1 b1 c1   e1 e2             h1   j1 j2       m1 m2 m3               y1   y3 z z1
receive SUP_STATE/preparedreceived/y           e1 e2             h1   j1 j2       m1   m3                   y3   y3
receive SUP_STATE/preparedreceived           e1 e2             h1   j1 j2       m1   m3                   y3   y3
receive SUP_STATE/unknown   z z z z y0 y0       y0 y0 z l1   z z z z l1 m1 m2 m3 z z z z z z y0 y1   y3 z z
decide to be prepared     e1   e1                                                            
decide to be prepared/cancel     e2   e2                                                            
decide to confirm autonomously           h1                                     n2                    
decide to cancel autonomously           j1 z1                                   n3                    
apply ordered confirmation               f2 f2                                                    
remove prepared information                     g2 g2                       n1           z          
detect problem   m2 m2   m2 m3 m3 m3 m3   m3 m3                                              
detect and record problem                                           m1 m1   n4                    
disruption 0 i1 a1 b1 c1 d1 e1 e2 f0 f1 f2 g0 g1 g2 h1 h2 j1 j2 j3 k1 l1 m1 m2 m3 n0 n1 n2 n3 n4 n5 y0 y1 y2 y3 z z1
disruption I   z z z z     e1 e2 z e1 e2 z   h1 j2   z       z   e1 z         e1          
disruption II         b1