From b7648ef5c3f4fad5e496249bfe31028de53e4fe7 Mon Sep 17 00:00:00 2001
From: Fedor Isakov <fisakov@gmail.com>
Date: Mon, 7 Jan 2019 11:03:55 +0100
Subject: [PATCH] Document judgements and reasonings in Fitch sample languages.

---
 .../models/editor.mps                         |  53 +++
 .../models/editor.mps                         | 166 +++++++++
 .../models/editor.mps                         | 317 ++++++++++++++++++
 .../languages/samples.fitch/models/editor.mps |  93 +++++
 4 files changed, 629 insertions(+)

diff --git a/samples/fitch/languages/samples.fitch.firstOrderLogic/models/editor.mps b/samples/fitch/languages/samples.fitch.firstOrderLogic/models/editor.mps
index a078235f..57bce355 100644
--- a/samples/fitch/languages/samples.fitch.firstOrderLogic/models/editor.mps
+++ b/samples/fitch/languages/samples.fitch.firstOrderLogic/models/editor.mps
@@ -40,6 +40,9 @@
       <concept id="1080736578640" name="jetbrains.mps.lang.editor.structure.BaseEditorComponent" flags="ig" index="2wURMF">
         <child id="1080736633877" name="cellModel" index="2wV5jI" />
       </concept>
+      <concept id="1078938745671" name="jetbrains.mps.lang.editor.structure.EditorComponentDeclaration" flags="ig" index="PKFIW">
+        <child id="7033942394258392116" name="overridenEditorComponent" index="1PM95z" />
+      </concept>
       <concept id="1078939183254" name="jetbrains.mps.lang.editor.structure.CellModel_Component" flags="sg" stub="3162947552742194261" index="PMmxH">
         <reference id="1078939183255" name="editorComponent" index="PMmxG" />
       </concept>
@@ -81,6 +84,9 @@
       <concept id="1225900081164" name="jetbrains.mps.lang.editor.structure.CellModel_ReadOnlyModelAccessor" flags="sg" stub="3708815482283559694" index="1HlG4h">
         <child id="1225900141900" name="modelAccessor" index="1HlULh" />
       </concept>
+      <concept id="7033942394256351208" name="jetbrains.mps.lang.editor.structure.EditorComponentDeclarationReference" flags="ng" index="1PE4EZ">
+        <reference id="7033942394256351817" name="editorComponent" index="1PE7su" />
+      </concept>
       <concept id="1176717841777" name="jetbrains.mps.lang.editor.structure.QueryFunction_ModelAccess_Getter" flags="in" index="3TQlhw" />
       <concept id="1166049232041" name="jetbrains.mps.lang.editor.structure.AbstractComponent" flags="ng" index="1XWOmA">
         <reference id="1166049300910" name="conceptDeclaration" index="1XX52x" />
@@ -117,6 +123,9 @@
       <concept id="1133920641626" name="jetbrains.mps.lang.core.structure.BaseConcept" flags="ng" index="2VYdi">
         <property id="1193676396447" name="virtualPackage" index="3GE5qa" />
       </concept>
+      <concept id="1169194658468" name="jetbrains.mps.lang.core.structure.INamedConcept" flags="ng" index="TrEIO">
+        <property id="1169194664001" name="name" index="TrG5h" />
+      </concept>
     </language>
   </registry>
   <node concept="24kQdi" id="3w0n0hzkN7k">
@@ -370,5 +379,49 @@
       <node concept="l2Vlx" id="$u9BK_zdQp" role="2iSdaV" />
     </node>
   </node>
+  <node concept="PKFIW" id="4h0MmDW88l0">
+    <property role="3GE5qa" value="proof.rule" />
+    <property role="TrG5h" value="EqualityElim_DOC" />
+    <ref role="1XX52x" to="yhz9:3w0n0hzkQ4j" resolve="EqualityElim" />
+    <node concept="3EZMnI" id="4h0MmDW88l4" role="2wV5jI">
+      <node concept="3F0ifn" id="4h0MmDW88lb" role="3EZMnx">
+        <property role="3F0ifm" value="Equality Elimination" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW88le" role="3EZMnx" />
+      <node concept="3F0ifn" id="4h0MmDW88lh" role="3EZMnx">
+        <property role="3F0ifm" value="Eliminator for equality relation." />
+        <node concept="Vb9p2" id="4h0MmDW88ll" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW88ln" role="3EZMnx">
+        <property role="3F0ifm" value="Must have two bases (premises) : PREMISE and an equality of the form (LEFT = RIGHT)." />
+        <node concept="Vb9p2" id="4h0MmDW88X5" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW88X7" role="3EZMnx">
+        <property role="3F0ifm" value="Conclusion must match PREMISE after consistently replacing LEFT with RIGHT (or the other way around)." />
+        <node concept="Vb9p2" id="4h0MmDW88Xg" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW88Xi" role="3EZMnx" />
+      <node concept="3F0ifn" id="4h0MmDW88WY" role="3EZMnx">
+        <property role="3F0ifm" value="Replacement must be substitutable for the term being replaced." />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW88Xt" role="3EZMnx" />
+      <node concept="3F0ifn" id="4h0MmDW88XD" role="3EZMnx">
+        <property role="3F0ifm" value="The following quotation describes what it means for a term to be free for a variable:" />
+        <node concept="Vb9p2" id="4h0MmDW88Yj" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW88XQ" role="3EZMnx">
+        <property role="3F0ifm" value="   &quot;a term t is free for a variable x in a sentence s if and only if" />
+        <node concept="Vb9p2" id="4h0MmDW88Yl" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW88Y4" role="3EZMnx">
+        <property role="3F0ifm" value="    no free occurrence of x occurs within the scope of a quantifier of some variable in t&quot;" />
+        <node concept="Vb9p2" id="4h0MmDW88Yn" role="3F10Kt" />
+      </node>
+      <node concept="2iRkQZ" id="4h0MmDW88l7" role="2iSdaV" />
+    </node>
+    <node concept="1PE4EZ" id="4h0MmDW88l2" role="1PM95z">
+      <ref role="1PE7su" to="8v9h:4h0MmDW7NkU" resolve="Judgement_DOC" />
+    </node>
+  </node>
 </model>
 
diff --git a/samples/fitch/languages/samples.fitch.herbrandLogic/models/editor.mps b/samples/fitch/languages/samples.fitch.herbrandLogic/models/editor.mps
index 00de236c..b83c4628 100644
--- a/samples/fitch/languages/samples.fitch.herbrandLogic/models/editor.mps
+++ b/samples/fitch/languages/samples.fitch.herbrandLogic/models/editor.mps
@@ -63,6 +63,9 @@
         <child id="1638911550608610281" name="executeFunction" index="IWgqQ" />
         <child id="5692353713941573325" name="textFunction" index="1hCUd6" />
       </concept>
+      <concept id="1078938745671" name="jetbrains.mps.lang.editor.structure.EditorComponentDeclaration" flags="ig" index="PKFIW">
+        <child id="7033942394258392116" name="overridenEditorComponent" index="1PM95z" />
+      </concept>
       <concept id="1078939183254" name="jetbrains.mps.lang.editor.structure.CellModel_Component" flags="sg" stub="3162947552742194261" index="PMmxH">
         <reference id="1078939183255" name="editorComponent" index="PMmxG" />
       </concept>
@@ -70,6 +73,9 @@
       <concept id="4323500428136740385" name="jetbrains.mps.lang.editor.structure.CellIdReferenceSelector" flags="ng" index="2TlHUq">
         <reference id="4323500428136742952" name="id" index="2TlMyj" />
       </concept>
+      <concept id="1186403751766" name="jetbrains.mps.lang.editor.structure.FontStyleStyleClassItem" flags="ln" index="Vb9p2">
+        <property id="1186403771423" name="style" index="Vbekb" />
+      </concept>
       <concept id="1186414536763" name="jetbrains.mps.lang.editor.structure.BooleanStyleSheetItem" flags="ln" index="VOi$J">
         <property id="1186414551515" name="flag" index="VOm3f" />
       </concept>
@@ -143,6 +149,9 @@
         <child id="1948540814633499358" name="editorContext" index="lBI5i" />
         <child id="1948540814635895774" name="cellSelector" index="lGT1i" />
       </concept>
+      <concept id="7033942394256351208" name="jetbrains.mps.lang.editor.structure.EditorComponentDeclarationReference" flags="ng" index="1PE4EZ">
+        <reference id="7033942394256351817" name="editorComponent" index="1PE7su" />
+      </concept>
       <concept id="1161622981231" name="jetbrains.mps.lang.editor.structure.ConceptFunctionParameter_editorContext" flags="nn" index="1Q80Hx" />
       <concept id="7980428675268276156" name="jetbrains.mps.lang.editor.structure.TransformationMenuSection" flags="ng" index="1Qtc8_">
         <child id="7980428675268276157" name="locations" index="1Qtc8$" />
@@ -991,5 +1000,162 @@
     <property role="3GE5qa" value="proof" />
     <ref role="aqKnT" to="bw37:3w0n0hzg5do" resolve="HerbrandProof" />
   </node>
+  <node concept="PKFIW" id="4h0MmDW8b4o">
+    <property role="3GE5qa" value="proof.rule" />
+    <property role="TrG5h" value="ExistsElim_DOC" />
+    <ref role="1XX52x" to="bw37:Vo$tzLEGtG" resolve="ExistsElim" />
+    <node concept="3EZMnI" id="4h0MmDW8b4s" role="2wV5jI">
+      <node concept="3F0ifn" id="4h0MmDW8b4z" role="3EZMnx">
+        <property role="3F0ifm" value="Existential Elimination" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8b4A" role="3EZMnx" />
+      <node concept="3F0ifn" id="4h0MmDW8b4D" role="3EZMnx">
+        <property role="3F0ifm" value="Eliminator for existential quantifier (∃)." />
+        <node concept="Vb9p2" id="4h0MmDW8b4H" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8b4J" role="3EZMnx">
+        <property role="3F0ifm" value="Must have two bases (premises) : " />
+        <node concept="Vb9p2" id="4h0MmDW8b4R" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8b4T" role="3EZMnx">
+        <property role="3F0ifm" value="    first of the form (∃ X. SENTENCE)," />
+        <node concept="Vb9p2" id="4h0MmDW8b4U" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8b53" role="3EZMnx">
+        <property role="3F0ifm" value="    and second of the form (∀ Y. UNI_SENTENCE =&gt; CONCLUSION)," />
+        <node concept="Vb9p2" id="4h0MmDW8b54" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8bOi" role="3EZMnx">
+        <property role="3F0ifm" value="    where CONCLUSION is the judgement's conclusion." />
+        <node concept="Vb9p2" id="4h0MmDW8bOu" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8bOw" role="3EZMnx">
+        <property role="3F0ifm" value="SENTENCE must match UNI_SENTENCE after consistently replacing X with Y." />
+        <node concept="Vb9p2" id="4h0MmDW8bPf" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8bOI" role="3EZMnx" />
+      <node concept="3F0ifn" id="4h0MmDW8bOX" role="3EZMnx">
+        <property role="3F0ifm" value="The variable must not occurr free in the conclusion." />
+      </node>
+      <node concept="2iRkQZ" id="4h0MmDW8b4v" role="2iSdaV" />
+    </node>
+    <node concept="1PE4EZ" id="4h0MmDW8b4q" role="1PM95z">
+      <ref role="1PE7su" to="8v9h:4h0MmDW7NkU" resolve="Judgement_DOC" />
+    </node>
+  </node>
+  <node concept="PKFIW" id="4h0MmDW8gM_">
+    <property role="3GE5qa" value="proof.rule" />
+    <property role="TrG5h" value="ExistsIntro_DOC" />
+    <ref role="1XX52x" to="bw37:Vo$tzLEGtF" resolve="ExistsIntro" />
+    <node concept="3EZMnI" id="4h0MmDW8gMD" role="2wV5jI">
+      <node concept="3F0ifn" id="4h0MmDW8gMK" role="3EZMnx">
+        <property role="3F0ifm" value="Existential Introduction" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8gMN" role="3EZMnx" />
+      <node concept="3F0ifn" id="4h0MmDW8gMQ" role="3EZMnx">
+        <property role="3F0ifm" value="Constructor for existential quantifier (∃)." />
+        <node concept="Vb9p2" id="4h0MmDW8gMU" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8gMW" role="3EZMnx">
+        <property role="3F0ifm" value="Must have one arbitrary basis (premise) : PREMISE." />
+        <node concept="Vb9p2" id="4h0MmDW8gN2" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8gN4" role="3EZMnx">
+        <property role="3F0ifm" value="Conclusion must match (∃ X. SENTENCE)," />
+        <node concept="Vb9p2" id="4h0MmDW8gNl" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8gNc" role="3EZMnx">
+        <property role="3F0ifm" value="    where SENTENCE must match PREMISE after consistently replacing X with a fresh variable." />
+        <node concept="Vb9p2" id="4h0MmDW8gNn" role="3F10Kt" />
+      </node>
+      <node concept="2iRkQZ" id="4h0MmDW8gMG" role="2iSdaV" />
+    </node>
+    <node concept="1PE4EZ" id="4h0MmDW8gMB" role="1PM95z">
+      <ref role="1PE7su" to="8v9h:4h0MmDW7NkU" resolve="Judgement_DOC" />
+    </node>
+  </node>
+  <node concept="PKFIW" id="4h0MmDW8lQU">
+    <property role="3GE5qa" value="proof.rule" />
+    <property role="TrG5h" value="ForallElim_DOC" />
+    <ref role="1XX52x" to="bw37:Vo$tzLEGtE" resolve="ForallElim" />
+    <node concept="3EZMnI" id="4h0MmDW8lQY" role="2wV5jI">
+      <node concept="3F0ifn" id="4h0MmDW8lX_" role="3EZMnx">
+        <property role="3F0ifm" value="Universal Elimination" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8lXC" role="3EZMnx" />
+      <node concept="3F0ifn" id="4h0MmDW8lXF" role="3EZMnx">
+        <property role="3F0ifm" value="Eliminator for universal quantifier (∀)." />
+        <node concept="Vb9p2" id="4h0MmDW8lXJ" role="3F10Kt">
+          <property role="Vbekb" value="PLAIN" />
+        </node>
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8lXL" role="3EZMnx">
+        <property role="3F0ifm" value="Must have one basis (premise) : a universal sentence (∀ X.SENTENCE)," />
+        <node concept="Vb9p2" id="4h0MmDW8lXY" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8lY0" role="3EZMnx">
+        <property role="3F0ifm" value="    where SENTENCE must match the conclusion after consistently replacing X with a fresh variable." />
+        <node concept="Vb9p2" id="4h0MmDW8lY9" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8lXR" role="3EZMnx" />
+      <node concept="3F0ifn" id="4h0MmDW88XD" role="3EZMnx">
+        <property role="3F0ifm" value="The following quotation describes what it means for a term to be free for a variable:" />
+        <node concept="Vb9p2" id="4h0MmDW88Yj" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW88XQ" role="3EZMnx">
+        <property role="3F0ifm" value="   &quot;a term t is free for a variable x in a sentence s if and only if" />
+        <node concept="Vb9p2" id="4h0MmDW88Yl" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW88Y4" role="3EZMnx">
+        <property role="3F0ifm" value="    no free occurrence of x occurs within the scope of a quantifier of some variable in t&quot;" />
+        <node concept="Vb9p2" id="4h0MmDW88Yn" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8lYb" role="3EZMnx" />
+      <node concept="2iRkQZ" id="4h0MmDW8lR1" role="2iSdaV" />
+    </node>
+    <node concept="1PE4EZ" id="4h0MmDW8lQW" role="1PM95z">
+      <ref role="1PE7su" to="8v9h:4h0MmDW7NkU" resolve="Judgement_DOC" />
+    </node>
+  </node>
+  <node concept="PKFIW" id="4h0MmDW8lZG">
+    <property role="3GE5qa" value="proof.rule" />
+    <property role="TrG5h" value="ForallIntro_DOC" />
+    <ref role="1XX52x" to="bw37:Vo$tzLEGtD" resolve="ForallIntro" />
+    <node concept="3EZMnI" id="4h0MmDW8lZK" role="2wV5jI">
+      <node concept="3F0ifn" id="4h0MmDW8lZR" role="3EZMnx">
+        <property role="3F0ifm" value="Universal Introduction" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8lZU" role="3EZMnx" />
+      <node concept="3F0ifn" id="4h0MmDW8lZX" role="3EZMnx">
+        <property role="3F0ifm" value="Constructor for universal quantifier (∀). " />
+        <node concept="Vb9p2" id="4h0MmDW8m0$" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8m0l" role="3EZMnx">
+        <property role="3F0ifm" value="Must have one basis (premise) PREMISE." />
+        <node concept="Vb9p2" id="4h0MmDW8m1v" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8m0M" role="3EZMnx">
+        <property role="3F0ifm" value="Conclusion must be of the form (∀ X.PREMISE)." />
+        <node concept="Vb9p2" id="4h0MmDW8m1x" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8m0T" role="3EZMnx" />
+      <node concept="3F0ifn" id="4h0MmDW8m1k" role="3EZMnx">
+        <property role="3F0ifm" value="The following quote explains what it means for the quantified variable to be valid:" />
+        <node concept="Vb9p2" id="4h0MmDW8m1B" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8m11" role="3EZMnx">
+        <property role="3F0ifm" value="    &quot;if the variable being quantified appears in the sentence being quantified," />
+        <node concept="Vb9p2" id="4h0MmDW8m1z" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8m1a" role="3EZMnx">
+        <property role="3F0ifm" value="    it must not appear free in any active assumption&quot;." />
+        <node concept="Vb9p2" id="4h0MmDW8m1_" role="3F10Kt" />
+      </node>
+      <node concept="2iRkQZ" id="4h0MmDW8lZN" role="2iSdaV" />
+    </node>
+    <node concept="1PE4EZ" id="4h0MmDW8lZI" role="1PM95z">
+      <ref role="1PE7su" to="8v9h:4h0MmDW7NkU" resolve="Judgement_DOC" />
+    </node>
+  </node>
 </model>
 
diff --git a/samples/fitch/languages/samples.fitch.propositionalLogic/models/editor.mps b/samples/fitch/languages/samples.fitch.propositionalLogic/models/editor.mps
index 69bd5348..80d7f41b 100644
--- a/samples/fitch/languages/samples.fitch.propositionalLogic/models/editor.mps
+++ b/samples/fitch/languages/samples.fitch.propositionalLogic/models/editor.mps
@@ -67,9 +67,13 @@
         <child id="1638911550608610281" name="executeFunction" index="IWgqQ" />
         <child id="5692353713941573325" name="textFunction" index="1hCUd6" />
       </concept>
+      <concept id="1078938745671" name="jetbrains.mps.lang.editor.structure.EditorComponentDeclaration" flags="ig" index="PKFIW">
+        <child id="7033942394258392116" name="overridenEditorComponent" index="1PM95z" />
+      </concept>
       <concept id="1078939183254" name="jetbrains.mps.lang.editor.structure.CellModel_Component" flags="sg" stub="3162947552742194261" index="PMmxH">
         <reference id="1078939183255" name="editorComponent" index="PMmxG" />
       </concept>
+      <concept id="1186403751766" name="jetbrains.mps.lang.editor.structure.FontStyleStyleClassItem" flags="ln" index="Vb9p2" />
       <concept id="1186414536763" name="jetbrains.mps.lang.editor.structure.BooleanStyleSheetItem" flags="ln" index="VOi$J">
         <property id="1186414551515" name="flag" index="VOm3f" />
       </concept>
@@ -132,6 +136,9 @@
       <concept id="5624877018228264944" name="jetbrains.mps.lang.editor.structure.TransformationMenuContribution" flags="ng" index="3INDKC">
         <child id="6718020819489956031" name="menuReference" index="AmTjC" />
       </concept>
+      <concept id="7033942394256351208" name="jetbrains.mps.lang.editor.structure.EditorComponentDeclarationReference" flags="ng" index="1PE4EZ">
+        <reference id="7033942394256351817" name="editorComponent" index="1PE7su" />
+      </concept>
       <concept id="1161622981231" name="jetbrains.mps.lang.editor.structure.ConceptFunctionParameter_editorContext" flags="nn" index="1Q80Hx" />
       <concept id="7980428675268276156" name="jetbrains.mps.lang.editor.structure.TransformationMenuSection" flags="ng" index="1Qtc8_">
         <child id="7980428675268276157" name="locations" index="1Qtc8$" />
@@ -1397,5 +1404,315 @@
     <property role="3GE5qa" value="proof" />
     <ref role="aqKnT" to="27wh:3JXBM6C3Fs$" resolve="PropositionalProof" />
   </node>
+  <node concept="PKFIW" id="4h0MmDW7NlC">
+    <property role="3GE5qa" value="proof.rule" />
+    <property role="TrG5h" value="AndElim_DOC" />
+    <ref role="1XX52x" to="27wh:3JXBM6C3UTz" resolve="AndElim" />
+    <node concept="3EZMnI" id="4h0MmDW7NlG" role="2wV5jI">
+      <node concept="3F0ifn" id="4h0MmDW7NlN" role="3EZMnx">
+        <property role="3F0ifm" value="And Elimination" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW7NlQ" role="3EZMnx" />
+      <node concept="3F0ifn" id="4h0MmDW7NlT" role="3EZMnx">
+        <property role="3F0ifm" value="Eliminator for And (&amp;)." />
+        <node concept="Vb9p2" id="4h0MmDW7NlX" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW7Os5" role="3EZMnx">
+        <property role="3F0ifm" value="Requires one basis (premise), which must have a form of conjunction." />
+        <node concept="Vb9p2" id="4h0MmDW7Osb" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW83hg" role="3EZMnx">
+        <property role="3F0ifm" value="Conclusion must match one of the conjunction members." />
+        <node concept="Vb9p2" id="4h0MmDW83ho" role="3F10Kt" />
+      </node>
+      <node concept="2iRkQZ" id="4h0MmDW7NlJ" role="2iSdaV" />
+    </node>
+    <node concept="1PE4EZ" id="4h0MmDW7NlE" role="1PM95z">
+      <ref role="1PE7su" to="8v9h:4h0MmDW7NkU" resolve="Judgement_DOC" />
+    </node>
+  </node>
+  <node concept="PKFIW" id="4h0MmDW83hN">
+    <property role="3GE5qa" value="proof.rule" />
+    <property role="TrG5h" value="AndIntro_DOC" />
+    <ref role="1XX52x" to="27wh:3JXBM6C3URE" resolve="AndIntro" />
+    <node concept="3EZMnI" id="4h0MmDW83hR" role="2wV5jI">
+      <node concept="3F0ifn" id="4h0MmDW83hY" role="3EZMnx">
+        <property role="3F0ifm" value="And Introduction" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW83i1" role="3EZMnx" />
+      <node concept="3F0ifn" id="4h0MmDW83i4" role="3EZMnx">
+        <property role="3F0ifm" value="Constructor for And (&amp;)." />
+        <node concept="Vb9p2" id="4h0MmDW83i8" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW83ia" role="3EZMnx">
+        <property role="3F0ifm" value="Must have two bases (premises) : A and B." />
+        <node concept="Vb9p2" id="4h0MmDW83ig" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW83ii" role="3EZMnx">
+        <property role="3F0ifm" value="Conclusion must be a conjunction of its bases : (A &amp; B)." />
+        <node concept="Vb9p2" id="4h0MmDW83iq" role="3F10Kt" />
+      </node>
+      <node concept="2iRkQZ" id="4h0MmDW83hU" role="2iSdaV" />
+    </node>
+    <node concept="1PE4EZ" id="4h0MmDW83hP" role="1PM95z">
+      <ref role="1PE7su" to="8v9h:4h0MmDW7NkU" resolve="Judgement_DOC" />
+    </node>
+  </node>
+  <node concept="PKFIW" id="4h0MmDW8yNo">
+    <property role="3GE5qa" value="proof.rule" />
+    <property role="TrG5h" value="IfElim_DOC" />
+    <ref role="1XX52x" to="27wh:3JXBM6C3ZJm" resolve="IfElim" />
+    <node concept="3EZMnI" id="4h0MmDW8yNs" role="2wV5jI">
+      <node concept="3F0ifn" id="4h0MmDW8yNz" role="3EZMnx">
+        <property role="3F0ifm" value="Implication Elimination" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8yNA" role="3EZMnx" />
+      <node concept="3F0ifn" id="4h0MmDW8yND" role="3EZMnx">
+        <property role="3F0ifm" value="Eliminator for implication (=&gt;) (modus ponens). " />
+        <node concept="Vb9p2" id="4h0MmDW8yNM" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8yNH" role="3EZMnx">
+        <property role="3F0ifm" value="Must have two bases (premises) :•" />
+        <node concept="Vb9p2" id="4h0MmDW8yO8" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8yNO" role="3EZMnx">
+        <property role="3F0ifm" value="    first of the form (SENTENCE =&gt; CONCLUSION)," />
+        <node concept="Vb9p2" id="4h0MmDW8yNV" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8yNX" role="3EZMnx">
+        <property role="3F0ifm" value="    and second SENTENCE," />
+        <node concept="Vb9p2" id="4h0MmDW8yO6" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8z3P" role="3EZMnx">
+        <property role="3F0ifm" value="    where CONCLUSION is the judgement's conslusion." />
+        <node concept="Vb9p2" id="4h0MmDW8z41" role="3F10Kt" />
+      </node>
+      <node concept="2iRkQZ" id="4h0MmDW8yNv" role="2iSdaV" />
+    </node>
+    <node concept="1PE4EZ" id="4h0MmDW8yNq" role="1PM95z">
+      <ref role="1PE7su" to="8v9h:4h0MmDW7NkU" resolve="Judgement_DOC" />
+    </node>
+  </node>
+  <node concept="PKFIW" id="4h0MmDW8yP0">
+    <property role="3GE5qa" value="proof.rule" />
+    <property role="TrG5h" value="IfIntro_DOC" />
+    <ref role="1XX52x" to="27wh:3JXBM6C3ZJ9" resolve="IfIntro" />
+    <node concept="3EZMnI" id="4h0MmDW8yP4" role="2wV5jI">
+      <node concept="3F0ifn" id="4h0MmDW8yPb" role="3EZMnx">
+        <property role="3F0ifm" value="Implication Introduction" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8yPe" role="3EZMnx" />
+      <node concept="3F0ifn" id="4h0MmDW8yPh" role="3EZMnx">
+        <property role="3F0ifm" value="Constructor for implication (=&gt;)." />
+        <node concept="Vb9p2" id="4h0MmDW8yPl" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8yVE" role="3EZMnx">
+        <property role="3F0ifm" value="Must have one basis (premise) which is an assumption in the preceding subproof." />
+        <node concept="Vb9p2" id="4h0MmDW8yVR" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8yVK" role="3EZMnx">
+        <property role="3F0ifm" value="Conclusion must be be of the form (ASSUMPTION =&gt; LAST)," />
+        <node concept="Vb9p2" id="4h0MmDW8yVT" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8Ooi" role="3EZMnx">
+        <property role="3F0ifm" value="   where ASSUMPTION is the assumption in the preceding subproof," />
+        <node concept="Vb9p2" id="4h0MmDW8OoB" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8Oos" role="3EZMnx">
+        <property role="3F0ifm" value="   and LAST is the last judgement in the same subproof." />
+        <node concept="Vb9p2" id="4h0MmDW8OoD" role="3F10Kt" />
+      </node>
+      <node concept="2iRkQZ" id="4h0MmDW8yP7" role="2iSdaV" />
+    </node>
+    <node concept="1PE4EZ" id="4h0MmDW8yP2" role="1PM95z">
+      <ref role="1PE7su" to="8v9h:4h0MmDW7NkU" resolve="Judgement_DOC" />
+    </node>
+  </node>
+  <node concept="PKFIW" id="4h0MmDW8yWk">
+    <property role="3GE5qa" value="proof.rule" />
+    <property role="TrG5h" value="IffElim_DOC" />
+    <ref role="1XX52x" to="27wh:3JXBM6C3ZJo" resolve="IffElim" />
+    <node concept="3EZMnI" id="4h0MmDW8yWo" role="2wV5jI">
+      <node concept="2iRkQZ" id="4h0MmDW8yWr" role="2iSdaV" />
+      <node concept="3F0ifn" id="4h0MmDW8yWv" role="3EZMnx">
+        <property role="3F0ifm" value="Biconditional Elimination" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8yWx" role="3EZMnx" />
+      <node concept="3F0ifn" id="4h0MmDW8z1a" role="3EZMnx">
+        <property role="3F0ifm" value="Eliminator for Biconditional (&lt;=&gt;). " />
+        <node concept="Vb9p2" id="4h0MmDW8z1i" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8yW$" role="3EZMnx">
+        <property role="3F0ifm" value="Must have one basis (premise) of the form (A &lt;=&gt; B) or (B &lt;=&gt; A). " />
+        <node concept="Vb9p2" id="4h0MmDW8z0e" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8z09" role="3EZMnx">
+        <property role="3F0ifm" value="Conclusion must be of the form (A =&gt; B). " />
+        <node concept="Vb9p2" id="4h0MmDW8z0g" role="3F10Kt" />
+      </node>
+    </node>
+    <node concept="1PE4EZ" id="4h0MmDW8yWm" role="1PM95z">
+      <ref role="1PE7su" to="8v9h:4h0MmDW7NkU" resolve="Judgement_DOC" />
+    </node>
+  </node>
+  <node concept="PKFIW" id="4h0MmDW8z0F">
+    <property role="3GE5qa" value="proof.rule" />
+    <property role="TrG5h" value="IffIntro_DOC" />
+    <ref role="1XX52x" to="27wh:3JXBM6C3ZJn" resolve="IffIntro" />
+    <node concept="3EZMnI" id="4h0MmDW8z0J" role="2wV5jI">
+      <node concept="3F0ifn" id="4h0MmDW8z0Q" role="3EZMnx">
+        <property role="3F0ifm" value="Biconditional Introduction" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8z13" role="3EZMnx" />
+      <node concept="3F0ifn" id="4h0MmDW8z16" role="3EZMnx">
+        <property role="3F0ifm" value="Constructor for Biconditinoal (&lt;=&gt;)." />
+        <node concept="Vb9p2" id="4h0MmDW8z1k" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8z1m" role="3EZMnx">
+        <property role="3F0ifm" value="Must have two bases (premises) of the form (A =&gt; B) and (B =&gt; A)." />
+        <node concept="Vb9p2" id="4h0MmDW8z1z" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8z1s" role="3EZMnx">
+        <property role="3F0ifm" value="Conclusion must be of the form (A &lt;=&gt; B)." />
+        <node concept="Vb9p2" id="4h0MmDW8z1_" role="3F10Kt" />
+      </node>
+      <node concept="2iRkQZ" id="4h0MmDW8z0M" role="2iSdaV" />
+    </node>
+    <node concept="1PE4EZ" id="4h0MmDW8z0H" role="1PM95z">
+      <ref role="1PE7su" to="8v9h:4h0MmDW7NkU" resolve="Judgement_DOC" />
+    </node>
+  </node>
+  <node concept="PKFIW" id="4h0MmDW8z20">
+    <property role="3GE5qa" value="proof.rule" />
+    <property role="TrG5h" value="NotElim_DOC" />
+    <ref role="1XX52x" to="27wh:3JXBM6C3ZJ8" resolve="NotElim" />
+    <node concept="3EZMnI" id="4h0MmDW8z24" role="2wV5jI">
+      <node concept="3F0ifn" id="4h0MmDW8z2b" role="3EZMnx">
+        <property role="3F0ifm" value="Negation Elimination" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8z2e" role="3EZMnx" />
+      <node concept="3F0ifn" id="4h0MmDW8z2h" role="3EZMnx">
+        <property role="3F0ifm" value="Eliminator for negation (~)." />
+        <node concept="Vb9p2" id="4h0MmDW8z2l" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8z2n" role="3EZMnx">
+        <property role="3F0ifm" value="Must have one basis (premise) of the form (~~CONCLUSION)," />
+        <node concept="Vb9p2" id="4h0MmDW8z2t" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8z43" role="3EZMnx">
+        <property role="3F0ifm" value="    where CONCLUSION is the judgement's conclusion." />
+        <node concept="Vb9p2" id="4h0MmDW8z4b" role="3F10Kt" />
+      </node>
+      <node concept="2iRkQZ" id="4h0MmDW8z27" role="2iSdaV" />
+    </node>
+    <node concept="1PE4EZ" id="4h0MmDW8z22" role="1PM95z">
+      <ref role="1PE7su" to="8v9h:4h0MmDW7NkU" resolve="Judgement_DOC" />
+    </node>
+  </node>
+  <node concept="PKFIW" id="4h0MmDW8z2S">
+    <property role="3GE5qa" value="proof.rule" />
+    <property role="TrG5h" value="NotIntro_DOC" />
+    <ref role="1XX52x" to="27wh:3JXBM6C3UTA" resolve="NotIntro" />
+    <node concept="3EZMnI" id="4h0MmDW8z2W" role="2wV5jI">
+      <node concept="3F0ifn" id="4h0MmDW8z33" role="3EZMnx">
+        <property role="3F0ifm" value="Negation Introduction" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8z36" role="3EZMnx" />
+      <node concept="3F0ifn" id="4h0MmDW8z39" role="3EZMnx">
+        <property role="3F0ifm" value="Constructor for negation (~)." />
+        <node concept="Vb9p2" id="4h0MmDW8z3d" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8z3f" role="3EZMnx">
+        <property role="3F0ifm" value="Must have two bases (premises) : " />
+        <node concept="Vb9p2" id="4h0MmDW8z3H" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8z3l" role="3EZMnx">
+        <property role="3F0ifm" value="   one of the form (SENTENCE =&gt; A)," />
+        <node concept="Vb9p2" id="4h0MmDW8z3J" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8z3s" role="3EZMnx">
+        <property role="3F0ifm" value="   and another of the form (SENTENCE =&gt; ~A)" />
+        <node concept="Vb9p2" id="4h0MmDW8z3L" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8z3$" role="3EZMnx">
+        <property role="3F0ifm" value="Conclusion must be of the form ~SENTENCE." />
+        <node concept="Vb9p2" id="4h0MmDW8z3N" role="3F10Kt" />
+      </node>
+      <node concept="2iRkQZ" id="4h0MmDW8z2Z" role="2iSdaV" />
+    </node>
+    <node concept="1PE4EZ" id="4h0MmDW8z2U" role="1PM95z">
+      <ref role="1PE7su" to="8v9h:4h0MmDW7NkU" resolve="Judgement_DOC" />
+    </node>
+  </node>
+  <node concept="PKFIW" id="4h0MmDW8z4A">
+    <property role="3GE5qa" value="proof.rule" />
+    <property role="TrG5h" value="OrElim_DOC" />
+    <ref role="1XX52x" to="27wh:3JXBM6C3UT_" resolve="OrElim" />
+    <node concept="3EZMnI" id="4h0MmDW8z4E" role="2wV5jI">
+      <node concept="3F0ifn" id="4h0MmDW8z4L" role="3EZMnx">
+        <property role="3F0ifm" value="Or Elimination" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8z4O" role="3EZMnx" />
+      <node concept="3F0ifn" id="4h0MmDW8z4R" role="3EZMnx">
+        <property role="3F0ifm" value="Eliminator for Or (|)." />
+        <node concept="Vb9p2" id="4h0MmDW8z50" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8z52" role="3EZMnx">
+        <property role="3F0ifm" value="Must have three bases (premises): " />
+        <node concept="Vb9p2" id="4h0MmDW8$bP" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8$bf" role="3EZMnx">
+        <property role="3F0ifm" value="    first of the form (A =&gt; CONCLUSION)," />
+        <node concept="Vb9p2" id="4h0MmDW8$bR" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8$bn" role="3EZMnx">
+        <property role="3F0ifm" value="    second of the form (B =&gt; CONCLUSION)," />
+        <node concept="Vb9p2" id="4h0MmDW8$bT" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8$bw" role="3EZMnx">
+        <property role="3F0ifm" value="    and third of the form (A | B) or (B | A)," />
+        <node concept="Vb9p2" id="4h0MmDW8$bV" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8$bE" role="3EZMnx">
+        <property role="3F0ifm" value="    where CONCLUSION is the judgement's conclusion." />
+        <node concept="Vb9p2" id="4h0MmDW8$bX" role="3F10Kt" />
+      </node>
+      <node concept="2iRkQZ" id="4h0MmDW8z4H" role="2iSdaV" />
+    </node>
+    <node concept="1PE4EZ" id="4h0MmDW8z4C" role="1PM95z">
+      <ref role="1PE7su" to="8v9h:4h0MmDW7NkU" resolve="Judgement_DOC" />
+    </node>
+  </node>
+  <node concept="PKFIW" id="4h0MmDW8$cA">
+    <property role="3GE5qa" value="proof.rule" />
+    <property role="TrG5h" value="OrIntro_DOC" />
+    <ref role="1XX52x" to="27wh:3JXBM6C3UT$" resolve="OrIntro" />
+    <node concept="3EZMnI" id="4h0MmDW8$cE" role="2wV5jI">
+      <node concept="3F0ifn" id="4h0MmDW8$cL" role="3EZMnx">
+        <property role="3F0ifm" value="Or Introduction" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8$cO" role="3EZMnx" />
+      <node concept="3F0ifn" id="4h0MmDW8$cR" role="3EZMnx">
+        <property role="3F0ifm" value="Constructor for Or (|)." />
+        <node concept="Vb9p2" id="4h0MmDW8$cV" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8$cX" role="3EZMnx">
+        <property role="3F0ifm" value="Must have one basis (premise) : PREMISE." />
+        <node concept="Vb9p2" id="4h0MmDW8$kk" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8$k5" role="3EZMnx">
+        <property role="3F0ifm" value="Conclusion must be of the form (SENTENCE | PREMISE) or (PREMISE | SENTENCE)," />
+        <node concept="Vb9p2" id="4h0MmDW8$km" role="3F10Kt" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8$kc" role="3EZMnx">
+        <property role="3F0ifm" value="    where SENTENCE is any sentence." />
+        <node concept="Vb9p2" id="4h0MmDW8$ko" role="3F10Kt" />
+      </node>
+      <node concept="2iRkQZ" id="4h0MmDW8$cH" role="2iSdaV" />
+    </node>
+    <node concept="1PE4EZ" id="4h0MmDW8$cC" role="1PM95z">
+      <ref role="1PE7su" to="8v9h:4h0MmDW7NkU" resolve="Judgement_DOC" />
+    </node>
+  </node>
 </model>
 
diff --git a/samples/fitch/languages/samples.fitch/models/editor.mps b/samples/fitch/languages/samples.fitch/models/editor.mps
index 91141bcc..fc9875ae 100644
--- a/samples/fitch/languages/samples.fitch/models/editor.mps
+++ b/samples/fitch/languages/samples.fitch/models/editor.mps
@@ -19,6 +19,7 @@
         <child id="414384289274416996" name="parts" index="3ft7WO" />
       </concept>
       <concept id="1071666914219" name="jetbrains.mps.lang.editor.structure.ConceptEditorDeclaration" flags="ig" index="24kQdi">
+        <child id="1078153129734" name="inspectedCellModel" index="6VMZX" />
         <child id="2597348684684069742" name="contextHints" index="CpUAK" />
       </concept>
       <concept id="6822301196700715228" name="jetbrains.mps.lang.editor.structure.ConceptEditorHintDeclarationReference" flags="ig" index="2aJ2om">
@@ -33,6 +34,7 @@
       <concept id="1196434649611" name="jetbrains.mps.lang.editor.structure.SubstituteMenu_SimpleString" flags="ng" index="2h3Zct">
         <property id="1196434851095" name="text" index="2h4Kg1" />
       </concept>
+      <concept id="1106270571710" name="jetbrains.mps.lang.editor.structure.CellLayout_Vertical" flags="nn" index="2iRkQZ" />
       <concept id="1237303669825" name="jetbrains.mps.lang.editor.structure.CellLayout_Indent" flags="nn" index="l2Vlx" />
       <concept id="1237307900041" name="jetbrains.mps.lang.editor.structure.IndentLayoutIndentStyleClassItem" flags="ln" index="lj46D" />
       <concept id="1237308012275" name="jetbrains.mps.lang.editor.structure.IndentLayoutNewLineStyleClassItem" flags="ln" index="ljvvj" />
@@ -61,6 +63,9 @@
         <child id="8371900013785948365" name="parameterQuery" index="2$S_pT" />
       </concept>
       <concept id="1638911550608571617" name="jetbrains.mps.lang.editor.structure.TransformationMenu_Default" flags="ng" index="IW6AY" />
+      <concept id="1078938745671" name="jetbrains.mps.lang.editor.structure.EditorComponentDeclaration" flags="ig" index="PKFIW">
+        <child id="7033942394258392116" name="overridenEditorComponent" index="1PM95z" />
+      </concept>
       <concept id="1078939183254" name="jetbrains.mps.lang.editor.structure.CellModel_Component" flags="sg" stub="3162947552742194261" index="PMmxH">
         <reference id="1078939183255" name="editorComponent" index="PMmxG" />
       </concept>
@@ -123,6 +128,9 @@
       <concept id="1225900081164" name="jetbrains.mps.lang.editor.structure.CellModel_ReadOnlyModelAccessor" flags="sg" stub="3708815482283559694" index="1HlG4h">
         <child id="1225900141900" name="modelAccessor" index="1HlULh" />
       </concept>
+      <concept id="7033942394256351208" name="jetbrains.mps.lang.editor.structure.EditorComponentDeclarationReference" flags="ng" index="1PE4EZ">
+        <reference id="7033942394256351817" name="editorComponent" index="1PE7su" />
+      </concept>
       <concept id="1176717841777" name="jetbrains.mps.lang.editor.structure.QueryFunction_ModelAccess_Getter" flags="in" index="3TQlhw" />
       <concept id="2722384699544370949" name="jetbrains.mps.lang.editor.structure.SubstituteMenuPart_Placeholder" flags="ng" index="3VyMlK" />
       <concept id="4307758654696938365" name="jetbrains.mps.lang.editor.structure.QueryFunction_SubstituteMenu_RefPresentation" flags="ig" index="1WAQ3h" />
@@ -310,6 +318,9 @@
       </node>
       <node concept="l2Vlx" id="3JXBM6C3MQ8" role="2iSdaV" />
     </node>
+    <node concept="PMmxH" id="4h0MmDW7Yu1" role="6VMZX">
+      <ref role="PMmxG" node="4h0MmDW7NkU" resolve="Judgement_DOC" />
+    </node>
   </node>
   <node concept="24kQdi" id="3JXBM6C3Pwn">
     <property role="3GE5qa" value="proof.reasoning" />
@@ -320,6 +331,9 @@
       </node>
       <node concept="l2Vlx" id="3JXBM6C3Pws" role="2iSdaV" />
     </node>
+    <node concept="PMmxH" id="4h0MmDW7Nkt" role="6VMZX">
+      <ref role="PMmxG" node="4h0MmDW7Nk2" resolve="Assumption_DOC" />
+    </node>
   </node>
   <node concept="24kQdi" id="3JXBM6C3UQE">
     <property role="3GE5qa" value="proof" />
@@ -629,6 +643,9 @@
     <node concept="2aJ2om" id="$u9BK_zG8W" role="CpUAK">
       <ref role="2$4xQ3" node="$u9BK_zG6f" resolve="BASIS" />
     </node>
+    <node concept="PMmxH" id="4h0MmDW7Nkv" role="6VMZX">
+      <ref role="PMmxG" node="4h0MmDW7Nk2" resolve="Assumption_DOC" />
+    </node>
   </node>
   <node concept="24kQdi" id="$u9BK_zGGT">
     <property role="3GE5qa" value="proof.reasoning" />
@@ -681,6 +698,9 @@
     <node concept="2aJ2om" id="$u9BK_zGGX" role="CpUAK">
       <ref role="2$4xQ3" node="$u9BK_zG6f" resolve="BASIS" />
     </node>
+    <node concept="PMmxH" id="4h0MmDW7YtZ" role="6VMZX">
+      <ref role="PMmxG" node="4h0MmDW7NkU" resolve="Judgement_DOC" />
+    </node>
   </node>
   <node concept="24kQdi" id="$u9BK__JRm">
     <property role="3GE5qa" value="proof.reasoning" />
@@ -691,6 +711,9 @@
         <ref role="1NtTu8" to="jfgh:2aBGSFggvpT" resolve="conclusion" />
       </node>
     </node>
+    <node concept="PMmxH" id="4h0MmDW7E1K" role="6VMZX">
+      <ref role="PMmxG" node="4h0MmDW7E1r" resolve="Premise_DOC" />
+    </node>
   </node>
   <node concept="24kQdi" id="$u9BK__JRu">
     <property role="3GE5qa" value="proof.reasoning" />
@@ -705,6 +728,9 @@
     <node concept="2aJ2om" id="$u9BK__JRw" role="CpUAK">
       <ref role="2$4xQ3" node="$u9BK_zG6f" resolve="BASIS" />
     </node>
+    <node concept="PMmxH" id="4h0MmDW7E1M" role="6VMZX">
+      <ref role="PMmxG" node="4h0MmDW7E1r" resolve="Premise_DOC" />
+    </node>
   </node>
   <node concept="24kQdi" id="$u9BK__JR_">
     <property role="3GE5qa" value="proof.reasoning" />
@@ -1004,5 +1030,72 @@
   <node concept="IW6AY" id="2DPo4JTQI2h">
     <ref role="aqKnT" to="jfgh:4LBPYGV4cY1" resolve="Sentence" />
   </node>
+  <node concept="PKFIW" id="4h0MmDW7E1r">
+    <property role="3GE5qa" value="proof.reasoning" />
+    <property role="TrG5h" value="Premise_DOC" />
+    <ref role="1XX52x" to="jfgh:$u9BK__JRe" resolve="Premise" />
+    <node concept="3EZMnI" id="4h0MmDW7E1t" role="2wV5jI">
+      <node concept="3F0ifn" id="4h0MmDW7E1$" role="3EZMnx">
+        <property role="3F0ifm" value="Premise" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW7IEj" role="3EZMnx" />
+      <node concept="3F0ifn" id="4h0MmDW7E1B" role="3EZMnx">
+        <property role="3F0ifm" value="A sentence that serves as an input to the proof. Must be on top level. Doesn't require a proof." />
+        <node concept="Vb9p2" id="4h0MmDW7IEh" role="3F10Kt" />
+      </node>
+      <node concept="2iRkQZ" id="4h0MmDW7E1w" role="2iSdaV" />
+    </node>
+  </node>
+  <node concept="PKFIW" id="4h0MmDW7Nk2">
+    <property role="3GE5qa" value="proof.reasoning" />
+    <property role="TrG5h" value="Assumption_DOC" />
+    <ref role="1XX52x" to="jfgh:3JXBM6C3Pwi" resolve="Assumption" />
+    <node concept="3EZMnI" id="4h0MmDW7Nk4" role="2wV5jI">
+      <node concept="3F0ifn" id="4h0MmDW7Nkb" role="3EZMnx">
+        <property role="3F0ifm" value="Assumption" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW7Nke" role="3EZMnx" />
+      <node concept="3F0ifn" id="4h0MmDW7Nkh" role="3EZMnx">
+        <property role="3F0ifm" value="Introduce assumption. Starts a new subproof. " />
+        <node concept="Vb9p2" id="4h0MmDW7Nkl" role="3F10Kt" />
+      </node>
+      <node concept="2iRkQZ" id="4h0MmDW7Nk7" role="2iSdaV" />
+    </node>
+  </node>
+  <node concept="PKFIW" id="4h0MmDW7NkU">
+    <property role="3GE5qa" value="proof.reasoning" />
+    <property role="TrG5h" value="Judgement_DOC" />
+    <ref role="1XX52x" to="jfgh:3JXBM6C3FsA" resolve="Judgement" />
+    <node concept="3EZMnI" id="4h0MmDW7NkW" role="2wV5jI">
+      <node concept="3F0ifn" id="4h0MmDW7Nl3" role="3EZMnx">
+        <property role="3F0ifm" value="Judgement" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW7Nl6" role="3EZMnx" />
+      <node concept="3F0ifn" id="4h0MmDW7Nl9" role="3EZMnx">
+        <property role="3F0ifm" value="Judgement is an act of making a conclusion." />
+        <node concept="Vb9p2" id="4h0MmDW7Nld" role="3F10Kt" />
+      </node>
+      <node concept="2iRkQZ" id="4h0MmDW7NkZ" role="2iSdaV" />
+    </node>
+  </node>
+  <node concept="PKFIW" id="4h0MmDW8$kN">
+    <property role="3GE5qa" value="proof.reasoning" />
+    <property role="TrG5h" value="Reiteration_DOC" />
+    <ref role="1XX52x" to="jfgh:5jVx7S1Yau5" resolve="Reiteration" />
+    <node concept="3EZMnI" id="4h0MmDW8$kR" role="2wV5jI">
+      <node concept="3F0ifn" id="4h0MmDW8$kY" role="3EZMnx">
+        <property role="3F0ifm" value="Reiteration" />
+      </node>
+      <node concept="3F0ifn" id="4h0MmDW8$l1" role="3EZMnx" />
+      <node concept="3F0ifn" id="4h0MmDW8$l4" role="3EZMnx">
+        <property role="3F0ifm" value="Allows to reuse a previous assumption or a premise." />
+        <node concept="Vb9p2" id="4h0MmDW8z3H" role="3F10Kt" />
+      </node>
+      <node concept="2iRkQZ" id="4h0MmDW8$kU" role="2iSdaV" />
+    </node>
+    <node concept="1PE4EZ" id="4h0MmDW8$kP" role="1PM95z">
+      <ref role="1PE7su" node="4h0MmDW7NkU" resolve="Judgement_DOC" />
+    </node>
+  </node>
 </model>