2011-11-20から1日間の記事一覧
今回は # g( `!p q. p*p=2*q*q ==> q=0` );; val it : goalstack = 1 subgoal (1 total)`!p q. p * p = 2 * q * q ==> q = 0` をpについての wellfounded induction で証明します.方針は,p*p=2*q*qならばpは偶数,p=2r従って2*r*r=q*qと表せて仮定が使える…
今回は # g( `!p q. p*p=2*q*q ==> q=0` );; val it : goalstack = 1 subgoal (1 total)`!p q. p * p = 2 * q * q ==> q = 0` をpについての wellfounded induction で証明します.方針は,p*p=2*q*qならばpは偶数,p=2r従って2*r*r=q*qと表せて仮定が使える…