I have not read the full proof, yet, but I see a flaw: a1 =: _100 + rnd 27 $ 200
This should be a1 =: _100 + 27 rnd 200 Otherwise you might have multiple values that are the same in a1, and if one of those is selected by ij that violates your condition b1 (this happens when you assign a value to 't'). Also, I do not understand what n and m represent, so I had to stop reading the proof when I got to that point. Thanks, -- Raul On Mon, Mar 3, 2014 at 12:40 AM, Michal Wallace <[email protected]> wrote: > ( I think this got marked as spam yesterday because I used HTML formatting, > so I'm trying again. > There was a longer transcript of a j session using the logic stuff. I'll > repost that on the programming list. ) > > Here's a derivation of the quadratic formula in J. > > https://github.com/tangentstorm/tangentlabs/blob/master/j/quadratic.ijs#L132 > > I also use this quite a bit on IRC: > > https://github.com/tangentstorm/tangentlabs/blob/master/j/logic.ijs > > The majority of the lines in those files are just assertions, using a > slightly modified version of the 'assert' verb in the z locale. > A large portion of the lines are in fact identities. > ---------------------------------------------------------------------- > For information about J forums see http://www.jsoftware.com/forums.htm ---------------------------------------------------------------------- For information about J forums see http://www.jsoftware.com/forums.htm
