2014-06-03から1日間の記事一覧
以前にも書いた排中律ネタですが,今回は連言から存在量化を纏める形のものです. g `!p:A->bool. !q:bool. (?x. p x ==> q) ==> (?y. q ==> p y) ==> (?z. p z <=> q)`;; e( REPEAT STRIP_TAC );; e( DISJ_CASES_TAC (SPEC `q:bool` EXCLUDED_MIDDLE) );; e…
以前にも書いた排中律ネタですが,今回は連言から存在量化を纏める形のものです. g `!p:A->bool. !q:bool. (?x. p x ==> q) ==> (?y. q ==> p y) ==> (?z. p z <=> q)`;; e( REPEAT STRIP_TAC );; e( DISJ_CASES_TAC (SPEC `q:bool` EXCLUDED_MIDDLE) );; e…