Ported to latest version of Android SDK

[logicplayer.git] / mainActivity / app / src / main / java / com / example / furt / myapplication / RuleImplElimination.java

diff --git a/mainActivity/app/src/main/java/com/example/furt/myapplication/RuleImplElimination.java b/mainActivity/app/src/main/java/com/example/furt/myapplication/RuleImplElimination.java
new file mode 100644 (file)
index 0000000..f2fd1ff
--- /dev/null
+++ b/mainActivity/app/src/main/java/com/example/furt/myapplication/RuleImplElimination.java
@@ -0,0 +1,31 @@
+package com.example.furt.myapplication;
+
+public class RuleImplElimination implements EliminationRule
+{
+    String ruleName;
+    FormulaImpl Fn;
+    RuleImplElimination(FormulaImpl F)
+    {
+        Fn=F;
+        ruleName="⇒e";
+    }
+    public Node createNodes(Formula F,askFormula ask)
+    {
+        Formula C;
+        if (F==null) {
+            C=ask.Ask();
+            if (!(C.toString().equals(Fn.rightF.toString())))
+                return null;
+        }
+        else
+            if (!(F.toString().equals(Fn.rightF.toString())))
+                return null;
+            Node elNode=new Node(Fn);
+            Node lNode=new Node(Fn.leftF);
+            Node bNode=new Node(Fn.rightF);
+            bNode.addChild(elNode);
+            bNode.addChild(lNode);
+            bNode.ruleName=ruleName;
+            return bNode;
+    }
+}