2010-11-19から1日間の記事一覧
だんだん込み入ってきた。 Include "../usr/guru-lang/lib/nat.g". Include "../usr/guru-lang/lib/plus.g". Define plusZ' := foralli(x:nat)(u : {x = Z}). trans cong (plus * *) u % (plus x x) = (plus Z Z) join (plus Z Z) Z. % (plus Z Z) = Z Defin…