Mathematics - 2017-09-10 (page 1 of 6)

Secret

00:07

Last night dream:

Let $L$ be a linear operator expressed in a vector space with a countable basis set and $a$ be a convergent countable sequence. Then $L$ has the following property:

$$\exists a, La=\lambda a$$

where $\sum_{n=1}^{\infty}a_n = \lambda$

Daminark

You mean a Schauder basis in particular, right?

Oh wait ofc

Sorry

But yeah I'm not clear what $a$ is here, do you mean $\lim a_n = a$ and there exists an eigenvector $b$?

Secret

$a$ is a convergent sequence which is an eigenvector of $L$, which has the property where its eigenvalue is the infinite sum of all its terms

Daminark

Oh so the vector space is a sequence space?

Secret

yup

Secret

00:28

Rarely do I recall the maths in dreams exactly and that it at least does not sounds gibberish

Daminark

Ah okay I'm following now

And fair

Secret

I have not learnt functional analysis yet, thus further investigation of it has to be done later

But my gut feeling is that that equation might restrict the possible Ls alot due to the eigenvalue depends on all terms in the eigenvector

Daminark

Actually in thinking about the Hamel vs Schauder basis thing I've realized you can prove that a Banach space cannot have a countable basis via BCT

It's really nifty, so you can show that a proper subspace of a normed space has empty interior

Because if you take a ball $B(x,r) \subset S$ (the subspace), then note that for any $z\in V$, you have $x + \frac{r}{2\|z\|}z \in S$

But then $z$ is a scalar multiple of that vector minus $x$, so $z\in S$

Now if you have a Banach space, assume $\{x_n\}$ form a Hamel basis

Then $\textrm{Span}(x_1,\ldots,x_n) = X_n$

Each $X_n$ is closed and has empty interior

But then their union can't be everything by BCT

Which is fun

Jasper

00:54

@Daminark Next time, in your exam, write nifty as well, lol.

Daminark

"Yo Professor [REDACTED] check out this sick lemma"

I'm not sure which of the two fits better

Jasper

lmao

I have a joke, so listen.

You can only lmao once in your life, because once you do it, you no longer have an ass.

Daminark

Heh

Jasper

@LeakyNun I seriously doubt the authenticity of that news.

@Daminark What would happen if you said 'Yo Professor, you are sick!' LOL

Secret

Grrr, this proof is immune to visualisation...

hmm...

The subspace $S$ is spanned by any $B(x,r) \subset S \subset V$ ?

thus it has no choice but to be V itself?

Hmm...

How about this:

In a normed space, $z \in V$ can always be rescaled because it can be converted into a unit vector. This result in any $z$ to lie within some $S$ where $B(x,r) \subset S$ for any $B \subset V$. Since we can start with picking a $z \in V -S$, it then follows that $V-S$ is empty

Daminark

01:19

I mean the finite dimensional picture is that a ball "pokes out" into each dimension

Secret

01:32

Another thing I noticed is that any $z \in V$ will end up be $\in S$, thus $S$ cannot be proper if it contains balls

@Daminark Btw, since the above theorem holds for any normed space, moving back to $\Bbb{R}^3$ with the eucledian norm, and picking a plane passing through the origin (thus a 2 dimensional subspace) does it mean that every point on this plane is the boundary in the topological sense?

Daminark

01:54

Yup

Secret

Ah, now it makes sense, because back in the times I am a layman (or at least back in linear algebra 1st year undergrad), all the points inside the plane will be intuitively like the interior to me

Daminark

02:06

Yeah, the trick is what dimensional ball

Secret

02:24

Let $X = \bigcup_{n \in \Bbb{N}}X_n$, where $X_n$ is defined as above the span of the hamel basis. Since by BCT $X \subset V$, is there a name for the space $V-X$?

One thing I am interested is how going from countable to uncountable will allow the space to reach $V-X$

Secret

02:38

hmm...

Actually, suppose I have a set of 2-balls in $\Bbb{R}^3$

then it logically follows that if I want the union of all 2-balls to be $\Bbb{R}^3$ itself, I will need uncountably many of them?

But maybe the analogy is not correct, as a countable union of finite sets is countable

Daminark

Closed 2-balls, yeah, by BCT

Secret

I am trying to understand the hamel basis in countable normed space. Since in such space, each vector has countably many components, then since a countable union of finite dimensional sets is countable, then it may seemed that countably many suitably chosen balls that spans 2 or 3 dimensions each should be able to fill in the whole space, but it does not as the property that the only subspace that has an interior is the whole space itself, and thus by BCT they cannot union to fill in the whole

space

So the question is then what do the missing points in $V-X$ look like, such that it takes uncountably many balls to reach them

Daminark

When you're in a Banach space, I dunno if you wanna think about components

Unless you're specifically looking at a sequence space

Secret

02:55

sequence spaces $\ell^p$ ($\in \Bbb{N} \cup \{\infty\}$) seemed to be the most simple and one of the most ubiquitous example of a countable banach space, thus I think we can start with that as an example

Daminark

Define "countable" Banach space

One with a Schauder basis?

Secret

Yeah I think so, as otherwise we cannot talk about each component of the vectors I think?

I think what I have in mind is the following:

In sequence space, we can index each element of the sequence with the natural numbers, thus each sequence has coutably many elements

I think I am trying to generalise that to some kind of formal sequence which is any countable set and these countable sets form a normed vector space

Daminark

Okay, so one way of saying it is a complete normed subspace of R^(infinity)

Secret

yeah that sounds right

Daminark

I mean the best thing is to explicitly say you're working in l^p

Secret

03:00

right, so that means sequence space is the word I am looking for

Daminark

Other Banach spaces with a Schauder basis have a coordinatization of the similar sort but thinking about linear operators through that tends to be clunky

I guess unless you're in L^p and doing Fourier but I dunno about that so I'll refrain from opening that can of worms

Leaky Nun

tahc ih.

@Jasper it's an urban legend lol

Daminark

Oy

Secret

Right, so the question narrows down to that we knew the hamel basis of a sequence space is also uncountable based on the BCT proof we just went through. In order to understand how so in a more "geometric" point of view, I need to know what the points $\ell^p -X$ look like

The following is my initial thought on how I think I can span this space with countably many finite dimensional balls that seemed make sense, but is wrong because it does not agree with the BCT proof

Let $\{X_n\}$ be a collection of finite dimensional subspaces of $\ell^p$ indexed by the natural numbers

The components of each $a\in \ell^p$ can likewise be given as $a_i$ for $i \in \Bbb{N}$

Now construct $\{X_n\}$ as follows:

Leaky Nun

@Secret use linear algebra to find $\displaystyle \int x^{10} \ln x \ \mathrm dx$ :P

Secret

03:10

For $e_i$ basis vectors in each $X_n$:
Let $X_1 = \text{span}(e_1,e_2,e_3)$
Let $X_2 = \text{span}(e_4,e_5,e_6)$
Let $X_2 = \text{span}(e_7,e_8,e_9)$
...
Let $X_2 = \text{span}(e_n,e_{n+1},e_{n+2}), n \in \Bbb{N}$

Thus $X = \bigcup_{n\in \Bbb{N}} X_n$

Yet by BCT, $X \subset \ell^p$, therefore what do the missing elements look like?

bolbteppa

2

Q: Hahn-Banach From Systems of Linear Equations

In this paper on the history of functional analysis, the author mentions the following example of an infinite system of linear equations in an infinite number of variables $c_i = A_{ij} x_j$: \begin{align*} \begin{array}{ccccccccc} 1 & = & x_1 & + & x_2 & + & x_3 & + & \dots \\ 1 & = & & &...

Who wouldn't find it interesting

Secret

03:31

Well I guess a probably naive comment of the above MSE is that: In the countable case is it even possible to reach the equation $x_{something}=1$

as without that, there is no way to know whether the equation is consistent

@LeakyNun If this is something related to minimal polynomials, then I have no idea

Leaky Nun

@Secret nothing with minimal polynomials

Secret

I only know that by IBP it equals to $\frac{x^{11}}{11}\ln x - \frac{x^{11}}{121}+C$

Leaky Nun

Not using IBP is the point

Secret

what kind of linear algebra do I need, it does not look very linear algebra like (other than $\int$ is a linear operator, but that's functional analysis)?

Leaky Nun

@Secret well use the fact that $\displaystyle \int$ is a linear operator :P

Secret

03:57

Hmm... if the question is $\int P(x)dx$ where $P(x)$ is a polynomial, then it is easy to see that $\int$ will have a finite matrix representation thus it can be multiplied to the matrix representation of $P(x)$ to solve for its integral.

So that means, we need some finite dimensional vector space that has $x \ln x$ as an element

and take its basis

Alternately, we can always use taylor series on $\ln x$ and solve it as a power series, but that's cheating because it is technically speaking an approximation

Leaky Nun

@Secret It's technically speaking not an approximation

@Secret right, so you need 24 dimensions:P

Secret

I don't really know how one can systematically find the finite linear combination of a function

if the basis or set of vectors is not given

$\{1,x,x^2,x^3,x^4,x^5,x^6,x^7,x^8,x^9,x^{10},ln x,noidea\}$

Leaky Nun

I already said 24 dimensions

Secret

$\frac{d}{dx}x^{10} \ln x = 10x^9 \ln x + \frac{x^{10}}{x}$

I have no idea how you derive 24

Leaky Nun

because $x^9 \ln x$ is not in your vector space

Secret

04:16

$\{1,x,x^2,x^3,x,x^5,x^6,x^7,x^8,x^9,x^{10},x^{11},\ln x, x\ln x\ln x,x^2\ln x,x^3\ln x,x^4\ln x,x^5\ln x,x^6\ln x,x^7\ln x,x^8\ln x,x^9\ln x,x^{10}\ln x,x^{11}\ln x\}$

sounds really ad hoc...

Leaky Nun

bingo

Secret

hmm...

$$\int f(x) dx$$

Let $f(x)=g(x)h(x)$

If $g(x)$ is a polynomial, then:

$\int^{(k)} g(x) dx$ is a polynomial for any $k \in \Bbb{N}$

If $g(x) = \ln x$, then:

$\int \ln x dx= x\ln x -x$
$\int^{(2)} \ln x dx = P(x) \ln x +Q(x)$
...
$\int^{(k)} \ln x dx$ is a linear combination of a polynomial times a ln x + a polynomial

That means...:

given a function $h(x) \in S$

If $$\int^{(k)} h(x) dx \in S, \forall k \in \Bbb{N}$$

and $g(x) \in S$ , then $\int g(x) dx$ can be solved via matrix representation of $\int$

where $|S| < \infty$

Risch algorithm

In symbolic computation (or computer algebra), at the intersection of mathematics and computer science, the Risch algorithm is an algorithm for indefinite integration. It is used in some computer algebra systems to find antiderivatives. It is named after the American mathematician Robert Henry Risch, a specialist in computer algebra who developed it in 1968. The algorithm transforms the problem of integration into a problem in algebra. It is based on the form of the function being integrated and on methods for integrating rational functions, radicals, logarithms, and exponential functions. Risch...

O wait, that might be the generalisation of the Rische algorithm I am seeking for

Leaky Nun

04:39

maybe try to solve it using power series lol

Kasmir Khaan

Hello

Leaky :D

Leaky Nun

hi

Kasmir Khaan

well I got some homework assigments

I need some help with

:D

If you are free ofc =p

Leaky Nun

ok

Kasmir Khaan

Btw leaky are you a proffesor of math ?

3

Leaky Nun

04:42

see my profile

Kasmir Khaan

oh :D

whats imperical

imprial Ä

imperial college* i mean lol

Leaky Nun

imperial college london

Kasmir Khaan

Is that like very good uni?

Leaky Nun

lol

Kasmir Khaan

sorry ><

Lets focus on problems =p

all righty , most of the problems has something to do with isomorphism

Abcd

04:44

@KasmirKhaan Lol, that's what I asked him some days ago

Kasmir Khaan

the thing is we did not do any theorem about that

@Abcd haha same questions ? ><

Leaky Nun

go on

Abcd

@KasmirKhaan Yes exactly same question xD

Kasmir Khaan

Ehm so without having the theorems for isomorphims

How to prove the groups are the same

my ideas are

group table

if we they are the same, like structure is the same , we can say they are isomorphic, up to relabling of the elements

Leaky Nun

visualize the group

Kasmir Khaan

04:46

is that considered a proof?

Leaky Nun

no, it helps your intuition

Kasmir Khaan

but I can't find a function phi

such that f(xy) = f(x)f(y)

Leaky Nun

what are the groups?

Kasmir Khaan

S_3 and GL_2(Z/2)

I found the 1-1 map

I can associate each element from one group to the other

checked it works

Leaky Nun

no, you don't find a 1-1 map

Kasmir Khaan

04:48

i meant

1-1 correspondance

Leaky Nun

that's hardly how you do this kind of problems

Kasmir Khaan

Hmm then how do we do them ?

Leaky Nun

isomorphism requires homomorphism and bijection

Kasmir Khaan

I get that

Leaky Nun

work with homomorphism, not bijection

Kasmir Khaan

04:49

should I write the 36 products?

in the proof I mean

Leaky Nun

...

of course not

Kasmir Khaan

How to prove that its a hom then ?

Leaky Nun

list the elements of S_3

(so that we have the same notation)

Kasmir Khaan

okay

e, (12) , (13) , (23) , (123), (132)

Leaky Nun

$\begin{bmatrix}1&0\\0&1\end{bmatrix}$ $\begin{bmatrix}1&0\\1&1\end{bmatrix}$ $\begin{bmatrix}1&1\\0&1\end{bmatrix}$
$\begin{bmatrix}0&1\\1&0\end{bmatrix}$ $\begin{bmatrix}1&1\\1&0\end{bmatrix}$ $\begin{bmatrix}0&1\\1&1\end{bmatrix}$

tell me what e maps to @KasmirKhaan

Kasmir Khaan

04:52

okay lets go from left to write

Leaky Nun

56 secs ago, by Leaky Nun

tell me what e maps to @KasmirKhaan

you should be able to answer this in one second.

@KasmirKhaan no, I'm not going from left to right

Kasmir Khaan

e , (13), (23) , (1,2) ,(123) , (132)

I meant

from what you sent me ,

@anon Hello !

Leaky Nun

@KasmirKhaan, follow my guides.

Kasmir Khaan

Okay

Leaky Nun

3 mins ago, by Leaky Nun

tell me what e maps to @KasmirKhaan

Kasmir Khaan

04:55

e maps to e

allways =p

Identity matrxi

Leaky Nun

which one?

right

4 mins ago, by Leaky Nun

$\begin{bmatrix}1&0\\0&1\end{bmatrix}$ $\begin{bmatrix}1&0\\1&1\end{bmatrix}$ $\begin{bmatrix}1&1\\0&1\end{bmatrix}$
$\begin{bmatrix}0&1\\1&0\end{bmatrix}$ $\begin{bmatrix}1&1\\1&0\end{bmatrix}$ $\begin{bmatrix}0&1\\1&1\end{bmatrix}$

find an element with order 3 from here

Kasmir Khaan

Yes I answered that question based on those elements you wrote

Leaky Nun

1 min ago, by Leaky Nun

find an element with order 3 from here

this is my second question

Kasmir Khaan

(123) , (132)

Leaky I allready did this part =p

I am just wonderign , besides writing the group tables

is there another way to show that they are isomorphic

Leaky Nun

well

you just need to find what the two generators map to, and then express the other elements in both groups in terms of the two generators

Daminark

04:59

Hai

Kasmir Khaan

Its like, they both non abelian, both not cyclic , elements of some order are the same

(123) and (23) generates S_3

I think any transpotion with total permutation does

but did not prove that

Leaky Nun

I usually use (1,2) and (2,3) but whatever floats your boat

Kasmir Khaan

hmm

let me think one second here =p

Leaky Nun

after finding the generators, express the elements in terms of them

Kasmir Khaan

if we same that 2 elements generate the group

can we have one elemnt to the power 0 ?

Leaky Nun

05:03

of course

Kasmir Khaan

lets use (12) , (23) , so we have

(12), (23) , (123) =(12) (23) , (132) = (23) (12) ,

we have e also

let me see how we get (13)

(12) (23)(12) = (13)

Leaky Nun

is that it?

Kasmir Khaan

all righty , S_3 = < (12),(23) >

Yes we got 6 elements

Leaky Nun

ok, then find out what those map to

and then express the other elements in terms of the image

Kasmir Khaan

(12) maps to 1's on the second diagonal

0's on the rest

(23) maps to all 1's exept for entry 21 of the matrix is 0

upper triangular

express the other elements in terms of the image ?

Leaky Nun

05:10

yes

Kasmir Khaan

I dont know what that means

Leaky Nun

i mean in terms of the two matrices

Kasmir Khaan

Yes I know that the image is the elements of GL

did you mean f(xy) = f(x) f(y)

using the generators?

Leaky Nun

you mapped the two generators to two matrices

Kasmir Khaan

Yes

Leaky Nun

05:12

express other matrices in terms of them

Kasmir Khaan

oh

but thats the same thing

oh well I think I got it :D

since the order of the groups is the same

I need only to show that this map is 1-1

and ill be done :D

I got few more more questions =p

@LeakyNun by analyzing the multiplication table, prove that every group of order 4 is isomorphic to either Z/2 x Z/2 or Z/4

I think here the important point is that

in a group each element can accur only once in each row and column

Leaky Nun

go on

Kasmir Khaan

from that I can exclude things like order of g = 3

in case of Z/4

since Z/4 is cyclic

G = <a> = {e, a,aa,aaa}

and I can show the hom easy ,1-1 and onto easy from a^k is mapper to 1^k

and for Z/2 x Z/2 , we can exclude order of elemnt to be 4

because that would be a copy of Z/4

order 3 is also excluded because then it wont be a group

only thing left is order 2

so that group is a^2 = e for all a in G

These are not formal ideas I know but how to make them more formal ?@LeakyNun

Leaky Nun

by analyzing the multiplication table.

Kasmir Khaan

Yes I did that

I mean i have the tables infront of me

but that is the problem that i have

dont know how to make things formal

Leaky Nun

05:25

1

Q: Classifying groups of order 4

Let $G$ be a group of order $4$ then either $ G \cong C_4$ or $G \cong C_2 \times C_2$ the proof my lecture gave goes as follows: Let $x \in G$ then by Lagrange $\text{ord}(x)$ divides $|G| =4 $ so w ehave either 1) $\exists x \in G$ with $x^4 = 1$ or 2) $\forall x \in G, x^2 = 1$ He then go...

abstract-algebra group-theory finite-groups

Kasmir Khaan

Thanks :D

Did you give me that because you knew I understood the concept

or just because -.-

Leaky Nun

what?

Kasmir Khaan

I mean like

Did you give me the answer because you knew I understood the concept

because I don't want the answer , I want to learn how to do things right

Well I can do the rest on my own now =p

Btw can I still send you emails on the homeworks?

Leaky Nun

you just asked me how to make it formal

@KasmirKhaan ok

Kasmir Khaan

( once they are on textstudio ofc ) ><

Yes Ineed to see more examples how to write things to get exprience =p

Leaky Nun

05:31

ok

Kasmir Khaan

All righty then =p

I think that is all the help I need from the second assigment :D

once am done with them, Ill email them for you :D

@LeakyNun Thanks for all your help again :D I have to go so see you later :)

Leaky Nun

ok

Secret

Btw some typo in the previous message:

Little Rookie

3

Q: Question regarding Gambler's Ruin

Consider a gambling process $(X_n)_{n∈\mathbb{N}}$ on the state space $S = {0, 1, . . . , N}$, with probability $p$, resp. $q$, of moving up, resp. down, at each time step. For $x = 0, 1, . . . , N$, let $τ_x$ denote the first hitting time, $τ_x := \inf\{n ≥ 0 : X_n = x\}$ Let $p_x := P(τ_{x+1} <...

probability stochastic-processes markov-chains

Secret

Right, so the question narrows down to that we knew the hamel basis of a sequence space is also uncountable based on the BCT proof we just went through. In order to understand how so in a more "geometric" point of view, I need to know what the points $\ell^p -X$ look like
The following is my initial thought on how I think I can span this space with countably many finite dimensional balls that seemed make sense, but is wrong because it does not agree with the BCT proof
Let $\{X_n\}$ be a collection of finite dimensional subspaces of $\ell^p$ indexed by the natural numbers

Leaky Nun

06:04

Is Collatz conjecture expressible in first-order Peano logic?

Alessandro Codenotti

06:30

Yes but it requires some work

Let $s(n)$ be a finite sequence of natural numbers such that for all $n$ such that $n+1$ is in the domain of $s$ we have $2s(n+1)=s(n)$ if $n$ is even and $s(n+1)=3s(n)+1$ if $n$ is odd. Then Collatz says "for all $k$ there is such an $s$ and an $n$ with $s(0)=k$ and $s(n)$=1$

usukidoll

hello

Alessandro Codenotti

Gödel worked out how to code finite sequences of natural numbers in PA but I forgot the details

Leaky Nun

@AlessandroCodenotti :O

usukidoll

PA?

Leaky Nun

@usukidoll Peano arithmetic

usukidoll

06:39

anyone wanna give feedback on a linear algebra proof? I think I got it but the way it's sounding is a bit off... :S

@LeakyNun OOOoh

Leaky Nun

@usukidoll just ask it.

Alessandro Codenotti

18

Q: How is exponentiation defined in Peano arithmetic?

How would exponentiation be defined in Peano arithmetic? Unless $n$ is fixed natural number, $x^n$ seems to be hard to define. Edit 2: So, what would be the way to define $x^n+y^n = z^n$ using $\Sigma_1^0$ formula? Edit: OK, I say Peano arithmetic has addition and multiplication stuffs. This a...

logic peano-axioms

Hm I always forget how to avoid that preview to pop up and take half of the chat space

Leaky Nun

@AlessandroCodenotti [link](link)

@AlessandroCodenotti it's so beautiful and mesmerizing...

usukidoll

:S

Martin Sleziak

@AlessandroCodenotti The post mentioned in general topology chat room might be related to this. (At least to some extent. To be honest, I am now less sure than when I typed my first response to you.)

But it might be worth having a look if you are still interested in that problem.

Leaky Nun

06:44

@MartinSleziak where does the question above about PA belong?

in terms of, you know, chatroom

Alessandro Codenotti

@MartinSleziak thanks, I didn't notice you posted it in another room! I've only dealt with (upper) semicontinuity once so I'm not really familiar with it, I'll get back to this problem after I'm done with my exam tomorrow though

usukidoll

ok it sounds a bit tacky... x_X! I'm referring to my proof answer. :S @LeakyNun should I still post it here?

Martin Sleziak

@Daminark Incidentally, uncountability of Hamel basis in Banach spaces was a topic recently in functional analysis chat room. And, as expected, there is a post on main about this: Let $X$ be an infinite dimensional Banach space. Prove that every Hamel basis of X is uncountable..

Leaky Nun

@usukidoll if you have a question, ask it. Don't ask "is anyone ..." because nobody is obliged to answer your problems

usukidoll

>:O kicking myself for finding a great topology supplemental book 3 weeks into the semester. ugh

Leaky Nun

06:48

@AlessandroCodenotti do you have some puzzles for PA?

Alessandro Codenotti

Not really, I don't know much about logic

Leaky Nun

chat is behaving strangely these days

16

A: How is exponentiation defined in Peano arithmetic?

Using the following abbreviations $$\begin{align}a\le b&\equiv\exists n\colon a+n=b\\ a< b&\equiv Sa\le b\\ \operatorname{mod}(a,b,c)&\equiv \exists n\colon a=b\cdot n+c\land c<b\\ \operatorname{seq}(a,b,k,x)&\equiv \operatorname{mod}(a,S(b\cdot Sk),x)\\ \operatorname{pow}(a,b,c)&\equiv\exists x...

@AlessandroCodenotti I find this answer neater than the accepted answer

@AkivaWeinberger hi

Akiva Weinberger

07:03

Hi

$\sqrt{x^2+1}+x$ and $\sqrt{x^2+1}-x$ are multiplicative inverses

Leaky Nun

Are you interested in PA?

@AkivaWeinberger right

Akiva Weinberger

They are also reflections of each other in the $y$-axis

and they kinda look like $e^x$ if it grew linearly

(in that it's always positive and goes to zero as $x$ goes to $-\infty$)

Leaky Nun

neat

Akiva Weinberger

(The first one, at least; the second is the mirror image)

I think I should probably dip out of chat and go to bed though

Bye

Leaky Nun

Both $e^x$ and $\sqrt{x^2+1}+x$ satisfy the functional equation $f(x) f(-x) = 1$

usukidoll

07:12

cat stew

Kenny Lau

07:37

Assumptions:
S(x) !=  0.
S(x) = S(y) -> x = y.
exists y S(x) = y.
Goal:
S(0) != S(S(0)).

Proof generated:

1 S(x) = S(y) -> x = y # label(non_clause).  [assumption].
2 (exists x S(y) = x) # label(non_clause).  [assumption].
3 S(0) != S(S(0)) # label(non_clause) # label(goal).  [goal].
4 S(x) != 0.  [assumption].
5 S(x) != S(y) | x = y.  [clausify(1)].
6 S(x) = f1(x).  [clausify(2)].
7 S(S(0)) = S(0).  [deny(3)].
8 f1(f1(0)) = f1(0).  [copy(7),rewrite([6(2),6(3),6(5)])].
9 f1(x) != f1(y) | x = y.  [back_rewrite(5),rewrite([6(1),6(2)])].
10 f1(x) != 0.  [back_rewrite(4),rewrite([6(1)])].
11 f1(0) = 0.  [hyper(9,a,8,a)].

computers are so powerful now, lol

Transcript for

$Mathematics$ Mathematics