Talk:Proof: Difference between revisions
Content added Content deleted
m (→Satisfaction) |
No edit summary |
||
Line 89: | 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) |
:::::::: 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? == |
== Huh? == |