Revision as of 11:42, 1 June 2012 (view source) Rdm (talk \| contribs) (J: show some (boring but relevant) output) ← Older edit		Revision as of 19:58, 5 June 2012 (view source) Rdm (talk \| contribs) (J: bug fix) Newer edit →
Line 444: exists_in=: 1&e.@e. induction=:4 :0 3 :'(y)=:?~#all'&.>;:x assert (#all) > #;._1 LF,y assert 0 = # y -.&;: LF,defined,x

Proof: Difference between revisions

Proof (view source)