--- /dev/null
+package com.example.furt.myapplication;
+
+import java.util.ArrayList;
+import java.util.List;
+
+public class FormulaImpl extends GenericFormula implements Formula
+{
+ Formula leftF;
+ Formula rightF;
+ int leftPriority;
+ int rightPriority;
+ FormulaImpl(Formula F1,Formula F2)
+ {
+ priority=10;
+ leftF=F1;
+ rightF=F2;
+ leftPriority=11;
+ rightPriority=10;
+ }
+ @Override
+ public String Draw(int p)
+ {
+ if (priority >= p)
+ return leftF.Draw(leftPriority)+"⇒"+rightF.Draw(rightPriority);
+ else
+ return("(")+leftF.Draw(leftPriority)+"⇒"+rightF.Draw(rightPriority)+")";
+ }
+
+ public List<IntroductionRule> introductionRules(){
+ List<IntroductionRule> nodes=new ArrayList<IntroductionRule>();
+ nodes.addAll(super.introductionRules());
+ RuleIntroduction implIntro=new RuleIntroduction("⇒i",10);
+ Node ImplN=new Node(rightF);
+ List<Formula> implHP=new ArrayList<Formula>();
+ implHP.add(leftF);
+ ImplN.addHPFormula(implHP,true);
+ Node thisNode=new Node(this);
+ thisNode.addChild(ImplN);
+ implIntro.tempRule=thisNode;
+ nodes.add(implIntro);
+ return nodes;
+ }
+ public List<EliminationRule> EliminationRules()
+ {
+ List<EliminationRule> nodes=new ArrayList<EliminationRule>();
+ nodes.add(new RuleImplElimination(this));
+ return nodes;
+ }
+ @Override
+ public boolean Fill(Formula Filler) {
+ if(leftF.toString().equals("_")) {
+ this.leftF = Filler;
+ return true;
+ }
+ else if(rightF.toString().equals("_")) {
+ this.rightF = Filler;
+ return true;
+ }
+ return leftF.Fill(Filler) || rightF.Fill(Filler);
+ }
+
+ @Override
+ public boolean setCursor() {
+ return leftF.setCursor() || rightF.setCursor();
+ }
+
+ @Override
+ public Formula duplicate() {
+ return new FormulaImpl(leftF.duplicate(),rightF.duplicate());
+ }
+}