Anonymous user
Talk:Proof: Difference between revisions
no edit summary
m (→Satisfaction) |
No edit summary |
||
Line 89:
:::::::: Yes -- should be fixed now though. Free variables are now distinct in the context of arithmetic (and relations) but are associated with a canonical (but arbitrary) ordering when generating results. --[[User:Rdm|Rdm]] 21:17, 5 June 2012 (UTC)
::::::::: Now, there is a problem with large expressions:
::::::::: <lang j> 'A B C D' induction '(A addition (B addition (C addition D))) equals ((B addition (C addition D)) addition A)'
|assertion failure: assert
| assert(#all)>#;._1 LF,y</lang>
::::::::: I changed the code like this:
::::::::: <lang j>add=: +/ dyadic
mul=: */ dyadic
even=: [: context kernel@add~"0@,@kernel :[:
odd=: successor@even
defined=: '(zero -. exists_in odd successor equals is_member_of add mul even)'</lang>
::::::::: so that
::::::::: <lang j>'A B C D' induction '(A add (B add (C add D))) equals ((B add (C add D)) add A)'</lang>
::::::::: now holds (but it slow!), however:
::::::::: <lang j> 'A B C D E' induction '(A add ((B add E) add (C add D))) equals ((B add (C add D)) add (A add E))'
|assertion failure: assert
| assert 0!:3 y
'A B C' induction '(A mul (B mul C)) equals ((A mul B) mul C))'
|assertion failure: assert
| assert 0!:3 y</lang>
::::::::: Also, why is <code># all = 82</code>? Or it is context-dependent? — [[User:Ht|Ht]] 23:06, 5 June 2012 (UTC)
== Huh? ==
| |||