コンテンツにスキップ

Mizar/定義型/defpred

出典: フリー教科書『ウィキブックス(Wikibooks)』

defpred P[Nat] means $1*($1-1);

P[n]≡n*(n-1);