--- /dev/null
+package com.example.furt.myapplication;
+
+
+import java.util.ArrayList;
+import java.util.List;
+
+public class FormulaOr extends GenericFormula implements Formula
+{
+ Formula leftF;
+ Formula rightF;
+ int leftPriority;
+ int rightPriority;
+ FormulaOr(Formula F1,Formula F2)
+ {
+ priority=13;
+ leftF=F1;
+ rightF=F2;
+ leftPriority=13;
+ rightPriority=14;
+ }
+
+ @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()); //eredita la R.A.A.
+
+ //Introduzione sinistra dell'or
+ RuleIntroduction orIntroductionLeft=new RuleIntroduction("∨i(L)",6);
+ Node orLeft=new Node(leftF);
+ Node thisNodeL=new Node(this);
+ thisNodeL.addChild(orLeft);
+ orIntroductionLeft.tempRule=thisNodeL;
+ nodes.add(orIntroductionLeft);
+
+ //Introduzione destra dell'or
+ RuleIntroduction orIntroductionRight=new RuleIntroduction("∨i(R)",5);
+ Node orRight=new Node(rightF);
+ Node thisNodeR=new Node(this);
+ thisNodeR.addChild(orRight);
+ orIntroductionRight.tempRule=thisNodeR;
+ nodes.add(orIntroductionRight);
+
+ return nodes;
+ }
+
+ public List<EliminationRule> EliminationRules()
+ {
+ List<EliminationRule> nodes=new ArrayList<EliminationRule>();
+ nodes.add(new RuleOrElimination(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 FormulaOr(leftF.duplicate(),rightF.duplicate());
+ }
+}
+