satysfi-derive:SATySFi 命令和 DSL，用于显示具有可维护代码的派生树

满足性 SATySFi命令和DSL用于显示具有可维护代码的派生树。 @ require: math @ require: base / typeset / satysfi - it @ require: derive / derive open Derive in satysfi - it $ { \proven ! ( open DeriveDSL in derive $ { \vdash A \wedge \paren { B \vee C } } |> by { $ {\wedge} I } |> from [ assume $ {\vdash A }; derive $ {\vdash B \vee C } |> by { $ {\vee} I } |> from [