日本語風証明

i, j, k, l, m, n は 自然 数 とする。
このとき
i + k = j + k ならば i = j
証明:
  まず 述語を定義する: P[自然 数] とは
    i + $1 = j + $1 ならば i=j であること。
  (A1): P[0] ※帰納法のベース
  証明:
    次を仮定する:
    (B0): i + 0 = j + 0 。
    このとき
    (B1): i + 0 = i 根拠は INDUCT:3 。
    (B2): j + 0 = j 根拠は INDUCT:3 。
    従って 目的の命題 根拠は B0,B1,B2 。
  終り。
  (A2): 任意の k ただし P[k] に対して P[succ k] ※帰納法のステップ
  証明:
    考えよう m を、ただし
    (C1): P[m] 。
    次を仮定する:
    (C2): i + (succ m) = j + (succ m) 。
    すると
    (C3): succ(i + m) = j + (succ m) 根拠は C2,INDUCT:4
                     .= succ(j + m)  根拠は INDUCT:4。
    従って 目的の命題 根拠は C1,INDUCT:2 。
  終り。
  任意の k に対して P[k] 推論は INDUCT:sch 1(A1,A2)。
  従って 目的の命題。
終り。

対応表

日本語	Miar
。	;
とする（語順変更）	reserve
自然	natural
数	number
このとき	- （捨て言葉）
ならば	implies
証明:	proof
まず、	-
述語を定義する:	defpred
とは	means
であること	-
次を仮定する:	assume
根拠は	by
従って	hence
終り	end
任意の	for
ただし	st
に対して	holds
考えよう	let
すると	then
推論は	from