1 | | ~~Notation:~~ |

2 | | ~~{{{~~ |

3 | | ~~m,n,k: natural numbers~~ |

4 | | ~~a,b,c: types of kind Nat~~ |

5 | | ~~}}}~~ |

6 | | |

7 | | ~~Top-level interactions for {{{TypeNat}}}:~~ |

8 | | ~~{{{~~ |

9 | | ~~TypeNat m~~ |

10 | | ~~}}}~~ |

11 | | |

12 | | ~~Top-level interactions for <=~~ |

13 | | ~~{{{~~ |

14 | | ~~m <= n <=> {m <= n} = True~~ |

15 | | ~~0 <= a <=> True~~ |

16 | | ~~a <= 0 <=> a ~ 0~~ |

17 | | ~~}}}~~ |

18 | | |

19 | | ~~Top-level interactions for +.~~ |

20 | | ~~{{{~~ |

21 | | ~~(m + n ~ k) <=> {m + n} = k~~ |

22 | | ~~(m + a ~ n) <=> a ~ {n - m} -- n >= m~~ |

23 | | ~~(a + m ~ n) <=> a ~ {n - m} -- n >= m~~ |

24 | | ~~(0 + a ~ b) <=> a ~ b~~ |

25 | | ~~(a + 0 ~ b) <=> a ~ b~~ |

26 | | ~~(a + b ~ 0) <=> (a ~ 0, b ~ 0)~~ |

27 | | ~~(a + b ~ a) <=> (b ~ 0)~~ |

28 | | ~~(a + b ~ b) <=> (a ~ 0)~~ |

29 | | ~~(a + a ~ b) <=> (2 * a ~ b)~~ |

30 | | ~~}}}~~ |

31 | | |

32 | | ~~Top-level interactions for *.~~ |

33 | | ~~{{{~~ |

34 | | ~~(m * n ~ k) <=> {m * n} = k~~ |

35 | | ~~(m * a ~ n) <=> a ~ {n / m} -- m `divides` n~~ |

36 | | ~~(a * m ~ n) <=> a ~ {n / m} -- m `divides` n~~ |

37 | | ~~(0 * a ~ b) <=> b ~ 0~~ |

38 | | ~~(a * 0 ~ b) <=> b ~ 0~~ |

39 | | ~~(1 * a ~ b) <=> a ~ b~~ |

40 | | ~~(a * 1 ~ b) <=> a ~ b~~ |

41 | | ~~(a * b ~ 1) <=> (a ~ 1, b ~ 1)~~ |

42 | | ~~(a + a ~ b) <=> 2 ^ a ~ b~~ |

43 | | ~~}}}~~ |

44 | | |

45 | | ~~Top-level interactions for ^~~ |

46 | | ~~{{{~~ |

47 | | ~~(m ^ n ~ k) <=> {m ^ n} = k~~ |

48 | | ~~(m ^ a ~ n) <=> a ~ {log m n} -- log (base m) of n exists~~ |

49 | | ~~(a ^ m ~ n) <=> a ~ {root m n} -- m-th root of n exists~~ |

50 | | ~~(a ^ 0 ~ b) <=> b ~ 1~~ |

51 | | ~~(1 ^ a ~ b) <=> b ~ 1 ~~ |

52 | | ~~}}}~~ |