Hyperoperators [n] basics for large n

We could inductively define hyperoperators as follows:

a, b, n being positive integers:

a[1]b := a + b

n > 1 -> a[n]1 := a

a[n+1](b + 1) := a[n](a[n+1]b)

From this some lemmas can be proven:

1. a[2]b = a * b

2. a[3]b = a ^ b

3. 2[n]2 = 4

4. n > 2 -> 1[n]b = 1

5. a > 1 -> a[n](b + 1) > a[n]b

6. (a + 1)[n]b > a[n]b

7. ((a > 2 or b > 2) and a > 1 and b > 1) -> a[n+1]b > a[n]b

8.

1 < a < b

c = rounded up to integer

m > 0, k >= 0

Then: a [4] m >= c * (b + k) -> a [4] (m + k + 1) >= b [4] (k + 2)

Is this the common definition here?

Have proofs been given somewhere for the lemmas?

I wrote them down long time ago, and I was about to do it again before I discovered this forum.

[edit]Some minor corrections made in this post[/edit]

We could inductively define hyperoperators as follows:

a, b, n being positive integers:

a[1]b := a + b

n > 1 -> a[n]1 := a

a[n+1](b + 1) := a[n](a[n+1]b)

From this some lemmas can be proven:

1. a[2]b = a * b

2. a[3]b = a ^ b

3. 2[n]2 = 4

4. n > 2 -> 1[n]b = 1

5. a > 1 -> a[n](b + 1) > a[n]b

6. (a + 1)[n]b > a[n]b

7. ((a > 2 or b > 2) and a > 1 and b > 1) -> a[n+1]b > a[n]b

8.

1 < a < b

c = rounded up to integer

m > 0, k >= 0

Then: a [4] m >= c * (b + k) -> a [4] (m + k + 1) >= b [4] (k + 2)

Is this the common definition here?

Have proofs been given somewhere for the lemmas?

I wrote them down long time ago, and I was about to do it again before I discovered this forum.

[edit]Some minor corrections made in this post[/edit]