2013-02-27から1日間の記事一覧
∀,∃を消去するには,仮定と結論を分離し,十分条件などに帰着させる方法が一般的です. # g `(!x. &0<x ==> a<x )==> a<= &0` ;; Warning: Free variables in goal: a val it : goalstack = 1 subgoal (1 total) `(!x. &0 < x ==> a < x) ==> a <= &0` # e( STRIP_TAC );</x></x>…
∀,∃を消去するには,仮定と結論を分離し,十分条件などに帰着させる方法が一般的です. # g `(!x. &0<x ==> a<x )==> a<= &0` ;; Warning: Free variables in goal: a val it : goalstack = 1 subgoal (1 total) `(!x. &0 < x ==> a < x) ==> a <= &0` # e( STRIP_TAC );</x></x>…