(VAR M1 M2 M N1 N2 N V X1 X2 X Y ) (THEORY (AC ---osb-os-osb-BasinSet-os-csb-csb-osb-os-osb-BasinSet-os-csb-csb) ) (RULES 3 -> s--osb-os-osb-Nat-os-csb-csb (s--osb-os-osb-Nat-os-csb-csb ( s--osb-os-osb-Nat-os-csb-csb (0 ))) 4 -> s--osb-os-osb-Nat-os-csb-csb (3 ) 5 -> s--osb-os-osb-Nat-os-csb-csb (4 ) 8 -> -+--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (3 ,5 ) initial -> ---osb-os-osb-BasinSet-os-csb-csb-osb-os-osb-BasinSet-os-csb-csb ( basin-osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (3 ,0 ), ---osb-os-osb-BasinSet-os-csb-csb-osb-os-osb-BasinSet-os-csb-csb ( basin-osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (5 ,0 ), basin-osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (8 ,0 ))) -+--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (0 ,N )-> N -+--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb ( s--osb-os-osb-Nat-os-csb-csb (N ),M )-> s--osb-os-osb-Nat-os-csb-csb ( -+--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (N ,M )) ---osb-os-osb-BasinSet-os-csb-csb-osb-os-osb-BasinSet-os-csb-csb ( basin-osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (M1 ,N1 ), basin-osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (M2 ,N2 ))-> U11 (equal-osb-os-osb-os-osb-Bool-os-csb-os-csb-csb-osb-os-osb-os-osb-Bool-os-csb-os-csb-csb (osb---csb-osb-os-osb-Bool-os-csb-csb ( -<=--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb ( -+--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (N1 ,N2 ),M2 )), osb---csb-osb-os-osb-Bool-os-csb-csb (true )),M1 ,M2 ,N1 ,N2 ) ---osb-os-osb-BasinSet-os-csb-csb-osb-os-osb-BasinSet-os-csb-csb ( basin-osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (M1 ,N1 ), basin-osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (M2 ,N2 ))-> U21 (equal-osb-os-osb-os-osb-Bool-os-csb-os-csb-csb-osb-os-osb-os-osb-Bool-os-csb-os-csb-csb (osb---csb-osb-os-osb-Bool-os-csb-csb ( ->--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb ( -+--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (N1 ,N2 ),M2 )), osb---csb-osb-os-osb-Bool-os-csb-csb (true )),M1 ,M2 ,N1 ,N2 ) -<=--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (0 ,N )-> true -<=--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (N ,N )-> true -<=--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb ( s--osb-os-osb-Nat-os-csb-csb (N ),0 )-> false -<=--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb ( s--osb-os-osb-Nat-os-csb-csb (N ),s--osb-os-osb-Nat-os-csb-csb (M ))-> -<=--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (N ,M ) ->--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (N ,M )-> not-osb-os-osb-Bool-os-csb-csb ( -<=--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (N ,M )) U101 (osb---csb-osb-os-osb-Nat-os-csb-csb (Y ),X2 )-> osb---csb-osb-os-osb-Bool-os-csb-csb ( ->--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (Y ,X2 )) U11 (tt ,M1 ,M2 ,N1 ,N2 )-> ---osb-os-osb-BasinSet-os-csb-csb-osb-os-osb-BasinSet-os-csb-csb ( basin-osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (M1 ,0 ), basin-osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (M2 , -+--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (N1 ,N2 ))) U111 (osb---csb-osb-os-osb-Bool-os-csb-csb (Y ))-> osb---csb-osb-os-osb-Bool-os-csb-csb (not-osb-os-osb-Bool-os-csb-csb (Y )) U121 (osb---csb-osb-os-osb-Nat-os-csb-csb (Y ),X1 )-> osb---csb-osb-os-osb-Nat-os-csb-csb ( -+--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (X1 ,Y )) U131 (osb---csb-osb-os-osb-Nat-os-csb-csb (Y ),X2 )-> osb---csb-osb-os-osb-Nat-os-csb-csb ( -+--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (Y ,X2 )) U141 (osb---csb-osb-os-osb-Nat-os-csb-csb (Y ))-> osb---csb-osb-os-osb-Nat-os-csb-csb (s--osb-os-osb-Nat-os-csb-csb (Y )) U151 (osb---csb-osb-os-osb-Nat-os-csb-csb (Y ),X1 )-> osb---csb-osb-os-osb-Nat-os-csb-csb ( sd-osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (X1 ,Y )) U161 (osb---csb-osb-os-osb-Nat-os-csb-csb (Y ),X2 )-> osb---csb-osb-os-osb-Nat-os-csb-csb ( sd-osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (Y ,X2 )) U171 (osb---csb-osb-os-osb-BasinSet-os-csb-csb (Y ))-> osb---csb-osb-os-osb-Thruth-os-csb-csb ( is'Basin-osb-os-osb-BasinSet-os-csb-csb (Y )) U181 (osb---csb-osb-os-osb-BasinSet-os-csb-csb (Y ))-> osb---csb-osb-os-osb-Thruth-os-csb-csb ( is'BasinSet-osb-os-osb-BasinSet-os-csb-csb (Y )) U191 (osb---csb-osb-os-osb-Bool-os-csb-csb (Y ))-> osb---csb-osb-os-osb-Thruth-os-csb-csb (is'Bool-osb-os-osb-Bool-os-csb-csb (Y )) U201 (osb---csb-osb-os-osb-Nat-os-csb-csb (Y ))-> osb---csb-osb-os-osb-Thruth-os-csb-csb (is'Nat-osb-os-osb-Nat-os-csb-csb (Y )) U21 (tt ,M1 ,M2 ,N1 ,N2 )-> ---osb-os-osb-BasinSet-os-csb-csb-osb-os-osb-BasinSet-os-csb-csb ( basin-osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (M1 , sd-osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb ( -+--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (N1 ,N2 ),M2 )), basin-osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (M2 ,M2 )) U31 (osb---csb-osb-os-osb-BasinSet-os-csb-csb (Y ),X1 )-> osb---csb-osb-os-osb-BasinSet-os-csb-csb ( ---osb-os-osb-BasinSet-os-csb-csb-osb-os-osb-BasinSet-os-csb-csb (X1 ,Y )) U41 (osb---csb-osb-os-osb-BasinSet-os-csb-csb (Y ),X2 )-> osb---csb-osb-os-osb-BasinSet-os-csb-csb ( ---osb-os-osb-BasinSet-os-csb-csb-osb-os-osb-BasinSet-os-csb-csb (Y ,X2 )) U51 (osb---csb-osb-os-osb-Nat-os-csb-csb (Y ),X1 )-> osb---csb-osb-os-osb-BasinSet-os-csb-csb ( basin-osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (X1 ,Y )) U61 (osb---csb-osb-os-osb-Nat-os-csb-csb (Y ),X2 )-> osb---csb-osb-os-osb-BasinSet-os-csb-csb ( basin-osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (Y ,X2 )) U71 (osb---csb-osb-os-osb-Nat-os-csb-csb (Y ),X1 )-> osb---csb-osb-os-osb-Bool-os-csb-csb ( -<=--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (X1 ,Y )) U81 (osb---csb-osb-os-osb-Nat-os-csb-csb (Y ),X2 )-> osb---csb-osb-os-osb-Bool-os-csb-csb ( -<=--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (Y ,X2 )) U91 (osb---csb-osb-os-osb-Nat-os-csb-csb (Y ),X1 )-> osb---csb-osb-os-osb-Bool-os-csb-csb ( ->--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (X1 ,Y )) basin-osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (M1 ,N1 )-> basin-osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (M1 ,0 ) basin-osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (M1 ,N1 )-> basin-osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (M1 ,M1 ) equal-osb-os-osb-os-osb-BasinSet-os-csb-os-csb-csb-osb-os-osb-os-osb-BasinSet-os-csb-os-csb-csb (osb---csb-osb-os-osb-BasinSet-os-csb-csb (X ), osb---csb-osb-os-osb-BasinSet-os-csb-csb (X ))-> tt equal-osb-os-osb-os-osb-Bool-os-csb-os-csb-csb-osb-os-osb-os-osb-Bool-os-csb-os-csb-csb (osb---csb-osb-os-osb-Bool-os-csb-csb (X ), osb---csb-osb-os-osb-Bool-os-csb-csb (X ))-> tt equal-osb-os-osb-os-osb-Nat-os-csb-os-csb-csb-osb-os-osb-os-osb-Nat-os-csb-os-csb-csb (osb---csb-osb-os-osb-Nat-os-csb-csb (X ), osb---csb-osb-os-osb-Nat-os-csb-csb (X ))-> tt equal-osb-os-osb-os-osb-Thruth-os-csb-os-csb-csb-osb-os-osb-os-osb-Thruth-os-csb-os-csb-csb (osb---csb-osb-os-osb-Thruth-os-csb-csb (X ), osb---csb-osb-os-osb-Thruth-os-csb-csb (X ))-> tt is'Basin-osb-os-osb-BasinSet-os-csb-csb (V )-> tt is'BasinSet-osb-os-osb-BasinSet-os-csb-csb (V )-> tt is'Bool-osb-os-osb-Bool-os-csb-csb (V )-> tt is'Nat-osb-os-osb-Nat-os-csb-csb (V )-> tt not-osb-os-osb-Bool-os-csb-csb (false )-> true not-osb-os-osb-Bool-os-csb-csb (true )-> false ocb---ccb-osb-os-osb-BasinSet-os-csb-csb (initial )-> osb---csb-osb-os-osb-BasinSet-os-csb-csb ( ---osb-os-osb-BasinSet-os-csb-csb-osb-os-osb-BasinSet-os-csb-csb ( basin-osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (3 ,0 ), ---osb-os-osb-BasinSet-os-csb-csb-osb-os-osb-BasinSet-os-csb-csb ( basin-osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (5 ,0 ), basin-osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (8 ,0 )))) ocb---ccb-osb-os-osb-BasinSet-os-csb-csb ( ---osb-os-osb-BasinSet-os-csb-csb-osb-os-osb-BasinSet-os-csb-csb (X1 ,X2 ))-> U31 (ocb---ccb-osb-os-osb-BasinSet-os-csb-csb (X2 ),X1 ) ocb---ccb-osb-os-osb-BasinSet-os-csb-csb ( ---osb-os-osb-BasinSet-os-csb-csb-osb-os-osb-BasinSet-os-csb-csb (X1 ,X2 ))-> U41 (ocb---ccb-osb-os-osb-BasinSet-os-csb-csb (X1 ),X2 ) ocb---ccb-osb-os-osb-BasinSet-os-csb-csb ( basin-osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (X1 ,X2 ))-> U51 (ocb---ccb-osb-os-osb-Nat-os-csb-csb (X2 ),X1 ) ocb---ccb-osb-os-osb-BasinSet-os-csb-csb ( basin-osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (X1 ,X2 ))-> U61 (ocb---ccb-osb-os-osb-Nat-os-csb-csb (X1 ),X2 ) ocb---ccb-osb-os-osb-Bool-os-csb-csb ( -<=--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (0 ,N ))-> osb---csb-osb-os-osb-Bool-os-csb-csb (true ) ocb---ccb-osb-os-osb-Bool-os-csb-csb ( -<=--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (N ,N ))-> osb---csb-osb-os-osb-Bool-os-csb-csb (true ) ocb---ccb-osb-os-osb-Bool-os-csb-csb ( -<=--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (X1 ,X2 ))-> U71 ( ocb---ccb-osb-os-osb-Nat-os-csb-csb (X2 ),X1 ) ocb---ccb-osb-os-osb-Bool-os-csb-csb ( -<=--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (X1 ,X2 ))-> U81 ( ocb---ccb-osb-os-osb-Nat-os-csb-csb (X1 ),X2 ) ocb---ccb-osb-os-osb-Bool-os-csb-csb ( -<=--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb ( s--osb-os-osb-Nat-os-csb-csb (N ),0 ))-> osb---csb-osb-os-osb-Bool-os-csb-csb (false ) ocb---ccb-osb-os-osb-Bool-os-csb-csb ( -<=--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb ( s--osb-os-osb-Nat-os-csb-csb (N ),s--osb-os-osb-Nat-os-csb-csb (M )))-> osb---csb-osb-os-osb-Bool-os-csb-csb ( -<=--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (N ,M )) ocb---ccb-osb-os-osb-Bool-os-csb-csb ( ->--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (N ,M ))-> osb---csb-osb-os-osb-Bool-os-csb-csb (not-osb-os-osb-Bool-os-csb-csb ( -<=--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (N ,M ))) ocb---ccb-osb-os-osb-Bool-os-csb-csb ( ->--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (X1 ,X2 ))-> U101 ( ocb---ccb-osb-os-osb-Nat-os-csb-csb (X1 ),X2 ) ocb---ccb-osb-os-osb-Bool-os-csb-csb ( ->--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (X1 ,X2 ))-> U91 ( ocb---ccb-osb-os-osb-Nat-os-csb-csb (X2 ),X1 ) ocb---ccb-osb-os-osb-Bool-os-csb-csb (not-osb-os-osb-Bool-os-csb-csb (X1 ))-> U111 (ocb---ccb-osb-os-osb-Bool-os-csb-csb (X1 )) ocb---ccb-osb-os-osb-Bool-os-csb-csb (not-osb-os-osb-Bool-os-csb-csb (false ))-> osb---csb-osb-os-osb-Bool-os-csb-csb (true ) ocb---ccb-osb-os-osb-Bool-os-csb-csb (not-osb-os-osb-Bool-os-csb-csb (true ))-> osb---csb-osb-os-osb-Bool-os-csb-csb (false ) ocb---ccb-osb-os-osb-Nat-os-csb-csb (3 )-> osb---csb-osb-os-osb-Nat-os-csb-csb (s--osb-os-osb-Nat-os-csb-csb (s--osb-os-osb-Nat-os-csb-csb ( s--osb-os-osb-Nat-os-csb-csb (0 )))) ocb---ccb-osb-os-osb-Nat-os-csb-csb (4 )-> osb---csb-osb-os-osb-Nat-os-csb-csb (s--osb-os-osb-Nat-os-csb-csb (3 )) ocb---ccb-osb-os-osb-Nat-os-csb-csb (5 )-> osb---csb-osb-os-osb-Nat-os-csb-csb (s--osb-os-osb-Nat-os-csb-csb (4 )) ocb---ccb-osb-os-osb-Nat-os-csb-csb (8 )-> osb---csb-osb-os-osb-Nat-os-csb-csb (-+--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (3 ,5 )) ocb---ccb-osb-os-osb-Nat-os-csb-csb ( -+--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (0 ,N ))-> osb---csb-osb-os-osb-Nat-os-csb-csb (N ) ocb---ccb-osb-os-osb-Nat-os-csb-csb ( -+--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (X1 ,X2 ))-> U121 ( ocb---ccb-osb-os-osb-Nat-os-csb-csb (X2 ),X1 ) ocb---ccb-osb-os-osb-Nat-os-csb-csb ( -+--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (X1 ,X2 ))-> U131 ( ocb---ccb-osb-os-osb-Nat-os-csb-csb (X1 ),X2 ) ocb---ccb-osb-os-osb-Nat-os-csb-csb ( -+--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb ( s--osb-os-osb-Nat-os-csb-csb (N ),M ))-> osb---csb-osb-os-osb-Nat-os-csb-csb (s--osb-os-osb-Nat-os-csb-csb ( -+--osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (N ,M ))) ocb---ccb-osb-os-osb-Nat-os-csb-csb (s--osb-os-osb-Nat-os-csb-csb (X1 ))-> U141 (ocb---ccb-osb-os-osb-Nat-os-csb-csb (X1 )) ocb---ccb-osb-os-osb-Nat-os-csb-csb ( sd-osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (0 ,N ))-> osb---csb-osb-os-osb-Nat-os-csb-csb (N ) ocb---ccb-osb-os-osb-Nat-os-csb-csb ( sd-osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (N ,0 ))-> osb---csb-osb-os-osb-Nat-os-csb-csb (N ) ocb---ccb-osb-os-osb-Nat-os-csb-csb ( sd-osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (X1 ,X2 ))-> U151 ( ocb---ccb-osb-os-osb-Nat-os-csb-csb (X2 ),X1 ) ocb---ccb-osb-os-osb-Nat-os-csb-csb ( sd-osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (X1 ,X2 ))-> U161 ( ocb---ccb-osb-os-osb-Nat-os-csb-csb (X1 ),X2 ) ocb---ccb-osb-os-osb-Nat-os-csb-csb ( sd-osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb ( s--osb-os-osb-Nat-os-csb-csb (N ),s--osb-os-osb-Nat-os-csb-csb (M )))-> osb---csb-osb-os-osb-Nat-os-csb-csb ( sd-osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (N ,M )) ocb---ccb-osb-os-osb-Thruth-os-csb-csb ( is'Basin-osb-os-osb-BasinSet-os-csb-csb (V ))-> osb---csb-osb-os-osb-Thruth-os-csb-csb (tt ) ocb---ccb-osb-os-osb-Thruth-os-csb-csb ( is'Basin-osb-os-osb-BasinSet-os-csb-csb (X1 ))-> U171 ( ocb---ccb-osb-os-osb-BasinSet-os-csb-csb (X1 )) ocb---ccb-osb-os-osb-Thruth-os-csb-csb ( is'BasinSet-osb-os-osb-BasinSet-os-csb-csb (V ))-> osb---csb-osb-os-osb-Thruth-os-csb-csb (tt ) ocb---ccb-osb-os-osb-Thruth-os-csb-csb ( is'BasinSet-osb-os-osb-BasinSet-os-csb-csb (X1 ))-> U181 ( ocb---ccb-osb-os-osb-BasinSet-os-csb-csb (X1 )) ocb---ccb-osb-os-osb-Thruth-os-csb-csb (is'Bool-osb-os-osb-Bool-os-csb-csb (V ))-> osb---csb-osb-os-osb-Thruth-os-csb-csb (tt ) ocb---ccb-osb-os-osb-Thruth-os-csb-csb (is'Bool-osb-os-osb-Bool-os-csb-csb (X1 ))-> U191 (ocb---ccb-osb-os-osb-Bool-os-csb-csb (X1 )) ocb---ccb-osb-os-osb-Thruth-os-csb-csb (is'Nat-osb-os-osb-Nat-os-csb-csb (V ))-> osb---csb-osb-os-osb-Thruth-os-csb-csb (tt ) ocb---ccb-osb-os-osb-Thruth-os-csb-csb (is'Nat-osb-os-osb-Nat-os-csb-csb (X1 ))-> U201 (ocb---ccb-osb-os-osb-Nat-os-csb-csb (X1 )) sd-osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (0 ,N )-> N sd-osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (N ,0 )-> N sd-osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb ( s--osb-os-osb-Nat-os-csb-csb (N ),s--osb-os-osb-Nat-os-csb-csb (M ))-> sd-osb-os-osb-Nat-os-csb-csb-osb-os-osb-Nat-os-csb-csb (N ,M ) )