2011-11-13から1日間の記事一覧
今回は,量化,論理結合,対称式を含んだ # g `!x y:real. &0 (&0 &0 val it : goalstack = 1 subgoal (1 total)`!x y. &0 (&0 &0 を場合分けを用いて証明します.なお,証明自体は,REAL_FIELDでは # REAL_FIELD `!x y. &0 (&0 &0 と失敗しますが,MESONに …
今回は,量化,論理結合,対称式を含んだ # g `!x y:real. &0 (&0 &0 val it : goalstack = 1 subgoal (1 total)`!x y. &0 (&0 &0 を場合分けを用いて証明します.なお,証明自体は,REAL_FIELDでは # REAL_FIELD `!x y. &0 (&0 &0 と失敗しますが,MESONに …