natas_hw
/
mps-coderules
mirror of https://github.com/JetBrains/mps-coderules
0
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Updated to latest MPS and typechecking plugin.

This commit is contained in:
Fedor Isakov 2018-04-05 16:33:55 +02:00
parent 2aa168e32e
commit 9f1632b018
11 changed files with 613 additions and 459 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
samples/fitch/languages/jetbrains.mps.fitch/jetbrains.mps.fitch.mpl
View File

@ -7,7 +7,7 @@
</models>
<accessoryModels />
<generators>
<generator alias="main" namespace="jetbrains.mps.fitch#4322786184247805322" uuid="65b2d9d2-5a92-4dd0-abf5-f3a1bd399bec" reflective-queries="true">
<generator alias="main" namespace="jetbrains.mps.fitch#4322786184247805322" uuid="65b2d9d2-5a92-4dd0-abf5-f3a1bd399bec">
<models>
<modelRoot contentPath="${module}/generator/template" type="default">
<sourceRoot location="." />
@ -15,7 +15,7 @@
</models>
<external-templates />
<languageVersions>
<language slang="l:f3061a53-9226-4cc5-a443-f952ceaf5816:jetbrains.mps.baseLanguage" version="5" />
<language slang="l:f3061a53-9226-4cc5-a443-f952ceaf5816:jetbrains.mps.baseLanguage" version="6" />
<language slang="l:fd392034-7849-419d-9071-12563d152375:jetbrains.mps.baseLanguage.closures" version="0" />
<language slang="l:83888646-71ce-4f1c-9c53-c54016f6ad4f:jetbrains.mps.baseLanguage.collections" version="0" />
<language slang="l:f2801650-65d5-424e-bb1b-463a8781b786:jetbrains.mps.baseLanguage.javadoc" version="2" />
@ -25,9 +25,10 @@
<language slang="l:b401a680-8325-4110-8fd3-84331ff25bef:jetbrains.mps.lang.generator" version="0" />
<language slang="l:d7706f63-9be2-479c-a3da-ae92af1e64d5:jetbrains.mps.lang.generator.generationContext" version="0" />
<language slang="l:289fcc83-6543-41e8-a5ca-768235715ce4:jetbrains.mps.lang.generator.generationParameters" version="0" />
<language slang="l:446c26eb-2b7b-4bf0-9b35-f83fa582753e:jetbrains.mps.lang.modelapi" version="0" />
<language slang="l:3a13115c-633c-4c5c-bbcc-75c4219e9555:jetbrains.mps.lang.quotation" version="0" />
<language slang="l:13744753-c81f-424a-9c1b-cf8943bf4e86:jetbrains.mps.lang.sharedConcepts" version="0" />
<language slang="l:7866978e-a0f0-4cc7-81bc-4d213d9375e1:jetbrains.mps.lang.smodel" version="8" />
<language slang="l:7866978e-a0f0-4cc7-81bc-4d213d9375e1:jetbrains.mps.lang.smodel" version="11" />
<language slang="l:c7fb639f-be78-4307-89b0-b5959c3fa8c8:jetbrains.mps.lang.text" version="0" />
<language slang="l:9ded098b-ad6a-4657-bfd9-48636cfe8bc3:jetbrains.mps.lang.traceable" version="0" />
</languageVersions>
@ -39,15 +40,13 @@
<module reference="06b7c5c7-e359-4f4b-a581-5d0c9323af39(jetbrains.mps.fitch)" version="1" />
<module reference="65b2d9d2-5a92-4dd0-abf5-f3a1bd399bec(jetbrains.mps.fitch#4322786184247805322)" version="0" />
<module reference="ceab5195-25ea-4f22-9b92-103b95ca8c0c(jetbrains.mps.lang.core)" version="0" />
<module reference="d7eb0a2a-bd50-4576-beae-e4a89db35f20(jetbrains.mps.lang.scopes.runtime)" version="0" />
<module reference="c72da2b9-7cce-4447-8389-f407dc1158b7(jetbrains.mps.lang.structure)" version="0" />
</dependencyVersions>
<mapping-priorities />
</generator>
</generators>
<sourcePath />
<languageVersions>
<language slang="l:f3061a53-9226-4cc5-a443-f952ceaf5816:jetbrains.mps.baseLanguage" version="5" />
<language slang="l:f3061a53-9226-4cc5-a443-f952ceaf5816:jetbrains.mps.baseLanguage" version="6" />
<language slang="l:443f4c36-fcf5-4eb6-9500-8d06ed259e3e:jetbrains.mps.baseLanguage.classifiers" version="0" />
<language slang="l:fd392034-7849-419d-9071-12563d152375:jetbrains.mps.baseLanguage.closures" version="0" />
<language slang="l:83888646-71ce-4f1c-9c53-c54016f6ad4f:jetbrains.mps.baseLanguage.collections" version="0" />
@ -72,19 +71,21 @@
<language slang="l:d7a92d38-f7db-40d0-8431-763b0c3c9f20:jetbrains.mps.lang.intentions" version="0" />
<language slang="l:90746344-04fd-4286-97d5-b46ae6a81709:jetbrains.mps.lang.migration" version="0" />
<language slang="l:9882f4ad-1955-46fe-8269-94189e5dbbf2:jetbrains.mps.lang.migration.util" version="0" />
<language slang="l:446c26eb-2b7b-4bf0-9b35-f83fa582753e:jetbrains.mps.lang.modelapi" version="0" />
<language slang="l:d4615e3b-d671-4ba9-af01-2b78369b0ba7:jetbrains.mps.lang.pattern" version="1" />
<language slang="l:3a13115c-633c-4c5c-bbcc-75c4219e9555:jetbrains.mps.lang.quotation" version="0" />
<language slang="l:3ecd7c84-cde3-45de-886c-135ecc69b742:jetbrains.mps.lang.refactoring" version="0" />
<language slang="l:982eb8df-2c96-4bd7-9963-11712ea622e5:jetbrains.mps.lang.resources" version="2" />
<language slang="l:0eddeefa-c2d6-4437-bc2c-de50fd4ce470:jetbrains.mps.lang.script" version="0" />
<language slang="l:13744753-c81f-424a-9c1b-cf8943bf4e86:jetbrains.mps.lang.sharedConcepts" version="0" />
<language slang="l:7866978e-a0f0-4cc7-81bc-4d213d9375e1:jetbrains.mps.lang.smodel" version="8" />
<language slang="l:7866978e-a0f0-4cc7-81bc-4d213d9375e1:jetbrains.mps.lang.smodel" version="11" />
<language slang="l:cba985fe-1e96-4f16-9f8d-b07434405d4f:jetbrains.mps.lang.smodel.types" version="0" />
<language slang="l:c72da2b9-7cce-4447-8389-f407dc1158b7:jetbrains.mps.lang.structure" version="6" />
<language slang="l:c7fb639f-be78-4307-89b0-b5959c3fa8c8:jetbrains.mps.lang.text" version="0" />
<language slang="l:b83431fe-5c8f-40bc-8a36-65e25f4dd253:jetbrains.mps.lang.textGen" version="1" />
<language slang="l:9ded098b-ad6a-4657-bfd9-48636cfe8bc3:jetbrains.mps.lang.traceable" version="0" />
<language slang="l:7a5dda62-9140-4668-ab76-d5ed1746f2b2:jetbrains.mps.lang.typesystem" version="1" />
<language slang="l:c4803b19-6d89-4a3b-bf82-390769514add:jetbrains.mps.lang.typesystem2" version="7" />
<language slang="l:c4803b19-6d89-4a3b-bf82-390769514add:jetbrains.mps.lang.typesystem2" version="8" />
<language slang="l:35320f26-77cb-4c55-be9f-a97a27770af1:jetbrains.mps.logic" version="2" />
</languageVersions>
<dependencyVersions>
@ -95,8 +96,6 @@
<module reference="06b7c5c7-e359-4f4b-a581-5d0c9323af39(jetbrains.mps.fitch)" version="1" />
<module reference="ceab5195-25ea-4f22-9b92-103b95ca8c0c(jetbrains.mps.lang.core)" version="0" />
<module reference="a9e4c532-c5f5-4bb7-99ef-42abb73bbb70(jetbrains.mps.lang.descriptor.aspects)" version="0" />
<module reference="d7eb0a2a-bd50-4576-beae-e4a89db35f20(jetbrains.mps.lang.scopes.runtime)" version="0" />
<module reference="c72da2b9-7cce-4447-8389-f407dc1158b7(jetbrains.mps.lang.structure)" version="0" />
</dependencyVersions>
<extendedLanguages />
</language>

35
samples/fitch/languages/jetbrains.mps.fitch/models/types.mps
View File

@ -2,8 +2,8 @@
<model ref="r:30efdd3a-609b-4e7b-a8f2-60af62d5341f(jetbrains.mps.fitch.types)">
<persistence version="9" />
<languages>
<use id="c4803b19-6d89-4a3b-bf82-390769514add" name="jetbrains.mps.lang.typesystem2" version="7" />
<use id="f3061a53-9226-4cc5-a443-f952ceaf5816" name="jetbrains.mps.baseLanguage" version="5" />
<use id="c4803b19-6d89-4a3b-bf82-390769514add" name="jetbrains.mps.lang.typesystem2" version="8" />
<use id="f3061a53-9226-4cc5-a443-f952ceaf5816" name="jetbrains.mps.baseLanguage" version="6" />
<devkit ref="2677cb18-f558-4e33-bc38-a5139cee06dc(jetbrains.mps.devkit.language-design)" />
</languages>
<imports>
@ -49,6 +49,9 @@
</concept>
</language>
<language id="c4803b19-6d89-4a3b-bf82-390769514add" name="jetbrains.mps.lang.typesystem2">
<concept id="8456919074560454386" name="jetbrains.mps.lang.typesystem2.structure.ParameterContainer" flags="ng" index="0eUR_">
<child id="8456919074560454898" name="parameter" index="0eVf_" />
</concept>
<concept id="1618328391714701929" name="jetbrains.mps.lang.typesystem2.structure.TermTemplate" flags="ng" index="0oftK" />
<concept id="6086839168138086051" name="jetbrains.mps.lang.typesystem2.structure.TermTable" flags="ng" index="1HGPq">
<child id="6086839168138086052" name="termDeclaration" index="1HGPt" />
@ -70,6 +73,7 @@
<child id="6856711987714624233" name="code" index="HKQng" />
</concept>
<concept id="5372587443975633709" name="jetbrains.mps.lang.typesystem2.structure.AbstractRule" flags="ng" index="3wqRzX">
<child id="8456919074560456757" name="parameter" index="0eVGy" />
<child id="7509376976631847095" name="input" index="20_v8_" />
<child id="1427485783570316357" name="head" index="3orSU4" />
<child id="1427485783571962463" name="body" index="3otmyu" />
@ -89,7 +93,6 @@
</concept>
<concept id="7368070394766963523" name="jetbrains.mps.lang.typesystem2.structure.RuleComponent" flags="ng" index="3Aq9uZ">
<child id="2316688792939037645" name="logic" index="3Ip0Jz" />
<child id="965748826975413053" name="parameter" index="3Nuqhd" />
</concept>
<concept id="7368070394766966388" name="jetbrains.mps.lang.typesystem2.structure.Body" flags="ng" index="3Aq9E8" />
<concept id="7368070394767067636" name="jetbrains.mps.lang.typesystem2.structure.ConstraintDeclaration" flags="ng" index="3AqmO8">
@ -342,13 +345,15 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="2YqrT$P6Q3v" role="3Nuqhd">
</node>
<node concept="0eUR_" id="3dsgZciwaju" role="0eVGy">
<node concept="3NuqgR" id="2YqrT$P6Q3v" role="0eVf_">
<node concept="aZer4" id="2YqrT$P6Q3w" role="3XD1gS">
<property role="TrG5h" value="Node" />
</node>
<node concept="3Tqbb2" id="2YqrT$P6Q3x" role="3vLBG7" />
</node>
<node concept="3NuqgR" id="2YqrT$P6Qsx" role="3Nuqhd">
<node concept="3NuqgR" id="2YqrT$P6Qsx" role="0eVf_">
<node concept="aZer4" id="2YqrT$P6Qsy" role="3XD1gS">
<property role="TrG5h" value="Msg" />
</node>
@ -388,12 +393,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="2YqrT$P7SuF" role="3Nuqhd">
<node concept="aZer4" id="2YqrT$P7SuG" role="3XD1gS">
<property role="TrG5h" value="Node" />
</node>
<node concept="3Tqbb2" id="2YqrT$P7SuH" role="3vLBG7" />
</node>
</node>
<node concept="2t___k" id="2YqrT$P7StQ" role="20_v8_">
<ref role="2t_S0q" to="jfgh:$u9BK__SA8" resolve="Goal" />
@ -430,6 +429,14 @@
</node>
</node>
</node>
<node concept="0eUR_" id="3dsgZciwajt" role="0eVGy">
<node concept="3NuqgR" id="2YqrT$P7SuF" role="0eVf_">
<node concept="aZer4" id="2YqrT$P7SuG" role="3XD1gS">
<property role="TrG5h" value="Node" />
</node>
<node concept="3Tqbb2" id="2YqrT$P7SuH" role="3vLBG7" />
</node>
</node>
</node>
<node concept="AVZhu" id="2YqrT$P7SAz" role="3ArX_J">
<property role="TrG5h" value="error_Goal" />
@ -481,13 +488,15 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="2YqrT$P7SAS" role="3Nuqhd">
</node>
<node concept="0eUR_" id="3dsgZciwajs" role="0eVGy">
<node concept="3NuqgR" id="2YqrT$P7SAS" role="0eVf_">
<node concept="aZer4" id="2YqrT$P7SAT" role="3XD1gS">
<property role="TrG5h" value="Node" />
</node>
<node concept="3Tqbb2" id="2YqrT$P7SAU" role="3vLBG7" />
</node>
<node concept="3NuqgR" id="2YqrT$P7SAV" role="3Nuqhd">
<node concept="3NuqgR" id="2YqrT$P7SAV" role="0eVf_">
<node concept="aZer4" id="2YqrT$P7SAW" role="3XD1gS">
<property role="TrG5h" value="Msg" />
</node>

76
samples/fitch/languages/jetbrains.mps.fitch/sandbox/models/jetbrains.mps.fitch.propositional.mps
View File

@ -1586,5 +1586,81 @@
</node>
</node>
</node>
<node concept="2jWMw5" id="4wvktoXPtyv">
<property role="TrG5h" value="Foo" />
<property role="26WHrx" value="(x &amp; y) z" />
<node concept="GydIM" id="4wvktoXPtyx" role="2jVTa7">
<node concept="2jWLFD" id="4wvktoXPtyA" role="3MT$nN">
<property role="TrG5h" value="x" />
</node>
</node>
<node concept="GydIM" id="4wvktoXPtyG" role="2jVTa7">
<node concept="2jWLFD" id="4wvktoXPtyN" role="3MT$nN">
<property role="TrG5h" value="y" />
</node>
</node>
<node concept="GydIM" id="4wvktoXPtyV" role="2jVTa7">
<node concept="2jWLFD" id="4wvktoXPtz4" role="3MT$nN">
<property role="TrG5h" value="z" />
</node>
</node>
<node concept="GydIM" id="4wvktoXPt_T" role="2jVTa7">
<node concept="2jWLFD" id="4wvktoXPtAi" role="3MT$nN">
<property role="TrG5h" value="w" />
</node>
</node>
<node concept="2jWzbb" id="4wvktoXPtze" role="2jVTa7">
<node concept="2jWMwi" id="4wvktoXPtzs" role="2jWFax">
<ref role="2jWMyc" node="4wvktoXPtyx" />
</node>
<node concept="2jWMwi" id="4wvktoXPtzy" role="2jWFax">
<ref role="2jWMyc" node="4wvktoXPtyG" />
</node>
<node concept="2jWMFq" id="4wvktoXPtzD" role="3MT$nN">
<node concept="2jWLFD" id="4wvktoXPtzA" role="2jWMFt">
<property role="TrG5h" value="x" />
</node>
<node concept="2jWLFD" id="4wvktoXPtzK" role="2jWMFt">
<property role="TrG5h" value="y" />
</node>
</node>
</node>
<node concept="2jWzbb" id="4wvktoXPt$1" role="2jVTa7">
<node concept="2jWMwi" id="4wvktoXPt$l" role="2jWFax">
<ref role="2jWMyc" node="4wvktoXPtze" />
</node>
<node concept="2jWMwi" id="4wvktoXPt$r" role="2jWFax">
<ref role="2jWMyc" node="4wvktoXPtyV" />
</node>
<node concept="2jWMFq" id="4wvktoXPt$H" role="3MT$nN">
<node concept="2jWMFq" id="4wvktoXPt$y" role="2jWMFt">
<node concept="2jWLFD" id="4wvktoXPt$v" role="2jWMFt">
<property role="TrG5h" value="x" />
</node>
<node concept="2jWLFD" id="4wvktoXPt$D" role="2jWMFt">
<property role="TrG5h" value="y" />
</node>
</node>
<node concept="2jWLFD" id="4wvktoXPt$S" role="2jWMFt">
<property role="TrG5h" value="z" />
</node>
</node>
</node>
<node concept="GyqZO" id="4wvktoXPt$X" role="GyqZB">
<node concept="2jWMFq" id="4wvktoXPt_g" role="GyqZP">
<node concept="2jWMFq" id="4wvktoXPt_4" role="2jWMFt">
<node concept="2jWLFD" id="4wvktoXPt_1" role="2jWMFt">
<property role="TrG5h" value="x" />
</node>
<node concept="2jWLFD" id="4wvktoXPt_b" role="2jWMFt">
<property role="TrG5h" value="y" />
</node>
</node>
<node concept="2jWLFD" id="4wvktoXPt_r" role="2jWMFt">
<property role="TrG5h" value="a" />
</node>
</node>
</node>
</node>
</model>

19
samples/fitch/languages/jetbrains.mps.logic.firstOrder/jetbrains.mps.logic.firstOrder.mpl
View File

@ -7,7 +7,7 @@
</models>
<accessoryModels />
<generators>
<generator alias="main" namespace="jetbrains.mps.logic.firstOrder#4035326440039985569" uuid="467b3222-f5a8-48be-9fe1-6c009ed73049" reflective-queries="true">
<generator alias="main" namespace="jetbrains.mps.logic.firstOrder#4035326440039985569" uuid="467b3222-f5a8-48be-9fe1-6c009ed73049">
<models>
<modelRoot contentPath="${module}/generator/template" type="default">
<sourceRoot location="." />
@ -15,7 +15,7 @@
</models>
<external-templates />
<languageVersions>
<language slang="l:f3061a53-9226-4cc5-a443-f952ceaf5816:jetbrains.mps.baseLanguage" version="5" />
<language slang="l:f3061a53-9226-4cc5-a443-f952ceaf5816:jetbrains.mps.baseLanguage" version="6" />
<language slang="l:fd392034-7849-419d-9071-12563d152375:jetbrains.mps.baseLanguage.closures" version="0" />
<language slang="l:83888646-71ce-4f1c-9c53-c54016f6ad4f:jetbrains.mps.baseLanguage.collections" version="0" />
<language slang="l:f2801650-65d5-424e-bb1b-463a8781b786:jetbrains.mps.baseLanguage.javadoc" version="2" />
@ -25,9 +25,10 @@
<language slang="l:b401a680-8325-4110-8fd3-84331ff25bef:jetbrains.mps.lang.generator" version="0" />
<language slang="l:d7706f63-9be2-479c-a3da-ae92af1e64d5:jetbrains.mps.lang.generator.generationContext" version="0" />
<language slang="l:289fcc83-6543-41e8-a5ca-768235715ce4:jetbrains.mps.lang.generator.generationParameters" version="0" />
<language slang="l:446c26eb-2b7b-4bf0-9b35-f83fa582753e:jetbrains.mps.lang.modelapi" version="0" />
<language slang="l:3a13115c-633c-4c5c-bbcc-75c4219e9555:jetbrains.mps.lang.quotation" version="0" />
<language slang="l:13744753-c81f-424a-9c1b-cf8943bf4e86:jetbrains.mps.lang.sharedConcepts" version="0" />
<language slang="l:7866978e-a0f0-4cc7-81bc-4d213d9375e1:jetbrains.mps.lang.smodel" version="8" />
<language slang="l:7866978e-a0f0-4cc7-81bc-4d213d9375e1:jetbrains.mps.lang.smodel" version="11" />
<language slang="l:c7fb639f-be78-4307-89b0-b5959c3fa8c8:jetbrains.mps.lang.text" version="0" />
<language slang="l:9ded098b-ad6a-4657-bfd9-48636cfe8bc3:jetbrains.mps.lang.traceable" version="0" />
</languageVersions>
@ -38,8 +39,6 @@
<module reference="8865b7a8-5271-43d3-884c-6fd1d9cfdd34(MPS.OpenAPI)" version="0" />
<module reference="06b7c5c7-e359-4f4b-a581-5d0c9323af39(jetbrains.mps.fitch)" version="1" />
<module reference="ceab5195-25ea-4f22-9b92-103b95ca8c0c(jetbrains.mps.lang.core)" version="0" />
<module reference="d7eb0a2a-bd50-4576-beae-e4a89db35f20(jetbrains.mps.lang.scopes.runtime)" version="0" />
<module reference="c72da2b9-7cce-4447-8389-f407dc1158b7(jetbrains.mps.lang.structure)" version="0" />
<module reference="ddb01c98-e78e-4c79-b11a-aeba193668d4(jetbrains.mps.logic.firstOrder)" version="0" />
<module reference="467b3222-f5a8-48be-9fe1-6c009ed73049(jetbrains.mps.logic.firstOrder#4035326440039985569)" version="0" />
<module reference="748b3ba1-2791-4ee8-b985-a5598baa7112(jetbrains.mps.logic.herbrand)" version="0" />
@ -54,7 +53,7 @@
<dependency reexport="false">ddb01c98-e78e-4c79-b11a-aeba193668d4(jetbrains.mps.logic.firstOrder)</dependency>
</dependencies>
<languageVersions>
<language slang="l:f3061a53-9226-4cc5-a443-f952ceaf5816:jetbrains.mps.baseLanguage" version="5" />
<language slang="l:f3061a53-9226-4cc5-a443-f952ceaf5816:jetbrains.mps.baseLanguage" version="6" />
<language slang="l:443f4c36-fcf5-4eb6-9500-8d06ed259e3e:jetbrains.mps.baseLanguage.classifiers" version="0" />
<language slang="l:fd392034-7849-419d-9071-12563d152375:jetbrains.mps.baseLanguage.closures" version="0" />
<language slang="l:83888646-71ce-4f1c-9c53-c54016f6ad4f:jetbrains.mps.baseLanguage.collections" version="0" />
@ -75,19 +74,21 @@
<language slang="l:b401a680-8325-4110-8fd3-84331ff25bef:jetbrains.mps.lang.generator" version="0" />
<language slang="l:d7706f63-9be2-479c-a3da-ae92af1e64d5:jetbrains.mps.lang.generator.generationContext" version="0" />
<language slang="l:d7a92d38-f7db-40d0-8431-763b0c3c9f20:jetbrains.mps.lang.intentions" version="0" />
<language slang="l:446c26eb-2b7b-4bf0-9b35-f83fa582753e:jetbrains.mps.lang.modelapi" version="0" />
<language slang="l:d4615e3b-d671-4ba9-af01-2b78369b0ba7:jetbrains.mps.lang.pattern" version="1" />
<language slang="l:3a13115c-633c-4c5c-bbcc-75c4219e9555:jetbrains.mps.lang.quotation" version="0" />
<language slang="l:3ecd7c84-cde3-45de-886c-135ecc69b742:jetbrains.mps.lang.refactoring" version="0" />
<language slang="l:982eb8df-2c96-4bd7-9963-11712ea622e5:jetbrains.mps.lang.resources" version="2" />
<language slang="l:0eddeefa-c2d6-4437-bc2c-de50fd4ce470:jetbrains.mps.lang.script" version="0" />
<language slang="l:13744753-c81f-424a-9c1b-cf8943bf4e86:jetbrains.mps.lang.sharedConcepts" version="0" />
<language slang="l:7866978e-a0f0-4cc7-81bc-4d213d9375e1:jetbrains.mps.lang.smodel" version="8" />
<language slang="l:7866978e-a0f0-4cc7-81bc-4d213d9375e1:jetbrains.mps.lang.smodel" version="11" />
<language slang="l:cba985fe-1e96-4f16-9f8d-b07434405d4f:jetbrains.mps.lang.smodel.types" version="0" />
<language slang="l:c72da2b9-7cce-4447-8389-f407dc1158b7:jetbrains.mps.lang.structure" version="6" />
<language slang="l:c7fb639f-be78-4307-89b0-b5959c3fa8c8:jetbrains.mps.lang.text" version="0" />
<language slang="l:b83431fe-5c8f-40bc-8a36-65e25f4dd253:jetbrains.mps.lang.textGen" version="1" />
<language slang="l:9ded098b-ad6a-4657-bfd9-48636cfe8bc3:jetbrains.mps.lang.traceable" version="0" />
<language slang="l:7a5dda62-9140-4668-ab76-d5ed1746f2b2:jetbrains.mps.lang.typesystem" version="1" />
<language slang="l:c4803b19-6d89-4a3b-bf82-390769514add:jetbrains.mps.lang.typesystem2" version="7" />
<language slang="l:c4803b19-6d89-4a3b-bf82-390769514add:jetbrains.mps.lang.typesystem2" version="8" />
<language slang="l:35320f26-77cb-4c55-be9f-a97a27770af1:jetbrains.mps.logic" version="2" />
</languageVersions>
<dependencyVersions>
@ -98,8 +99,6 @@
<module reference="06b7c5c7-e359-4f4b-a581-5d0c9323af39(jetbrains.mps.fitch)" version="1" />
<module reference="ceab5195-25ea-4f22-9b92-103b95ca8c0c(jetbrains.mps.lang.core)" version="0" />
<module reference="a9e4c532-c5f5-4bb7-99ef-42abb73bbb70(jetbrains.mps.lang.descriptor.aspects)" version="0" />
<module reference="d7eb0a2a-bd50-4576-beae-e4a89db35f20(jetbrains.mps.lang.scopes.runtime)" version="0" />
<module reference="c72da2b9-7cce-4447-8389-f407dc1158b7(jetbrains.mps.lang.structure)" version="0" />
<module reference="ddb01c98-e78e-4c79-b11a-aeba193668d4(jetbrains.mps.logic.firstOrder)" version="0" />
<module reference="748b3ba1-2791-4ee8-b985-a5598baa7112(jetbrains.mps.logic.herbrand)" version="0" />
<module reference="ec79e64d-4cbb-4f6c-b7b7-108dd125aba6(jetbrains.mps.logic.propositional)" version="0" />

133
samples/fitch/languages/jetbrains.mps.logic.firstOrder/models/types.mps
View File

@ -2,7 +2,7 @@
<model ref="r:a40f7100-fd07-4b1c-98c5-112d92c92128(jetbrains.mps.logic.firstOrder.types)">
<persistence version="9" />
<languages>
<use id="c4803b19-6d89-4a3b-bf82-390769514add" name="jetbrains.mps.lang.typesystem2" version="7" />
<use id="c4803b19-6d89-4a3b-bf82-390769514add" name="jetbrains.mps.lang.typesystem2" version="8" />
<devkit ref="2677cb18-f558-4e33-bc38-a5139cee06dc(jetbrains.mps.devkit.language-design)" />
</languages>
<imports>
@ -187,6 +187,9 @@
<concept id="1172254888721" name="jetbrains.mps.baseLanguage.collections.structure.ContainsOperation" flags="nn" index="3JPx81" />
</language>
<language id="c4803b19-6d89-4a3b-bf82-390769514add" name="jetbrains.mps.lang.typesystem2">
<concept id="8456919074560454386" name="jetbrains.mps.lang.typesystem2.structure.ParameterContainer" flags="ng" index="0eUR_">
<child id="8456919074560454898" name="parameter" index="0eVf_" />
</concept>
<concept id="1618328391714701929" name="jetbrains.mps.lang.typesystem2.structure.TermTemplate" flags="ng" index="0oftK">
<child id="1618328391714701961" name="feature" index="0ofug" />
</concept>
@ -260,6 +263,7 @@
</concept>
<concept id="8908809128801951597" name="jetbrains.mps.lang.typesystem2.structure.MacroBodyLogicalDeclaration" flags="ng" index="3uniRu" />
<concept id="5372587443975633709" name="jetbrains.mps.lang.typesystem2.structure.AbstractRule" flags="ng" index="3wqRzX">
<child id="8456919074560456757" name="parameter" index="0eVGy" />
<child id="7509376976633120254" name="letBlock" index="20w6XG" />
<child id="7509376976631847095" name="input" index="20_v8_" />
<child id="1427485783571243167" name="guard" index="3oo59u" />
@ -282,7 +286,6 @@
</concept>
<concept id="7368070394766963523" name="jetbrains.mps.lang.typesystem2.structure.RuleComponent" flags="ng" index="3Aq9uZ">
<child id="2316688792939037645" name="logic" index="3Ip0Jz" />
<child id="965748826975413053" name="parameter" index="3Nuqhd" />
</concept>
<concept id="7368070394766966158" name="jetbrains.mps.lang.typesystem2.structure.Guard" flags="ng" index="3Aq9_M" />
<concept id="7368070394766966388" name="jetbrains.mps.lang.typesystem2.structure.Body" flags="ng" index="3Aq9E8" />
@ -492,11 +495,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="3w0n0hzminr" role="3Nuqhd">
<node concept="aZer4" id="3w0n0hzmins" role="3XD1gS">
<property role="TrG5h" value="Stc" />
</node>
</node>
</node>
<node concept="2t___k" id="3w0n0hzmfJW" role="20_v8_">
<ref role="2t_S0q" to="yhz9:3w0n0hzkQ4g" resolve="EqualityIntro" />
@ -504,6 +502,13 @@
<property role="TrG5h" value="eqi" />
</node>
</node>
<node concept="0eUR_" id="3dsgZciwak0" role="0eVGy">
<node concept="3NuqgR" id="3w0n0hzminr" role="0eVf_">
<node concept="aZer4" id="3w0n0hzmins" role="3XD1gS">
<property role="TrG5h" value="Stc" />
</node>
</node>
</node>
</node>
<node concept="AVZhu" id="3w0n0hzm35X" role="3ArX_J">
<property role="TrG5h" value="equalityIntro" />
@ -557,14 +562,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="3w0n0hzmj4b" role="3Nuqhd">
<node concept="aZer4" id="3w0n0hzmj4x" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="3w0n0hzmj4c" role="3XD1gS">
<property role="TrG5h" value="Term" />
</node>
</node>
</node>
<node concept="2t___k" id="3w0n0hzm35Z" role="20_v8_">
<ref role="2t_S0q" to="yhz9:3w0n0hzkQ4g" resolve="EqualityIntro" />
@ -586,6 +583,16 @@
</node>
</node>
</node>
<node concept="0eUR_" id="3dsgZciwak3" role="0eVGy">
<node concept="3NuqgR" id="3w0n0hzmj4b" role="0eVf_">
<node concept="aZer4" id="3w0n0hzmj4x" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="3w0n0hzmj4c" role="3XD1gS">
<property role="TrG5h" value="Term" />
</node>
</node>
</node>
</node>
<node concept="AVZhu" id="3w0n0hzm3e9" role="3ArX_J">
<property role="TrG5h" value="equalityElimLeft" />
@ -695,23 +702,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="3w0n0hzmjfi" role="3Nuqhd">
<node concept="aZer4" id="3w0n0hzmjg7" role="3XD1gS">
<property role="TrG5h" value="Prem" />
</node>
<node concept="aZer4" id="3w0n0hzmjfj" role="3XD1gS">
<property role="TrG5h" value="Eq" />
</node>
<node concept="aZer4" id="3w0n0hzmjfs" role="3XD1gS">
<property role="TrG5h" value="EqLeft" />
</node>
<node concept="aZer4" id="3w0n0hzmjfI" role="3XD1gS">
<property role="TrG5h" value="EqRight" />
</node>
<node concept="aZer4" id="3w0n0hzmrDC" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
</node>
</node>
<node concept="3Aq93q" id="3w0n0hzmfIX" role="3orSU4">
<property role="3ArMco" value="true" />
@ -867,12 +857,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="2CF5XF5v8Q8" role="3Nuqhd">
<node concept="aZer4" id="2CF5XF5v8Q9" role="3XD1gS">
<property role="TrG5h" value="Msg" />
</node>
<node concept="17QB3L" id="2CF5XF5vbtE" role="3vLBG7" />
</node>
</node>
<node concept="2caHhw" id="3w0n0hzmrNx" role="20w6XG">
<node concept="391aah" id="3w0n0hzmrNy" role="390Shn">
@ -1246,6 +1230,31 @@
</node>
</node>
</node>
<node concept="0eUR_" id="3dsgZciwak1" role="0eVGy">
<node concept="3NuqgR" id="3w0n0hzmjfi" role="0eVf_">
<node concept="aZer4" id="3w0n0hzmjg7" role="3XD1gS">
<property role="TrG5h" value="Prem" />
</node>
<node concept="aZer4" id="3w0n0hzmjfj" role="3XD1gS">
<property role="TrG5h" value="Eq" />
</node>
<node concept="aZer4" id="3w0n0hzmjfs" role="3XD1gS">
<property role="TrG5h" value="EqLeft" />
</node>
<node concept="aZer4" id="3w0n0hzmjfI" role="3XD1gS">
<property role="TrG5h" value="EqRight" />
</node>
<node concept="aZer4" id="3w0n0hzmrDC" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
</node>
<node concept="3NuqgR" id="2CF5XF5v8Q8" role="0eVf_">
<node concept="aZer4" id="2CF5XF5v8Q9" role="3XD1gS">
<property role="TrG5h" value="Msg" />
</node>
<node concept="17QB3L" id="2CF5XF5vbtE" role="3vLBG7" />
</node>
</node>
</node>
<node concept="AVZhu" id="3w0n0hznwzA" role="3ArX_J">
<property role="TrG5h" value="equalityElimRight" />
@ -1355,23 +1364,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="3w0n0hznw$i" role="3Nuqhd">
<node concept="aZer4" id="3w0n0hznw$j" role="3XD1gS">
<property role="TrG5h" value="Prem" />
</node>
<node concept="aZer4" id="3w0n0hznw$k" role="3XD1gS">
<property role="TrG5h" value="Eq" />
</node>
<node concept="aZer4" id="3w0n0hznw$l" role="3XD1gS">
<property role="TrG5h" value="EqLeft" />
</node>
<node concept="aZer4" id="3w0n0hznw$m" role="3XD1gS">
<property role="TrG5h" value="EqRight" />
</node>
<node concept="aZer4" id="3w0n0hznw$n" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
</node>
</node>
<node concept="3Aq93q" id="3w0n0hznw$o" role="3orSU4">
<property role="3ArMco" value="true" />
@ -1527,12 +1519,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="3w0n0hznw_o" role="3Nuqhd">
<node concept="aZer4" id="3w0n0hznw_p" role="3XD1gS">
<property role="TrG5h" value="Msg" />
</node>
<node concept="17QB3L" id="3w0n0hznw_q" role="3vLBG7" />
</node>
</node>
<node concept="2caHhw" id="3w0n0hznw_r" role="20w6XG">
<node concept="391aah" id="3w0n0hznw_s" role="390Shn">
@ -1906,6 +1892,31 @@
</node>
</node>
</node>
<node concept="0eUR_" id="3dsgZciwak2" role="0eVGy">
<node concept="3NuqgR" id="3w0n0hznw$i" role="0eVf_">
<node concept="aZer4" id="3w0n0hznw$j" role="3XD1gS">
<property role="TrG5h" value="Prem" />
</node>
<node concept="aZer4" id="3w0n0hznw$k" role="3XD1gS">
<property role="TrG5h" value="Eq" />
</node>
<node concept="aZer4" id="3w0n0hznw$l" role="3XD1gS">
<property role="TrG5h" value="EqLeft" />
</node>
<node concept="aZer4" id="3w0n0hznw$m" role="3XD1gS">
<property role="TrG5h" value="EqRight" />
</node>
<node concept="aZer4" id="3w0n0hznw$n" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
</node>
<node concept="3NuqgR" id="3w0n0hznw_o" role="0eVf_">
<node concept="aZer4" id="3w0n0hznw_p" role="3XD1gS">
<property role="TrG5h" value="Msg" />
</node>
<node concept="17QB3L" id="3w0n0hznw_q" role="3vLBG7" />
</node>
</node>
</node>
</node>
</model>

19
samples/fitch/languages/jetbrains.mps.logic.herbrand/jetbrains.mps.logic.herbrand.mpl
View File

@ -7,7 +7,7 @@
</models>
<accessoryModels />
<generators>
<generator alias="main" namespace="jetbrains.mps.logic.herbrand#3059457401298723545" uuid="8efed383-9c82-409e-81c8-4bd2a012c164" reflective-queries="true">
<generator alias="main" namespace="jetbrains.mps.logic.herbrand#3059457401298723545" uuid="8efed383-9c82-409e-81c8-4bd2a012c164">
<models>
<modelRoot contentPath="${module}/generator/template" type="default">
<sourceRoot location="." />
@ -15,7 +15,7 @@
</models>
<external-templates />
<languageVersions>
<language slang="l:f3061a53-9226-4cc5-a443-f952ceaf5816:jetbrains.mps.baseLanguage" version="5" />
<language slang="l:f3061a53-9226-4cc5-a443-f952ceaf5816:jetbrains.mps.baseLanguage" version="6" />
<language slang="l:fd392034-7849-419d-9071-12563d152375:jetbrains.mps.baseLanguage.closures" version="0" />
<language slang="l:83888646-71ce-4f1c-9c53-c54016f6ad4f:jetbrains.mps.baseLanguage.collections" version="0" />
<language slang="l:f2801650-65d5-424e-bb1b-463a8781b786:jetbrains.mps.baseLanguage.javadoc" version="2" />
@ -25,9 +25,10 @@
<language slang="l:b401a680-8325-4110-8fd3-84331ff25bef:jetbrains.mps.lang.generator" version="0" />
<language slang="l:d7706f63-9be2-479c-a3da-ae92af1e64d5:jetbrains.mps.lang.generator.generationContext" version="0" />
<language slang="l:289fcc83-6543-41e8-a5ca-768235715ce4:jetbrains.mps.lang.generator.generationParameters" version="0" />
<language slang="l:446c26eb-2b7b-4bf0-9b35-f83fa582753e:jetbrains.mps.lang.modelapi" version="0" />
<language slang="l:3a13115c-633c-4c5c-bbcc-75c4219e9555:jetbrains.mps.lang.quotation" version="0" />
<language slang="l:13744753-c81f-424a-9c1b-cf8943bf4e86:jetbrains.mps.lang.sharedConcepts" version="0" />
<language slang="l:7866978e-a0f0-4cc7-81bc-4d213d9375e1:jetbrains.mps.lang.smodel" version="8" />
<language slang="l:7866978e-a0f0-4cc7-81bc-4d213d9375e1:jetbrains.mps.lang.smodel" version="11" />
<language slang="l:c7fb639f-be78-4307-89b0-b5959c3fa8c8:jetbrains.mps.lang.text" version="0" />
<language slang="l:9ded098b-ad6a-4657-bfd9-48636cfe8bc3:jetbrains.mps.lang.traceable" version="0" />
</languageVersions>
@ -38,8 +39,6 @@
<module reference="8865b7a8-5271-43d3-884c-6fd1d9cfdd34(MPS.OpenAPI)" version="0" />
<module reference="06b7c5c7-e359-4f4b-a581-5d0c9323af39(jetbrains.mps.fitch)" version="1" />
<module reference="ceab5195-25ea-4f22-9b92-103b95ca8c0c(jetbrains.mps.lang.core)" version="0" />
<module reference="d7eb0a2a-bd50-4576-beae-e4a89db35f20(jetbrains.mps.lang.scopes.runtime)" version="0" />
<module reference="c72da2b9-7cce-4447-8389-f407dc1158b7(jetbrains.mps.lang.structure)" version="0" />
<module reference="748b3ba1-2791-4ee8-b985-a5598baa7112(jetbrains.mps.logic.herbrand)" version="0" />
<module reference="8efed383-9c82-409e-81c8-4bd2a012c164(jetbrains.mps.logic.herbrand#3059457401298723545)" version="0" />
<module reference="ec79e64d-4cbb-4f6c-b7b7-108dd125aba6(jetbrains.mps.logic.propositional)" version="0" />
@ -55,7 +54,7 @@
<dependency reexport="false">ceab5195-25ea-4f22-9b92-103b95ca8c0c(jetbrains.mps.lang.core)</dependency>
</dependencies>
<languageVersions>
<language slang="l:f3061a53-9226-4cc5-a443-f952ceaf5816:jetbrains.mps.baseLanguage" version="5" />
<language slang="l:f3061a53-9226-4cc5-a443-f952ceaf5816:jetbrains.mps.baseLanguage" version="6" />
<language slang="l:443f4c36-fcf5-4eb6-9500-8d06ed259e3e:jetbrains.mps.baseLanguage.classifiers" version="0" />
<language slang="l:fd392034-7849-419d-9071-12563d152375:jetbrains.mps.baseLanguage.closures" version="0" />
<language slang="l:83888646-71ce-4f1c-9c53-c54016f6ad4f:jetbrains.mps.baseLanguage.collections" version="0" />
@ -77,19 +76,21 @@
<language slang="l:b401a680-8325-4110-8fd3-84331ff25bef:jetbrains.mps.lang.generator" version="0" />
<language slang="l:d7706f63-9be2-479c-a3da-ae92af1e64d5:jetbrains.mps.lang.generator.generationContext" version="0" />
<language slang="l:d7a92d38-f7db-40d0-8431-763b0c3c9f20:jetbrains.mps.lang.intentions" version="0" />
<language slang="l:446c26eb-2b7b-4bf0-9b35-f83fa582753e:jetbrains.mps.lang.modelapi" version="0" />
<language slang="l:d4615e3b-d671-4ba9-af01-2b78369b0ba7:jetbrains.mps.lang.pattern" version="1" />
<language slang="l:3a13115c-633c-4c5c-bbcc-75c4219e9555:jetbrains.mps.lang.quotation" version="0" />
<language slang="l:3ecd7c84-cde3-45de-886c-135ecc69b742:jetbrains.mps.lang.refactoring" version="0" />
<language slang="l:982eb8df-2c96-4bd7-9963-11712ea622e5:jetbrains.mps.lang.resources" version="2" />
<language slang="l:0eddeefa-c2d6-4437-bc2c-de50fd4ce470:jetbrains.mps.lang.script" version="0" />
<language slang="l:13744753-c81f-424a-9c1b-cf8943bf4e86:jetbrains.mps.lang.sharedConcepts" version="0" />
<language slang="l:7866978e-a0f0-4cc7-81bc-4d213d9375e1:jetbrains.mps.lang.smodel" version="8" />
<language slang="l:7866978e-a0f0-4cc7-81bc-4d213d9375e1:jetbrains.mps.lang.smodel" version="11" />
<language slang="l:cba985fe-1e96-4f16-9f8d-b07434405d4f:jetbrains.mps.lang.smodel.types" version="0" />
<language slang="l:c72da2b9-7cce-4447-8389-f407dc1158b7:jetbrains.mps.lang.structure" version="6" />
<language slang="l:c7fb639f-be78-4307-89b0-b5959c3fa8c8:jetbrains.mps.lang.text" version="0" />
<language slang="l:b83431fe-5c8f-40bc-8a36-65e25f4dd253:jetbrains.mps.lang.textGen" version="1" />
<language slang="l:9ded098b-ad6a-4657-bfd9-48636cfe8bc3:jetbrains.mps.lang.traceable" version="0" />
<language slang="l:7a5dda62-9140-4668-ab76-d5ed1746f2b2:jetbrains.mps.lang.typesystem" version="1" />
<language slang="l:c4803b19-6d89-4a3b-bf82-390769514add:jetbrains.mps.lang.typesystem2" version="7" />
<language slang="l:c4803b19-6d89-4a3b-bf82-390769514add:jetbrains.mps.lang.typesystem2" version="8" />
<language slang="l:35320f26-77cb-4c55-be9f-a97a27770af1:jetbrains.mps.logic" version="2" />
</languageVersions>
<dependencyVersions>
@ -104,8 +105,6 @@
<module reference="2d3c70e9-aab2-4870-8d8d-6036800e4103(jetbrains.mps.kernel)" version="0" />
<module reference="ceab5195-25ea-4f22-9b92-103b95ca8c0c(jetbrains.mps.lang.core)" version="0" />
<module reference="a9e4c532-c5f5-4bb7-99ef-42abb73bbb70(jetbrains.mps.lang.descriptor.aspects)" version="0" />
<module reference="d7eb0a2a-bd50-4576-beae-e4a89db35f20(jetbrains.mps.lang.scopes.runtime)" version="0" />
<module reference="c72da2b9-7cce-4447-8389-f407dc1158b7(jetbrains.mps.lang.structure)" version="0" />
<module reference="9ded098b-ad6a-4657-bfd9-48636cfe8bc3(jetbrains.mps.lang.traceable)" version="0" />
<module reference="748b3ba1-2791-4ee8-b985-a5598baa7112(jetbrains.mps.logic.herbrand)" version="0" />
<module reference="ec79e64d-4cbb-4f6c-b7b7-108dd125aba6(jetbrains.mps.logic.propositional)" version="0" />

187
samples/fitch/languages/jetbrains.mps.logic.herbrand/models/types.mps
View File

@ -2,7 +2,7 @@
<model ref="r:2e585daf-c5c7-4735-a41f-b2044cd9b207(jetbrains.mps.logic.herbrand.types)">
<persistence version="9" />
<languages>
<use id="c4803b19-6d89-4a3b-bf82-390769514add" name="jetbrains.mps.lang.typesystem2" version="7" />
<use id="c4803b19-6d89-4a3b-bf82-390769514add" name="jetbrains.mps.lang.typesystem2" version="8" />
<use id="83888646-71ce-4f1c-9c53-c54016f6ad4f" name="jetbrains.mps.baseLanguage.collections" version="0" />
<use id="f2801650-65d5-424e-bb1b-463a8781b786" name="jetbrains.mps.baseLanguage.javadoc" version="2" />
<devkit ref="2677cb18-f558-4e33-bc38-a5139cee06dc(jetbrains.mps.devkit.language-design)" />
@ -273,6 +273,9 @@
<concept id="1172254888721" name="jetbrains.mps.baseLanguage.collections.structure.ContainsOperation" flags="nn" index="3JPx81" />
</language>
<language id="c4803b19-6d89-4a3b-bf82-390769514add" name="jetbrains.mps.lang.typesystem2">
<concept id="8456919074560454386" name="jetbrains.mps.lang.typesystem2.structure.ParameterContainer" flags="ng" index="0eUR_">
<child id="8456919074560454898" name="parameter" index="0eVf_" />
</concept>
<concept id="1618328391714701929" name="jetbrains.mps.lang.typesystem2.structure.TermTemplate" flags="ng" index="0oftK">
<child id="1618328391714701961" name="feature" index="0ofug" />
</concept>
@ -348,6 +351,7 @@
</concept>
<concept id="8908809128801951597" name="jetbrains.mps.lang.typesystem2.structure.MacroBodyLogicalDeclaration" flags="ng" index="3uniRu" />
<concept id="5372587443975633709" name="jetbrains.mps.lang.typesystem2.structure.AbstractRule" flags="ng" index="3wqRzX">
<child id="8456919074560456757" name="parameter" index="0eVGy" />
<child id="7509376976633120254" name="letBlock" index="20w6XG" />
<child id="7509376976631847095" name="input" index="20_v8_" />
<child id="1427485783571243167" name="guard" index="3oo59u" />
@ -376,7 +380,6 @@
</concept>
<concept id="7368070394766963523" name="jetbrains.mps.lang.typesystem2.structure.RuleComponent" flags="ng" index="3Aq9uZ">
<child id="2316688792939037645" name="logic" index="3Ip0Jz" />
<child id="965748826975413053" name="parameter" index="3Nuqhd" />
</concept>
<concept id="7368070394766966158" name="jetbrains.mps.lang.typesystem2.structure.Guard" flags="ng" index="3Aq9_M" />
<concept id="7368070394766966388" name="jetbrains.mps.lang.typesystem2.structure.Body" flags="ng" index="3Aq9E8" />
@ -1254,17 +1257,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="2oO2uzBWT6y" role="3Nuqhd">
<node concept="aZer4" id="2oO2uzBWT6z" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="2oO2uzBWT6$" role="3XD1gS">
<property role="TrG5h" value="Prem" />
</node>
<node concept="aZer4" id="2oO2uzBWTdP" role="3XD1gS">
<property role="TrG5h" value="Var" />
</node>
</node>
</node>
<node concept="3Aq93q" id="Vo$tzLEGvs" role="3orSU4">
<property role="3ArMco" value="true" />
@ -1373,12 +1365,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="2CF5XF5tE6h" role="3Nuqhd">
<node concept="aZer4" id="2CF5XF5tE6i" role="3XD1gS">
<property role="TrG5h" value="Msg" />
</node>
<node concept="17QB3L" id="2CF5XF5vcBK" role="3vLBG7" />
</node>
</node>
<node concept="2caHhw" id="2CF5XF5rJR2" role="20w6XG">
<node concept="391aah" id="2CF5XF5rJR3" role="390Shn">
@ -1515,6 +1501,25 @@
</node>
</node>
</node>
<node concept="0eUR_" id="3dsgZciwakT" role="0eVGy">
<node concept="3NuqgR" id="2oO2uzBWT6y" role="0eVf_">
<node concept="aZer4" id="2oO2uzBWT6z" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="2oO2uzBWT6$" role="3XD1gS">
<property role="TrG5h" value="Prem" />
</node>
<node concept="aZer4" id="2oO2uzBWTdP" role="3XD1gS">
<property role="TrG5h" value="Var" />
</node>
</node>
<node concept="3NuqgR" id="2CF5XF5tE6h" role="0eVf_">
<node concept="aZer4" id="2CF5XF5tE6i" role="3XD1gS">
<property role="TrG5h" value="Msg" />
</node>
<node concept="17QB3L" id="2CF5XF5vcBK" role="3vLBG7" />
</node>
</node>
</node>
<node concept="AVZhu" id="2oO2uzBWNfg" role="3ArX_J">
<property role="TrG5h" value="forallElim" />
@ -1602,23 +1607,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="2oO2uzBXpHP" role="3Nuqhd">
<node concept="aZer4" id="2oO2uzBWNhT" role="3XD1gS">
<property role="TrG5h" value="Prem" />
</node>
<node concept="aZer4" id="2oO2uzBWNnU" role="3XD1gS">
<property role="TrG5h" value="Var" />
</node>
<node concept="aZer4" id="2S9ARS6yyhD" role="3XD1gS">
<property role="TrG5h" value="Fresh" />
</node>
<node concept="aZer4" id="2oO2uzBXx8g" role="3XD1gS">
<property role="TrG5h" value="Stc" />
</node>
<node concept="aZer4" id="2oO2uzBWNhK" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
</node>
</node>
<node concept="3Aq93q" id="2oO2uzBWQ4w" role="3orSU4">
<property role="3ArMco" value="true" />
@ -1699,12 +1687,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="2CF5XF5v8Q8" role="3Nuqhd">
<node concept="aZer4" id="2CF5XF5v8Q9" role="3XD1gS">
<property role="TrG5h" value="Msg" />
</node>
<node concept="17QB3L" id="2CF5XF5vbtE" role="3vLBG7" />
</node>
</node>
<node concept="3Aq9_M" id="2oO2uzBYjOv" role="3oo59u">
<node concept="3I6sU6" id="2oO2uzBYjOw" role="3Ip0Jz">
@ -2052,6 +2034,31 @@
</node>
</node>
</node>
<node concept="0eUR_" id="3dsgZciwakQ" role="0eVGy">
<node concept="3NuqgR" id="2oO2uzBXpHP" role="0eVf_">
<node concept="aZer4" id="2oO2uzBWNhT" role="3XD1gS">
<property role="TrG5h" value="Prem" />
</node>
<node concept="aZer4" id="2oO2uzBWNnU" role="3XD1gS">
<property role="TrG5h" value="Var" />
</node>
<node concept="aZer4" id="2S9ARS6yyhD" role="3XD1gS">
<property role="TrG5h" value="Fresh" />
</node>
<node concept="aZer4" id="2oO2uzBXx8g" role="3XD1gS">
<property role="TrG5h" value="Stc" />
</node>
<node concept="aZer4" id="2oO2uzBWNhK" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
</node>
<node concept="3NuqgR" id="2CF5XF5v8Q8" role="0eVf_">
<node concept="aZer4" id="2CF5XF5v8Q9" role="3XD1gS">
<property role="TrG5h" value="Msg" />
</node>
<node concept="17QB3L" id="2CF5XF5vbtE" role="3vLBG7" />
</node>
</node>
</node>
<node concept="AVZhu" id="2CF5XF5qrg8" role="3ArX_J">
<property role="TrG5h" value="existsIntro" />
@ -2161,23 +2168,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="2CF5XF5qrJn" role="3Nuqhd">
<node concept="aZer4" id="2CF5XF5qrJo" role="3XD1gS">
<property role="TrG5h" value="Prem" />
</node>
<node concept="aZer4" id="2CF5XF5qrJ$" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="2CF5XF5qukG" role="3XD1gS">
<property role="TrG5h" value="Var" />
</node>
<node concept="aZer4" id="2CF5XF5q_9W" role="3XD1gS">
<property role="TrG5h" value="Fresh" />
</node>
<node concept="aZer4" id="2CF5XF5quzw" role="3XD1gS">
<property role="TrG5h" value="Stc" />
</node>
</node>
</node>
<node concept="3Aq93q" id="2CF5XF5qrJ6" role="3orSU4">
<property role="3ArMco" value="true" />
@ -2245,6 +2235,25 @@
</node>
</node>
</node>
<node concept="0eUR_" id="3dsgZciwakR" role="0eVGy">
<node concept="3NuqgR" id="2CF5XF5qrJn" role="0eVf_">
<node concept="aZer4" id="2CF5XF5qrJo" role="3XD1gS">
<property role="TrG5h" value="Prem" />
</node>
<node concept="aZer4" id="2CF5XF5qrJ$" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="2CF5XF5qukG" role="3XD1gS">
<property role="TrG5h" value="Var" />
</node>
<node concept="aZer4" id="2CF5XF5q_9W" role="3XD1gS">
<property role="TrG5h" value="Fresh" />
</node>
<node concept="aZer4" id="2CF5XF5quzw" role="3XD1gS">
<property role="TrG5h" value="Stc" />
</node>
</node>
</node>
</node>
<node concept="AVZhu" id="2CF5XF5q_hg" role="3ArX_J">
<property role="TrG5h" value="existsElim" />
@ -2415,29 +2424,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="2CF5XF5qAsd" role="3Nuqhd">
<node concept="aZer4" id="2CF5XF5qAse" role="3XD1gS">
<property role="TrG5h" value="Ex" />
</node>
<node concept="aZer4" id="2CF5XF5qAtH" role="3XD1gS">
<property role="TrG5h" value="ExVar" />
</node>
<node concept="aZer4" id="2CF5XF5qOwG" role="3XD1gS">
<property role="TrG5h" value="ExStc" />
</node>
<node concept="aZer4" id="2CF5XF5qAzp" role="3XD1gS">
<property role="TrG5h" value="Uni" />
</node>
<node concept="aZer4" id="2CF5XF5qNbA" role="3XD1gS">
<property role="TrG5h" value="UniVar" />
</node>
<node concept="aZer4" id="2CF5XF5qAtS" role="3XD1gS">
<property role="TrG5h" value="UniStc" />
</node>
<node concept="aZer4" id="2CF5XF5qF8v" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
</node>
</node>
<node concept="3Aq93q" id="2CF5XF5qFel" role="3orSU4">
<property role="3ArMco" value="true" />
@ -2571,12 +2557,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="2cLnr$rI$Mk" role="3Nuqhd">
<node concept="aZer4" id="2cLnr$rI$Ml" role="3XD1gS">
<property role="TrG5h" value="Msg" />
</node>
<node concept="17QB3L" id="2cLnr$rI$Mm" role="3vLBG7" />
</node>
</node>
<node concept="3Aq9_M" id="2CF5XF5qPeh" role="3oo59u">
<node concept="3I6sU6" id="2CF5XF5qPei" role="3Ip0Jz">
@ -2689,6 +2669,37 @@
</node>
</node>
</node>
<node concept="0eUR_" id="3dsgZciwakS" role="0eVGy">
<node concept="3NuqgR" id="2CF5XF5qAsd" role="0eVf_">
<node concept="aZer4" id="2CF5XF5qAse" role="3XD1gS">
<property role="TrG5h" value="Ex" />
</node>
<node concept="aZer4" id="2CF5XF5qAtH" role="3XD1gS">
<property role="TrG5h" value="ExVar" />
</node>
<node concept="aZer4" id="2CF5XF5qOwG" role="3XD1gS">
<property role="TrG5h" value="ExStc" />
</node>
<node concept="aZer4" id="2CF5XF5qAzp" role="3XD1gS">
<property role="TrG5h" value="Uni" />
</node>
<node concept="aZer4" id="2CF5XF5qNbA" role="3XD1gS">
<property role="TrG5h" value="UniVar" />
</node>
<node concept="aZer4" id="2CF5XF5qAtS" role="3XD1gS">
<property role="TrG5h" value="UniStc" />
</node>
<node concept="aZer4" id="2CF5XF5qF8v" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
</node>
<node concept="3NuqgR" id="2cLnr$rI$Mk" role="0eVf_">
<node concept="aZer4" id="2cLnr$rI$Ml" role="3XD1gS">
<property role="TrG5h" value="Msg" />
</node>
<node concept="17QB3L" id="2cLnr$rI$Mm" role="3vLBG7" />
</node>
</node>
</node>
</node>
<node concept="312cEu" id="Vo$tzLFdFq">

19
samples/fitch/languages/jetbrains.mps.logic.propositional/jetbrains.mps.logic.propositional.mpl
View File

@ -7,7 +7,7 @@
</models>
<accessoryModels />
<generators>
<generator alias="main" namespace="jetbrains.mps.logic.propositional#5505606474790531941" uuid="53b8ab24-cc4a-4fe2-b461-11a91d798670" reflective-queries="true">
<generator alias="main" namespace="jetbrains.mps.logic.propositional#5505606474790531941" uuid="53b8ab24-cc4a-4fe2-b461-11a91d798670">
<models>
<modelRoot contentPath="${module}/generator/template" type="default">
<sourceRoot location="." />
@ -15,7 +15,7 @@
</models>
<external-templates />
<languageVersions>
<language slang="l:f3061a53-9226-4cc5-a443-f952ceaf5816:jetbrains.mps.baseLanguage" version="5" />
<language slang="l:f3061a53-9226-4cc5-a443-f952ceaf5816:jetbrains.mps.baseLanguage" version="6" />
<language slang="l:fd392034-7849-419d-9071-12563d152375:jetbrains.mps.baseLanguage.closures" version="0" />
<language slang="l:83888646-71ce-4f1c-9c53-c54016f6ad4f:jetbrains.mps.baseLanguage.collections" version="0" />
<language slang="l:f2801650-65d5-424e-bb1b-463a8781b786:jetbrains.mps.baseLanguage.javadoc" version="2" />
@ -25,9 +25,10 @@
<language slang="l:b401a680-8325-4110-8fd3-84331ff25bef:jetbrains.mps.lang.generator" version="0" />
<language slang="l:d7706f63-9be2-479c-a3da-ae92af1e64d5:jetbrains.mps.lang.generator.generationContext" version="0" />
<language slang="l:289fcc83-6543-41e8-a5ca-768235715ce4:jetbrains.mps.lang.generator.generationParameters" version="0" />
<language slang="l:446c26eb-2b7b-4bf0-9b35-f83fa582753e:jetbrains.mps.lang.modelapi" version="0" />
<language slang="l:3a13115c-633c-4c5c-bbcc-75c4219e9555:jetbrains.mps.lang.quotation" version="0" />
<language slang="l:13744753-c81f-424a-9c1b-cf8943bf4e86:jetbrains.mps.lang.sharedConcepts" version="0" />
<language slang="l:7866978e-a0f0-4cc7-81bc-4d213d9375e1:jetbrains.mps.lang.smodel" version="8" />
<language slang="l:7866978e-a0f0-4cc7-81bc-4d213d9375e1:jetbrains.mps.lang.smodel" version="11" />
<language slang="l:c7fb639f-be78-4307-89b0-b5959c3fa8c8:jetbrains.mps.lang.text" version="0" />
<language slang="l:9ded098b-ad6a-4657-bfd9-48636cfe8bc3:jetbrains.mps.lang.traceable" version="0" />
</languageVersions>
@ -38,8 +39,6 @@
<module reference="8865b7a8-5271-43d3-884c-6fd1d9cfdd34(MPS.OpenAPI)" version="0" />
<module reference="06b7c5c7-e359-4f4b-a581-5d0c9323af39(jetbrains.mps.fitch)" version="1" />
<module reference="ceab5195-25ea-4f22-9b92-103b95ca8c0c(jetbrains.mps.lang.core)" version="0" />
<module reference="d7eb0a2a-bd50-4576-beae-e4a89db35f20(jetbrains.mps.lang.scopes.runtime)" version="0" />
<module reference="c72da2b9-7cce-4447-8389-f407dc1158b7(jetbrains.mps.lang.structure)" version="0" />
<module reference="ec79e64d-4cbb-4f6c-b7b7-108dd125aba6(jetbrains.mps.logic.propositional)" version="0" />
<module reference="53b8ab24-cc4a-4fe2-b461-11a91d798670(jetbrains.mps.logic.propositional#5505606474790531941)" version="0" />
</dependencyVersions>
@ -51,7 +50,7 @@
<dependency reexport="false">daafa647-f1f7-4b0b-b096-69cd7c8408c0(jetbrains.mps.baseLanguage.regexp)</dependency>
</dependencies>
<languageVersions>
<language slang="l:f3061a53-9226-4cc5-a443-f952ceaf5816:jetbrains.mps.baseLanguage" version="5" />
<language slang="l:f3061a53-9226-4cc5-a443-f952ceaf5816:jetbrains.mps.baseLanguage" version="6" />
<language slang="l:443f4c36-fcf5-4eb6-9500-8d06ed259e3e:jetbrains.mps.baseLanguage.classifiers" version="0" />
<language slang="l:fd392034-7849-419d-9071-12563d152375:jetbrains.mps.baseLanguage.closures" version="0" />
<language slang="l:83888646-71ce-4f1c-9c53-c54016f6ad4f:jetbrains.mps.baseLanguage.collections" version="0" />
@ -73,19 +72,21 @@
<language slang="l:b401a680-8325-4110-8fd3-84331ff25bef:jetbrains.mps.lang.generator" version="0" />
<language slang="l:d7706f63-9be2-479c-a3da-ae92af1e64d5:jetbrains.mps.lang.generator.generationContext" version="0" />
<language slang="l:d7a92d38-f7db-40d0-8431-763b0c3c9f20:jetbrains.mps.lang.intentions" version="0" />
<language slang="l:446c26eb-2b7b-4bf0-9b35-f83fa582753e:jetbrains.mps.lang.modelapi" version="0" />
<language slang="l:d4615e3b-d671-4ba9-af01-2b78369b0ba7:jetbrains.mps.lang.pattern" version="1" />
<language slang="l:3a13115c-633c-4c5c-bbcc-75c4219e9555:jetbrains.mps.lang.quotation" version="0" />
<language slang="l:3ecd7c84-cde3-45de-886c-135ecc69b742:jetbrains.mps.lang.refactoring" version="0" />
<language slang="l:982eb8df-2c96-4bd7-9963-11712ea622e5:jetbrains.mps.lang.resources" version="2" />
<language slang="l:0eddeefa-c2d6-4437-bc2c-de50fd4ce470:jetbrains.mps.lang.script" version="0" />
<language slang="l:13744753-c81f-424a-9c1b-cf8943bf4e86:jetbrains.mps.lang.sharedConcepts" version="0" />
<language slang="l:7866978e-a0f0-4cc7-81bc-4d213d9375e1:jetbrains.mps.lang.smodel" version="8" />
<language slang="l:7866978e-a0f0-4cc7-81bc-4d213d9375e1:jetbrains.mps.lang.smodel" version="11" />
<language slang="l:cba985fe-1e96-4f16-9f8d-b07434405d4f:jetbrains.mps.lang.smodel.types" version="0" />
<language slang="l:c72da2b9-7cce-4447-8389-f407dc1158b7:jetbrains.mps.lang.structure" version="6" />
<language slang="l:c7fb639f-be78-4307-89b0-b5959c3fa8c8:jetbrains.mps.lang.text" version="0" />
<language slang="l:b83431fe-5c8f-40bc-8a36-65e25f4dd253:jetbrains.mps.lang.textGen" version="1" />
<language slang="l:9ded098b-ad6a-4657-bfd9-48636cfe8bc3:jetbrains.mps.lang.traceable" version="0" />
<language slang="l:7a5dda62-9140-4668-ab76-d5ed1746f2b2:jetbrains.mps.lang.typesystem" version="1" />
<language slang="l:c4803b19-6d89-4a3b-bf82-390769514add:jetbrains.mps.lang.typesystem2" version="7" />
<language slang="l:c4803b19-6d89-4a3b-bf82-390769514add:jetbrains.mps.lang.typesystem2" version="8" />
<language slang="l:35320f26-77cb-4c55-be9f-a97a27770af1:jetbrains.mps.logic" version="2" />
</languageVersions>
<dependencyVersions>
@ -100,8 +101,6 @@
<module reference="2d3c70e9-aab2-4870-8d8d-6036800e4103(jetbrains.mps.kernel)" version="0" />
<module reference="ceab5195-25ea-4f22-9b92-103b95ca8c0c(jetbrains.mps.lang.core)" version="0" />
<module reference="a9e4c532-c5f5-4bb7-99ef-42abb73bbb70(jetbrains.mps.lang.descriptor.aspects)" version="0" />
<module reference="d7eb0a2a-bd50-4576-beae-e4a89db35f20(jetbrains.mps.lang.scopes.runtime)" version="0" />
<module reference="c72da2b9-7cce-4447-8389-f407dc1158b7(jetbrains.mps.lang.structure)" version="0" />
<module reference="9ded098b-ad6a-4657-bfd9-48636cfe8bc3(jetbrains.mps.lang.traceable)" version="0" />
<module reference="ec79e64d-4cbb-4f6c-b7b7-108dd125aba6(jetbrains.mps.logic.propositional)" version="0" />
</dependencyVersions>

4
samples/fitch/languages/jetbrains.mps.logic.propositional/models/constraints.mps
View File

@ -3,9 +3,9 @@
<persistence version="9" />
<languages>
<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="f3061a53-9226-4cc5-a443-f952ceaf5816" name="jetbrains.mps.baseLanguage" version="6" />
<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="7866978e-a0f0-4cc7-81bc-4d213d9375e1" name="jetbrains.mps.lang.smodel" version="11" />
<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)" />

4
samples/fitch/languages/jetbrains.mps.logic.propositional/models/editor.mps
View File

@ -3,8 +3,8 @@
<persistence version="9" />
<languages>
<use id="18bc6592-03a6-4e29-a83a-7ff23bde13ba" name="jetbrains.mps.lang.editor" version="11" />
<use id="f3061a53-9226-4cc5-a443-f952ceaf5816" name="jetbrains.mps.baseLanguage" version="5" />
<use id="7866978e-a0f0-4cc7-81bc-4d213d9375e1" name="jetbrains.mps.lang.smodel" version="8" />
<use id="f3061a53-9226-4cc5-a443-f952ceaf5816" name="jetbrains.mps.baseLanguage" version="6" />
<use id="7866978e-a0f0-4cc7-81bc-4d213d9375e1" name="jetbrains.mps.lang.smodel" version="11" />
<use id="83888646-71ce-4f1c-9c53-c54016f6ad4f" name="jetbrains.mps.baseLanguage.collections" version="0" />
<use id="daafa647-f1f7-4b0b-b096-69cd7c8408c0" name="jetbrains.mps.baseLanguage.regexp" version="0" />
<devkit ref="2677cb18-f558-4e33-bc38-a5139cee06dc(jetbrains.mps.devkit.language-design)" />

557
samples/fitch/languages/jetbrains.mps.logic.propositional/models/types.mps
View File

@ -2,9 +2,9 @@
<model ref="r:30d249b0-c2b0-4934-8bd8-e1d7a37c3b3b(jetbrains.mps.logic.propositional.types)">
<persistence version="9" />
<languages>
<use id="c4803b19-6d89-4a3b-bf82-390769514add" name="jetbrains.mps.lang.typesystem2" version="7" />
<use id="f3061a53-9226-4cc5-a443-f952ceaf5816" name="jetbrains.mps.baseLanguage" version="5" />
<use id="7866978e-a0f0-4cc7-81bc-4d213d9375e1" name="jetbrains.mps.lang.smodel" version="8" />
<use id="c4803b19-6d89-4a3b-bf82-390769514add" name="jetbrains.mps.lang.typesystem2" version="8" />
<use id="f3061a53-9226-4cc5-a443-f952ceaf5816" name="jetbrains.mps.baseLanguage" version="6" />
<use id="7866978e-a0f0-4cc7-81bc-4d213d9375e1" name="jetbrains.mps.lang.smodel" version="11" />
<use id="35320f26-77cb-4c55-be9f-a97a27770af1" name="jetbrains.mps.logic" version="2" />
<use id="83888646-71ce-4f1c-9c53-c54016f6ad4f" name="jetbrains.mps.baseLanguage.collections" version="0" />
<devkit ref="2677cb18-f558-4e33-bc38-a5139cee06dc(jetbrains.mps.devkit.language-design)" />
@ -151,6 +151,9 @@
<concept id="1176501494711" name="jetbrains.mps.baseLanguage.collections.structure.IsNotEmptyOperation" flags="nn" index="3GX2aA" />
</language>
<language id="c4803b19-6d89-4a3b-bf82-390769514add" name="jetbrains.mps.lang.typesystem2">
<concept id="8456919074560454386" name="jetbrains.mps.lang.typesystem2.structure.ParameterContainer" flags="ng" index="0eUR_">
<child id="8456919074560454898" name="parameter" index="0eVf_" />
</concept>
<concept id="1618328391714701929" name="jetbrains.mps.lang.typesystem2.structure.TermTemplate" flags="ng" index="0oftK">
<child id="1618328391714701961" name="feature" index="0ofug" />
</concept>
@ -206,6 +209,7 @@
<child id="8908809128801951592" name="code" index="3uniRr" />
</concept>
<concept id="5372587443975633709" name="jetbrains.mps.lang.typesystem2.structure.AbstractRule" flags="ng" index="3wqRzX">
<child id="8456919074560456757" name="parameter" index="0eVGy" />
<child id="7509376976631847095" name="input" index="20_v8_" />
<child id="1427485783570316357" name="head" index="3orSU4" />
<child id="1427485783571962463" name="body" index="3otmyu" />
@ -223,7 +227,6 @@
</concept>
<concept id="7368070394766963523" name="jetbrains.mps.lang.typesystem2.structure.RuleComponent" flags="ng" index="3Aq9uZ">
<child id="2316688792939037645" name="logic" index="3Ip0Jz" />
<child id="965748826975413053" name="parameter" index="3Nuqhd" />
</concept>
<concept id="7368070394766966388" name="jetbrains.mps.lang.typesystem2.structure.Body" flags="ng" index="3Aq9E8" />
<concept id="7368070394766978092" name="jetbrains.mps.lang.typesystem2.structure.EmitConstraintStatement" flags="ng" index="3Aqczg">
@ -953,11 +956,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="2aBGSFgfAEt" role="3Nuqhd">
<node concept="aZer4" id="2aBGSFgfAEu" role="3XD1gS">
<property role="TrG5h" value="Stc" />
</node>
</node>
</node>
<node concept="2t___k" id="2aBGSFgfAE8" role="20_v8_">
<ref role="2t_S0q" to="jfgh:3JXBM6C3FsA" resolve="Judgement" />
@ -965,6 +963,13 @@
<property role="TrG5h" value="jdg" />
</node>
</node>
<node concept="0eUR_" id="3dsgZciwamm" role="0eVGy">
<node concept="3NuqgR" id="2aBGSFgfAEt" role="0eVf_">
<node concept="aZer4" id="2aBGSFgfAEu" role="3XD1gS">
<property role="TrG5h" value="Stc" />
</node>
</node>
</node>
</node>
<node concept="AVZhu" id="5jVx7S22gUI" role="3ArX_J">
<property role="TrG5h" value="premise_valid" />
@ -1015,7 +1020,9 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="5jVx7S22gV2" role="3Nuqhd">
</node>
<node concept="0eUR_" id="3dsgZciwama" role="0eVGy">
<node concept="3NuqgR" id="5jVx7S22gV2" role="0eVf_">
<node concept="aZer4" id="5jVx7S22gV3" role="3XD1gS">
<property role="TrG5h" value="Stc" />
</node>
@ -1071,7 +1078,9 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="5RfK0kxl_zV" role="3Nuqhd">
</node>
<node concept="0eUR_" id="3dsgZciwamg" role="0eVGy">
<node concept="3NuqgR" id="5RfK0kxl_zV" role="0eVf_">
<node concept="aZer4" id="2aBGSFgfVxh" role="3XD1gS">
<property role="TrG5h" value="Stc" />
</node>
@ -1142,14 +1151,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="5jVx7S217sO" role="3Nuqhd">
<node concept="aZer4" id="5jVx7S21pW_" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="5jVx7S217sP" role="3XD1gS">
<property role="TrG5h" value="Ass" />
</node>
</node>
</node>
<node concept="3Aq93q" id="5jVx7S21pWi" role="3orSU4">
<property role="3ArMco" value="true" />
@ -1207,6 +1208,16 @@
</node>
</node>
</node>
<node concept="0eUR_" id="3dsgZciwam1" role="0eVGy">
<node concept="3NuqgR" id="5jVx7S217sO" role="0eVf_">
<node concept="aZer4" id="5jVx7S21pW_" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="5jVx7S217sP" role="3XD1gS">
<property role="TrG5h" value="Ass" />
</node>
</node>
</node>
</node>
<node concept="AVZhu" id="2AfSc6Jv_r_" role="3ArX_J">
<property role="TrG5h" value="and_intro1" />
@ -1333,17 +1344,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="2AfSc6JvIq_" role="3Nuqhd">
<node concept="aZer4" id="2AfSc6JvIqA" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="2AfSc6JvIqJ" role="3XD1gS">
<property role="TrG5h" value="Prem1" />
</node>
<node concept="aZer4" id="2AfSc6JvIr1" role="3XD1gS">
<property role="TrG5h" value="Prem2" />
</node>
</node>
</node>
<node concept="3Aq93q" id="2AfSc6JvNhR" role="3orSU4">
<property role="3ArMco" value="true" />
@ -1428,6 +1428,19 @@
</node>
</node>
</node>
<node concept="0eUR_" id="3dsgZciwamf" role="0eVGy">
<node concept="3NuqgR" id="2AfSc6JvIq_" role="0eVf_">
<node concept="aZer4" id="2AfSc6JvIqA" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="2AfSc6JvIqJ" role="3XD1gS">
<property role="TrG5h" value="Prem1" />
</node>
<node concept="aZer4" id="2AfSc6JvIr1" role="3XD1gS">
<property role="TrG5h" value="Prem2" />
</node>
</node>
</node>
</node>
<node concept="AVZhu" id="2AfSc6JvO60" role="3ArX_J">
<property role="TrG5h" value="and_intro2" />
@ -1554,17 +1567,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="2AfSc6JvO6O" role="3Nuqhd">
<node concept="aZer4" id="2AfSc6JvO6P" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="2AfSc6JvO6Q" role="3XD1gS">
<property role="TrG5h" value="Prem1" />
</node>
<node concept="aZer4" id="2AfSc6JvO6R" role="3XD1gS">
<property role="TrG5h" value="Prem2" />
</node>
</node>
</node>
<node concept="3Aq93q" id="2AfSc6JvO6S" role="3orSU4">
<property role="3ArMco" value="true" />
@ -1649,6 +1651,19 @@
</node>
</node>
</node>
<node concept="0eUR_" id="3dsgZciwamc" role="0eVGy">
<node concept="3NuqgR" id="2AfSc6JvO6O" role="0eVf_">
<node concept="aZer4" id="2AfSc6JvO6P" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="2AfSc6JvO6Q" role="3XD1gS">
<property role="TrG5h" value="Prem1" />
</node>
<node concept="aZer4" id="2AfSc6JvO6R" role="3XD1gS">
<property role="TrG5h" value="Prem2" />
</node>
</node>
</node>
</node>
<node concept="AVZhu" id="2AfSc6Jw7DR" role="3ArX_J">
<property role="TrG5h" value="and_elim1" />
@ -1737,14 +1752,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="2AfSc6JwgnT" role="3Nuqhd">
<node concept="aZer4" id="2AfSc6JwgnU" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="2AfSc6Jwgo9" role="3XD1gS">
<property role="TrG5h" value="Prem" />
</node>
</node>
</node>
<node concept="3Aq93q" id="2AfSc6JwnRE" role="3orSU4">
<property role="3ArMco" value="true" />
@ -1802,6 +1809,16 @@
</node>
</node>
</node>
<node concept="0eUR_" id="3dsgZciwam5" role="0eVGy">
<node concept="3NuqgR" id="2AfSc6JwgnT" role="0eVf_">
<node concept="aZer4" id="2AfSc6JwgnU" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="2AfSc6Jwgo9" role="3XD1gS">
<property role="TrG5h" value="Prem" />
</node>
</node>
</node>
</node>
<node concept="AVZhu" id="2AfSc6Jw_So" role="3ArX_J">
<property role="TrG5h" value="and_elim2" />
@ -1890,14 +1907,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="2AfSc6Jw_T4" role="3Nuqhd">
<node concept="aZer4" id="2AfSc6Jw_T5" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="2AfSc6Jw_T6" role="3XD1gS">
<property role="TrG5h" value="Prem" />
</node>
</node>
</node>
<node concept="3Aq93q" id="2AfSc6Jw_T7" role="3orSU4">
<property role="3ArMco" value="true" />
@ -1955,6 +1964,16 @@
</node>
</node>
</node>
<node concept="0eUR_" id="3dsgZciwamh" role="0eVGy">
<node concept="3NuqgR" id="2AfSc6Jw_T4" role="0eVf_">
<node concept="aZer4" id="2AfSc6Jw_T5" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="2AfSc6Jw_T6" role="3XD1gS">
<property role="TrG5h" value="Prem" />
</node>
</node>
</node>
</node>
<node concept="AVZhu" id="2aBGSFgfrJr" role="3ArX_J">
<property role="TrG5h" value="orIntro_valid1" />
@ -2029,14 +2048,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="2aBGSFgfwOw" role="3Nuqhd">
<node concept="aZer4" id="2aBGSFgfFks" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="2aBGSFgfwOx" role="3XD1gS">
<property role="TrG5h" value="Prem" />
</node>
</node>
</node>
<node concept="3Aq93q" id="2YqrT$P6wDP" role="3orSU4">
<property role="3ArMco" value="true" />
@ -2103,6 +2114,16 @@
</node>
</node>
</node>
<node concept="0eUR_" id="3dsgZciwami" role="0eVGy">
<node concept="3NuqgR" id="2aBGSFgfwOw" role="0eVf_">
<node concept="aZer4" id="2aBGSFgfFks" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="2aBGSFgfwOx" role="3XD1gS">
<property role="TrG5h" value="Prem" />
</node>
</node>
</node>
</node>
<node concept="AVZhu" id="2aBGSFgfGfo" role="3ArX_J">
<property role="TrG5h" value="orIntro_valid2" />
@ -2177,14 +2198,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="2aBGSFgfGfQ" role="3Nuqhd">
<node concept="aZer4" id="2aBGSFgfGfR" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="2aBGSFgfGfS" role="3XD1gS">
<property role="TrG5h" value="Prem" />
</node>
</node>
</node>
<node concept="3Aq93q" id="2YqrT$P6AUH" role="3orSU4">
<property role="3ArMco" value="true" />
@ -2251,6 +2264,16 @@
</node>
</node>
</node>
<node concept="0eUR_" id="3dsgZciwamd" role="0eVGy">
<node concept="3NuqgR" id="2aBGSFgfGfQ" role="0eVf_">
<node concept="aZer4" id="2aBGSFgfGfR" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="2aBGSFgfGfS" role="3XD1gS">
<property role="TrG5h" value="Prem" />
</node>
</node>
</node>
</node>
<node concept="AVZhu" id="2AfSc6JyKIL" role="3ArX_J">
<property role="TrG5h" value="orElim_valid1" />
@ -2471,26 +2494,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="2AfSc6JyU4Q" role="3Nuqhd">
<node concept="aZer4" id="2AfSc6JyU4R" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="3l440nVo6AP" role="3XD1gS">
<property role="TrG5h" value="PremOr" />
</node>
<node concept="aZer4" id="3l440nVnmQi" role="3XD1gS">
<property role="TrG5h" value="Disj1" />
</node>
<node concept="aZer4" id="3l440nVnmVa" role="3XD1gS">
<property role="TrG5h" value="Disj2" />
</node>
<node concept="aZer4" id="2AfSc6JyU68" role="3XD1gS">
<property role="TrG5h" value="PremIf1" />
</node>
<node concept="aZer4" id="2AfSc6JyU6p" role="3XD1gS">
<property role="TrG5h" value="PremIf2" />
</node>
</node>
</node>
<node concept="3Aq93q" id="2AfSc6JyZJE" role="3orSU4">
<property role="3ArMco" value="true" />
@ -2600,6 +2603,28 @@
</node>
</node>
</node>
<node concept="0eUR_" id="3dsgZciwamj" role="0eVGy">
<node concept="3NuqgR" id="2AfSc6JyU4Q" role="0eVf_">
<node concept="aZer4" id="2AfSc6JyU4R" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="3l440nVo6AP" role="3XD1gS">
<property role="TrG5h" value="PremOr" />
</node>
<node concept="aZer4" id="3l440nVnmQi" role="3XD1gS">
<property role="TrG5h" value="Disj1" />
</node>
<node concept="aZer4" id="3l440nVnmVa" role="3XD1gS">
<property role="TrG5h" value="Disj2" />
</node>
<node concept="aZer4" id="2AfSc6JyU68" role="3XD1gS">
<property role="TrG5h" value="PremIf1" />
</node>
<node concept="aZer4" id="2AfSc6JyU6p" role="3XD1gS">
<property role="TrG5h" value="PremIf2" />
</node>
</node>
</node>
</node>
<node concept="AVZhu" id="3l440nVo7RX" role="3ArX_J">
<property role="TrG5h" value="orElim_valid2" />
@ -2820,26 +2845,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="3l440nVo7Ti" role="3Nuqhd">
<node concept="aZer4" id="3l440nVo7Tj" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="3l440nVo7Tk" role="3XD1gS">
<property role="TrG5h" value="PremOr" />
</node>
<node concept="aZer4" id="3l440nVo7Tl" role="3XD1gS">
<property role="TrG5h" value="Disj1" />
</node>
<node concept="aZer4" id="3l440nVo7Tm" role="3XD1gS">
<property role="TrG5h" value="Disj2" />
</node>
<node concept="aZer4" id="3l440nVo7Tn" role="3XD1gS">
<property role="TrG5h" value="PremIf1" />
</node>
<node concept="aZer4" id="3l440nVo7To" role="3XD1gS">
<property role="TrG5h" value="PremIf2" />
</node>
</node>
</node>
<node concept="3Aq93q" id="3l440nVo7Tp" role="3orSU4">
<property role="3ArMco" value="true" />
@ -2949,6 +2954,28 @@
</node>
</node>
</node>
<node concept="0eUR_" id="3dsgZciwam7" role="0eVGy">
<node concept="3NuqgR" id="3l440nVo7Ti" role="0eVf_">
<node concept="aZer4" id="3l440nVo7Tj" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="3l440nVo7Tk" role="3XD1gS">
<property role="TrG5h" value="PremOr" />
</node>
<node concept="aZer4" id="3l440nVo7Tl" role="3XD1gS">
<property role="TrG5h" value="Disj1" />
</node>
<node concept="aZer4" id="3l440nVo7Tm" role="3XD1gS">
<property role="TrG5h" value="Disj2" />
</node>
<node concept="aZer4" id="3l440nVo7Tn" role="3XD1gS">
<property role="TrG5h" value="PremIf1" />
</node>
<node concept="aZer4" id="3l440nVo7To" role="3XD1gS">
<property role="TrG5h" value="PremIf2" />
</node>
</node>
</node>
</node>
<node concept="AVZhu" id="2YqrT$P4vBU" role="3ArX_J">
<property role="TrG5h" value="notIntro_valid1" />
@ -3128,17 +3155,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="2YqrT$P4CCj" role="3Nuqhd">
<node concept="aZer4" id="2YqrT$P4D5$" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="2YqrT$P4CCk" role="3XD1gS">
<property role="TrG5h" value="PremAtcd" />
</node>
<node concept="aZer4" id="2YqrT$P4CCw" role="3XD1gS">
<property role="TrG5h" value="PremCsq" />
</node>
</node>
</node>
<node concept="3Aq93q" id="2YqrT$P6B1z" role="3orSU4">
<property role="3ArMco" value="true" />
@ -3223,6 +3239,19 @@
</node>
</node>
</node>
<node concept="0eUR_" id="3dsgZciwamb" role="0eVGy">
<node concept="3NuqgR" id="2YqrT$P4CCj" role="0eVf_">
<node concept="aZer4" id="2YqrT$P4D5$" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="2YqrT$P4CCk" role="3XD1gS">
<property role="TrG5h" value="PremAtcd" />
</node>
<node concept="aZer4" id="2YqrT$P4CCw" role="3XD1gS">
<property role="TrG5h" value="PremCsq" />
</node>
</node>
</node>
</node>
<node concept="AVZhu" id="2YqrT$P4Iqr" role="3ArX_J">
<property role="TrG5h" value="notIntro_valid2" />
@ -3402,17 +3431,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="2YqrT$P4Irv" role="3Nuqhd">
<node concept="aZer4" id="2YqrT$P4Irw" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="2YqrT$P4Irx" role="3XD1gS">
<property role="TrG5h" value="PremAtcd" />
</node>
<node concept="aZer4" id="2YqrT$P4Iry" role="3XD1gS">
<property role="TrG5h" value="PremCsq" />
</node>
</node>
</node>
<node concept="3Aq93q" id="2YqrT$P6D$T" role="3orSU4">
<property role="3ArMco" value="true" />
@ -3497,6 +3515,19 @@
</node>
</node>
</node>
<node concept="0eUR_" id="3dsgZciwamn" role="0eVGy">
<node concept="3NuqgR" id="2YqrT$P4Irv" role="0eVf_">
<node concept="aZer4" id="2YqrT$P4Irw" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="2YqrT$P4Irx" role="3XD1gS">
<property role="TrG5h" value="PremAtcd" />
</node>
<node concept="aZer4" id="2YqrT$P4Iry" role="3XD1gS">
<property role="TrG5h" value="PremCsq" />
</node>
</node>
</node>
</node>
<node concept="AVZhu" id="2YqrT$P4RUb" role="3ArX_J">
<property role="TrG5h" value="notElim_valid" />
@ -3590,14 +3621,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="2YqrT$P4S08" role="3Nuqhd">
<node concept="aZer4" id="2YqrT$P4S09" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="2YqrT$P54za" role="3XD1gS">
<property role="TrG5h" value="Prem" />
</node>
</node>
</node>
<node concept="3Aq93q" id="2YqrT$P6DId" role="3orSU4">
<property role="3ArMco" value="true" />
@ -3628,11 +3651,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="2YqrT$P6DI_" role="3Nuqhd">
<node concept="aZer4" id="2YqrT$P6DIA" role="3XD1gS">
<property role="TrG5h" value="OK" />
</node>
</node>
</node>
<node concept="2t___k" id="2YqrT$P4RZQ" role="20_v8_">
<ref role="2t_S0q" to="27wh:3JXBM6C3ZJ8" resolve="NotElim" />
@ -3662,6 +3680,21 @@
</node>
</node>
</node>
<node concept="0eUR_" id="3dsgZciwam8" role="0eVGy">
<node concept="3NuqgR" id="2YqrT$P4S08" role="0eVf_">
<node concept="aZer4" id="2YqrT$P4S09" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="2YqrT$P54za" role="3XD1gS">
<property role="TrG5h" value="Prem" />
</node>
</node>
<node concept="3NuqgR" id="2YqrT$P6DI_" role="0eVf_">
<node concept="aZer4" id="2YqrT$P6DIA" role="3XD1gS">
<property role="TrG5h" value="OK" />
</node>
</node>
</node>
</node>
<node concept="AVZhu" id="2YqrT$P5VD9" role="3ArX_J">
<property role="TrG5h" value="IfIntro_valid" />
@ -3809,17 +3842,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="2YqrT$P64rX" role="3Nuqhd">
<node concept="aZer4" id="2YqrT$P64rY" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="2YqrT$P64s7" role="3XD1gS">
<property role="TrG5h" value="Atcd" />
</node>
<node concept="aZer4" id="2YqrT$P64tc" role="3XD1gS">
<property role="TrG5h" value="Csqt" />
</node>
</node>
</node>
<node concept="3Aq93q" id="2YqrT$P6EGB" role="3orSU4">
<property role="3ArMco" value="true" />
@ -3928,6 +3950,19 @@
</node>
</node>
</node>
<node concept="0eUR_" id="3dsgZciwam4" role="0eVGy">
<node concept="3NuqgR" id="2YqrT$P64rX" role="0eVf_">
<node concept="aZer4" id="2YqrT$P64rY" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="2YqrT$P64s7" role="3XD1gS">
<property role="TrG5h" value="Atcd" />
</node>
<node concept="aZer4" id="2YqrT$P64tc" role="3XD1gS">
<property role="TrG5h" value="Csqt" />
</node>
</node>
</node>
</node>
<node concept="AVZhu" id="2AfSc6JxXJ4" role="3ArX_J">
<property role="TrG5h" value="IfIntro_valid_singular" />
@ -4035,14 +4070,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="2AfSc6JxXK2" role="3Nuqhd">
<node concept="aZer4" id="2AfSc6JxXK3" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="2AfSc6JxXK4" role="3XD1gS">
<property role="TrG5h" value="Ass" />
</node>
</node>
</node>
<node concept="3Aq93q" id="2AfSc6JxXK6" role="3orSU4">
<property role="3ArMco" value="true" />
@ -4151,6 +4178,16 @@
</node>
</node>
</node>
<node concept="0eUR_" id="3dsgZciwam6" role="0eVGy">
<node concept="3NuqgR" id="2AfSc6JxXK2" role="0eVf_">
<node concept="aZer4" id="2AfSc6JxXK3" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="2AfSc6JxXK4" role="3XD1gS">
<property role="TrG5h" value="Ass" />
</node>
</node>
</node>
</node>
<node concept="AVZhu" id="2AfSc6JuwTt" role="3ArX_J">
<property role="TrG5h" value="IfElim_valid" />
@ -4274,17 +4311,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="2AfSc6JuwUr" role="3Nuqhd">
<node concept="aZer4" id="2AfSc6JuwUs" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="2AfSc6JuA9o" role="3XD1gS">
<property role="TrG5h" value="AtcdPrem" />
</node>
<node concept="aZer4" id="2AfSc6Juz0Q" role="3XD1gS">
<property role="TrG5h" value="IfPrem" />
</node>
</node>
</node>
<node concept="3Aq93q" id="2AfSc6JuwUv" role="3orSU4">
<property role="3ArMco" value="true" />
@ -4369,6 +4395,19 @@
</node>
</node>
</node>
<node concept="0eUR_" id="3dsgZciwam0" role="0eVGy">
<node concept="3NuqgR" id="2AfSc6JuwUr" role="0eVf_">
<node concept="aZer4" id="2AfSc6JuwUs" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="2AfSc6JuA9o" role="3XD1gS">
<property role="TrG5h" value="AtcdPrem" />
</node>
<node concept="aZer4" id="2AfSc6Juz0Q" role="3XD1gS">
<property role="TrG5h" value="IfPrem" />
</node>
</node>
</node>
</node>
<node concept="AVZhu" id="3l440nVrAaZ" role="3ArX_J">
<property role="TrG5h" value="IffIntro_valid1" />
@ -4558,23 +4597,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="3l440nVrMcf" role="3Nuqhd">
<node concept="aZer4" id="3l440nVrMcg" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="3l440nVrMcp" role="3XD1gS">
<property role="TrG5h" value="Atcd" />
</node>
<node concept="aZer4" id="3l440nVrMcF" role="3XD1gS">
<property role="TrG5h" value="Csqt" />
</node>
<node concept="aZer4" id="3l440nVrMrr" role="3XD1gS">
<property role="TrG5h" value="Prem1" />
</node>
<node concept="aZer4" id="3l440nVrMuk" role="3XD1gS">
<property role="TrG5h" value="Prem2" />
</node>
</node>
</node>
<node concept="3Aq93q" id="3l440nVrUnb" role="3orSU4">
<property role="3ArMco" value="true" />
@ -4659,6 +4681,25 @@
</node>
</node>
</node>
<node concept="0eUR_" id="3dsgZciwam2" role="0eVGy">
<node concept="3NuqgR" id="3l440nVrMcf" role="0eVf_">
<node concept="aZer4" id="3l440nVrMcg" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="3l440nVrMcp" role="3XD1gS">
<property role="TrG5h" value="Atcd" />
</node>
<node concept="aZer4" id="3l440nVrMcF" role="3XD1gS">
<property role="TrG5h" value="Csqt" />
</node>
<node concept="aZer4" id="3l440nVrMrr" role="3XD1gS">
<property role="TrG5h" value="Prem1" />
</node>
<node concept="aZer4" id="3l440nVrMuk" role="3XD1gS">
<property role="TrG5h" value="Prem2" />
</node>
</node>
</node>
</node>
<node concept="AVZhu" id="3l440nVrS79" role="3ArX_J">
<property role="TrG5h" value="IffIntro_valid2" />
@ -4848,23 +4889,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="3l440nVrS8h" role="3Nuqhd">
<node concept="aZer4" id="3l440nVrS8i" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="3l440nVrS8j" role="3XD1gS">
<property role="TrG5h" value="Atcd" />
</node>
<node concept="aZer4" id="3l440nVrS8k" role="3XD1gS">
<property role="TrG5h" value="Csqt" />
</node>
<node concept="aZer4" id="3l440nVrS8l" role="3XD1gS">
<property role="TrG5h" value="Prem1" />
</node>
<node concept="aZer4" id="3l440nVrS8m" role="3XD1gS">
<property role="TrG5h" value="Prem2" />
</node>
</node>
</node>
<node concept="2t___k" id="3l440nVrS8n" role="20_v8_">
<ref role="2t_S0q" to="27wh:3JXBM6C3ZJn" resolve="IffIntro" />
@ -4894,6 +4918,25 @@
</node>
</node>
</node>
<node concept="0eUR_" id="3dsgZciwam3" role="0eVGy">
<node concept="3NuqgR" id="3l440nVrS8h" role="0eVf_">
<node concept="aZer4" id="3l440nVrS8i" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="3l440nVrS8j" role="3XD1gS">
<property role="TrG5h" value="Atcd" />
</node>
<node concept="aZer4" id="3l440nVrS8k" role="3XD1gS">
<property role="TrG5h" value="Csqt" />
</node>
<node concept="aZer4" id="3l440nVrS8l" role="3XD1gS">
<property role="TrG5h" value="Prem1" />
</node>
<node concept="aZer4" id="3l440nVrS8m" role="3XD1gS">
<property role="TrG5h" value="Prem2" />
</node>
</node>
</node>
</node>
<node concept="AVZhu" id="3l440nVqpRf" role="3ArX_J">
<property role="TrG5h" value="IffElim_valid1" />
@ -5020,20 +5063,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="3l440nVqBe8" role="3Nuqhd">
<node concept="aZer4" id="3l440nVqBe9" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="3l440nVqBi1" role="3XD1gS">
<property role="TrG5h" value="Prem" />
</node>
<node concept="aZer4" id="3l440nVqBii" role="3XD1gS">
<property role="TrG5h" value="Acdt" />
</node>
<node concept="aZer4" id="3l440nVqBiE" role="3XD1gS">
<property role="TrG5h" value="Csqt" />
</node>
</node>
</node>
<node concept="3Aq93q" id="3l440nVqJdt" role="3orSU4">
<property role="3ArMco" value="true" />
@ -5091,6 +5120,22 @@
</node>
</node>
</node>
<node concept="0eUR_" id="3dsgZciwame" role="0eVGy">
<node concept="3NuqgR" id="3l440nVqBe8" role="0eVf_">
<node concept="aZer4" id="3l440nVqBe9" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="3l440nVqBi1" role="3XD1gS">
<property role="TrG5h" value="Prem" />
</node>
<node concept="aZer4" id="3l440nVqBii" role="3XD1gS">
<property role="TrG5h" value="Acdt" />
</node>
<node concept="aZer4" id="3l440nVqBiE" role="3XD1gS">
<property role="TrG5h" value="Csqt" />
</node>
</node>
</node>
</node>
<node concept="AVZhu" id="3l440nVqJk_" role="3ArX_J">
<property role="TrG5h" value="IffElim_valid2" />
@ -5217,20 +5262,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="3l440nVqJlq" role="3Nuqhd">
<node concept="aZer4" id="3l440nVqJlr" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="3l440nVqJls" role="3XD1gS">
<property role="TrG5h" value="Prem" />
</node>
<node concept="aZer4" id="3l440nVqJlt" role="3XD1gS">
<property role="TrG5h" value="Acdt" />
</node>
<node concept="aZer4" id="3l440nVqJlu" role="3XD1gS">
<property role="TrG5h" value="Csqt" />
</node>
</node>
</node>
<node concept="3Aq93q" id="3l440nVqJlv" role="3orSU4">
<property role="3ArMco" value="true" />
@ -5288,6 +5319,22 @@
</node>
</node>
</node>
<node concept="0eUR_" id="3dsgZciwaml" role="0eVGy">
<node concept="3NuqgR" id="3l440nVqJlq" role="0eVf_">
<node concept="aZer4" id="3l440nVqJlr" role="3XD1gS">
<property role="TrG5h" value="Con" />
</node>
<node concept="aZer4" id="3l440nVqJls" role="3XD1gS">
<property role="TrG5h" value="Prem" />
</node>
<node concept="aZer4" id="3l440nVqJlt" role="3XD1gS">
<property role="TrG5h" value="Acdt" />
</node>
<node concept="aZer4" id="3l440nVqJlu" role="3XD1gS">
<property role="TrG5h" value="Csqt" />
</node>
</node>
</node>
</node>
<node concept="AVZhu" id="2AfSc6JuwTb" role="3ArX_J">
<property role="TrG5h" value="goal" />
@ -5322,11 +5369,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="2AfSc6JuwTp" role="3Nuqhd">
<node concept="aZer4" id="2AfSc6JuwTq" role="3XD1gS">
<property role="TrG5h" value="Goal" />
</node>
</node>
</node>
<node concept="2t___k" id="2AfSc6JuwTr" role="20_v8_">
<ref role="2t_S0q" to="jfgh:$u9BK__SA8" resolve="Goal" />
@ -5334,6 +5376,13 @@
<property role="TrG5h" value="goal" />
</node>
</node>
<node concept="0eUR_" id="3dsgZciwam9" role="0eVGy">
<node concept="3NuqgR" id="2AfSc6JuwTp" role="0eVf_">
<node concept="aZer4" id="2AfSc6JuwTq" role="3XD1gS">
<property role="TrG5h" value="Goal" />
</node>
</node>
</node>
</node>
<node concept="AVZhu" id="2YqrT$P7HVI" role="3ArX_J">
<property role="TrG5h" value="goal_valid" />
@ -5395,14 +5444,6 @@
</node>
</node>
</node>
<node concept="3NuqgR" id="2YqrT$P7QXy" role="3Nuqhd">
<node concept="aZer4" id="2YqrT$P7QXz" role="3XD1gS">
<property role="TrG5h" value="Goal" />
</node>
<node concept="aZer4" id="2YqrT$P7QXD" role="3XD1gS">
<property role="TrG5h" value="ProofCon" />
</node>
</node>
</node>
<node concept="3Aq93q" id="2YqrT$P7I4B" role="3orSU4">
<property role="3ArMco" value="true" />
@ -5489,6 +5530,16 @@
</node>
</node>
</node>
<node concept="0eUR_" id="3dsgZciwamk" role="0eVGy">
<node concept="3NuqgR" id="2YqrT$P7QXy" role="0eVf_">
<node concept="aZer4" id="2YqrT$P7QXz" role="3XD1gS">
<property role="TrG5h" value="Goal" />
</node>
<node concept="aZer4" id="2YqrT$P7QXD" role="3XD1gS">
<property role="TrG5h" value="ProofCon" />
</node>
</node>
</node>
</node>
<node concept="3AqmO8" id="2aBGSFgfwNi" role="8PkJo">
<property role="TrG5h" value="conclusion" />