Examine individual changes

This page allows you to examine the variables generated by the Abuse Filter for an individual change.

Variables generated for this change

Variable	Value
Edit count of the user `(user_editcount)`	483
Name of the user account `(user_name)`	'Hakerh400'
Age of the user account `(user_age)`	78421206
Groups (including implicit) the user is in `(user_groups)`	[ 0 => '*', 1 => 'user', 2 => 'autoconfirmed' ]
Page ID `(page_id)`	0
Page namespace `(page_namespace)`	2
Page title (without namespace) `(page_title)`	'Hakerh400/Theorem prover'
Full page title `(page_prefixedtitle)`	'User:Hakerh400/Theorem prover'
Action `(action)`	'edit'
Edit summary/reason `(summary)`	'Theorem prover'
Old content model `(old_content_model)`	''
New content model `(new_content_model)`	'wikitext'
Old page wikitext, before the edit `(old_wikitext)`	''
New page wikitext, after the edit `(new_wikitext)`	'== Introduction == In this tutorial we explain how to create a very simple theorem prover in Haskell using generalised algebraic data types. We first define axioms and inference rules, then write a formal proof of a theorem and then write a program to check whether the proof is valid. == Formal system == The formal logic system that we use in this example is a simplified version of [[wikipedia:Łukasiewicz_logic\|Łukasiewicz system]]. We define the following inference rules (the first two are axioms because they have no premises and the third one is [[wikipedia:Modus_ponens\|Modus ponens]]): <math> \begin{aligned} &\vdash x \to (y \to x) \\ &\vdash (x \to (y \to z)) \to ((x \to y) \to (x \to z)) \\ x, x \to y &\vdash y \end{aligned} </math> We call the first one <code>Ax1</code>, the second one <code>Ax2</code> and the third one <code>MP</code>. Implication is represented by <code>-></code> and the inference symbol is <code>\|-</code>. We want to prove that <math>(x\to x)</math> for any predicate <math>x</math> (the theorem of the reflexivity of the implication). Before we start, we want to make sure that <code>x,y,z</code> must be well-formed formulas. A well-formed formula in our system is only a predicate. A predicate is either an implication, or some contant predicate <code>P</code> (just as an example to reduce the generality). We can construct an implication only if both arguments are WFFs (well-formed formulas). The constant predicate <code>P</code> is a WFF by definition. == The program == <div style="background:#343D46;color:#D8DEE9;font-family:monospace;white-space:pre"> {-# <span style="color:#C695C6">LANGUAGE</span> GADTs #-} {-# <span style="color:#C695C6">LANGUAGE</span> ScopedTypeVariables #-} {-# <span style="color:#C695C6">LANGUAGE</span> KindSignatures #-} <span style="color:#5FB4B4">main</span> <span style="color:#C695C6">::</span> <span style="color:#C695C6"><i>IO</span></i> <span style="color:#C695C6"><i>()</span></i> main <span style="color:#F97B58">=</span> <span style="color:#6699CC"><i>putStrLn</span></i> output <span style="color:#5FB4B4">output</span> <span style="color:#C695C6">::</span> <span style="color:#C695C6"><i>String</span></i> output <span style="color:#F97B58">=</span> <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span>th_impl_refl <span style="color:#FFFFFF">(</span><span style="color:#C695C6">PredP</span> <span style="color:#C695C6">P</span><span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> <span style="color:#A6ACB9">----------------------------------------------------------------------------------------------------</span><span style="color:#A6ACB9"> </span> <span style="color:#C695C6">data</span> <span style="color:#C695C6">Pred</span> <span style="color:#F97B58">::</span> <span style="color:#F97B58"></span> <span style="color:#F97B58">-></span> <span style="color:#F97B58"></span> <span style="color:#C695C6">where</span> <span style="color:#C695C6">PredP</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">P</span> <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> <span style="color:#C695C6">P</span> <span style="color:#C695C6">PredImpl</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Impl</span> a b <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a b<span style="color:#FFFFFF">)</span> <span style="color:#C695C6">data</span> <span style="color:#C695C6">P</span> <span style="color:#F97B58">::</span> <span style="color:#F97B58"></span> <span style="color:#C695C6">where</span> <span style="color:#C695C6">P</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">P</span> <span style="color:#C695C6">data</span> <span style="color:#C695C6">Impl</span> <span style="color:#F97B58">::</span> <span style="color:#F97B58"></span> <span style="color:#F97B58">-></span> <span style="color:#F97B58"></span> <span style="color:#F97B58">-></span> <span style="color:#F97B58"></span> <span style="color:#C695C6">where</span> <span style="color:#C695C6">Impl</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> a <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> b <span style="color:#F97B58">-></span> <span style="color:#C695C6">Impl</span> a b <span style="color:#C695C6">data</span> <span style="color:#C695C6">Infer</span> <span style="color:#F97B58">::</span> <span style="color:#F97B58"></span> <span style="color:#F97B58">-></span> <span style="color:#F97B58"></span> <span style="color:#C695C6">where</span> <span style="color:#C695C6">Ax1</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> a <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> b <span style="color:#F97B58">-></span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> b a<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> <span style="color:#C695C6">Ax2</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> a <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> b <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> c <span style="color:#F97B58">-></span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> b c<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a b<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a c<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> <span style="color:#C695C6">MP</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">-></span> <span style="color:#C695C6">Infer</span> a <span style="color:#F97B58">-></span> <span style="color:#C695C6">Infer</span> b <span style="color:#A6ACB9">----------------------------------------------------------------------------------------------------</span><span style="color:#A6ACB9"> </span> <span style="color:#C695C6">instance</span> <span style="color:#C695C6"><i>Show</span></i> (<span style="color:#C695C6"><i>Pred</span></i> a) <span style="color:#C695C6">where</span> <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">PredP</span> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#6699CC"><i>show</span></i> a <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">PredImpl</span> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#6699CC"><i>show</span></i> a <span style="color:#C695C6">instance</span> <span style="color:#C695C6"><i>Show</span></i> <span style="color:#C695C6"><i>P</span></i> <span style="color:#C695C6">where</span> <span style="color:#6699CC"><i>show</span></i> P <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">P</span><span style="color:#5FB4B4">"</span> <span style="color:#C695C6">instance</span> <span style="color:#C695C6"><i>Show</span></i> (<span style="color:#C695C6"><i>Impl</span></i> a b) <span style="color:#C695C6">where</span> <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">(</span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794"> </span><span style="color:#99C794">-> </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">)</span><span style="color:#5FB4B4">"</span> <span style="color:#C695C6">instance</span> <span style="color:#C695C6"><i>Show</span></i> (<span style="color:#C695C6"><i>Infer</span></i> a) <span style="color:#C695C6">where</span> <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Ax1</span> a b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">(</span><span style="color:#99C794">Ax1 </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794"> </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">)</span><span style="color:#5FB4B4">"</span> <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Ax2</span> a b c<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">(</span><span style="color:#99C794">Ax2 </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794"> </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794"> </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> c<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">)</span><span style="color:#5FB4B4">"</span> <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">MP</span> a b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">(</span><span style="color:#99C794">MP </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794"> </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">)</span><span style="color:#5FB4B4">"</span> <span style="color:#A6ACB9">----------------------------------------------------------------------------------------------------</span><span style="color:#A6ACB9"> </span> <span style="color:#C695C6">type</span> <span style="color:#C695C6">T1</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> a a <span style="color:#C695C6">type</span> <span style="color:#C695C6">T2</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> a <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T1</span> a<span style="color:#FFFFFF">)</span> <span style="color:#C695C6">type</span> <span style="color:#C695C6">T3</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> a <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T1</span> a<span style="color:#FFFFFF">)</span> a<span style="color:#FFFFFF">)</span> <span style="color:#C695C6">type</span> <span style="color:#C695C6">T4</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T2</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T1</span> a<span style="color:#FFFFFF">)</span> <span style="color:#5FB4B4">th_impl_refl</span> <span style="color:#C695C6">::</span> forall a. <span style="color:#C695C6"><i>Pred</span></i> a <span style="color:#C695C6">-></span> <span style="color:#C695C6"><i>Infer</span></i> (<span style="color:#C695C6"><i>Impl</span></i> a a) th_impl_refl x <span style="color:#F97B58">=</span> step_6 <span style="color:#C695C6">where</span> step_1 <span style="color:#F97B58">=</span> <span style="color:#C695C6">PredImpl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> x x<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T1</span> a<span style="color:#FFFFFF">)</span> step_2 <span style="color:#F97B58">=</span> <span style="color:#C695C6">Ax1</span> x x <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T2</span> a<span style="color:#FFFFFF">)</span> step_3 <span style="color:#F97B58">=</span> <span style="color:#C695C6">Ax1</span> x step_1 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T3</span> a<span style="color:#FFFFFF">)</span> step_4 <span style="color:#F97B58">=</span> <span style="color:#C695C6">Ax2</span> x step_1 x <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T3</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T4</span> a<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> step_5 <span style="color:#F97B58">=</span> <span style="color:#C695C6">MP</span> step_4 step_3 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T4</span> a<span style="color:#FFFFFF">)</span> step_6 <span style="color:#F97B58">=</span> <span style="color:#C695C6">MP</span> step_5 step_2 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T1</span> a<span style="color:#FFFFFF">)</span> </div> == Explanation == === Data types === We define four data types. The first data type is <code>Pred</code>, which stands for predicate. It represents predicate WFF (currently the only type of WFF in our system). It is an "abstract" data type in the sense that it just represents a label that we assign to already constructed other data types. In particular, it says that we can label <code>P</code> as a predicate, or we cal label an implication as a predicate. It is like an abstract class in OOP languages. The next data type is <code>P</code>, which does not have any particular meaning in the system. It is just there for us to be able to examine the result of the proof (otherwise, any attemp to construct a predicate would not terminate). The third data type is <code>Impl</code>, which stands for implication. As we explained, it "asserts" that both of its arguments must be predicates. The last data type is <code>Infer</code>, which represents a proof of a predicate. We can construct it using three different constructors. We can either use one of the axioms (<code>Ax1</code> or <code>Ax2</code>), or we can apply Modus ponens. Next, we have some functions for stringifying our data types. They are just for analyzing the results. === Theorem === Finally, we define and prove theorem <code>th_impl_refl</code>, which states that for any predicate <code>a</code>, the statement <math>(a \to a)</math> is true. We prove it in six steps. The first step proves that if <code>a</code> is a predicate, then <code>Impl a a</code> is also a predicate (types T1..T4 are defined just as aliases to save space). Steps 2 and 3 apply axiom <code>Ax1</code>, step 4 applies axiom <code>Ax2</code> and steps 5 and 6 apply Modus ponens. The type signature of each step is used for correctness check. === Verifying the proof === If the program does not compile, either the proof is wrong, or you have syntax errors. If the program compiles, it still does not mean that the proof is correct, because you may have a cyclic theorem dependency in your proof. You need to run the program and make sure the program halts. If the program does not halt, it probably means you have a cyclic dependency somewhere. The output of the program is the proof of the theorem for sample statement <code>P</code> that we introduced just for this purpose. The program show the following output: (MP (MP (Ax2 P (P -> P) P) (Ax1 P (P -> P))) (Ax1 P P)) == Adding new features == It is very easy to add new features (axioms, inference rules, definitions, data types, theorems, etc). For example, if we want to add new axiom <code>Ax3</code> that defines negation: <math> \vdash(\lnot x\to\lnot y)\to(y\to x) </math> and we want to prove that <math>\lnot\lnot x\to(\lnot x\to x)</math> for any statement <math>x</math>, then we need update the program by adding a new data type <code>Not</code> for negation, new axiom <code>Ax3</code> as an <code>Infer</code> constructor, and finally theorem <code>th_2</code> that proves what we need. <div style="background:#343D46;color:#D8DEE9;font-family:monospace;white-space:pre"> {-# <span style="color:#C695C6">LANGUAGE</span> GADTs #-} {-# <span style="color:#C695C6">LANGUAGE</span> ScopedTypeVariables #-} {-# <span style="color:#C695C6">LANGUAGE</span> KindSignatures #-} <span style="color:#5FB4B4">main</span> <span style="color:#C695C6">::</span> <span style="color:#C695C6"><i>IO</span></i> <span style="color:#C695C6"><i>()</span></i> main <span style="color:#F97B58">=</span> <span style="color:#6699CC"><i>putStrLn</span></i> output <span style="color:#5FB4B4">output</span> <span style="color:#C695C6">::</span> <span style="color:#C695C6"><i>String</span></i> output <span style="color:#F97B58">=</span> <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span>th_2 <span style="color:#FFFFFF">(</span><span style="color:#C695C6">PredP</span> <span style="color:#C695C6">P</span><span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> <span style="color:#A6ACB9">----------------------------------------------------------------------------------------------------</span><span style="color:#A6ACB9"> </span> <span style="color:#C695C6">data</span> <span style="color:#C695C6">Pred</span> <span style="color:#F97B58">::</span> <span style="color:#F97B58"></span> <span style="color:#F97B58">-></span> <span style="color:#F97B58"></span> <span style="color:#C695C6">where</span> <span style="color:#C695C6">PredP</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">P</span> <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> <span style="color:#C695C6">P</span> <span style="color:#C695C6">PredImpl</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Impl</span> a b <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a b<span style="color:#FFFFFF">)</span> <span style="color:#C695C6">PredNot</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Not</span> a <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Not</span> a<span style="color:#FFFFFF">)</span> <span style="color:#C695C6">data</span> <span style="color:#C695C6">P</span> <span style="color:#F97B58">::</span> <span style="color:#F97B58"></span> <span style="color:#C695C6">where</span> <span style="color:#C695C6">P</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">P</span> <span style="color:#C695C6">data</span> <span style="color:#C695C6">Impl</span> <span style="color:#F97B58">::</span> <span style="color:#F97B58"></span> <span style="color:#F97B58">-></span> <span style="color:#F97B58"></span> <span style="color:#F97B58">-></span> <span style="color:#F97B58"></span> <span style="color:#C695C6">where</span> <span style="color:#C695C6">Impl</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> a <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> b <span style="color:#F97B58">-></span> <span style="color:#C695C6">Impl</span> a b <span style="color:#C695C6">data</span> <span style="color:#C695C6">Not</span> <span style="color:#F97B58">::</span> <span style="color:#F97B58"></span> <span style="color:#F97B58">-></span> <span style="color:#F97B58"></span> <span style="color:#C695C6">where</span> <span style="color:#C695C6">Not</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> a <span style="color:#F97B58">-></span> <span style="color:#C695C6">Not</span> a <span style="color:#C695C6">data</span> <span style="color:#C695C6">Infer</span> <span style="color:#F97B58">::</span> <span style="color:#F97B58"></span> <span style="color:#F97B58">-></span> <span style="color:#F97B58"></span> <span style="color:#C695C6">where</span> <span style="color:#C695C6">Ax1</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> a <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> b <span style="color:#F97B58">-></span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> b a<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> <span style="color:#C695C6">Ax2</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> a <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> b <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> c <span style="color:#F97B58">-></span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> b c<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a b<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a c<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> <span style="color:#C695C6">Ax3</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> a <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> b <span style="color:#F97B58">-></span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Not</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Not</span> b<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> b a<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> <span style="color:#C695C6">MP</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">-></span> <span style="color:#C695C6">Infer</span> a <span style="color:#F97B58">-></span> <span style="color:#C695C6">Infer</span> b <span style="color:#A6ACB9">----------------------------------------------------------------------------------------------------</span><span style="color:#A6ACB9"> </span> <span style="color:#C695C6">instance</span> <span style="color:#C695C6"><i>Show</span></i> (<span style="color:#C695C6"><i>Pred</span></i> a) <span style="color:#C695C6">where</span> <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">PredP</span> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#6699CC"><i>show</span></i> a <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">PredImpl</span> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#6699CC"><i>show</span></i> a <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">PredNot</span> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#6699CC"><i>show</span></i> a <span style="color:#C695C6">instance</span> <span style="color:#C695C6"><i>Show</span></i> <span style="color:#C695C6"><i>P</span></i> <span style="color:#C695C6">where</span> <span style="color:#6699CC"><i>show</span></i> <span style="color:#C695C6">P</span> <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">P</span><span style="color:#5FB4B4">"</span> <span style="color:#C695C6">instance</span> <span style="color:#C695C6"><i>Show</span></i> (<span style="color:#C695C6"><i>Impl</span></i> a b) <span style="color:#C695C6">where</span> <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">(</span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794"> </span><span style="color:#99C794">-> </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">)</span><span style="color:#5FB4B4">"</span> <span style="color:#C695C6">instance</span> <span style="color:#C695C6"><i>Show</span></i> (<span style="color:#C695C6"><i>Not</span></i> a) <span style="color:#C695C6">where</span> <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Not</span> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">~</span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> a<span style="color:#FFFFFF">)</span> <span style="color:#C695C6">instance</span> <span style="color:#C695C6"><i>Show</span></i> (<span style="color:#C695C6"><i>Infer</span></i> a) <span style="color:#C695C6">where</span> <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Ax1</span> a b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">(</span><span style="color:#99C794">Ax1 </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794"> </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">)</span><span style="color:#5FB4B4">"</span> <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Ax2</span> a b c<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">(</span><span style="color:#99C794">Ax2 </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794"> </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794"> </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> c<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">)</span><span style="color:#5FB4B4">"</span> <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Ax3</span> a b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">(</span><span style="color:#99C794">Ax3 </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794"> </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">)</span><span style="color:#5FB4B4">"</span> <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">MP</span> a b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">(</span><span style="color:#99C794">MP </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794"> </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">)</span><span style="color:#5FB4B4">"</span> <span style="color:#A6ACB9">----------------------------------------------------------------------------------------------------</span><span style="color:#A6ACB9"> </span> <span style="color:#C695C6">type</span> <span style="color:#C695C6">T1</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> a a <span style="color:#C695C6">type</span> <span style="color:#C695C6">T2</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> a <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T1</span> a<span style="color:#FFFFFF">)</span> <span style="color:#C695C6">type</span> <span style="color:#C695C6">T3</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> a <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T1</span> a<span style="color:#FFFFFF">)</span> a<span style="color:#FFFFFF">)</span> <span style="color:#C695C6">type</span> <span style="color:#C695C6">T4</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T2</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T1</span> a<span style="color:#FFFFFF">)</span> <span style="color:#5FB4B4">th_impl_refl</span> <span style="color:#C695C6">::</span> forall a. <span style="color:#C695C6"><i>Pred</span></i> a <span style="color:#C695C6">-></span> <span style="color:#C695C6"><i>Infer</span></i> (<span style="color:#C695C6"><i>Impl</span></i> a a) th_impl_refl x <span style="color:#F97B58">=</span> step_5 <span style="color:#C695C6">where</span> wff_1 <span style="color:#F97B58">=</span> <span style="color:#C695C6">PredImpl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> x x<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T1</span> a<span style="color:#FFFFFF">)</span> step_1 <span style="color:#F97B58">=</span> <span style="color:#C695C6">Ax1</span> x x <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T2</span> a<span style="color:#FFFFFF">)</span> step_2 <span style="color:#F97B58">=</span> <span style="color:#C695C6">Ax1</span> x wff_1 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T3</span> a<span style="color:#FFFFFF">)</span> step_3 <span style="color:#F97B58">=</span> <span style="color:#C695C6">Ax2</span> x wff_1 x <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T3</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T4</span> a<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> step_4 <span style="color:#F97B58">=</span> <span style="color:#C695C6">MP</span> step_3 step_2 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T4</span> a<span style="color:#FFFFFF">)</span> step_5 <span style="color:#F97B58">=</span> <span style="color:#C695C6">MP</span> step_4 step_1 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T1</span> a<span style="color:#FFFFFF">)</span> <span style="color:#C695C6">type</span> <span style="color:#C695C6">T5</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T6</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T9</span> a<span style="color:#FFFFFF">)</span> <span style="color:#C695C6">type</span> <span style="color:#C695C6">T6</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Not</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Not</span> a<span style="color:#FFFFFF">)</span> <span style="color:#C695C6">type</span> <span style="color:#C695C6">T7</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Not</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T6</span> a<span style="color:#FFFFFF">)</span> <span style="color:#C695C6">type</span> <span style="color:#C695C6">T8</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T6</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T7</span> a<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T6</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T10</span> a<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> <span style="color:#C695C6">type</span> <span style="color:#C695C6">T9</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T7</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T10</span> a<span style="color:#FFFFFF">)</span> <span style="color:#C695C6">type</span> <span style="color:#C695C6">T10</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Not</span> a<span style="color:#FFFFFF">)</span> a <span style="color:#5FB4B4">th_2</span> <span style="color:#C695C6">::</span> forall a. <span style="color:#C695C6"><i>Pred</span></i> a <span style="color:#C695C6">-></span> <span style="color:#C695C6"><i>Infer</span></i> (<span style="color:#C695C6"><i>Impl</span></i> (<span style="color:#C695C6"><i>Not</span></i> (<span style="color:#C695C6"><i>Not</span></i> a)) (<span style="color:#C695C6"><i>Impl</span></i> (<span style="color:#C695C6"><i>Not</span></i> a) a)) th_2 x <span style="color:#F97B58">=</span> step_7 <span style="color:#C695C6">where</span> wff_1 <span style="color:#F97B58">=</span> <span style="color:#C695C6">PredNot</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Not</span> x<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Not</span> a<span style="color:#FFFFFF">)</span> wff_2 <span style="color:#F97B58">=</span> <span style="color:#C695C6">PredNot</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Not</span> wff_1<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T6</span> a<span style="color:#FFFFFF">)</span> wff_3 <span style="color:#F97B58">=</span> <span style="color:#C695C6">PredImpl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> wff_1 wff_2<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T7</span> a<span style="color:#FFFFFF">)</span> wff_4 <span style="color:#F97B58">=</span> <span style="color:#C695C6">PredImpl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> wff_1 x<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T10</span> a<span style="color:#FFFFFF">)</span> wff_5 <span style="color:#F97B58">=</span> <span style="color:#C695C6">PredImpl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> wff_3 wff_4<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T9</span> a<span style="color:#FFFFFF">)</span> step_1 <span style="color:#F97B58">=</span> <span style="color:#C695C6">Ax3</span> x wff_1 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T9</span> a<span style="color:#FFFFFF">)</span> step_2 <span style="color:#F97B58">=</span> <span style="color:#C695C6">Ax1</span> wff_5 wff_2 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T9</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T5</span> a<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> step_3 <span style="color:#F97B58">=</span> <span style="color:#C695C6">MP</span> step_2 step_1 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T5</span> a<span style="color:#FFFFFF">)</span> step_4 <span style="color:#F97B58">=</span> <span style="color:#C695C6">Ax2</span> wff_2 wff_3 wff_4 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T5</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T8</span> a<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> step_5 <span style="color:#F97B58">=</span> <span style="color:#C695C6">MP</span> step_4 step_3 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T8</span> a<span style="color:#FFFFFF">)</span> step_6 <span style="color:#F97B58">=</span> <span style="color:#C695C6">Ax1</span> wff_2 wff_1 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T6</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T7</span> a<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> step_7 <span style="color:#F97B58">=</span> <span style="color:#C695C6">MP</span> step_5 step_6 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T6</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T10</span> a<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> </div> === Explanation === We renamed some of the steps to separate "WFF" proofs from "Infer" proofs (we also updated <code>th_impl_refl</code>). The program outputs the following proof: (MP (MP (Ax2 ~~P (~P -> ~~P) (~P -> P)) (MP (Ax1 ((~P -> ~~P) -> (~P -> P)) ~~P) (Ax3 P ~P))) (Ax1 ~~P ~P)) Notice that WFF steps are almost half of the total steps. If we remove the WFF checks, we can make the proof of the theorem a lot simpler. However, forcing a formula to be well-formed is important, because the system can be expanded to include other types of expressions (such as sets and proper classes). We want to make sure that the arguments of an implication are predicates, and not for example sets. Also, WFF can be generalized to any level of abstraction, so if we decide to introduce quantifiers, we can use WFF checks to ensure that there are no free identifiers in the top-level expression (each identifier must be bound to a quantifier parameter name). When we talk about identifiers, they can be implemented as [[Wikipedia:De_Bruijn_index\|De Bruijn indices]] and substitutions can be achieved by a recursive constraint that ensures that all occurrences of the bound variable are replaced.'
Unified diff of changes made by edit `(edit_diff)`	'@@ -1,0 +1,223 @@ +== Introduction == + +In this tutorial we explain how to create a very simple theorem prover in Haskell using generalised algebraic data types. We first define axioms and inference rules, then write a formal proof of a theorem and then write a program to check whether the proof is valid. + +== Formal system == + +The formal logic system that we use in this example is a simplified version of [[wikipedia:Łukasiewicz_logic\|Łukasiewicz system]]. We define the following inference rules (the first two are axioms because they have no premises and the third one is [[wikipedia:Modus_ponens\|Modus ponens]]): + +<math> + \begin{aligned} + &\vdash x \to (y \to x) \\ + &\vdash (x \to (y \to z)) \to ((x \to y) \to (x \to z)) \\ + x, x \to y &\vdash y + \end{aligned} +</math> + +We call the first one <code>Ax1</code>, the second one <code>Ax2</code> and the third one <code>MP</code>. Implication is represented by <code>-></code> and the inference symbol is <code>\|-</code>. We want to prove that <math>(x\to x)</math> for any predicate <math>x</math> (the theorem of the reflexivity of the implication). + +Before we start, we want to make sure that <code>x,y,z</code> must be well-formed formulas. A well-formed formula in our system is only a predicate. A predicate is either an implication, or some contant predicate <code>P</code> (just as an example to reduce the generality). We can construct an implication only if both arguments are WFFs (well-formed formulas). The constant predicate <code>P</code> is a WFF by definition. + +== The program == + +<div style="background:#343D46;color:#D8DEE9;font-family:monospace;white-space:pre"> + {-# <span style="color:#C695C6">LANGUAGE</span> GADTs #-} + {-# <span style="color:#C695C6">LANGUAGE</span> ScopedTypeVariables #-} + {-# <span style="color:#C695C6">LANGUAGE</span> KindSignatures #-} + + <span style="color:#5FB4B4">main</span> <span style="color:#C695C6">::</span> <span style="color:#C695C6"><i>IO</span></i> <span style="color:#C695C6"><i>()</span></i> + main <span style="color:#F97B58">=</span> <span style="color:#6699CC"><i>putStrLn</span></i> output + + <span style="color:#5FB4B4">output</span> <span style="color:#C695C6">::</span> <span style="color:#C695C6"><i>String</span></i> + output <span style="color:#F97B58">=</span> <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span>th_impl_refl <span style="color:#FFFFFF">(</span><span style="color:#C695C6">PredP</span> <span style="color:#C695C6">P</span><span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> + + <span style="color:#A6ACB9">----------------------------------------------------------------------------------------------------</span><span style="color:#A6ACB9"> + </span> + <span style="color:#C695C6">data</span> <span style="color:#C695C6">Pred</span> <span style="color:#F97B58">::</span> <span style="color:#F97B58"></span> <span style="color:#F97B58">-></span> <span style="color:#F97B58"></span> <span style="color:#C695C6">where</span> + <span style="color:#C695C6">PredP</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">P</span> <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> <span style="color:#C695C6">P</span> + <span style="color:#C695C6">PredImpl</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Impl</span> a b <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a b<span style="color:#FFFFFF">)</span> + + <span style="color:#C695C6">data</span> <span style="color:#C695C6">P</span> <span style="color:#F97B58">::</span> <span style="color:#F97B58"></span> <span style="color:#C695C6">where</span> + <span style="color:#C695C6">P</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">P</span> + + <span style="color:#C695C6">data</span> <span style="color:#C695C6">Impl</span> <span style="color:#F97B58">::</span> <span style="color:#F97B58"></span> <span style="color:#F97B58">-></span> <span style="color:#F97B58"></span> <span style="color:#F97B58">-></span> <span style="color:#F97B58"></span> <span style="color:#C695C6">where</span> + <span style="color:#C695C6">Impl</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> a <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> b <span style="color:#F97B58">-></span> <span style="color:#C695C6">Impl</span> a b + + <span style="color:#C695C6">data</span> <span style="color:#C695C6">Infer</span> <span style="color:#F97B58">::</span> <span style="color:#F97B58"></span> <span style="color:#F97B58">-></span> <span style="color:#F97B58"></span> <span style="color:#C695C6">where</span> + <span style="color:#C695C6">Ax1</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> a <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> b <span style="color:#F97B58">-></span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> b a<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> + <span style="color:#C695C6">Ax2</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> a <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> b <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> c <span style="color:#F97B58">-></span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> b c<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a b<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a c<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> + <span style="color:#C695C6">MP</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">-></span> <span style="color:#C695C6">Infer</span> a <span style="color:#F97B58">-></span> <span style="color:#C695C6">Infer</span> b + + <span style="color:#A6ACB9">----------------------------------------------------------------------------------------------------</span><span style="color:#A6ACB9"> + </span> + <span style="color:#C695C6">instance</span> <span style="color:#C695C6"><i>Show</span></i> (<span style="color:#C695C6"><i>Pred</span></i> a) <span style="color:#C695C6">where</span> + <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">PredP</span> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#6699CC"><i>show</span></i> a + <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">PredImpl</span> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#6699CC"><i>show</span></i> a + + <span style="color:#C695C6">instance</span> <span style="color:#C695C6"><i>Show</span></i> <span style="color:#C695C6"><i>P</span></i> <span style="color:#C695C6">where</span> + <span style="color:#6699CC"><i>show</span></i> P <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">P</span><span style="color:#5FB4B4">"</span> + + <span style="color:#C695C6">instance</span> <span style="color:#C695C6"><i>Show</span></i> (<span style="color:#C695C6"><i>Impl</span></i> a b) <span style="color:#C695C6">where</span> + <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">(</span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794"> </span><span style="color:#99C794">-> </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">)</span><span style="color:#5FB4B4">"</span> + + <span style="color:#C695C6">instance</span> <span style="color:#C695C6"><i>Show</span></i> (<span style="color:#C695C6"><i>Infer</span></i> a) <span style="color:#C695C6">where</span> + <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Ax1</span> a b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">(</span><span style="color:#99C794">Ax1 </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794"> </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">)</span><span style="color:#5FB4B4">"</span> + <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Ax2</span> a b c<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">(</span><span style="color:#99C794">Ax2 </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794"> </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794"> </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> c<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">)</span><span style="color:#5FB4B4">"</span> + <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">MP</span> a b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">(</span><span style="color:#99C794">MP </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794"> </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">)</span><span style="color:#5FB4B4">"</span> + + <span style="color:#A6ACB9">----------------------------------------------------------------------------------------------------</span><span style="color:#A6ACB9"> + </span> + <span style="color:#C695C6">type</span> <span style="color:#C695C6">T1</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> a a + <span style="color:#C695C6">type</span> <span style="color:#C695C6">T2</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> a <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T1</span> a<span style="color:#FFFFFF">)</span> + <span style="color:#C695C6">type</span> <span style="color:#C695C6">T3</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> a <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T1</span> a<span style="color:#FFFFFF">)</span> a<span style="color:#FFFFFF">)</span> + <span style="color:#C695C6">type</span> <span style="color:#C695C6">T4</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T2</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T1</span> a<span style="color:#FFFFFF">)</span> + + <span style="color:#5FB4B4">th_impl_refl</span> <span style="color:#C695C6">::</span> forall a. <span style="color:#C695C6"><i>Pred</span></i> a <span style="color:#C695C6">-></span> <span style="color:#C695C6"><i>Infer</span></i> (<span style="color:#C695C6"><i>Impl</span></i> a a) + th_impl_refl x <span style="color:#F97B58">=</span> step_6 <span style="color:#C695C6">where</span> + step_1 <span style="color:#F97B58">=</span> <span style="color:#C695C6">PredImpl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> x x<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T1</span> a<span style="color:#FFFFFF">)</span> + step_2 <span style="color:#F97B58">=</span> <span style="color:#C695C6">Ax1</span> x x <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T2</span> a<span style="color:#FFFFFF">)</span> + step_3 <span style="color:#F97B58">=</span> <span style="color:#C695C6">Ax1</span> x step_1 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T3</span> a<span style="color:#FFFFFF">)</span> + step_4 <span style="color:#F97B58">=</span> <span style="color:#C695C6">Ax2</span> x step_1 x <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T3</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T4</span> a<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> + step_5 <span style="color:#F97B58">=</span> <span style="color:#C695C6">MP</span> step_4 step_3 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T4</span> a<span style="color:#FFFFFF">)</span> + step_6 <span style="color:#F97B58">=</span> <span style="color:#C695C6">MP</span> step_5 step_2 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T1</span> a<span style="color:#FFFFFF">)</span> + +</div> + +== Explanation == + +=== Data types === + +We define four data types. The first data type is <code>Pred</code>, which stands for predicate. It represents predicate WFF (currently the only type of WFF in our system). It is an "abstract" data type in the sense that it just represents a label that we assign to already constructed other data types. In particular, it says that we can label <code>P</code> as a predicate, or we cal label an implication as a predicate. It is like an abstract class in OOP languages. + +The next data type is <code>P</code>, which does not have any particular meaning in the system. It is just there for us to be able to examine the result of the proof (otherwise, any attemp to construct a predicate would not terminate). + +The third data type is <code>Impl</code>, which stands for implication. As we explained, it "asserts" that both of its arguments must be predicates. + +The last data type is <code>Infer</code>, which represents a proof of a predicate. We can construct it using three different constructors. We can either use one of the axioms (<code>Ax1</code> or <code>Ax2</code>), or we can apply Modus ponens. + +Next, we have some functions for stringifying our data types. They are just for analyzing the results. + +=== Theorem === + +Finally, we define and prove theorem <code>th_impl_refl</code>, which states that for any predicate <code>a</code>, the statement <math>(a \to a)</math> is true. We prove it in six steps. The first step proves that if <code>a</code> is a predicate, then <code>Impl a a</code> is also a predicate (types T1..T4 are defined just as aliases to save space). Steps 2 and 3 apply axiom <code>Ax1</code>, step 4 applies axiom <code>Ax2</code> and steps 5 and 6 apply Modus ponens. The type signature of each step is used for correctness check. + +=== Verifying the proof === + +If the program does not compile, either the proof is wrong, or you have syntax errors. If the program compiles, it still does not mean that the proof is correct, because you may have a cyclic theorem dependency in your proof. You need to run the program and make sure the program halts. If the program does not halt, it probably means you have a cyclic dependency somewhere. + +The output of the program is the proof of the theorem for sample statement <code>P</code> that we introduced just for this purpose. The program show the following output: + + (MP (MP (Ax2 P (P -> P) P) (Ax1 P (P -> P))) (Ax1 P P)) + +== Adding new features == + +It is very easy to add new features (axioms, inference rules, definitions, data types, theorems, etc). For example, if we want to add new axiom <code>Ax3</code> that defines negation: + +<math> + \vdash(\lnot x\to\lnot y)\to(y\to x) +</math> + +and we want to prove that <math>\lnot\lnot x\to(\lnot x\to x)</math> for any statement <math>x</math>, then we need update the program by adding a new data type <code>Not</code> for negation, new axiom <code>Ax3</code> as an <code>Infer</code> constructor, and finally theorem <code>th_2</code> that proves what we need. + +<div style="background:#343D46;color:#D8DEE9;font-family:monospace;white-space:pre"> + {-# <span style="color:#C695C6">LANGUAGE</span> GADTs #-} + {-# <span style="color:#C695C6">LANGUAGE</span> ScopedTypeVariables #-} + {-# <span style="color:#C695C6">LANGUAGE</span> KindSignatures #-} + + <span style="color:#5FB4B4">main</span> <span style="color:#C695C6">::</span> <span style="color:#C695C6"><i>IO</span></i> <span style="color:#C695C6"><i>()</span></i> + main <span style="color:#F97B58">=</span> <span style="color:#6699CC"><i>putStrLn</span></i> output + + <span style="color:#5FB4B4">output</span> <span style="color:#C695C6">::</span> <span style="color:#C695C6"><i>String</span></i> + output <span style="color:#F97B58">=</span> <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span>th_2 <span style="color:#FFFFFF">(</span><span style="color:#C695C6">PredP</span> <span style="color:#C695C6">P</span><span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> + + <span style="color:#A6ACB9">----------------------------------------------------------------------------------------------------</span><span style="color:#A6ACB9"> + </span> + <span style="color:#C695C6">data</span> <span style="color:#C695C6">Pred</span> <span style="color:#F97B58">::</span> <span style="color:#F97B58"></span> <span style="color:#F97B58">-></span> <span style="color:#F97B58"></span> <span style="color:#C695C6">where</span> + <span style="color:#C695C6">PredP</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">P</span> <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> <span style="color:#C695C6">P</span> + <span style="color:#C695C6">PredImpl</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Impl</span> a b <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a b<span style="color:#FFFFFF">)</span> + <span style="color:#C695C6">PredNot</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Not</span> a <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Not</span> a<span style="color:#FFFFFF">)</span> + + <span style="color:#C695C6">data</span> <span style="color:#C695C6">P</span> <span style="color:#F97B58">::</span> <span style="color:#F97B58"></span> <span style="color:#C695C6">where</span> + <span style="color:#C695C6">P</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">P</span> + + <span style="color:#C695C6">data</span> <span style="color:#C695C6">Impl</span> <span style="color:#F97B58">::</span> <span style="color:#F97B58"></span> <span style="color:#F97B58">-></span> <span style="color:#F97B58"></span> <span style="color:#F97B58">-></span> <span style="color:#F97B58"></span> <span style="color:#C695C6">where</span> + <span style="color:#C695C6">Impl</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> a <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> b <span style="color:#F97B58">-></span> <span style="color:#C695C6">Impl</span> a b + + <span style="color:#C695C6">data</span> <span style="color:#C695C6">Not</span> <span style="color:#F97B58">::</span> <span style="color:#F97B58"></span> <span style="color:#F97B58">-></span> <span style="color:#F97B58"></span> <span style="color:#C695C6">where</span> + <span style="color:#C695C6">Not</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> a <span style="color:#F97B58">-></span> <span style="color:#C695C6">Not</span> a + + <span style="color:#C695C6">data</span> <span style="color:#C695C6">Infer</span> <span style="color:#F97B58">::</span> <span style="color:#F97B58"></span> <span style="color:#F97B58">-></span> <span style="color:#F97B58"></span> <span style="color:#C695C6">where</span> + <span style="color:#C695C6">Ax1</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> a <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> b <span style="color:#F97B58">-></span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> b a<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> + <span style="color:#C695C6">Ax2</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> a <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> b <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> c <span style="color:#F97B58">-></span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> b c<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a b<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a c<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> + <span style="color:#C695C6">Ax3</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> a <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> b <span style="color:#F97B58">-></span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Not</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Not</span> b<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> b a<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> + <span style="color:#C695C6">MP</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">-></span> <span style="color:#C695C6">Infer</span> a <span style="color:#F97B58">-></span> <span style="color:#C695C6">Infer</span> b + + <span style="color:#A6ACB9">----------------------------------------------------------------------------------------------------</span><span style="color:#A6ACB9"> + </span> + <span style="color:#C695C6">instance</span> <span style="color:#C695C6"><i>Show</span></i> (<span style="color:#C695C6"><i>Pred</span></i> a) <span style="color:#C695C6">where</span> + <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">PredP</span> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#6699CC"><i>show</span></i> a + <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">PredImpl</span> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#6699CC"><i>show</span></i> a + <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">PredNot</span> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#6699CC"><i>show</span></i> a + + <span style="color:#C695C6">instance</span> <span style="color:#C695C6"><i>Show</span></i> <span style="color:#C695C6"><i>P</span></i> <span style="color:#C695C6">where</span> + <span style="color:#6699CC"><i>show</span></i> <span style="color:#C695C6">P</span> <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">P</span><span style="color:#5FB4B4">"</span> + + <span style="color:#C695C6">instance</span> <span style="color:#C695C6"><i>Show</span></i> (<span style="color:#C695C6"><i>Impl</span></i> a b) <span style="color:#C695C6">where</span> + <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">(</span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794"> </span><span style="color:#99C794">-> </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">)</span><span style="color:#5FB4B4">"</span> + + <span style="color:#C695C6">instance</span> <span style="color:#C695C6"><i>Show</span></i> (<span style="color:#C695C6"><i>Not</span></i> a) <span style="color:#C695C6">where</span> + <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Not</span> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">~</span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> a<span style="color:#FFFFFF">)</span> + + <span style="color:#C695C6">instance</span> <span style="color:#C695C6"><i>Show</span></i> (<span style="color:#C695C6"><i>Infer</span></i> a) <span style="color:#C695C6">where</span> + <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Ax1</span> a b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">(</span><span style="color:#99C794">Ax1 </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794"> </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">)</span><span style="color:#5FB4B4">"</span> + <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Ax2</span> a b c<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">(</span><span style="color:#99C794">Ax2 </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794"> </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794"> </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> c<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">)</span><span style="color:#5FB4B4">"</span> + <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Ax3</span> a b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">(</span><span style="color:#99C794">Ax3 </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794"> </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">)</span><span style="color:#5FB4B4">"</span> + <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">MP</span> a b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">(</span><span style="color:#99C794">MP </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794"> </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">)</span><span style="color:#5FB4B4">"</span> + + <span style="color:#A6ACB9">----------------------------------------------------------------------------------------------------</span><span style="color:#A6ACB9"> + </span> + <span style="color:#C695C6">type</span> <span style="color:#C695C6">T1</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> a a + <span style="color:#C695C6">type</span> <span style="color:#C695C6">T2</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> a <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T1</span> a<span style="color:#FFFFFF">)</span> + <span style="color:#C695C6">type</span> <span style="color:#C695C6">T3</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> a <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T1</span> a<span style="color:#FFFFFF">)</span> a<span style="color:#FFFFFF">)</span> + <span style="color:#C695C6">type</span> <span style="color:#C695C6">T4</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T2</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T1</span> a<span style="color:#FFFFFF">)</span> + + <span style="color:#5FB4B4">th_impl_refl</span> <span style="color:#C695C6">::</span> forall a. <span style="color:#C695C6"><i>Pred</span></i> a <span style="color:#C695C6">-></span> <span style="color:#C695C6"><i>Infer</span></i> (<span style="color:#C695C6"><i>Impl</span></i> a a) + th_impl_refl x <span style="color:#F97B58">=</span> step_5 <span style="color:#C695C6">where</span> + wff_1 <span style="color:#F97B58">=</span> <span style="color:#C695C6">PredImpl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> x x<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T1</span> a<span style="color:#FFFFFF">)</span> + step_1 <span style="color:#F97B58">=</span> <span style="color:#C695C6">Ax1</span> x x <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T2</span> a<span style="color:#FFFFFF">)</span> + step_2 <span style="color:#F97B58">=</span> <span style="color:#C695C6">Ax1</span> x wff_1 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T3</span> a<span style="color:#FFFFFF">)</span> + step_3 <span style="color:#F97B58">=</span> <span style="color:#C695C6">Ax2</span> x wff_1 x <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T3</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T4</span> a<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> + step_4 <span style="color:#F97B58">=</span> <span style="color:#C695C6">MP</span> step_3 step_2 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T4</span> a<span style="color:#FFFFFF">)</span> + step_5 <span style="color:#F97B58">=</span> <span style="color:#C695C6">MP</span> step_4 step_1 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T1</span> a<span style="color:#FFFFFF">)</span> + + <span style="color:#C695C6">type</span> <span style="color:#C695C6">T5</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T6</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T9</span> a<span style="color:#FFFFFF">)</span> + <span style="color:#C695C6">type</span> <span style="color:#C695C6">T6</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Not</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Not</span> a<span style="color:#FFFFFF">)</span> + <span style="color:#C695C6">type</span> <span style="color:#C695C6">T7</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Not</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T6</span> a<span style="color:#FFFFFF">)</span> + <span style="color:#C695C6">type</span> <span style="color:#C695C6">T8</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T6</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T7</span> a<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T6</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T10</span> a<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> + <span style="color:#C695C6">type</span> <span style="color:#C695C6">T9</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T7</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T10</span> a<span style="color:#FFFFFF">)</span> + <span style="color:#C695C6">type</span> <span style="color:#C695C6">T10</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Not</span> a<span style="color:#FFFFFF">)</span> a + + <span style="color:#5FB4B4">th_2</span> <span style="color:#C695C6">::</span> forall a. <span style="color:#C695C6"><i>Pred</span></i> a <span style="color:#C695C6">-></span> <span style="color:#C695C6"><i>Infer</span></i> (<span style="color:#C695C6"><i>Impl</span></i> (<span style="color:#C695C6"><i>Not</span></i> (<span style="color:#C695C6"><i>Not</span></i> a)) (<span style="color:#C695C6"><i>Impl</span></i> (<span style="color:#C695C6"><i>Not</span></i> a) a)) + th_2 x <span style="color:#F97B58">=</span> step_7 <span style="color:#C695C6">where</span> + wff_1 <span style="color:#F97B58">=</span> <span style="color:#C695C6">PredNot</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Not</span> x<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Not</span> a<span style="color:#FFFFFF">)</span> + wff_2 <span style="color:#F97B58">=</span> <span style="color:#C695C6">PredNot</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Not</span> wff_1<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T6</span> a<span style="color:#FFFFFF">)</span> + wff_3 <span style="color:#F97B58">=</span> <span style="color:#C695C6">PredImpl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> wff_1 wff_2<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T7</span> a<span style="color:#FFFFFF">)</span> + wff_4 <span style="color:#F97B58">=</span> <span style="color:#C695C6">PredImpl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> wff_1 x<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T10</span> a<span style="color:#FFFFFF">)</span> + wff_5 <span style="color:#F97B58">=</span> <span style="color:#C695C6">PredImpl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> wff_3 wff_4<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T9</span> a<span style="color:#FFFFFF">)</span> + step_1 <span style="color:#F97B58">=</span> <span style="color:#C695C6">Ax3</span> x wff_1 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T9</span> a<span style="color:#FFFFFF">)</span> + step_2 <span style="color:#F97B58">=</span> <span style="color:#C695C6">Ax1</span> wff_5 wff_2 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T9</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T5</span> a<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> + step_3 <span style="color:#F97B58">=</span> <span style="color:#C695C6">MP</span> step_2 step_1 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T5</span> a<span style="color:#FFFFFF">)</span> + step_4 <span style="color:#F97B58">=</span> <span style="color:#C695C6">Ax2</span> wff_2 wff_3 wff_4 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T5</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T8</span> a<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> + step_5 <span style="color:#F97B58">=</span> <span style="color:#C695C6">MP</span> step_4 step_3 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T8</span> a<span style="color:#FFFFFF">)</span> + step_6 <span style="color:#F97B58">=</span> <span style="color:#C695C6">Ax1</span> wff_2 wff_1 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T6</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T7</span> a<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> + step_7 <span style="color:#F97B58">=</span> <span style="color:#C695C6">MP</span> step_5 step_6 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T6</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T10</span> a<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> + +</div> + +=== Explanation === + +We renamed some of the steps to separate "WFF" proofs from "Infer" proofs (we also updated <code>th_impl_refl</code>). The program outputs the following proof: + + (MP (MP (Ax2 ~~P (~P -> ~~P) (~P -> P)) (MP (Ax1 ((~P -> ~~P) -> (~P -> P)) ~~P) (Ax3 P ~P))) (Ax1 ~~P ~P)) + +Notice that WFF steps are almost half of the total steps. If we remove the WFF checks, we can make the proof of the theorem a lot simpler. However, forcing a formula to be well-formed is important, because the system can be expanded to include other types of expressions (such as sets and proper classes). We want to make sure that the arguments of an implication are predicates, and not for example sets. Also, WFF can be generalized to any level of abstraction, so if we decide to introduce quantifiers, we can use WFF checks to ensure that there are no free identifiers in the top-level expression (each identifier must be bound to a quantifier parameter name). When we talk about identifiers, they can be implemented as [[Wikipedia:De_Bruijn_index\|De Bruijn indices]] and substitutions can be achieved by a recursive constraint that ensures that all occurrences of the bound variable are replaced. '
New page size `(new_size)`	53455
Old page size `(old_size)`	0
Lines added in edit `(added_lines)`	[ 0 => '== Introduction ==', 1 => '', 2 => 'In this tutorial we explain how to create a very simple theorem prover in Haskell using generalised algebraic data types. We first define axioms and inference rules, then write a formal proof of a theorem and then write a program to check whether the proof is valid.', 3 => '', 4 => '== Formal system ==', 5 => '', 6 => 'The formal logic system that we use in this example is a simplified version of [[wikipedia:Łukasiewicz_logic\|Łukasiewicz system]]. We define the following inference rules (the first two are axioms because they have no premises and the third one is [[wikipedia:Modus_ponens\|Modus ponens]]):', 7 => '', 8 => '<math>', 9 => ' \begin{aligned}', 10 => ' &\vdash x \to (y \to x) \\', 11 => ' &\vdash (x \to (y \to z)) \to ((x \to y) \to (x \to z)) \\', 12 => ' x, x \to y &\vdash y', 13 => ' \end{aligned}', 14 => '</math>', 15 => '', 16 => 'We call the first one <code>Ax1</code>, the second one <code>Ax2</code> and the third one <code>MP</code>. Implication is represented by <code>-></code> and the inference symbol is <code>\|-</code>. We want to prove that <math>(x\to x)</math> for any predicate <math>x</math> (the theorem of the reflexivity of the implication).', 17 => '', 18 => 'Before we start, we want to make sure that <code>x,y,z</code> must be well-formed formulas. A well-formed formula in our system is only a predicate. A predicate is either an implication, or some contant predicate <code>P</code> (just as an example to reduce the generality). We can construct an implication only if both arguments are WFFs (well-formed formulas). The constant predicate <code>P</code> is a WFF by definition.', 19 => '', 20 => '== The program ==', 21 => '', 22 => '<div style="background:#343D46;color:#D8DEE9;font-family:monospace;white-space:pre">', 23 => ' {-# <span style="color:#C695C6">LANGUAGE</span> GADTs #-}', 24 => ' {-# <span style="color:#C695C6">LANGUAGE</span> ScopedTypeVariables #-}', 25 => ' {-# <span style="color:#C695C6">LANGUAGE</span> KindSignatures #-}', 26 => ' ', 27 => ' <span style="color:#5FB4B4">main</span> <span style="color:#C695C6">::</span> <span style="color:#C695C6"><i>IO</span></i> <span style="color:#C695C6"><i>()</span></i>', 28 => ' main <span style="color:#F97B58">=</span> <span style="color:#6699CC"><i>putStrLn</span></i> output', 29 => ' ', 30 => ' <span style="color:#5FB4B4">output</span> <span style="color:#C695C6">::</span> <span style="color:#C695C6"><i>String</span></i>', 31 => ' output <span style="color:#F97B58">=</span> <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span>th_impl_refl <span style="color:#FFFFFF">(</span><span style="color:#C695C6">PredP</span> <span style="color:#C695C6">P</span><span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span>', 32 => ' ', 33 => ' <span style="color:#A6ACB9">----------------------------------------------------------------------------------------------------</span><span style="color:#A6ACB9">', 34 => ' </span>', 35 => ' <span style="color:#C695C6">data</span> <span style="color:#C695C6">Pred</span> <span style="color:#F97B58">::</span> <span style="color:#F97B58"></span> <span style="color:#F97B58">-></span> <span style="color:#F97B58"></span> <span style="color:#C695C6">where</span>', 36 => ' <span style="color:#C695C6">PredP</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">P</span> <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> <span style="color:#C695C6">P</span>', 37 => ' <span style="color:#C695C6">PredImpl</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Impl</span> a b <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a b<span style="color:#FFFFFF">)</span>', 38 => ' ', 39 => ' <span style="color:#C695C6">data</span> <span style="color:#C695C6">P</span> <span style="color:#F97B58">::</span> <span style="color:#F97B58"></span> <span style="color:#C695C6">where</span>', 40 => ' <span style="color:#C695C6">P</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">P</span>', 41 => ' ', 42 => ' <span style="color:#C695C6">data</span> <span style="color:#C695C6">Impl</span> <span style="color:#F97B58">::</span> <span style="color:#F97B58"></span> <span style="color:#F97B58">-></span> <span style="color:#F97B58"></span> <span style="color:#F97B58">-></span> <span style="color:#F97B58"></span> <span style="color:#C695C6">where</span>', 43 => ' <span style="color:#C695C6">Impl</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> a <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> b <span style="color:#F97B58">-></span> <span style="color:#C695C6">Impl</span> a b', 44 => ' ', 45 => ' <span style="color:#C695C6">data</span> <span style="color:#C695C6">Infer</span> <span style="color:#F97B58">::</span> <span style="color:#F97B58"></span> <span style="color:#F97B58">-></span> <span style="color:#F97B58"></span> <span style="color:#C695C6">where</span>', 46 => ' <span style="color:#C695C6">Ax1</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> a <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> b <span style="color:#F97B58">-></span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> b a<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span>', 47 => ' <span style="color:#C695C6">Ax2</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> a <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> b <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> c <span style="color:#F97B58">-></span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> b c<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a b<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a c<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span>', 48 => ' <span style="color:#C695C6">MP</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">-></span> <span style="color:#C695C6">Infer</span> a <span style="color:#F97B58">-></span> <span style="color:#C695C6">Infer</span> b', 49 => ' ', 50 => ' <span style="color:#A6ACB9">----------------------------------------------------------------------------------------------------</span><span style="color:#A6ACB9">', 51 => ' </span>', 52 => ' <span style="color:#C695C6">instance</span> <span style="color:#C695C6"><i>Show</span></i> (<span style="color:#C695C6"><i>Pred</span></i> a) <span style="color:#C695C6">where</span>', 53 => ' <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">PredP</span> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#6699CC"><i>show</span></i> a', 54 => ' <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">PredImpl</span> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#6699CC"><i>show</span></i> a', 55 => ' ', 56 => ' <span style="color:#C695C6">instance</span> <span style="color:#C695C6"><i>Show</span></i> <span style="color:#C695C6"><i>P</span></i> <span style="color:#C695C6">where</span>', 57 => ' <span style="color:#6699CC"><i>show</span></i> P <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">P</span><span style="color:#5FB4B4">"</span>', 58 => ' ', 59 => ' <span style="color:#C695C6">instance</span> <span style="color:#C695C6"><i>Show</span></i> (<span style="color:#C695C6"><i>Impl</span></i> a b) <span style="color:#C695C6">where</span>', 60 => ' <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">(</span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794"> </span><span style="color:#99C794">-> </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">)</span><span style="color:#5FB4B4">"</span>', 61 => ' ', 62 => ' <span style="color:#C695C6">instance</span> <span style="color:#C695C6"><i>Show</span></i> (<span style="color:#C695C6"><i>Infer</span></i> a) <span style="color:#C695C6">where</span>', 63 => ' <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Ax1</span> a b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">(</span><span style="color:#99C794">Ax1 </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794"> </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">)</span><span style="color:#5FB4B4">"</span>', 64 => ' <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Ax2</span> a b c<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">(</span><span style="color:#99C794">Ax2 </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794"> </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794"> </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> c<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">)</span><span style="color:#5FB4B4">"</span>', 65 => ' <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">MP</span> a b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">(</span><span style="color:#99C794">MP </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794"> </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">)</span><span style="color:#5FB4B4">"</span>', 66 => ' ', 67 => ' <span style="color:#A6ACB9">----------------------------------------------------------------------------------------------------</span><span style="color:#A6ACB9">', 68 => ' </span>', 69 => ' <span style="color:#C695C6">type</span> <span style="color:#C695C6">T1</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> a a', 70 => ' <span style="color:#C695C6">type</span> <span style="color:#C695C6">T2</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> a <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T1</span> a<span style="color:#FFFFFF">)</span>', 71 => ' <span style="color:#C695C6">type</span> <span style="color:#C695C6">T3</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> a <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T1</span> a<span style="color:#FFFFFF">)</span> a<span style="color:#FFFFFF">)</span>', 72 => ' <span style="color:#C695C6">type</span> <span style="color:#C695C6">T4</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T2</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T1</span> a<span style="color:#FFFFFF">)</span>', 73 => ' ', 74 => ' <span style="color:#5FB4B4">th_impl_refl</span> <span style="color:#C695C6">::</span> forall a. <span style="color:#C695C6"><i>Pred</span></i> a <span style="color:#C695C6">-></span> <span style="color:#C695C6"><i>Infer</span></i> (<span style="color:#C695C6"><i>Impl</span></i> a a)', 75 => ' th_impl_refl x <span style="color:#F97B58">=</span> step_6 <span style="color:#C695C6">where</span>', 76 => ' step_1 <span style="color:#F97B58">=</span> <span style="color:#C695C6">PredImpl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> x x<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T1</span> a<span style="color:#FFFFFF">)</span>', 77 => ' step_2 <span style="color:#F97B58">=</span> <span style="color:#C695C6">Ax1</span> x x <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T2</span> a<span style="color:#FFFFFF">)</span>', 78 => ' step_3 <span style="color:#F97B58">=</span> <span style="color:#C695C6">Ax1</span> x step_1 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T3</span> a<span style="color:#FFFFFF">)</span>', 79 => ' step_4 <span style="color:#F97B58">=</span> <span style="color:#C695C6">Ax2</span> x step_1 x <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T3</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T4</span> a<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span>', 80 => ' step_5 <span style="color:#F97B58">=</span> <span style="color:#C695C6">MP</span> step_4 step_3 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T4</span> a<span style="color:#FFFFFF">)</span>', 81 => ' step_6 <span style="color:#F97B58">=</span> <span style="color:#C695C6">MP</span> step_5 step_2 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T1</span> a<span style="color:#FFFFFF">)</span>', 82 => '', 83 => '</div>', 84 => '', 85 => '== Explanation ==', 86 => '', 87 => '=== Data types ===', 88 => '', 89 => 'We define four data types. The first data type is <code>Pred</code>, which stands for predicate. It represents predicate WFF (currently the only type of WFF in our system). It is an "abstract" data type in the sense that it just represents a label that we assign to already constructed other data types. In particular, it says that we can label <code>P</code> as a predicate, or we cal label an implication as a predicate. It is like an abstract class in OOP languages.', 90 => '', 91 => 'The next data type is <code>P</code>, which does not have any particular meaning in the system. It is just there for us to be able to examine the result of the proof (otherwise, any attemp to construct a predicate would not terminate).', 92 => '', 93 => 'The third data type is <code>Impl</code>, which stands for implication. As we explained, it "asserts" that both of its arguments must be predicates.', 94 => '', 95 => 'The last data type is <code>Infer</code>, which represents a proof of a predicate. We can construct it using three different constructors. We can either use one of the axioms (<code>Ax1</code> or <code>Ax2</code>), or we can apply Modus ponens.', 96 => '', 97 => 'Next, we have some functions for stringifying our data types. They are just for analyzing the results.', 98 => '', 99 => '=== Theorem ===', 100 => '', 101 => 'Finally, we define and prove theorem <code>th_impl_refl</code>, which states that for any predicate <code>a</code>, the statement <math>(a \to a)</math> is true. We prove it in six steps. The first step proves that if <code>a</code> is a predicate, then <code>Impl a a</code> is also a predicate (types T1..T4 are defined just as aliases to save space). Steps 2 and 3 apply axiom <code>Ax1</code>, step 4 applies axiom <code>Ax2</code> and steps 5 and 6 apply Modus ponens. The type signature of each step is used for correctness check.', 102 => '', 103 => '=== Verifying the proof ===', 104 => '', 105 => 'If the program does not compile, either the proof is wrong, or you have syntax errors. If the program compiles, it still does not mean that the proof is correct, because you may have a cyclic theorem dependency in your proof. You need to run the program and make sure the program halts. If the program does not halt, it probably means you have a cyclic dependency somewhere.', 106 => '', 107 => 'The output of the program is the proof of the theorem for sample statement <code>P</code> that we introduced just for this purpose. The program show the following output:', 108 => '', 109 => ' (MP (MP (Ax2 P (P -> P) P) (Ax1 P (P -> P))) (Ax1 P P))', 110 => '', 111 => '== Adding new features ==', 112 => '', 113 => 'It is very easy to add new features (axioms, inference rules, definitions, data types, theorems, etc). For example, if we want to add new axiom <code>Ax3</code> that defines negation:', 114 => '', 115 => '<math>', 116 => ' \vdash(\lnot x\to\lnot y)\to(y\to x)', 117 => '</math>', 118 => '', 119 => 'and we want to prove that <math>\lnot\lnot x\to(\lnot x\to x)</math> for any statement <math>x</math>, then we need update the program by adding a new data type <code>Not</code> for negation, new axiom <code>Ax3</code> as an <code>Infer</code> constructor, and finally theorem <code>th_2</code> that proves what we need.', 120 => '', 121 => '<div style="background:#343D46;color:#D8DEE9;font-family:monospace;white-space:pre">', 122 => ' {-# <span style="color:#C695C6">LANGUAGE</span> GADTs #-}', 123 => ' {-# <span style="color:#C695C6">LANGUAGE</span> ScopedTypeVariables #-}', 124 => ' {-# <span style="color:#C695C6">LANGUAGE</span> KindSignatures #-}', 125 => ' ', 126 => ' <span style="color:#5FB4B4">main</span> <span style="color:#C695C6">::</span> <span style="color:#C695C6"><i>IO</span></i> <span style="color:#C695C6"><i>()</span></i>', 127 => ' main <span style="color:#F97B58">=</span> <span style="color:#6699CC"><i>putStrLn</span></i> output', 128 => ' ', 129 => ' <span style="color:#5FB4B4">output</span> <span style="color:#C695C6">::</span> <span style="color:#C695C6"><i>String</span></i>', 130 => ' output <span style="color:#F97B58">=</span> <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span>th_2 <span style="color:#FFFFFF">(</span><span style="color:#C695C6">PredP</span> <span style="color:#C695C6">P</span><span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span>', 131 => ' ', 132 => ' <span style="color:#A6ACB9">----------------------------------------------------------------------------------------------------</span><span style="color:#A6ACB9">', 133 => ' </span>', 134 => ' <span style="color:#C695C6">data</span> <span style="color:#C695C6">Pred</span> <span style="color:#F97B58">::</span> <span style="color:#F97B58"></span> <span style="color:#F97B58">-></span> <span style="color:#F97B58"></span> <span style="color:#C695C6">where</span>', 135 => ' <span style="color:#C695C6">PredP</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">P</span> <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> <span style="color:#C695C6">P</span>', 136 => ' <span style="color:#C695C6">PredImpl</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Impl</span> a b <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a b<span style="color:#FFFFFF">)</span>', 137 => ' <span style="color:#C695C6">PredNot</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Not</span> a <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Not</span> a<span style="color:#FFFFFF">)</span>', 138 => ' ', 139 => ' <span style="color:#C695C6">data</span> <span style="color:#C695C6">P</span> <span style="color:#F97B58">::</span> <span style="color:#F97B58"></span> <span style="color:#C695C6">where</span>', 140 => ' <span style="color:#C695C6">P</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">P</span>', 141 => ' ', 142 => ' <span style="color:#C695C6">data</span> <span style="color:#C695C6">Impl</span> <span style="color:#F97B58">::</span> <span style="color:#F97B58"></span> <span style="color:#F97B58">-></span> <span style="color:#F97B58"></span> <span style="color:#F97B58">-></span> <span style="color:#F97B58"></span> <span style="color:#C695C6">where</span>', 143 => ' <span style="color:#C695C6">Impl</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> a <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> b <span style="color:#F97B58">-></span> <span style="color:#C695C6">Impl</span> a b', 144 => ' ', 145 => ' <span style="color:#C695C6">data</span> <span style="color:#C695C6">Not</span> <span style="color:#F97B58">::</span> <span style="color:#F97B58"></span> <span style="color:#F97B58">-></span> <span style="color:#F97B58"></span> <span style="color:#C695C6">where</span>', 146 => ' <span style="color:#C695C6">Not</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> a <span style="color:#F97B58">-></span> <span style="color:#C695C6">Not</span> a', 147 => ' ', 148 => ' <span style="color:#C695C6">data</span> <span style="color:#C695C6">Infer</span> <span style="color:#F97B58">::</span> <span style="color:#F97B58"></span> <span style="color:#F97B58">-></span> <span style="color:#F97B58"></span> <span style="color:#C695C6">where</span>', 149 => ' <span style="color:#C695C6">Ax1</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> a <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> b <span style="color:#F97B58">-></span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> b a<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span>', 150 => ' <span style="color:#C695C6">Ax2</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> a <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> b <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> c <span style="color:#F97B58">-></span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> b c<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a b<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a c<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span>', 151 => ' <span style="color:#C695C6">Ax3</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> a <span style="color:#F97B58">-></span> <span style="color:#C695C6">Pred</span> b <span style="color:#F97B58">-></span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Not</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Not</span> b<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> b a<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span>', 152 => ' <span style="color:#C695C6">MP</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">-></span> <span style="color:#C695C6">Infer</span> a <span style="color:#F97B58">-></span> <span style="color:#C695C6">Infer</span> b', 153 => ' ', 154 => ' <span style="color:#A6ACB9">----------------------------------------------------------------------------------------------------</span><span style="color:#A6ACB9">', 155 => ' </span>', 156 => ' <span style="color:#C695C6">instance</span> <span style="color:#C695C6"><i>Show</span></i> (<span style="color:#C695C6"><i>Pred</span></i> a) <span style="color:#C695C6">where</span>', 157 => ' <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">PredP</span> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#6699CC"><i>show</span></i> a', 158 => ' <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">PredImpl</span> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#6699CC"><i>show</span></i> a', 159 => ' <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">PredNot</span> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#6699CC"><i>show</span></i> a', 160 => ' ', 161 => ' <span style="color:#C695C6">instance</span> <span style="color:#C695C6"><i>Show</span></i> <span style="color:#C695C6"><i>P</span></i> <span style="color:#C695C6">where</span>', 162 => ' <span style="color:#6699CC"><i>show</span></i> <span style="color:#C695C6">P</span> <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">P</span><span style="color:#5FB4B4">"</span>', 163 => ' ', 164 => ' <span style="color:#C695C6">instance</span> <span style="color:#C695C6"><i>Show</span></i> (<span style="color:#C695C6"><i>Impl</span></i> a b) <span style="color:#C695C6">where</span>', 165 => ' <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> a b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">(</span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794"> </span><span style="color:#99C794">-> </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">)</span><span style="color:#5FB4B4">"</span>', 166 => ' ', 167 => ' <span style="color:#C695C6">instance</span> <span style="color:#C695C6"><i>Show</span></i> (<span style="color:#C695C6"><i>Not</span></i> a) <span style="color:#C695C6">where</span>', 168 => ' <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Not</span> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">~</span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> a<span style="color:#FFFFFF">)</span>', 169 => ' ', 170 => ' <span style="color:#C695C6">instance</span> <span style="color:#C695C6"><i>Show</span></i> (<span style="color:#C695C6"><i>Infer</span></i> a) <span style="color:#C695C6">where</span>', 171 => ' <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Ax1</span> a b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">(</span><span style="color:#99C794">Ax1 </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794"> </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">)</span><span style="color:#5FB4B4">"</span>', 172 => ' <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Ax2</span> a b c<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">(</span><span style="color:#99C794">Ax2 </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794"> </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794"> </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> c<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">)</span><span style="color:#5FB4B4">"</span>', 173 => ' <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Ax3</span> a b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">(</span><span style="color:#99C794">Ax3 </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794"> </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">)</span><span style="color:#5FB4B4">"</span>', 174 => ' <span style="color:#6699CC"><i>show</span></i> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">MP</span> a b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">=</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">(</span><span style="color:#99C794">MP </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> a<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794"> </span><span style="color:#5FB4B4">"</span> <span style="color:#F97B58">++</span> <span style="color:#FFFFFF">(</span><span style="color:#6699CC"><i>show</span></i> b<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">++</span> <span style="color:#5FB4B4">"</span><span style="color:#99C794">)</span><span style="color:#5FB4B4">"</span>', 175 => ' ', 176 => ' <span style="color:#A6ACB9">----------------------------------------------------------------------------------------------------</span><span style="color:#A6ACB9">', 177 => ' </span>', 178 => ' <span style="color:#C695C6">type</span> <span style="color:#C695C6">T1</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> a a', 179 => ' <span style="color:#C695C6">type</span> <span style="color:#C695C6">T2</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> a <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T1</span> a<span style="color:#FFFFFF">)</span>', 180 => ' <span style="color:#C695C6">type</span> <span style="color:#C695C6">T3</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> a <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T1</span> a<span style="color:#FFFFFF">)</span> a<span style="color:#FFFFFF">)</span>', 181 => ' <span style="color:#C695C6">type</span> <span style="color:#C695C6">T4</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T2</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T1</span> a<span style="color:#FFFFFF">)</span>', 182 => ' ', 183 => ' <span style="color:#5FB4B4">th_impl_refl</span> <span style="color:#C695C6">::</span> forall a. <span style="color:#C695C6"><i>Pred</span></i> a <span style="color:#C695C6">-></span> <span style="color:#C695C6"><i>Infer</span></i> (<span style="color:#C695C6"><i>Impl</span></i> a a)', 184 => ' th_impl_refl x <span style="color:#F97B58">=</span> step_5 <span style="color:#C695C6">where</span>', 185 => ' wff_1 <span style="color:#F97B58">=</span> <span style="color:#C695C6">PredImpl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> x x<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T1</span> a<span style="color:#FFFFFF">)</span>', 186 => ' step_1 <span style="color:#F97B58">=</span> <span style="color:#C695C6">Ax1</span> x x <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T2</span> a<span style="color:#FFFFFF">)</span>', 187 => ' step_2 <span style="color:#F97B58">=</span> <span style="color:#C695C6">Ax1</span> x wff_1 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T3</span> a<span style="color:#FFFFFF">)</span>', 188 => ' step_3 <span style="color:#F97B58">=</span> <span style="color:#C695C6">Ax2</span> x wff_1 x <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T3</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T4</span> a<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span>', 189 => ' step_4 <span style="color:#F97B58">=</span> <span style="color:#C695C6">MP</span> step_3 step_2 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T4</span> a<span style="color:#FFFFFF">)</span>', 190 => ' step_5 <span style="color:#F97B58">=</span> <span style="color:#C695C6">MP</span> step_4 step_1 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T1</span> a<span style="color:#FFFFFF">)</span>', 191 => ' ', 192 => ' <span style="color:#C695C6">type</span> <span style="color:#C695C6">T5</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T6</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T9</span> a<span style="color:#FFFFFF">)</span>', 193 => ' <span style="color:#C695C6">type</span> <span style="color:#C695C6">T6</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Not</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Not</span> a<span style="color:#FFFFFF">)</span>', 194 => ' <span style="color:#C695C6">type</span> <span style="color:#C695C6">T7</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Not</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T6</span> a<span style="color:#FFFFFF">)</span>', 195 => ' <span style="color:#C695C6">type</span> <span style="color:#C695C6">T8</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T6</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T7</span> a<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T6</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T10</span> a<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span>', 196 => ' <span style="color:#C695C6">type</span> <span style="color:#C695C6">T9</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T7</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T10</span> a<span style="color:#FFFFFF">)</span>', 197 => ' <span style="color:#C695C6">type</span> <span style="color:#C695C6">T10</span> a <span style="color:#F97B58">=</span> <span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Not</span> a<span style="color:#FFFFFF">)</span> a', 198 => ' ', 199 => ' <span style="color:#5FB4B4">th_2</span> <span style="color:#C695C6">::</span> forall a. <span style="color:#C695C6"><i>Pred</span></i> a <span style="color:#C695C6">-></span> <span style="color:#C695C6"><i>Infer</span></i> (<span style="color:#C695C6"><i>Impl</span></i> (<span style="color:#C695C6"><i>Not</span></i> (<span style="color:#C695C6"><i>Not</span></i> a)) (<span style="color:#C695C6"><i>Impl</span></i> (<span style="color:#C695C6"><i>Not</span></i> a) a))', 200 => ' th_2 x <span style="color:#F97B58">=</span> step_7 <span style="color:#C695C6">where</span>', 201 => ' wff_1 <span style="color:#F97B58">=</span> <span style="color:#C695C6">PredNot</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Not</span> x<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Not</span> a<span style="color:#FFFFFF">)</span>', 202 => ' wff_2 <span style="color:#F97B58">=</span> <span style="color:#C695C6">PredNot</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Not</span> wff_1<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T6</span> a<span style="color:#FFFFFF">)</span>', 203 => ' wff_3 <span style="color:#F97B58">=</span> <span style="color:#C695C6">PredImpl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> wff_1 wff_2<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T7</span> a<span style="color:#FFFFFF">)</span>', 204 => ' wff_4 <span style="color:#F97B58">=</span> <span style="color:#C695C6">PredImpl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> wff_1 x<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T10</span> a<span style="color:#FFFFFF">)</span>', 205 => ' wff_5 <span style="color:#F97B58">=</span> <span style="color:#C695C6">PredImpl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> wff_3 wff_4<span style="color:#FFFFFF">)</span> <span style="color:#F97B58">::</span> <span style="color:#C695C6">Pred</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T9</span> a<span style="color:#FFFFFF">)</span>', 206 => ' step_1 <span style="color:#F97B58">=</span> <span style="color:#C695C6">Ax3</span> x wff_1 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T9</span> a<span style="color:#FFFFFF">)</span>', 207 => ' step_2 <span style="color:#F97B58">=</span> <span style="color:#C695C6">Ax1</span> wff_5 wff_2 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T9</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T5</span> a<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span>', 208 => ' step_3 <span style="color:#F97B58">=</span> <span style="color:#C695C6">MP</span> step_2 step_1 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T5</span> a<span style="color:#FFFFFF">)</span>', 209 => ' step_4 <span style="color:#F97B58">=</span> <span style="color:#C695C6">Ax2</span> wff_2 wff_3 wff_4 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T5</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T8</span> a<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span>', 210 => ' step_5 <span style="color:#F97B58">=</span> <span style="color:#C695C6">MP</span> step_4 step_3 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T8</span> a<span style="color:#FFFFFF">)</span>', 211 => ' step_6 <span style="color:#F97B58">=</span> <span style="color:#C695C6">Ax1</span> wff_2 wff_1 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T6</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T7</span> a<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span>', 212 => ' step_7 <span style="color:#F97B58">=</span> <span style="color:#C695C6">MP</span> step_5 step_6 <span style="color:#F97B58">::</span> <span style="color:#C695C6">Infer</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">Impl</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T6</span> a<span style="color:#FFFFFF">)</span> <span style="color:#FFFFFF">(</span><span style="color:#C695C6">T10</span> a<span style="color:#FFFFFF">)</span><span style="color:#FFFFFF">)</span>', 213 => '', 214 => '</div>', 215 => '', 216 => '=== Explanation ===', 217 => '', 218 => 'We renamed some of the steps to separate "WFF" proofs from "Infer" proofs (we also updated <code>th_impl_refl</code>). The program outputs the following proof:', 219 => '', 220 => ' (MP (MP (Ax2 ~~P (~P -> ~~P) (~P -> P)) (MP (Ax1 ((~P -> ~~P) -> (~P -> P)) ~~P) (Ax3 P ~P))) (Ax1 ~~P ~P))', 221 => '', 222 => 'Notice that WFF steps are almost half of the total steps. If we remove the WFF checks, we can make the proof of the theorem a lot simpler. However, forcing a formula to be well-formed is important, because the system can be expanded to include other types of expressions (such as sets and proper classes). We want to make sure that the arguments of an implication are predicates, and not for example sets. Also, WFF can be generalized to any level of abstraction, so if we decide to introduce quantifiers, we can use WFF checks to ensure that there are no free identifiers in the top-level expression (each identifier must be bound to a quantifier parameter name). When we talk about identifiers, they can be implemented as [[Wikipedia:De_Bruijn_index\|De Bruijn indices]] and substitutions can be achieved by a recursive constraint that ensures that all occurrences of the bound variable are replaced.' ]
Unix timestamp of change `(timestamp)`	1611170427

Examine individual changes

Variables generated for this change

Navigation menu

Search