--- /dev/null
+package com.example.furt.myapplication;
+
+import java.util.ArrayList;
+import java.util.List;
+
+public class FormulaAnd extends GenericFormula implements Formula
+{
+ Formula leftF;
+ Formula rightF;
+ int leftPriority;
+ int rightPriority;
+ FormulaAnd(Formula F1,Formula F2)
+ {
+ leftF=F1;
+ rightF=F2;
+ priority=15;
+ leftPriority=15;
+ rightPriority=16;
+ }
+ @Override
+ public String Draw(int p)
+ {
+ if (priority >= p)
+ return leftF.Draw(leftPriority)+"∧"+rightF.Draw(rightPriority);
+ else
+ return("(")+leftF.Draw(leftPriority)+"∧"+rightF.Draw(rightPriority)+")";
+ }
+
+ @Override
+ public List<IntroductionRule> introductionRules()
+ {
+ List<IntroductionRule> rules=new ArrayList<IntroductionRule>();
+ rules.addAll(super.introductionRules());
+
+ //Regola di introduzione dell'And
+ RuleIntroduction andIntroduction=new RuleIntroduction("∧i",5);
+ Node Left=new Node(leftF);
+ Node Right=new Node(rightF);
+ Node thisNode=new Node(this);
+ thisNode.addChild(Left);
+ thisNode.addChild(Right);
+ andIntroduction.tempRule=thisNode;
+ rules.add(andIntroduction);
+
+ return rules;
+ }
+ public List<EliminationRule> EliminationRules()
+ {
+ List<EliminationRule> nodes=new ArrayList<EliminationRule>();
+ nodes.add(new RuleAndElimination(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 FormulaAnd(leftF.duplicate(),rightF.duplicate());
+ }
+}
+