テキスト形式の群論の証明
群の積としてCircleTimes，単位元として
を使って，群論の公理を得る．群の元はデフォルトでは形式的な記号a，b，cとして表される．
公理の一つによると，右単位元が存在する．左単位元の存在を証明する．
証明の11ステップを人間が読める形式で得る．
群論の別の定理を証明する．
ステップのグラフを表示する．より重要な補助定理はより大きい円あるいは三角形で強調する．
‹›
