2010-11-18から1日間の記事一覧
Commutativityの証明。 Include "../guru-lang/lib/plus.g". Define ch4_th : Forall(n m:nat). { (plus n m) = (plus m n) } := induction(n:nat) return Forall(m:nat). { (plus n m) = (plus m n) } with Z => foralli(m:nat). trans cong (plus * m) n_e…