(VAR N V1 V ) (RULES U101 (tt )-> tt U11 (tt ,V )-> isInf-osb-os-osb-Nat-os-csb-csb (V ) U111 (tt )-> tt U121 (tt )-> tt U131 (tt )-> tt U21 (tt ,N )-> U22 (isNat-osb-os-osb-Nat-os-csb-csb (N ),N ) U22 (tt ,N )-> U23 (is'Inf-osb-os-osb-Nat-os-csb-csb ( s-osb-os-osb-Nat-os-csb-csb (s-osb-os-osb-Nat-os-csb-csb (N )))) U23 (tt )-> tt U31 (tt ,V )-> isNat-osb-os-osb-Nat-os-csb-csb (V ) U41 (tt )-> tt U51 (tt ,V )-> U52 (isInf-osb-os-osb-Nat-os-csb-csb (V )) U52 (tt )-> tt U61 (tt ,V1 )-> U62 (isNat-osb-os-osb-Nat-os-csb-csb (V1 )) U62 (tt )-> tt U71 (tt )-> tt U81 (tt )-> tt U91 (tt )-> tt is'Inf-osb-os-osb-Nat-os-csb-csb (V )-> U11 (isos-osb-Nat-os-csb (V ),V ) is'Inf-osb-os-osb-Nat-os-csb-csb (s-osb-os-osb-Nat-os-csb-csb (N ))-> U21 ( isos-osb-Nat-os-csb (N ),N ) is'Nat-osb-os-osb-Nat-os-csb-csb (V )-> U31 (isos-osb-Nat-os-csb (V ),V ) is'Thruth (V )-> isThruth (V ) is'Thruth-osb-os-osb-Thruth-os-csb-csb (V )-> U41 (isThruth (V )) is'os-osb-Nat-os-csb (V )-> isos-osb-Nat-os-csb (V ) is'os-osb-Thruth-os-csb (V )-> isos-osb-Thruth-os-csb (V ) isNat-osb-os-osb-Nat-os-csb-csb (0 )-> tt isNat-osb-os-osb-Nat-os-csb-csb (V )-> U51 (isos-osb-Nat-os-csb (V ),V ) isNat-osb-os-osb-Nat-os-csb-csb (s-osb-os-osb-Nat-os-csb-csb (V1 ))-> U61 ( isos-osb-Nat-os-csb (V1 ),V1 ) isThruth (tt )-> tt isos-osb-Nat-os-csb (0 )-> tt isos-osb-Nat-os-csb (s-osb-os-osb-Nat-os-csb-csb (V1 ))-> U71 ( isos-osb-Nat-os-csb (V1 )) isos-osb-Thruth-os-csb (V )-> U81 (is'Thruth (V )) isos-osb-Thruth-os-csb (tt )-> tt isos-osb-Thruth-os-csb (is'Inf-osb-os-osb-Nat-os-csb-csb (V1 ))-> U91 ( isos-osb-Nat-os-csb (V1 )) isos-osb-Thruth-os-csb (is'Nat-osb-os-osb-Nat-os-csb-csb (V1 ))-> U101 ( isos-osb-Nat-os-csb (V1 )) isos-osb-Thruth-os-csb (is'Thruth-osb-os-osb-Thruth-os-csb-csb (V1 ))-> U111 ( isos-osb-Thruth-os-csb (V1 )) isos-osb-Thruth-os-csb (isInf-osb-os-osb-Nat-os-csb-csb (V1 ))-> U121 ( isos-osb-Nat-os-csb (V1 )) isos-osb-Thruth-os-csb (isNat-osb-os-osb-Nat-os-csb-csb (V1 ))-> U131 ( isos-osb-Nat-os-csb (V1 )) )