6:20 AM
Morning :3

8 hours later…
1:56 PM
@YokaiTheMonster Morning :P
@LeakyNun :P
@user21820 And another user trying to learn Python. :P

1 hour later…
3:06 PM
Define 1/2 S.O.A.P. as follows:

S(0,n) = n
S(x,n) = S(r(x,n),n+1), x≠0

r(k,n,x) = k-1, natural k>0
r({a,0,c},n) = r({a,b,0},n) = a
r({a,b,c},n) = {{a,b,r(c,n)},r(b,n),a}
r({0},n) = n
Notation: x' = ordinal which corresponds to x.
k' = k
{0}' = ω
{a,0,c}' = a'+1
{a,1,c}' = a'+c'
{a,2,c}' = a'*c'
{a,3,c}' = a'^c'

x → c if repeatedly applying r to x will eventually result in c.

Theorem 1:
Apple sauce is good.

Proof:
By definition.

Theorem 2:
k → m, m < k

Proof:
By definition.

Theorem 3:
{a,0,b} → a.

Proof:
By definition.

Theorem 4:
If b → c, then {a,1,b} → {a,1,c}.

Proof:
If b = c, by definition.
Otherwise, assume theorem 4 holds for {a,1,r(b,n)}
r(r({a,1,b},n),n) = {a,1,r(b,n)}
Theorem 7:
If {a,1,b}' is a limit ordinal, then r({a,1,b},n)' ≥ (a'+b')[n].

Proof:
If b = {0}, then
r({a,1,b},n)' = {{a,1,n},0,a}' = a'+n+1 ≥ a'+n = (a'+b')[n]
Otherwise, if assume theorem 7 holds for b.
r({a,1,b},n)' = {{a,1,r(b,n)},0,a}' = a'+r(b,n)'+1 ≥ a'+(b'[n]) = (a'+b')[n].

Theorem 8:
If a → 0, a' > 0, and {a,2,b}' is a limit ordinal, then r({a,2,b},n)' ≥ (a'*b')[n].

Proof:
If b = {0}, then
r({a,2,b},n)' = {{a,2,n},1,a}' = a'*n+a' ≥ a'*n = (a'*b')[n]
Otherwise, if assume theorem 8 holds for b.
@user21820 =) Spent the last few days trying to write a good proof that S({{0},3,{{0},3,{0}}},n) ≥ f_(ω^ω)(n), and I think I done it.

Soap and apple sauce don't go well together.

Well I originally had something in theorem 1, but it turned out I didn't need it, so I replaced it with apple sauce.
Probably didn't need theorem 2 either.
Theorems 7-9 may depend on each other?
I wasn't sure how to make it come out to good induction or whatever all at once.
In the process, I also managed to prove S({a,1,b},n) > S(a,S(b,n))
Shoot, theorems 7-9 have a mistake case I forgot.
Forgot that a*b is a limit ordinal if a is a limit ordinal.

3:46 PM
x'D So many little things in my 'proof,' still working on it.
Requires me to assume that a' ≥ r(a,n,x)'.
But idk how to prove that.

1 hour later…

4 hours later…
8:55 PM
@SimplyBeautifulArt a promising start for my upgrade of my 512 byte program:

Ah yes
Wonderful

I realised I was making things way to complicated by generating code to define functions with exec. And now I'm fring my brain with all the free bytes I have

frying*
Or freeing?

8:58 PM
'fring'? Is that supposed to by 'frying' or 'firing'?

I suppose it just means fring

I suppose you could be heading to Norfolk

I meant frying

Frying your brain can be hazardous to your health.

9:01 PM
Who knew?

Yeah, it's a bit of an obscure bit of knowledge

Sorry, I can't understand what ur saying with my fried brain

@Mithrandir I guess you've learned it from the Norfolk?

indeed

9:23 PM
uuurg: I made a function that outputs a better version of itself. To avoid having to make a special wrapping function to be able to properly nest it, I made it so when you call it it redefines itself. Only to an hour later realise my nesting function only loads the function it nests once. That's a lot of time wasted (see what I'm getting at with the brain Norfolk)

@fejfo =P