(VAR N V1 V2 V ) (RULES U11-Thruth-os-osb-Nat-os-csb (tt ,N )-> U12-os-osb-Thruth-os-csb ( is'Inf-os-osb-Nat-os-csb (s-os-osb-Nat-os-csb (s-os-osb-Nat-os-csb (N )))) U11-os-osb-Thruth-os-csb-os-osb-Nat-os-csb (V1 ,V2 )-> U11-Thruth-os-osb-Nat-os-csb (V1 ,V2 ) U12-Thruth (tt )-> tt U21-Thruth (tt )-> tt U21-os-osb-Thruth-os-csb (V1 )-> U21-Thruth (V1 ) U31-Thruth (tt )-> tt U31-os-osb-Thruth-os-csb (V1 )-> U31-Thruth (V1 ) is'Inf-os-osb-Nat-os-csb (V )-> isInf-os-osb-Nat-os-csb (V ) is'Inf-os-osb-Nat-os-csb (s-os-osb-Nat-os-csb (N ))-> U11-os-osb-Thruth-os-csb-os-osb-Nat-os-csb (isNat-os-osb-Nat-os-csb (N ),N ) is'Nat-os-osb-Nat-os-csb (V )-> isNat-os-osb-Nat-os-csb (V ) is'Thruth-Thruth (V )-> tt is'Thruth-os-osb-Thruth-os-csb (V1 )-> is'Thruth-Thruth (V1 ) isNat-os-osb-Nat-os-csb (0 )-> tt isNat-os-osb-Nat-os-csb (V )-> U21-os-osb-Thruth-os-csb ( isInf-os-osb-Nat-os-csb (V )) isNat-os-osb-Nat-os-csb (s-os-osb-Nat-os-csb (V1 ))-> U31-os-osb-Thruth-os-csb (isNat-os-osb-Nat-os-csb (V1 )) )