THE HTML DUMP FEATURE
Creation of this website was greatly facilitated by the program's "HTML Dump" menu action. HTML Dump results in an html-lised translation of the content of the proof pane. For instance if the proof pane looks as follows,
then HTML Dump results in generates following HTML code:
<div class="proof">Const 0 c;<
span class="annotation"><span class="ok">OK. </span>
</span>
Var 0 d;<span class="annotation"><span class="ok">OK.
</span></span>
Var 0 x;<span class="annotation"><span class="ok">OK.
</span></span>
Var 0 e;<span class="annotation"><span class="ok">OK.
</span></span>Var 1 d<e;<span class="annotation">
<span class="ok">OK. </span></span
>T0: (c=c),(d=d)⊨(∀(<)(d=e)) Cheat;<span class="annotation">
<span class="ok">OK. </span></span>
T1: (c=c),e=e⊨((d=e)≡(d<e)) Cheat;<span class="annotation">
<span class="ok">OK. </span></span>
T2: d=d,e=e,c=c,x=x⊨(∀(<)(<span class="hilight2">d
<span class="hilight1"><span class="underline"><
</span></span>e</span>)) <span class="hilight2"
>SubLR(T0,T1)</span>;<span class="annotation"><
span class="error">Variable capture after free occurence 0 of LHS
of Δ<span class="subscript">T1</span> in Δ<span
class="subscript">T0</span> replaced with RHS of Δ
<span class="subscript">T1</span>. </span></span>
T3: d=d,e=e,c=c⊨(∀(<)(d=e)) <span class="hilight2">Rep(
<span class="hilight1"><span class="underline">T2</span>
</span>)</span>;<span class="annotation"><span
class="error">Atom 'T2' is not defined.</span></span>
</div>
This html code will then appear on this webpage as follows:
Const 0 c;OK.
Var 0 d;OK.
Var 0 x;OK.
Var 0 e;OK.
Var 1 d<e;OK.
T0: (c=c),(d=d)⊨(∀(<)(d=e)) Cheat;OK.
T1: (c=c),e=e⊨((d=e)≡(d<e)) Cheat;OK.
T2: d=d,e=e,c=c,x=x⊨(∀(<)(d<e)) SubLR(T0,T1);Variable capture after free occurence 0 of LHS of ΔT1 in ΔT0 replaced with RHS of ΔT1.
T3: d=d,e=e,c=c⊨(∀(<)(d=e)) Rep(T2);Atom 'T2' is not defined.
