19 rec_def "rec(k,a,b) == transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))" |
19 rec_def "rec(k,a,b) == transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))" |
20 |
20 |
21 add_def "m#+n == rec(m, n, %u v.succ(v))" |
21 add_def "m#+n == rec(m, n, %u v.succ(v))" |
22 diff_def "m#-n == rec(n, m, %u v. rec(v, 0, %x y.x))" |
22 diff_def "m#-n == rec(n, m, %u v. rec(v, 0, %x y.x))" |
23 mult_def "m#*n == rec(m, 0, %u v. n #+ v)" |
23 mult_def "m#*n == rec(m, 0, %u v. n #+ v)" |
24 mod_def "m mod n == transrec(m, %j f. if(j:n, j, f`(j#-n)))" |
24 mod_def "m mod n == transrec(m, %j f. if(j<n, j, f`(j#-n)))" |
25 div_def "m div n == transrec(m, %j f. if(j:n, 0, succ(f`(j#-n))))" |
25 div_def "m div n == transrec(m, %j f. if(j<n, 0, succ(f`(j#-n))))" |
26 end |
26 end |