A SMALL STEP, CHECKED.

把证明，走一遍。

每一步由同一个 Metamath 核心检查。

准备中

TARGET / 目标未选择

选择一个定理

⊢ …

有效假设 0

开始会话后显示目标的活动上下文。

在这个上下文中创建新目标

新目标继承所选定理之前的合法声明、全部活动假设和 $d 不交变量约束。只修改新标签与目标表达式；不会加入新公理。

输入一个标签，检查并应用它；失败不会改变已确认状态。

查找可见规则按标签、结论或类型码

这里列出活动假设、公理和此前已验证的定理。预览只检查当前栈能否执行这一步，不判断它对目标是否有用。

选择目标后显示其可见规则。

0 条

选择规则，查看其必要假设与结论。

空栈也是一个起点

应用假设或断言后，表达式会出现在这里。

等待动作

成功步骤将显示必要假设、同时代换及栈变化。

已确认的动作

保存源文件、目标和撤回后保留的动作；恢复时在新内核中重新验证、重放。失败会保留当前工作。

导入工作文件

点击保存时，至多 2 MiB 的工作也会留在本机浏览器；不会自动上传或无限量自动保存。

手动构造完成并通过检查后，可导出自足 .mm 文件。