Refactor out abstract proof, provide a mechanism to filter passing rules by the proof kind.
This commit is contained in:
Fedor Isakov
parent
5a550836b6
commit
848df81dd4
|
|
@ -33,17 +33,20 @@
|
|||
<concept id="1137021947720" name="jetbrains.mps.baseLanguage.structure.ConceptFunction" flags="in" index="2VMwT0">
|
||||
<child id="1137022507850" name="body" index="2VODD2" />
|
||||
</concept>
|
||||
<concept id="1070534644030" name="jetbrains.mps.baseLanguage.structure.BooleanType" flags="in" index="10P_77" />
|
||||
<concept id="1068431474542" name="jetbrains.mps.baseLanguage.structure.VariableDeclaration" flags="ng" index="33uBYm">
|
||||
<child id="1068431790190" name="initializer" index="33vP2m" />
|
||||
</concept>
|
||||
<concept id="1068498886296" name="jetbrains.mps.baseLanguage.structure.VariableReference" flags="nn" index="37vLTw">
|
||||
<reference id="1068581517664" name="variableDeclaration" index="3cqZAo" />
|
||||
</concept>
|
||||
<concept id="1068498886292" name="jetbrains.mps.baseLanguage.structure.ParameterDeclaration" flags="ir" index="37vLTG" />
|
||||
<concept id="4972933694980447171" name="jetbrains.mps.baseLanguage.structure.BaseVariableDeclaration" flags="ng" index="19Szcq">
|
||||
<child id="5680397130376446158" name="type" index="1tU5fm" />
|
||||
</concept>
|
||||
<concept id="1068580123132" name="jetbrains.mps.baseLanguage.structure.BaseMethodDeclaration" flags="ng" index="3clF44">
|
||||
<child id="1068580123133" name="returnType" index="3clF45" />
|
||||
<child id="1068580123134" name="parameter" index="3clF46" />
|
||||
<child id="1068580123135" name="body" index="3clF47" />
|
||||
</concept>
|
||||
<concept id="1068580123155" name="jetbrains.mps.baseLanguage.structure.ExpressionStatement" flags="nn" index="3clFbF">
|
||||
|
|
@ -82,6 +85,7 @@
|
|||
<child id="1145567471833" name="createdType" index="2T96Bj" />
|
||||
</concept>
|
||||
<concept id="1145572800087" name="jetbrains.mps.lang.smodel.structure.Node_GetPrevSiblingsOperation" flags="nn" index="2Ttrtt" />
|
||||
<concept id="6677504323281689838" name="jetbrains.mps.lang.smodel.structure.SConceptType" flags="in" index="3bZ5Sz" />
|
||||
<concept id="1139613262185" name="jetbrains.mps.lang.smodel.structure.Node_GetParentOperation" flags="nn" index="1mfA1w" />
|
||||
<concept id="1139621453865" name="jetbrains.mps.lang.smodel.structure.Node_IsInstanceOfOperation" flags="nn" index="1mIQ4w">
|
||||
<child id="1177027386292" name="conceptArgument" index="cj9EA" />
|
||||
|
|
@ -189,5 +193,24 @@
|
|||
<node concept="3clFbS" id="5jVx7S20nJs" role="2VODD2" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="13h7C7" id="3w0n0hzjKLx">
|
||||
<property role="3GE5qa" value="proof" />
|
||||
<ref role="13h7C2" to="jfgh:3JXBM6C5urr" resolve="Root" />
|
||||
<node concept="13i0hz" id="3w0n0hzjKLG" role="13h7CS">
|
||||
<property role="13i0iv" value="true" />
|
||||
<property role="13i0it" value="true" />
|
||||
<property role="TrG5h" value="isRuleSupported" />
|
||||
<node concept="37vLTG" id="3w0n0hzjKN7" role="3clF46">
|
||||
<property role="TrG5h" value="ruleConcept" />
|
||||
<node concept="3bZ5Sz" id="3w0n0hzjKO0" role="1tU5fm" />
|
||||
</node>
|
||||
<node concept="3Tm1VV" id="3w0n0hzjKLH" role="1B3o_S" />
|
||||
<node concept="10P_77" id="3w0n0hzjKLW" role="3clF45" />
|
||||
<node concept="3clFbS" id="3w0n0hzjKLJ" role="3clF47" />
|
||||
</node>
|
||||
<node concept="13hLZK" id="3w0n0hzjKLy" role="13h7CW">
|
||||
<node concept="3clFbS" id="3w0n0hzjKLz" role="2VODD2" />
|
||||
</node>
|
||||
</node>
|
||||
</model>
|
||||
|
||||
|
|
|
|||
|
|
@ -344,59 +344,6 @@
|
|||
</node>
|
||||
</node>
|
||||
</node>
|
||||
<node concept="1M2fIO" id="3JXBM6C4VbD">
|
||||
<property role="3GE5qa" value="proof" />
|
||||
<ref role="1M2myG" to="jfgh:3JXBM6C3Fs$" resolve="Proof" />
|
||||
<node concept="EnEH3" id="3JXBM6C4VbE" role="1MhHOB">
|
||||
<ref role="EomxK" to="jfgh:3JXBM6C4nuA" resolve="contentSize" />
|
||||
<node concept="Eqf_E" id="3JXBM6C4VbG" role="EtsB7">
|
||||
<node concept="3clFbS" id="3JXBM6C4VbH" role="2VODD2">
|
||||
<node concept="3clFbF" id="3JXBM6C4VsJ" role="3cqZAp">
|
||||
<node concept="2OqwBi" id="3JXBM6C4VsQ" role="3clFbG">
|
||||
<node concept="2OqwBi" id="3JXBM6C4VsR" role="2Oq$k0">
|
||||
<node concept="EsrRn" id="3JXBM6C4VsS" role="2Oq$k0" />
|
||||
<node concept="3Tsc0h" id="3JXBM6C4VsT" role="2OqNvi">
|
||||
<ref role="3TtcxE" to="jfgh:3JXBM6C4wQA" resolve="content" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="1MD8d$" id="3JXBM6C4VsU" role="2OqNvi">
|
||||
<node concept="1bVj0M" id="3JXBM6C4VsV" role="23t8la">
|
||||
<node concept="3clFbS" id="3JXBM6C4VsW" role="1bW5cS">
|
||||
<node concept="3clFbF" id="3JXBM6C4VsX" role="3cqZAp">
|
||||
<node concept="3cpWs3" id="3JXBM6C4VsY" role="3clFbG">
|
||||
<node concept="2OqwBi" id="3JXBM6C4VsZ" role="3uHU7w">
|
||||
<node concept="37vLTw" id="3JXBM6C4Vt0" role="2Oq$k0">
|
||||
<ref role="3cqZAo" node="3JXBM6C4Vt5" resolve="it" />
|
||||
</node>
|
||||
<node concept="3TrcHB" id="3JXBM6C4Vt1" role="2OqNvi">
|
||||
<ref role="3TsBF5" to="jfgh:3JXBM6C4nuA" resolve="contentSize" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="37vLTw" id="3JXBM6C4Vt2" role="3uHU7B">
|
||||
<ref role="3cqZAo" node="3JXBM6C4Vt3" resolve="s" />
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
<node concept="37vLTG" id="3JXBM6C4Vt3" role="1bW2Oz">
|
||||
<property role="TrG5h" value="s" />
|
||||
<node concept="10Oyi0" id="3JXBM6C4Vt4" role="1tU5fm" />
|
||||
</node>
|
||||
<node concept="Rh6nW" id="3JXBM6C4Vt5" role="1bW2Oz">
|
||||
<property role="TrG5h" value="it" />
|
||||
<node concept="2jxLKc" id="3JXBM6C4Vt6" role="1tU5fm" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="3cmrfG" id="3JXBM6C4Vt7" role="1MDeny">
|
||||
<property role="3cmrfH" value="0" />
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
<node concept="1M2fIO" id="5jVx7S22QGW">
|
||||
<property role="3GE5qa" value="proof.reasoning" />
|
||||
<ref role="1M2myG" to="jfgh:3JXBM6C3Pwi" resolve="Assumption" />
|
||||
|
|
@ -501,5 +448,58 @@
|
|||
</node>
|
||||
</node>
|
||||
</node>
|
||||
<node concept="1M2fIO" id="3w0n0hzhUPi">
|
||||
<property role="3GE5qa" value="proof" />
|
||||
<ref role="1M2myG" to="jfgh:3w0n0hzgWvH" resolve="AbstractProof" />
|
||||
<node concept="EnEH3" id="3JXBM6C4VbE" role="1MhHOB">
|
||||
<ref role="EomxK" to="jfgh:3JXBM6C4nuA" resolve="contentSize" />
|
||||
<node concept="Eqf_E" id="3JXBM6C4VbG" role="EtsB7">
|
||||
<node concept="3clFbS" id="3JXBM6C4VbH" role="2VODD2">
|
||||
<node concept="3clFbF" id="3JXBM6C4VsJ" role="3cqZAp">
|
||||
<node concept="2OqwBi" id="3JXBM6C4VsQ" role="3clFbG">
|
||||
<node concept="2OqwBi" id="3JXBM6C4VsR" role="2Oq$k0">
|
||||
<node concept="EsrRn" id="3JXBM6C4VsS" role="2Oq$k0" />
|
||||
<node concept="3Tsc0h" id="3JXBM6C4VsT" role="2OqNvi">
|
||||
<ref role="3TtcxE" to="jfgh:3JXBM6C4wQA" resolve="content" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="1MD8d$" id="3JXBM6C4VsU" role="2OqNvi">
|
||||
<node concept="1bVj0M" id="3JXBM6C4VsV" role="23t8la">
|
||||
<node concept="3clFbS" id="3JXBM6C4VsW" role="1bW5cS">
|
||||
<node concept="3clFbF" id="3JXBM6C4VsX" role="3cqZAp">
|
||||
<node concept="3cpWs3" id="3JXBM6C4VsY" role="3clFbG">
|
||||
<node concept="2OqwBi" id="3JXBM6C4VsZ" role="3uHU7w">
|
||||
<node concept="37vLTw" id="3JXBM6C4Vt0" role="2Oq$k0">
|
||||
<ref role="3cqZAo" node="3JXBM6C4Vt5" resolve="it" />
|
||||
</node>
|
||||
<node concept="3TrcHB" id="3JXBM6C4Vt1" role="2OqNvi">
|
||||
<ref role="3TsBF5" to="jfgh:3JXBM6C4nuA" resolve="contentSize" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="37vLTw" id="3JXBM6C4Vt2" role="3uHU7B">
|
||||
<ref role="3cqZAo" node="3JXBM6C4Vt3" resolve="s" />
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
<node concept="37vLTG" id="3JXBM6C4Vt3" role="1bW2Oz">
|
||||
<property role="TrG5h" value="s" />
|
||||
<node concept="10Oyi0" id="3JXBM6C4Vt4" role="1tU5fm" />
|
||||
</node>
|
||||
<node concept="Rh6nW" id="3JXBM6C4Vt5" role="1bW2Oz">
|
||||
<property role="TrG5h" value="it" />
|
||||
<node concept="2jxLKc" id="3JXBM6C4Vt6" role="1tU5fm" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="3cmrfG" id="3JXBM6C4Vt7" role="1MDeny">
|
||||
<property role="3cmrfH" value="0" />
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
</model>
|
||||
|
||||
|
|
|
|||
|
|
@ -10,7 +10,6 @@
|
|||
<imports>
|
||||
<import index="jfgh" ref="r:2003997c-f9a6-418f-99d4-03e1285a3e13(jetbrains.mps.fitch.structure)" />
|
||||
<import index="wyt6" ref="6354ebe7-c22a-4a0f-ac54-50b52ab9b065/java:java.lang(JDK/)" implicit="true" />
|
||||
<import index="tpck" ref="r:00000000-0000-4000-0000-011c89590288(jetbrains.mps.lang.core.structure)" implicit="true" />
|
||||
<import index="tpco" ref="r:00000000-0000-4000-0000-011c89590284(jetbrains.mps.lang.core.editor)" implicit="true" />
|
||||
<import index="qd7f" ref="r:6e0181fc-40ea-4aea-a8b0-3ba2d104ddef(jetbrains.mps.fitch.behavior)" implicit="true" />
|
||||
</imports>
|
||||
|
|
@ -34,8 +33,6 @@
|
|||
<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="1106270549637" name="jetbrains.mps.lang.editor.structure.CellLayout_Horizontal" flags="nn" index="2iRfu4" />
|
||||
<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" />
|
||||
|
|
@ -99,7 +96,6 @@
|
|||
<concept id="1219226236603" name="jetbrains.mps.lang.editor.structure.DrawBracketsStyleClassItem" flags="ln" index="3vyZuw" />
|
||||
<concept id="5425882385312046132" name="jetbrains.mps.lang.editor.structure.QueryFunctionParameter_SubstituteMenu_CurrentTargetNode" flags="nn" index="1yR$tW" />
|
||||
<concept id="1139848536355" name="jetbrains.mps.lang.editor.structure.CellModel_WithRole" flags="ng" index="1$h60E">
|
||||
<property id="1139852716018" name="noTargetText" index="1$x2rV" />
|
||||
<reference id="1140103550593" name="relationDeclaration" index="1NtTu8" />
|
||||
</concept>
|
||||
<concept id="7667708318090725848" name="jetbrains.mps.lang.editor.structure.IndentLayoutIndentAnchorStyleClassItem" flags="ln" index="1Bsynf" />
|
||||
|
|
@ -114,7 +110,6 @@
|
|||
<property id="1082639509531" name="nullText" index="ilYzB" />
|
||||
<property id="1073389577007" name="text" index="3F0ifm" />
|
||||
</concept>
|
||||
<concept id="1073389658414" name="jetbrains.mps.lang.editor.structure.CellModel_Property" flags="sg" stub="730538219796134133" index="3F0A7n" />
|
||||
<concept id="1219418625346" name="jetbrains.mps.lang.editor.structure.IStyleContainer" flags="ng" index="3F0Thp">
|
||||
<child id="1219418656006" name="styleItem" index="3F10Kt" />
|
||||
</concept>
|
||||
|
|
@ -380,148 +375,6 @@
|
|||
</node>
|
||||
</node>
|
||||
</node>
|
||||
<node concept="24kQdi" id="3JXBM6C3URg">
|
||||
<property role="3GE5qa" value="proof" />
|
||||
<ref role="1XX52x" to="jfgh:3JXBM6C3Fs$" resolve="Proof" />
|
||||
<node concept="3EZMnI" id="3JXBM6C3URi" role="2wV5jI">
|
||||
<node concept="3F0A7n" id="3JXBM6C4h$I" role="3EZMnx">
|
||||
<ref role="1NtTu8" to="tpck:h0TrG11" resolve="name" />
|
||||
<node concept="ljvvj" id="3JXBM6C4h$R" role="3F10Kt">
|
||||
<property role="VOm3f" value="true" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="3F0ifn" id="2AfSc6Jvjpp" role="3EZMnx">
|
||||
<property role="3F0ifm" value="" />
|
||||
<node concept="ljvvj" id="2AfSc6Jvjpq" role="3F10Kt">
|
||||
<property role="VOm3f" value="true" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="3F0A7n" id="2AfSc6Jvjoy" role="3EZMnx">
|
||||
<ref role="1NtTu8" to="jfgh:2AfSc6Jvjow" resolve="description" />
|
||||
<node concept="ljvvj" id="2AfSc6Jvjs0" role="3F10Kt">
|
||||
<property role="VOm3f" value="true" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="3F0ifn" id="$u9BK__SIy" role="3EZMnx">
|
||||
<property role="3F0ifm" value="" />
|
||||
<node concept="ljvvj" id="$u9BK__SJr" role="3F10Kt">
|
||||
<property role="VOm3f" value="true" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="3EZMnI" id="$u9BK__SDZ" role="3EZMnx">
|
||||
<node concept="ljvvj" id="$u9BK__SHA" role="3F10Kt">
|
||||
<property role="VOm3f" value="true" />
|
||||
</node>
|
||||
<node concept="VPM3Z" id="$u9BK__SE1" role="3F10Kt">
|
||||
<property role="VOm3f" value="false" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="$u9BK__SFC" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Goal:" />
|
||||
</node>
|
||||
<node concept="l2Vlx" id="$u9BK__SE4" role="2iSdaV" />
|
||||
<node concept="3F1sOY" id="$u9BK__SCz" role="3EZMnx">
|
||||
<property role="1$x2rV" value="<no goal>" />
|
||||
<ref role="1NtTu8" to="jfgh:$u9BK__SAr" resolve="goal" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="3EZMnI" id="$u9BK__SGu" role="3EZMnx">
|
||||
<node concept="VPM3Z" id="$u9BK__SGw" role="3F10Kt">
|
||||
<property role="VOm3f" value="false" />
|
||||
</node>
|
||||
<node concept="ljvvj" id="$u9BK__SHv" role="3F10Kt">
|
||||
<property role="VOm3f" value="true" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="$u9BK__SHp" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Proof:" />
|
||||
</node>
|
||||
<node concept="l2Vlx" id="$u9BK__SGz" role="2iSdaV" />
|
||||
</node>
|
||||
<node concept="3EZMnI" id="$u9BK_yCN6" role="3EZMnx">
|
||||
<node concept="3EZMnI" id="$u9BK_z1QP" role="3EZMnx">
|
||||
<node concept="VPM3Z" id="$u9BK_z1QR" role="3F10Kt">
|
||||
<property role="VOm3f" value="false" />
|
||||
</node>
|
||||
<node concept="2iRkQZ" id="$u9BK_z1QU" role="2iSdaV" />
|
||||
<node concept="3EZMnI" id="$u9BK_z6et" role="3EZMnx">
|
||||
<node concept="l2Vlx" id="$u9BK_z6eu" role="2iSdaV" />
|
||||
<node concept="VPM3Z" id="$u9BK_z6ev" role="3F10Kt">
|
||||
<property role="VOm3f" value="false" />
|
||||
</node>
|
||||
<node concept="3F2HdR" id="$u9BK_z6ez" role="3EZMnx">
|
||||
<property role="2czwfO" value=" " />
|
||||
<ref role="1NtTu8" to="jfgh:3JXBM6C4wQA" resolve="content" />
|
||||
<node concept="l2Vlx" id="$u9BK_z6e$" role="2czzBx" />
|
||||
<node concept="tppnM" id="$u9BK_zt0T" role="sWeuL">
|
||||
<node concept="ljvvj" id="$u9BK_zt0V" role="3F10Kt">
|
||||
<property role="VOm3f" value="true" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="2w$q5c" id="5RfK0kxj3Yz" role="78xua">
|
||||
<node concept="2aJ2om" id="5RfK0kxj3Y$" role="2w$qW5">
|
||||
<ref role="2$4xQ3" node="$u9BK_z27v" resolve="ID" />
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
<node concept="3EZMnI" id="$u9BK_yCN7" role="3EZMnx">
|
||||
<node concept="VPM3Z" id="$u9BK_yCN8" role="3F10Kt">
|
||||
<property role="VOm3f" value="false" />
|
||||
</node>
|
||||
<node concept="2iRkQZ" id="$u9BK_yCNa" role="2iSdaV" />
|
||||
<node concept="3EZMnI" id="3JXBM6C6j0E" role="3EZMnx">
|
||||
<node concept="VPM3Z" id="3JXBM6C6j0G" role="3F10Kt">
|
||||
<property role="VOm3f" value="false" />
|
||||
</node>
|
||||
<node concept="l2Vlx" id="3JXBM6C6j0J" role="2iSdaV" />
|
||||
<node concept="3F2HdR" id="3JXBM6C3URp" role="3EZMnx">
|
||||
<property role="2czwfO" value=" " />
|
||||
<ref role="1NtTu8" to="jfgh:3JXBM6C4wQA" resolve="content" />
|
||||
<node concept="l2Vlx" id="3JXBM6C3URr" role="2czzBx" />
|
||||
<node concept="tppnM" id="3JXBM6C3URw" role="sWeuL">
|
||||
<node concept="ljvvj" id="3JXBM6C3URy" role="3F10Kt">
|
||||
<property role="VOm3f" value="true" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="3F0ifn" id="3JXBM6C3UR$" role="2czzBI">
|
||||
<property role="3F0ifm" value="" />
|
||||
<property role="ilYzB" value="<no steps>" />
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
<node concept="2iRfu4" id="$u9BK_yCNb" role="2iSdaV" />
|
||||
<node concept="3EZMnI" id="$u9BK_zG5o" role="3EZMnx">
|
||||
<node concept="3EZMnI" id="$u9BK_$Qxk" role="3EZMnx">
|
||||
<node concept="l2Vlx" id="$u9BK_$Qxl" role="2iSdaV" />
|
||||
<node concept="VPM3Z" id="$u9BK_$Qxm" role="3F10Kt">
|
||||
<property role="VOm3f" value="false" />
|
||||
</node>
|
||||
<node concept="3F2HdR" id="$u9BK_$Qxn" role="3EZMnx">
|
||||
<property role="2czwfO" value=" " />
|
||||
<ref role="1NtTu8" to="jfgh:3JXBM6C4wQA" resolve="content" />
|
||||
<node concept="l2Vlx" id="$u9BK_$Qxo" role="2czzBx" />
|
||||
<node concept="tppnM" id="$u9BK_$Qxp" role="sWeuL">
|
||||
<node concept="ljvvj" id="$u9BK_$Qxq" role="3F10Kt">
|
||||
<property role="VOm3f" value="true" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="2w$q5c" id="$u9BK_$QxA" role="78xua">
|
||||
<node concept="2aJ2om" id="$u9BK_$QxB" role="2w$qW5">
|
||||
<ref role="2$4xQ3" node="$u9BK_zG6f" resolve="BASIS" />
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
<node concept="VPM3Z" id="$u9BK_zG5q" role="3F10Kt">
|
||||
<property role="VOm3f" value="false" />
|
||||
</node>
|
||||
<node concept="2iRkQZ" id="$u9BK_zG5t" role="2iSdaV" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="l2Vlx" id="3JXBM6C3URl" role="2iSdaV" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="3p36aQ" id="3JXBM6C6A54">
|
||||
<property role="3GE5qa" value="proof.reasoning" />
|
||||
<ref role="aqKnT" to="jfgh:3JXBM6C3FsN" resolve="Reference" />
|
||||
|
|
@ -575,10 +428,6 @@
|
|||
</node>
|
||||
</node>
|
||||
</node>
|
||||
<node concept="3p36aQ" id="3JXBM6C6F7z">
|
||||
<property role="3GE5qa" value="proof" />
|
||||
<ref role="aqKnT" to="jfgh:3JXBM6C3Fs$" resolve="Proof" />
|
||||
</node>
|
||||
<node concept="3p36aQ" id="3JXBM6C6Hgb">
|
||||
<property role="3GE5qa" value="proof" />
|
||||
<ref role="aqKnT" to="jfgh:3JXBM6C3UQ$" resolve="SubProof" />
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@
|
|||
<devkit ref="78434eb8-b0e5-444b-850d-e7c4ad2da9ab(jetbrains.mps.devkit.aspect.structure)" />
|
||||
</languages>
|
||||
<imports>
|
||||
<import index="tpck" ref="r:00000000-0000-4000-0000-011c89590288(jetbrains.mps.lang.core.structure)" implicit="true" />
|
||||
<import index="tpck" ref="r:00000000-0000-4000-0000-011c89590288(jetbrains.mps.lang.core.structure)" />
|
||||
</imports>
|
||||
<registry>
|
||||
<language id="c72da2b9-7cce-4447-8389-f407dc1158b7" name="jetbrains.mps.lang.structure">
|
||||
|
|
@ -26,7 +26,6 @@
|
|||
<reference id="1169127628841" name="intfc" index="PrY4T" />
|
||||
</concept>
|
||||
<concept id="1071489090640" name="jetbrains.mps.lang.structure.structure.ConceptDeclaration" flags="ig" index="1TIwiD">
|
||||
<property id="1096454100552" name="rootable" index="19KtqR" />
|
||||
<reference id="1071489389519" name="extends" index="1TJDcQ" />
|
||||
<child id="1169129564478" name="implements" index="PzmwI" />
|
||||
</concept>
|
||||
|
|
@ -51,38 +50,6 @@
|
|||
</concept>
|
||||
</language>
|
||||
</registry>
|
||||
<node concept="1TIwiD" id="3JXBM6C3Fs$">
|
||||
<property role="EcuMT" value="4322786184247818020" />
|
||||
<property role="TrG5h" value="Proof" />
|
||||
<property role="19KtqR" value="true" />
|
||||
<property role="34LRSv" value="proof" />
|
||||
<property role="3GE5qa" value="proof" />
|
||||
<ref role="1TJDcQ" to="tpck:gw2VY9q" resolve="BaseConcept" />
|
||||
<node concept="1TJgyi" id="2AfSc6Jvjow" role="1TKVEl">
|
||||
<property role="IQ2nx" value="2994859399702197792" />
|
||||
<property role="TrG5h" value="description" />
|
||||
<ref role="AX2Wp" to="tpck:fKAOsGN" resolve="string" />
|
||||
</node>
|
||||
<node concept="1TJgyj" id="$u9BK__SAr" role="1TKVEi">
|
||||
<property role="IQ2ns" value="657004910291159451" />
|
||||
<property role="20lmBu" value="aggregation" />
|
||||
<property role="20kJfa" value="goal" />
|
||||
<ref role="20lvS9" node="$u9BK__SA8" resolve="Goal" />
|
||||
</node>
|
||||
<node concept="1TJgyj" id="3JXBM6C4wQA" role="1TKVEi">
|
||||
<property role="IQ2ns" value="4322786184248036774" />
|
||||
<property role="20lmBu" value="aggregation" />
|
||||
<property role="20kJfa" value="content" />
|
||||
<property role="20lbJX" value="1..n" />
|
||||
<ref role="20lvS9" node="3JXBM6C3UQB" resolve="Node" />
|
||||
</node>
|
||||
<node concept="PrWs8" id="3JXBM6C3URC" role="PzmwI">
|
||||
<ref role="PrY4T" to="tpck:h0TrEE$" resolve="INamedConcept" />
|
||||
</node>
|
||||
<node concept="PrWs8" id="3JXBM6C5v8v" role="PzmwI">
|
||||
<ref role="PrY4T" node="3JXBM6C5urr" resolve="Root" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="1TIwiD" id="3JXBM6C3FsA">
|
||||
<property role="EcuMT" value="4322786184247818022" />
|
||||
<property role="TrG5h" value="Judgement" />
|
||||
|
|
@ -182,7 +149,7 @@
|
|||
</node>
|
||||
<node concept="PlHQZ" id="3JXBM6C5urr">
|
||||
<property role="EcuMT" value="4322786184248288987" />
|
||||
<property role="3GE5qa" value="proof.rule" />
|
||||
<property role="3GE5qa" value="proof" />
|
||||
<property role="TrG5h" value="Root" />
|
||||
<node concept="PrWs8" id="3JXBM6C5urs" role="PrDN$">
|
||||
<ref role="PrY4T" node="3JXBM6C3UQB" resolve="Node" />
|
||||
|
|
@ -229,5 +196,37 @@
|
|||
<property role="EcuMT" value="5505606474791964545" />
|
||||
<property role="TrG5h" value="Sentence" />
|
||||
</node>
|
||||
<node concept="1TIwiD" id="3w0n0hzgWvH">
|
||||
<property role="EcuMT" value="4035326440038975469" />
|
||||
<property role="3GE5qa" value="proof" />
|
||||
<property role="TrG5h" value="AbstractProof" />
|
||||
<property role="R5$K7" value="true" />
|
||||
<property role="R5$K2" value="false" />
|
||||
<ref role="1TJDcQ" to="tpck:gw2VY9q" resolve="BaseConcept" />
|
||||
<node concept="PrWs8" id="3w0n0hzgWvI" role="PzmwI">
|
||||
<ref role="PrY4T" to="tpck:h0TrEE$" resolve="INamedConcept" />
|
||||
</node>
|
||||
<node concept="1TJgyi" id="2AfSc6Jvjow" role="1TKVEl">
|
||||
<property role="IQ2nx" value="2994859399702197792" />
|
||||
<property role="TrG5h" value="description" />
|
||||
<ref role="AX2Wp" to="tpck:fKAOsGN" resolve="string" />
|
||||
</node>
|
||||
<node concept="1TJgyj" id="$u9BK__SAr" role="1TKVEi">
|
||||
<property role="IQ2ns" value="657004910291159451" />
|
||||
<property role="20lmBu" value="aggregation" />
|
||||
<property role="20kJfa" value="goal" />
|
||||
<ref role="20lvS9" node="$u9BK__SA8" resolve="Goal" />
|
||||
</node>
|
||||
<node concept="1TJgyj" id="3JXBM6C4wQA" role="1TKVEi">
|
||||
<property role="IQ2ns" value="4322786184248036774" />
|
||||
<property role="20lmBu" value="aggregation" />
|
||||
<property role="20kJfa" value="content" />
|
||||
<property role="20lbJX" value="1..n" />
|
||||
<ref role="20lvS9" node="3JXBM6C3UQB" resolve="Node" />
|
||||
</node>
|
||||
<node concept="PrWs8" id="3w0n0hzhVZC" role="PzmwI">
|
||||
<ref role="PrY4T" node="3JXBM6C5urr" resolve="Root" />
|
||||
</node>
|
||||
</node>
|
||||
</model>
|
||||
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load Diff
|
|
@ -5,7 +5,106 @@
|
|||
<use id="af65afd8-f0dd-4942-87d9-63a55f2a9db1" name="jetbrains.mps.lang.behavior" version="1" />
|
||||
<devkit ref="2677cb18-f558-4e33-bc38-a5139cee06dc(jetbrains.mps.devkit.language-design)" />
|
||||
</languages>
|
||||
<imports />
|
||||
<registry />
|
||||
<imports>
|
||||
<import index="qd7f" ref="r:6e0181fc-40ea-4aea-a8b0-3ba2d104ddef(jetbrains.mps.fitch.behavior)" />
|
||||
<import index="27wh" ref="r:459ba7ac-2a61-40fc-bcc4-f13a7956cbeb(jetbrains.mps.logic.propositional.structure)" implicit="true" />
|
||||
</imports>
|
||||
<registry>
|
||||
<language id="af65afd8-f0dd-4942-87d9-63a55f2a9db1" name="jetbrains.mps.lang.behavior">
|
||||
<concept id="1225194240794" name="jetbrains.mps.lang.behavior.structure.ConceptBehavior" flags="ng" index="13h7C7">
|
||||
<reference id="1225194240799" name="concept" index="13h7C2" />
|
||||
<child id="1225194240805" name="method" index="13h7CS" />
|
||||
<child id="1225194240801" name="constructor" index="13h7CW" />
|
||||
</concept>
|
||||
<concept id="1225194413805" name="jetbrains.mps.lang.behavior.structure.ConceptConstructorDeclaration" flags="in" index="13hLZK" />
|
||||
<concept id="1225194472830" name="jetbrains.mps.lang.behavior.structure.ConceptMethodDeclaration" flags="ng" index="13i0hz">
|
||||
<property id="1225194472832" name="isVirtual" index="13i0it" />
|
||||
<property id="1225194472834" name="isAbstract" index="13i0iv" />
|
||||
<reference id="1225194472831" name="overriddenMethod" index="13i0hy" />
|
||||
</concept>
|
||||
</language>
|
||||
<language id="f3061a53-9226-4cc5-a443-f952ceaf5816" name="jetbrains.mps.baseLanguage">
|
||||
<concept id="1197027756228" name="jetbrains.mps.baseLanguage.structure.DotExpression" flags="nn" index="2OqwBi">
|
||||
<child id="1197027771414" name="operand" index="2Oq$k0" />
|
||||
<child id="1197027833540" name="operation" index="2OqNvi" />
|
||||
</concept>
|
||||
<concept id="1137021947720" name="jetbrains.mps.baseLanguage.structure.ConceptFunction" flags="in" index="2VMwT0">
|
||||
<child id="1137022507850" name="body" index="2VODD2" />
|
||||
</concept>
|
||||
<concept id="1070534644030" name="jetbrains.mps.baseLanguage.structure.BooleanType" flags="in" index="10P_77" />
|
||||
<concept id="1068498886296" name="jetbrains.mps.baseLanguage.structure.VariableReference" flags="nn" index="37vLTw">
|
||||
<reference id="1068581517664" name="variableDeclaration" index="3cqZAo" />
|
||||
</concept>
|
||||
<concept id="1068498886292" name="jetbrains.mps.baseLanguage.structure.ParameterDeclaration" flags="ir" index="37vLTG" />
|
||||
<concept id="4972933694980447171" name="jetbrains.mps.baseLanguage.structure.BaseVariableDeclaration" flags="ng" index="19Szcq">
|
||||
<child id="5680397130376446158" name="type" index="1tU5fm" />
|
||||
</concept>
|
||||
<concept id="1068580123132" name="jetbrains.mps.baseLanguage.structure.BaseMethodDeclaration" flags="ng" index="3clF44">
|
||||
<child id="1068580123133" name="returnType" index="3clF45" />
|
||||
<child id="1068580123134" name="parameter" index="3clF46" />
|
||||
<child id="1068580123135" name="body" index="3clF47" />
|
||||
</concept>
|
||||
<concept id="1068580123155" name="jetbrains.mps.baseLanguage.structure.ExpressionStatement" flags="nn" index="3clFbF">
|
||||
<child id="1068580123156" name="expression" index="3clFbG" />
|
||||
</concept>
|
||||
<concept id="1068580123136" name="jetbrains.mps.baseLanguage.structure.StatementList" flags="sn" stub="5293379017992965193" index="3clFbS">
|
||||
<child id="1068581517665" name="statement" index="3cqZAp" />
|
||||
</concept>
|
||||
<concept id="1178549954367" name="jetbrains.mps.baseLanguage.structure.IVisible" flags="ng" index="1B3ioH">
|
||||
<child id="1178549979242" name="visibility" index="1B3o_S" />
|
||||
</concept>
|
||||
<concept id="1146644602865" name="jetbrains.mps.baseLanguage.structure.PublicVisibility" flags="nn" index="3Tm1VV" />
|
||||
</language>
|
||||
<language id="7866978e-a0f0-4cc7-81bc-4d213d9375e1" name="jetbrains.mps.lang.smodel">
|
||||
<concept id="1177026924588" name="jetbrains.mps.lang.smodel.structure.RefConcept_Reference" flags="nn" index="chp4Y">
|
||||
<reference id="1177026940964" name="conceptDeclaration" index="cht4Q" />
|
||||
</concept>
|
||||
<concept id="1180031783296" name="jetbrains.mps.lang.smodel.structure.Concept_IsSubConceptOfOperation" flags="nn" index="2Zo12i">
|
||||
<child id="1180031783297" name="conceptArgument" index="2Zo12j" />
|
||||
</concept>
|
||||
<concept id="6677504323281689838" name="jetbrains.mps.lang.smodel.structure.SConceptType" flags="in" index="3bZ5Sz" />
|
||||
</language>
|
||||
<language id="ceab5195-25ea-4f22-9b92-103b95ca8c0c" name="jetbrains.mps.lang.core">
|
||||
<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="13h7C7" id="3w0n0hzjKQg">
|
||||
<property role="3GE5qa" value="proof" />
|
||||
<ref role="13h7C2" to="27wh:3JXBM6C3Fs$" resolve="PropositionalProof" />
|
||||
<node concept="13hLZK" id="3w0n0hzjKQh" role="13h7CW">
|
||||
<node concept="3clFbS" id="3w0n0hzjKQi" role="2VODD2" />
|
||||
</node>
|
||||
<node concept="13i0hz" id="3w0n0hzjKQr" role="13h7CS">
|
||||
<property role="13i0iv" value="false" />
|
||||
<property role="13i0it" value="false" />
|
||||
<property role="TrG5h" value="isRuleSupported" />
|
||||
<ref role="13i0hy" to="qd7f:3w0n0hzjKLG" resolve="isRuleSupported" />
|
||||
<node concept="3Tm1VV" id="3w0n0hzjKQu" role="1B3o_S" />
|
||||
<node concept="3clFbS" id="3w0n0hzjKQx" role="3clF47">
|
||||
<node concept="3clFbF" id="3w0n0hzjKUz" role="3cqZAp">
|
||||
<node concept="2OqwBi" id="3w0n0hzjL4O" role="3clFbG">
|
||||
<node concept="37vLTw" id="3w0n0hzjKUy" role="2Oq$k0">
|
||||
<ref role="3cqZAo" node="3w0n0hzjKQy" resolve="ruleConcept" />
|
||||
</node>
|
||||
<node concept="2Zo12i" id="3w0n0hzjLsE" role="2OqNvi">
|
||||
<node concept="chp4Y" id="3w0n0hzjLys" role="2Zo12j">
|
||||
<ref role="cht4Q" to="27wh:3w0n0hziLcf" resolve="PropositionalRule" />
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
<node concept="37vLTG" id="3w0n0hzjKQy" role="3clF46">
|
||||
<property role="TrG5h" value="ruleConcept" />
|
||||
<node concept="3bZ5Sz" id="3w0n0hzjKQz" role="1tU5fm" />
|
||||
</node>
|
||||
<node concept="10P_77" id="3w0n0hzjKQ$" role="3clF45" />
|
||||
</node>
|
||||
</node>
|
||||
</model>
|
||||
|
||||
|
|
|
|||
|
|
@ -5,18 +5,30 @@
|
|||
<use id="3f4bc5f5-c6c1-4a28-8b10-c83066ffa4a1" name="jetbrains.mps.lang.constraints" version="4" />
|
||||
<use id="f3061a53-9226-4cc5-a443-f952ceaf5816" name="jetbrains.mps.baseLanguage" version="5" />
|
||||
<use id="daafa647-f1f7-4b0b-b096-69cd7c8408c0" name="jetbrains.mps.baseLanguage.regexp" version="0" />
|
||||
<use id="7866978e-a0f0-4cc7-81bc-4d213d9375e1" name="jetbrains.mps.lang.smodel" version="8" />
|
||||
<use id="83888646-71ce-4f1c-9c53-c54016f6ad4f" name="jetbrains.mps.baseLanguage.collections" version="0" />
|
||||
<use id="fd392034-7849-419d-9071-12563d152375" name="jetbrains.mps.baseLanguage.closures" version="0" />
|
||||
<devkit ref="00000000-0000-4000-0000-5604ebd4f22c(jetbrains.mps.devkit.aspect.constraints)" />
|
||||
</languages>
|
||||
<imports>
|
||||
<import index="27wh" ref="r:459ba7ac-2a61-40fc-bcc4-f13a7956cbeb(jetbrains.mps.logic.propositional.structure)" />
|
||||
<import index="tpck" ref="r:00000000-0000-4000-0000-011c89590288(jetbrains.mps.lang.core.structure)" />
|
||||
<import index="tpfp" ref="r:00000000-0000-4000-0000-011c89590519(jetbrains.mps.baseLanguage.regexp.jetbrains.mps.regexp.accessory)" />
|
||||
<import index="jfgh" ref="r:2003997c-f9a6-418f-99d4-03e1285a3e13(jetbrains.mps.fitch.structure)" />
|
||||
<import index="qd7f" ref="r:6e0181fc-40ea-4aea-a8b0-3ba2d104ddef(jetbrains.mps.fitch.behavior)" implicit="true" />
|
||||
</imports>
|
||||
<registry>
|
||||
<language id="f3061a53-9226-4cc5-a443-f952ceaf5816" name="jetbrains.mps.baseLanguage">
|
||||
<concept id="1197027756228" name="jetbrains.mps.baseLanguage.structure.DotExpression" flags="nn" index="2OqwBi">
|
||||
<child id="1197027771414" name="operand" index="2Oq$k0" />
|
||||
<child id="1197027833540" name="operation" index="2OqNvi" />
|
||||
</concept>
|
||||
<concept id="1137021947720" name="jetbrains.mps.baseLanguage.structure.ConceptFunction" flags="in" index="2VMwT0">
|
||||
<child id="1137022507850" name="body" index="2VODD2" />
|
||||
</concept>
|
||||
<concept id="1068580123155" name="jetbrains.mps.baseLanguage.structure.ExpressionStatement" flags="nn" index="3clFbF">
|
||||
<child id="1068580123156" name="expression" index="3clFbG" />
|
||||
</concept>
|
||||
<concept id="1068580123136" name="jetbrains.mps.baseLanguage.structure.StatementList" flags="sn" stub="5293379017992965193" index="3clFbS">
|
||||
<child id="1068581517665" name="statement" index="3cqZAp" />
|
||||
</concept>
|
||||
|
|
@ -26,8 +38,15 @@
|
|||
<concept id="1068581242878" name="jetbrains.mps.baseLanguage.structure.ReturnStatement" flags="nn" index="3cpWs6">
|
||||
<child id="1068581517676" name="expression" index="3cqZAk" />
|
||||
</concept>
|
||||
<concept id="1204053956946" name="jetbrains.mps.baseLanguage.structure.IMethodCall" flags="ng" index="1ndlxa">
|
||||
<reference id="1068499141037" name="baseMethodDeclaration" index="37wK5l" />
|
||||
<child id="1068499141038" name="actualArgument" index="37wK5m" />
|
||||
</concept>
|
||||
</language>
|
||||
<language id="3f4bc5f5-c6c1-4a28-8b10-c83066ffa4a1" name="jetbrains.mps.lang.constraints">
|
||||
<concept id="6702802731807351367" name="jetbrains.mps.lang.constraints.structure.ConstraintFunction_CanBeAChild" flags="in" index="9S07l" />
|
||||
<concept id="1202989658459" name="jetbrains.mps.lang.constraints.structure.ConstraintFunctionParameter_parentNode" flags="nn" index="nLn13" />
|
||||
<concept id="4303308395523096213" name="jetbrains.mps.lang.constraints.structure.ConstraintFunctionParameter_childConcept" flags="ng" index="2DD5aU" />
|
||||
<concept id="1147467115080" name="jetbrains.mps.lang.constraints.structure.NodePropertyConstraint" flags="ng" index="EnEH3">
|
||||
<reference id="1147467295099" name="applicableProperty" index="EomxK" />
|
||||
<child id="1212097481299" name="propertyValidator" index="QCWH9" />
|
||||
|
|
@ -35,10 +54,25 @@
|
|||
<concept id="1212096972063" name="jetbrains.mps.lang.constraints.structure.ConstraintFunction_PropertyValidator" flags="in" index="QB0g5" />
|
||||
<concept id="1213093968558" name="jetbrains.mps.lang.constraints.structure.ConceptConstraints" flags="ng" index="1M2fIO">
|
||||
<reference id="1213093996982" name="concept" index="1M2myG" />
|
||||
<child id="6702802731807737306" name="canBeChild" index="9Vyp8" />
|
||||
<child id="1213098023997" name="property" index="1MhHOB" />
|
||||
</concept>
|
||||
<concept id="1153138554286" name="jetbrains.mps.lang.constraints.structure.ConstraintsFunctionParameter_propertyValue" flags="nn" index="1Wqviy" />
|
||||
</language>
|
||||
<language id="7866978e-a0f0-4cc7-81bc-4d213d9375e1" name="jetbrains.mps.lang.smodel">
|
||||
<concept id="1177026924588" name="jetbrains.mps.lang.smodel.structure.RefConcept_Reference" flags="nn" index="chp4Y">
|
||||
<reference id="1177026940964" name="conceptDeclaration" index="cht4Q" />
|
||||
</concept>
|
||||
<concept id="1138411891628" name="jetbrains.mps.lang.smodel.structure.SNodeOperation" flags="nn" index="eCIE_">
|
||||
<child id="1144104376918" name="parameter" index="1xVPHs" />
|
||||
</concept>
|
||||
<concept id="1179409122411" name="jetbrains.mps.lang.smodel.structure.Node_ConceptMethodCall" flags="nn" index="2qgKlT" />
|
||||
<concept id="1171407110247" name="jetbrains.mps.lang.smodel.structure.Node_GetAncestorOperation" flags="nn" index="2Xjw5R" />
|
||||
<concept id="1144100932627" name="jetbrains.mps.lang.smodel.structure.OperationParm_Inclusion" flags="ng" index="1xIGOp" />
|
||||
<concept id="1144101972840" name="jetbrains.mps.lang.smodel.structure.OperationParm_Concept" flags="ng" index="1xMEDy">
|
||||
<child id="1207343664468" name="conceptArgument" index="ri$Ld" />
|
||||
</concept>
|
||||
</language>
|
||||
<language id="ceab5195-25ea-4f22-9b92-103b95ca8c0c" name="jetbrains.mps.lang.core">
|
||||
<concept id="1133920641626" name="jetbrains.mps.lang.core.structure.BaseConcept" flags="ng" index="2VYdi">
|
||||
<property id="1193676396447" name="virtualPackage" index="3GE5qa" />
|
||||
|
|
@ -97,5 +131,32 @@
|
|||
</node>
|
||||
</node>
|
||||
</node>
|
||||
<node concept="1M2fIO" id="3w0n0hzjH5f">
|
||||
<property role="3GE5qa" value="proof.rule" />
|
||||
<ref role="1M2myG" to="27wh:3w0n0hziLcf" resolve="PropositionalRule" />
|
||||
<node concept="9S07l" id="3w0n0hzjH5g" role="9Vyp8">
|
||||
<node concept="3clFbS" id="3w0n0hzjH5h" role="2VODD2">
|
||||
<node concept="3clFbF" id="3w0n0hzjEJQ" role="3cqZAp">
|
||||
<node concept="2OqwBi" id="3w0n0hzjFH7" role="3clFbG">
|
||||
<node concept="2OqwBi" id="3w0n0hzjEZ0" role="2Oq$k0">
|
||||
<node concept="nLn13" id="3w0n0hzjEJP" role="2Oq$k0" />
|
||||
<node concept="2Xjw5R" id="3w0n0hzjFfL" role="2OqNvi">
|
||||
<node concept="1xMEDy" id="3w0n0hzjSnx" role="1xVPHs">
|
||||
<node concept="chp4Y" id="3w0n0hzjS$2" role="ri$Ld">
|
||||
<ref role="cht4Q" to="jfgh:3JXBM6C5urr" resolve="Root" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="1xIGOp" id="3w0n0hzjSWs" role="1xVPHs" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="2qgKlT" id="3w0n0hzjTgg" role="2OqNvi">
|
||||
<ref role="37wK5l" to="qd7f:3w0n0hzjKLG" resolve="isRuleSupported" />
|
||||
<node concept="2DD5aU" id="3w0n0hzjTDM" role="37wK5m" />
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
</model>
|
||||
|
||||
|
|
|
|||
|
|
@ -14,6 +14,8 @@
|
|||
<import index="tpck" ref="r:00000000-0000-4000-0000-011c89590288(jetbrains.mps.lang.core.structure)" />
|
||||
<import index="tpfp" ref="r:00000000-0000-4000-0000-011c89590519(jetbrains.mps.baseLanguage.regexp.jetbrains.mps.regexp.accessory)" />
|
||||
<import index="jfgh" ref="r:2003997c-f9a6-418f-99d4-03e1285a3e13(jetbrains.mps.fitch.structure)" />
|
||||
<import index="8v9h" ref="r:873e37f0-b045-47b9-ae9e-db79c2628975(jetbrains.mps.fitch.editor)" />
|
||||
<import index="tpco" ref="r:00000000-0000-4000-0000-011c89590284(jetbrains.mps.lang.core.editor)" implicit="true" />
|
||||
</imports>
|
||||
<registry>
|
||||
<language id="18bc6592-03a6-4e29-a83a-7ff23bde13ba" name="jetbrains.mps.lang.editor">
|
||||
|
|
@ -23,6 +25,9 @@
|
|||
</concept>
|
||||
<concept id="1071666914219" name="jetbrains.mps.lang.editor.structure.ConceptEditorDeclaration" flags="ig" index="24kQdi" />
|
||||
<concept id="1597643335227097138" name="jetbrains.mps.lang.editor.structure.QueryFunctionParameter_TransformationMenu_node" flags="ng" index="7Obwk" />
|
||||
<concept id="6822301196700715228" name="jetbrains.mps.lang.editor.structure.ConceptEditorHintDeclarationReference" flags="ig" index="2aJ2om">
|
||||
<reference id="5944657839026714445" name="hint" index="2$4xQ3" />
|
||||
</concept>
|
||||
<concept id="1140524381322" name="jetbrains.mps.lang.editor.structure.CellModel_ListWithRole" flags="ng" index="2czfm3">
|
||||
<property id="1140524450557" name="separatorText" index="2czwfO" />
|
||||
<child id="1140524464360" name="cellLayout" index="2czzBx" />
|
||||
|
|
@ -32,8 +37,11 @@
|
|||
<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="1106270549637" name="jetbrains.mps.lang.editor.structure.CellLayout_Horizontal" flags="nn" index="2iRfu4" />
|
||||
<concept id="1106270571710" name="jetbrains.mps.lang.editor.structure.CellLayout_Vertical" flags="nn" index="2iRkQZ" />
|
||||
<concept id="3459162043708467089" name="jetbrains.mps.lang.editor.structure.CellActionMap_CanExecuteFunction" flags="in" index="jK8Ss" />
|
||||
<concept id="1237303669825" name="jetbrains.mps.lang.editor.structure.CellLayout_Indent" flags="nn" index="l2Vlx" />
|
||||
<concept id="1237308012275" name="jetbrains.mps.lang.editor.structure.IndentLayoutNewLineStyleClassItem" flags="ln" index="ljvvj" />
|
||||
<concept id="1233148810477" name="jetbrains.mps.lang.editor.structure.InlineStyleDeclaration" flags="ng" index="tppnM" />
|
||||
<concept id="1177327274449" name="jetbrains.mps.lang.editor.structure.QueryFunctionParameter_pattern" flags="nn" index="ub8z3" />
|
||||
<concept id="1177327570013" name="jetbrains.mps.lang.editor.structure.QueryFunction_SubstituteMenu_Substitute" flags="in" index="ucgPf" />
|
||||
|
|
@ -41,6 +49,9 @@
|
|||
<child id="8478191136883534238" name="features" index="upBLP" />
|
||||
</concept>
|
||||
<concept id="1177335944525" name="jetbrains.mps.lang.editor.structure.QueryFunction_SubstituteMenu_SubstituteString" flags="in" index="uGdhv" />
|
||||
<concept id="4242538589859161874" name="jetbrains.mps.lang.editor.structure.ExplicitHintsSpecification" flags="ng" index="2w$q5c">
|
||||
<child id="4242538589859162459" name="hints" index="2w$qW5" />
|
||||
</concept>
|
||||
<concept id="1080736578640" name="jetbrains.mps.lang.editor.structure.BaseEditorComponent" flags="ig" index="2wURMF">
|
||||
<child id="1080736633877" name="cellModel" index="2wV5jI" />
|
||||
</concept>
|
||||
|
|
@ -56,6 +67,9 @@
|
|||
<child id="1638911550608610281" name="executeFunction" index="IWgqQ" />
|
||||
<child id="5692353713941573325" name="textFunction" index="1hCUd6" />
|
||||
</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="1186414536763" name="jetbrains.mps.lang.editor.structure.BooleanStyleSheetItem" flags="ln" index="VOi$J">
|
||||
<property id="1186414551515" name="flag" index="VOm3f" />
|
||||
</concept>
|
||||
|
|
@ -90,6 +104,7 @@
|
|||
<concept id="5692353713941573329" name="jetbrains.mps.lang.editor.structure.QueryFunction_TransformationMenu_ActionLabelText" flags="ig" index="1hCUdq" />
|
||||
<concept id="3308396621974580100" name="jetbrains.mps.lang.editor.structure.SubstituteMenu_Default" flags="ng" index="3p36aQ" />
|
||||
<concept id="1139848536355" name="jetbrains.mps.lang.editor.structure.CellModel_WithRole" flags="ng" index="1$h60E">
|
||||
<property id="1139852716018" name="noTargetText" index="1$x2rV" />
|
||||
<reference id="1140103550593" name="relationDeclaration" index="1NtTu8" />
|
||||
</concept>
|
||||
<concept id="1073389214265" name="jetbrains.mps.lang.editor.structure.EditorCellModel" flags="ng" index="3EYTF0">
|
||||
|
|
@ -108,7 +123,9 @@
|
|||
<child id="1219418656006" name="styleItem" index="3F10Kt" />
|
||||
</concept>
|
||||
<concept id="1073389882823" name="jetbrains.mps.lang.editor.structure.CellModel_RefNode" flags="sg" stub="730538219795960754" index="3F1sOY" />
|
||||
<concept id="1073390211982" name="jetbrains.mps.lang.editor.structure.CellModel_RefNodeList" flags="sg" stub="2794558372793454595" index="3F2HdR" />
|
||||
<concept id="1073390211982" name="jetbrains.mps.lang.editor.structure.CellModel_RefNodeList" flags="sg" stub="2794558372793454595" index="3F2HdR">
|
||||
<child id="7279578193766667846" name="addHints" index="78xua" />
|
||||
</concept>
|
||||
<concept id="5624877018228267058" name="jetbrains.mps.lang.editor.structure.ITransformationMenu" flags="ng" index="3INCJE">
|
||||
<child id="1638911550608572412" name="sections" index="IW6Ez" />
|
||||
</concept>
|
||||
|
|
@ -1231,5 +1248,154 @@
|
|||
</node>
|
||||
</node>
|
||||
</node>
|
||||
<node concept="24kQdi" id="3JXBM6C3URg">
|
||||
<property role="3GE5qa" value="proof" />
|
||||
<ref role="1XX52x" to="27wh:3JXBM6C3Fs$" resolve="PropositionalProof" />
|
||||
<node concept="3EZMnI" id="3JXBM6C3URi" role="2wV5jI">
|
||||
<node concept="PMmxH" id="3w0n0hzhNuL" role="3EZMnx">
|
||||
<ref role="PMmxG" to="tpco:2wZex4PafBj" resolve="alias" />
|
||||
</node>
|
||||
<node concept="3F0A7n" id="3JXBM6C4h$I" role="3EZMnx">
|
||||
<ref role="1NtTu8" to="tpck:h0TrG11" resolve="name" />
|
||||
<node concept="ljvvj" id="3JXBM6C4h$R" role="3F10Kt">
|
||||
<property role="VOm3f" value="true" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="3F0ifn" id="2AfSc6Jvjpp" role="3EZMnx">
|
||||
<property role="3F0ifm" value="" />
|
||||
<node concept="ljvvj" id="2AfSc6Jvjpq" role="3F10Kt">
|
||||
<property role="VOm3f" value="true" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="3F0A7n" id="2AfSc6Jvjoy" role="3EZMnx">
|
||||
<ref role="1NtTu8" to="jfgh:2AfSc6Jvjow" resolve="description" />
|
||||
<node concept="ljvvj" id="2AfSc6Jvjs0" role="3F10Kt">
|
||||
<property role="VOm3f" value="true" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="3F0ifn" id="$u9BK__SIy" role="3EZMnx">
|
||||
<property role="3F0ifm" value="" />
|
||||
<node concept="ljvvj" id="$u9BK__SJr" role="3F10Kt">
|
||||
<property role="VOm3f" value="true" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="3EZMnI" id="$u9BK__SDZ" role="3EZMnx">
|
||||
<node concept="ljvvj" id="$u9BK__SHA" role="3F10Kt">
|
||||
<property role="VOm3f" value="true" />
|
||||
</node>
|
||||
<node concept="VPM3Z" id="$u9BK__SE1" role="3F10Kt">
|
||||
<property role="VOm3f" value="false" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="$u9BK__SFC" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Goal:" />
|
||||
</node>
|
||||
<node concept="l2Vlx" id="$u9BK__SE4" role="2iSdaV" />
|
||||
<node concept="3F1sOY" id="$u9BK__SCz" role="3EZMnx">
|
||||
<property role="1$x2rV" value="<no goal>" />
|
||||
<ref role="1NtTu8" to="jfgh:$u9BK__SAr" resolve="goal" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="3EZMnI" id="$u9BK__SGu" role="3EZMnx">
|
||||
<node concept="VPM3Z" id="$u9BK__SGw" role="3F10Kt">
|
||||
<property role="VOm3f" value="false" />
|
||||
</node>
|
||||
<node concept="ljvvj" id="$u9BK__SHv" role="3F10Kt">
|
||||
<property role="VOm3f" value="true" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="$u9BK__SHp" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Proof:" />
|
||||
</node>
|
||||
<node concept="l2Vlx" id="$u9BK__SGz" role="2iSdaV" />
|
||||
</node>
|
||||
<node concept="3EZMnI" id="$u9BK_yCN6" role="3EZMnx">
|
||||
<node concept="3EZMnI" id="$u9BK_z1QP" role="3EZMnx">
|
||||
<node concept="VPM3Z" id="$u9BK_z1QR" role="3F10Kt">
|
||||
<property role="VOm3f" value="false" />
|
||||
</node>
|
||||
<node concept="2iRkQZ" id="$u9BK_z1QU" role="2iSdaV" />
|
||||
<node concept="3EZMnI" id="$u9BK_z6et" role="3EZMnx">
|
||||
<node concept="l2Vlx" id="$u9BK_z6eu" role="2iSdaV" />
|
||||
<node concept="VPM3Z" id="$u9BK_z6ev" role="3F10Kt">
|
||||
<property role="VOm3f" value="false" />
|
||||
</node>
|
||||
<node concept="3F2HdR" id="$u9BK_z6ez" role="3EZMnx">
|
||||
<property role="2czwfO" value=" " />
|
||||
<ref role="1NtTu8" to="jfgh:3JXBM6C4wQA" resolve="content" />
|
||||
<node concept="l2Vlx" id="$u9BK_z6e$" role="2czzBx" />
|
||||
<node concept="tppnM" id="$u9BK_zt0T" role="sWeuL">
|
||||
<node concept="ljvvj" id="$u9BK_zt0V" role="3F10Kt">
|
||||
<property role="VOm3f" value="true" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="2w$q5c" id="5RfK0kxj3Yz" role="78xua">
|
||||
<node concept="2aJ2om" id="5RfK0kxj3Y$" role="2w$qW5">
|
||||
<ref role="2$4xQ3" to="8v9h:$u9BK_z27v" resolve="ID" />
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
<node concept="3EZMnI" id="$u9BK_yCN7" role="3EZMnx">
|
||||
<node concept="VPM3Z" id="$u9BK_yCN8" role="3F10Kt">
|
||||
<property role="VOm3f" value="false" />
|
||||
</node>
|
||||
<node concept="2iRkQZ" id="$u9BK_yCNa" role="2iSdaV" />
|
||||
<node concept="3EZMnI" id="3JXBM6C6j0E" role="3EZMnx">
|
||||
<node concept="VPM3Z" id="3JXBM6C6j0G" role="3F10Kt">
|
||||
<property role="VOm3f" value="false" />
|
||||
</node>
|
||||
<node concept="l2Vlx" id="3JXBM6C6j0J" role="2iSdaV" />
|
||||
<node concept="3F2HdR" id="3JXBM6C3URp" role="3EZMnx">
|
||||
<property role="2czwfO" value=" " />
|
||||
<ref role="1NtTu8" to="jfgh:3JXBM6C4wQA" resolve="content" />
|
||||
<node concept="l2Vlx" id="3JXBM6C3URr" role="2czzBx" />
|
||||
<node concept="tppnM" id="3JXBM6C3URw" role="sWeuL">
|
||||
<node concept="ljvvj" id="3JXBM6C3URy" role="3F10Kt">
|
||||
<property role="VOm3f" value="true" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="3F0ifn" id="3JXBM6C3UR$" role="2czzBI">
|
||||
<property role="3F0ifm" value="" />
|
||||
<property role="ilYzB" value="<no steps>" />
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
<node concept="2iRfu4" id="$u9BK_yCNb" role="2iSdaV" />
|
||||
<node concept="3EZMnI" id="$u9BK_zG5o" role="3EZMnx">
|
||||
<node concept="3EZMnI" id="$u9BK_$Qxk" role="3EZMnx">
|
||||
<node concept="l2Vlx" id="$u9BK_$Qxl" role="2iSdaV" />
|
||||
<node concept="VPM3Z" id="$u9BK_$Qxm" role="3F10Kt">
|
||||
<property role="VOm3f" value="false" />
|
||||
</node>
|
||||
<node concept="3F2HdR" id="$u9BK_$Qxn" role="3EZMnx">
|
||||
<property role="2czwfO" value=" " />
|
||||
<ref role="1NtTu8" to="jfgh:3JXBM6C4wQA" resolve="content" />
|
||||
<node concept="l2Vlx" id="$u9BK_$Qxo" role="2czzBx" />
|
||||
<node concept="tppnM" id="$u9BK_$Qxp" role="sWeuL">
|
||||
<node concept="ljvvj" id="$u9BK_$Qxq" role="3F10Kt">
|
||||
<property role="VOm3f" value="true" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="2w$q5c" id="$u9BK_$QxA" role="78xua">
|
||||
<node concept="2aJ2om" id="$u9BK_$QxB" role="2w$qW5">
|
||||
<ref role="2$4xQ3" to="8v9h:$u9BK_zG6f" resolve="BASIS" />
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
</node>
|
||||
<node concept="VPM3Z" id="$u9BK_zG5q" role="3F10Kt">
|
||||
<property role="VOm3f" value="false" />
|
||||
</node>
|
||||
<node concept="2iRkQZ" id="$u9BK_zG5t" role="2iSdaV" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="l2Vlx" id="3JXBM6C3URl" role="2iSdaV" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="3p36aQ" id="3JXBM6C6F7z">
|
||||
<property role="3GE5qa" value="proof" />
|
||||
<ref role="aqKnT" to="27wh:3JXBM6C3Fs$" resolve="PropositionalProof" />
|
||||
</node>
|
||||
</model>
|
||||
|
||||
|
|
|
|||
|
|
@ -24,6 +24,7 @@
|
|||
<reference id="1169127628841" name="intfc" index="PrY4T" />
|
||||
</concept>
|
||||
<concept id="1071489090640" name="jetbrains.mps.lang.structure.structure.ConceptDeclaration" flags="ig" index="1TIwiD">
|
||||
<property id="1096454100552" name="rootable" index="19KtqR" />
|
||||
<reference id="1071489389519" name="extends" index="1TJDcQ" />
|
||||
<child id="1169129564478" name="implements" index="PzmwI" />
|
||||
</concept>
|
||||
|
|
@ -170,6 +171,9 @@
|
|||
<property role="34LRSv" value="&E" />
|
||||
<property role="R4oN_" value="And Elimination" />
|
||||
<ref role="1TJDcQ" to="jfgh:3JXBM6C3FsA" resolve="Judgement" />
|
||||
<node concept="PrWs8" id="3w0n0hziLcg" role="PzmwI">
|
||||
<ref role="PrY4T" node="3w0n0hziLcf" resolve="PropositionalRule" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="1TIwiD" id="3JXBM6C3URE">
|
||||
<property role="EcuMT" value="4322786184247881194" />
|
||||
|
|
@ -178,6 +182,9 @@
|
|||
<property role="34LRSv" value="&I" />
|
||||
<property role="R4oN_" value="And Introduction" />
|
||||
<ref role="1TJDcQ" to="jfgh:3JXBM6C3FsA" resolve="Judgement" />
|
||||
<node concept="PrWs8" id="3w0n0hziLci" role="PzmwI">
|
||||
<ref role="PrY4T" node="3w0n0hziLcf" resolve="PropositionalRule" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="1TIwiD" id="3JXBM6C3ZJm">
|
||||
<property role="EcuMT" value="4322786184247901142" />
|
||||
|
|
@ -186,6 +193,9 @@
|
|||
<property role="34LRSv" value="=>E" />
|
||||
<property role="R4oN_" value="Implication Elimination" />
|
||||
<ref role="1TJDcQ" to="jfgh:3JXBM6C3FsA" resolve="Judgement" />
|
||||
<node concept="PrWs8" id="3w0n0hziLck" role="PzmwI">
|
||||
<ref role="PrY4T" node="3w0n0hziLcf" resolve="PropositionalRule" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="1TIwiD" id="3JXBM6C3ZJ9">
|
||||
<property role="EcuMT" value="4322786184247901129" />
|
||||
|
|
@ -194,6 +204,9 @@
|
|||
<property role="34LRSv" value="=>I" />
|
||||
<property role="R4oN_" value="Implication Introduction" />
|
||||
<ref role="1TJDcQ" to="jfgh:3JXBM6C3FsA" resolve="Judgement" />
|
||||
<node concept="PrWs8" id="3w0n0hziLcm" role="PzmwI">
|
||||
<ref role="PrY4T" node="3w0n0hziLcf" resolve="PropositionalRule" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="1TIwiD" id="3JXBM6C3ZJo">
|
||||
<property role="EcuMT" value="4322786184247901144" />
|
||||
|
|
@ -202,6 +215,9 @@
|
|||
<property role="34LRSv" value="<=>E" />
|
||||
<property role="R4oN_" value="Biconditional Elimination" />
|
||||
<ref role="1TJDcQ" to="jfgh:3JXBM6C3FsA" resolve="Judgement" />
|
||||
<node concept="PrWs8" id="3w0n0hziLco" role="PzmwI">
|
||||
<ref role="PrY4T" node="3w0n0hziLcf" resolve="PropositionalRule" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="1TIwiD" id="3JXBM6C3ZJn">
|
||||
<property role="EcuMT" value="4322786184247901143" />
|
||||
|
|
@ -210,6 +226,9 @@
|
|||
<property role="34LRSv" value="<=>I" />
|
||||
<property role="R4oN_" value="Biconditional Introduction" />
|
||||
<ref role="1TJDcQ" to="jfgh:3JXBM6C3FsA" resolve="Judgement" />
|
||||
<node concept="PrWs8" id="3w0n0hziLcq" role="PzmwI">
|
||||
<ref role="PrY4T" node="3w0n0hziLcf" resolve="PropositionalRule" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="1TIwiD" id="3JXBM6C3ZJ8">
|
||||
<property role="EcuMT" value="4322786184247901128" />
|
||||
|
|
@ -218,6 +237,9 @@
|
|||
<property role="34LRSv" value="~E" />
|
||||
<property role="R4oN_" value="Negation Elimination" />
|
||||
<ref role="1TJDcQ" to="jfgh:3JXBM6C3FsA" resolve="Judgement" />
|
||||
<node concept="PrWs8" id="3w0n0hziLcs" role="PzmwI">
|
||||
<ref role="PrY4T" node="3w0n0hziLcf" resolve="PropositionalRule" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="1TIwiD" id="3JXBM6C3UTA">
|
||||
<property role="EcuMT" value="4322786184247881318" />
|
||||
|
|
@ -226,6 +248,9 @@
|
|||
<property role="34LRSv" value="~I" />
|
||||
<property role="R4oN_" value="Negation Introduction" />
|
||||
<ref role="1TJDcQ" to="jfgh:3JXBM6C3FsA" resolve="Judgement" />
|
||||
<node concept="PrWs8" id="3w0n0hziLcu" role="PzmwI">
|
||||
<ref role="PrY4T" node="3w0n0hziLcf" resolve="PropositionalRule" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="1TIwiD" id="3JXBM6C3UT_">
|
||||
<property role="EcuMT" value="4322786184247881317" />
|
||||
|
|
@ -234,6 +259,9 @@
|
|||
<property role="34LRSv" value="|E" />
|
||||
<property role="R4oN_" value="Or Elimination" />
|
||||
<ref role="1TJDcQ" to="jfgh:3JXBM6C3FsA" resolve="Judgement" />
|
||||
<node concept="PrWs8" id="3w0n0hziLcw" role="PzmwI">
|
||||
<ref role="PrY4T" node="3w0n0hziLcf" resolve="PropositionalRule" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="1TIwiD" id="3JXBM6C3UT$">
|
||||
<property role="EcuMT" value="4322786184247881316" />
|
||||
|
|
@ -242,6 +270,28 @@
|
|||
<property role="34LRSv" value="|I" />
|
||||
<property role="R4oN_" value="OrIntroduction" />
|
||||
<ref role="1TJDcQ" to="jfgh:3JXBM6C3FsA" resolve="Judgement" />
|
||||
<node concept="PrWs8" id="3w0n0hziLcy" role="PzmwI">
|
||||
<ref role="PrY4T" node="3w0n0hziLcf" resolve="PropositionalRule" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="1TIwiD" id="3JXBM6C3Fs$">
|
||||
<property role="EcuMT" value="4322786184247818020" />
|
||||
<property role="TrG5h" value="PropositionalProof" />
|
||||
<property role="19KtqR" value="true" />
|
||||
<property role="34LRSv" value="Propositional Proof" />
|
||||
<property role="3GE5qa" value="proof" />
|
||||
<ref role="1TJDcQ" to="jfgh:3w0n0hzgWvH" resolve="AbstractProof" />
|
||||
<node concept="PrWs8" id="3JXBM6C3URC" role="PzmwI">
|
||||
<ref role="PrY4T" to="tpck:h0TrEE$" resolve="INamedConcept" />
|
||||
</node>
|
||||
<node concept="PrWs8" id="3JXBM6C5v8v" role="PzmwI">
|
||||
<ref role="PrY4T" to="jfgh:3JXBM6C5urr" resolve="Root" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="PlHQZ" id="3w0n0hziLcf">
|
||||
<property role="EcuMT" value="4035326440039453455" />
|
||||
<property role="3GE5qa" value="proof.rule" />
|
||||
<property role="TrG5h" value="PropositionalRule" />
|
||||
</node>
|
||||
</model>
|
||||
|
||||
|
|
|
|||
|
|
@ -5356,8 +5356,8 @@
|
|||
<node concept="2OqwBi" id="2YqrT$P7QYz" role="2Oq$k0">
|
||||
<node concept="1PxgMI" id="2YqrT$P7QY$" role="2Oq$k0">
|
||||
<property role="1BlNFB" value="true" />
|
||||
<node concept="chp4Y" id="2YqrT$P7QY_" role="3oSUPX">
|
||||
<ref role="cht4Q" to="jfgh:3JXBM6C3Fs$" resolve="Proof" />
|
||||
<node concept="chp4Y" id="3w0n0hzgXvI" role="3oSUPX">
|
||||
<ref role="cht4Q" to="jfgh:3w0n0hzgWvH" resolve="AbstractProof" />
|
||||
</node>
|
||||
<node concept="2OqwBi" id="2YqrT$P7QYA" role="1m5AlR">
|
||||
<node concept="3A2sRY" id="2YqrT$P7QYB" role="2Oq$k0">
|
||||
|
|
@ -5415,8 +5415,8 @@
|
|||
<node concept="2OqwBi" id="2YqrT$P7QS9" role="2Oq$k0">
|
||||
<node concept="1PxgMI" id="2YqrT$P7QSa" role="2Oq$k0">
|
||||
<property role="1BlNFB" value="true" />
|
||||
<node concept="chp4Y" id="2YqrT$P7QSb" role="3oSUPX">
|
||||
<ref role="cht4Q" to="jfgh:3JXBM6C3Fs$" resolve="Proof" />
|
||||
<node concept="chp4Y" id="3w0n0hzgXrv" role="3oSUPX">
|
||||
<ref role="cht4Q" to="jfgh:3w0n0hzgWvH" resolve="AbstractProof" />
|
||||
</node>
|
||||
<node concept="2OqwBi" id="2YqrT$P7QSc" role="1m5AlR">
|
||||
<node concept="3A2sRY" id="2YqrT$P7QSd" role="2Oq$k0">
|
||||
|
|
@ -5450,8 +5450,8 @@
|
|||
<node concept="2OqwBi" id="2YqrT$P7JQA" role="2Oq$k0">
|
||||
<node concept="1PxgMI" id="2YqrT$P7J$X" role="2Oq$k0">
|
||||
<property role="1BlNFB" value="true" />
|
||||
<node concept="chp4Y" id="2YqrT$P7JEG" role="3oSUPX">
|
||||
<ref role="cht4Q" to="jfgh:3JXBM6C3Fs$" resolve="Proof" />
|
||||
<node concept="chp4Y" id="3w0n0hzgWPN" role="3oSUPX">
|
||||
<ref role="cht4Q" to="jfgh:3w0n0hzgWvH" resolve="AbstractProof" />
|
||||
</node>
|
||||
<node concept="2OqwBi" id="2YqrT$P7IdR" role="1m5AlR">
|
||||
<node concept="3A2sRY" id="2YqrT$P7I5i" role="2Oq$k0">
|
||||
|
|
|
|||
Loading…
Reference in New Issue