∀ x0 . x0 ∈ setminus omega (Sing 0) ⟶ ∀ x1 . x1 ∈ int ⟶ ∀ x2 : ο . (∀ x3 . and (x3 ∈ int) (∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (x1 = add_SNo (mul_SNo x3 x0) x5) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2 |
|
|
|
name |
---|
quotient_remainder_int |
|
|
|
|
|
|
|