equal
deleted
inserted
replaced
667 rec(a, 0, \%u v. rec(succ(v) |-| b, 0, \%x y.succ(v))) |
667 rec(a, 0, \%u v. rec(succ(v) |-| b, 0, \%x y.succ(v))) |
668 |
668 |
669 \tdx{div_def} a div b == |
669 \tdx{div_def} a div b == |
670 rec(a, 0, \%u v. rec(succ(u) mod b, succ(v), \%x y.v)) |
670 rec(a, 0, \%u v. rec(succ(u) mod b, succ(v), \%x y.v)) |
671 |
671 |
672 |
|
673 \tdx{add_typing} [| a:N; b:N |] ==> a #+ b : N |
672 \tdx{add_typing} [| a:N; b:N |] ==> a #+ b : N |
674 \tdx{addC0} b:N ==> 0 #+ b = b : N |
673 \tdx{addC0} b:N ==> 0 #+ b = b : N |
675 \tdx{addC_succ} [| a:N; b:N |] ==> succ(a) #+ b = succ(a #+ b) : N |
674 \tdx{addC_succ} [| a:N; b:N |] ==> succ(a) #+ b = succ(a #+ b) : N |
676 |
675 |
677 \tdx{add_assoc} [| a:N; b:N; c:N |] ==> |
676 \tdx{add_assoc} [| a:N; b:N; c:N |] ==> |