12:24 AM
Got it. Define simple custom notions of equals, unequals, or, then ask it if the question equation can be proven equal or unequal. It terminates and upon inspection I see it proved that 1+1 is unequal to 3.
```axioms={
ForAll[a,equals[a,a]==true],
ForAll[{a,b},equals[a,b]==equals[b,a]],
ForAll[a,notequals[s[a],a]==true],
ForAll[a,notequals[s[a],0]==true],
ForAll[{a,b},notequals[a,b]==notequals[b,a]],
ForAll[a,or[true,a]==true],
ForAll[a,or[a,true]==true],
ForAll[a,ForAll[a,plus[a,0]==a]],
ForAll[{a,b},plus[a,s[b]]==s[plus[a,b]]]
};
FindEquationalProof[or[equals[s[s[s[0]]],plus[s[0],s[0]]],notequals[s[s[s[0]]],plus[s[0],s[0]]]]==true,axioms]```
Fun!

8 hours later…
8:10 AM
@Alucard, in principal may is fine too, thought the sooner the internship starts the better. Go ahead and apply and we will see if we can work out things from there.

5 hours later…
1:30 PM
Can anyone point me to a QA with, more or less, how to draw the unit vector components at the end of a vector, i.e. off of the arrow head?
Thank you kindly, in advance! I am pretty keyword illiterate and can't find it to save my life.
It's probably not even the unit vector components I'm trying to visualize, it's more-so the two normal components to the vector as it is at that moment of time, so then they're parameterized such that, I suppose, the tip of the vector is the new origin? I remember seeing a coin flip QA with them added. like UVW instead of XYZ

2:08 PM
@CATrevillian I can't really be certain of what you mean... but something like `With[{vec={3,1,2}},Graphics3D[{Arrow[Tube@{{0,0,0},vec}],Arrow[Tube@{vec,vec+#}]&/@(vec IdentityMatrix[3])}]]` comes to mind...

2:25 PM
That's nearly there, I think I cobbled something horrendous together that works for what I was trying to do
which is make something like this
But without spiraling in, yet, haha. Thank you for the more general approach, I will see what I can muster, and post later what monstrosity I brought into existence

2:39 PM
@CATrevillian I'd say my code is pretty much... "write-only." :o
but you can do curved `Arrow`s too.