diff --git a/src/main/antlr4/edu/kit/formal/proofscriptparser/ScriptLanguage.g4 b/src/main/antlr4/edu/kit/formal/proofscriptparser/ScriptLanguage.g4
index 5af4878bdb23431bb02fcc8b080d3392d9ff8229..37304c51157bf313fa559dc3137a9b79a781e991 100644
--- a/src/main/antlr4/edu/kit/formal/proofscriptparser/ScriptLanguage.g4
+++ b/src/main/antlr4/edu/kit/formal/proofscriptparser/ScriptLanguage.g4
@@ -76,8 +76,11 @@ literals :
 
      </pre>*/
 matchPattern
-    :   MATCH (pattern=expression
-        (USING LBRACKET argList RBRACKET)?) | DERIVABLE TERM_LITERAL | IFCLOSED
+    :
+       MATCH (
+         derivable=DERIVABLE derivableExpression=expression
+       | (pattern=expression (USING LBRACKET argList RBRACKET)?)
+       )
     ;
 
 scriptVar
@@ -98,9 +101,17 @@ casesStmt
     ;
 
 casesList
-    :   CASE expression COLON? INDENT stmtList DEDENT
+  //  : simpleCase
+   // | closableCase
+    :   CASE (MATCH ISCLOSED | expression) COLON? INDENT stmtList DEDENT
     ;
-
+/*simpleCase
+    : CASE expression COLON? INDENT stmtList DEDENT
+    ;
+closableCase
+    : CASE MATCH ISCLOSED COLON? INDENT stmtList DEDENT
+    ;
+*/
 forEachStmt
     :   FOREACH INDENT stmtList DEDENT
     ;
@@ -131,6 +142,8 @@ MULTI_LINE_COMMENT  : '/*' (MULTI_LINE_COMMENT|.)*? '*/' -> channel(HIDDEN);
 
 CASES: 'cases';
 CASE: 'case';
+ISCLOSED: 'isCloseable';
+DERIVABLE : 'derivable';
 DEFAULT: 'default';
 ASSIGN : ':=';
 LBRACKET: '[';
@@ -147,8 +160,6 @@ BOOL: 'bool' ;
 TERMTYPE : 'term' ;*/
 FOREACH : 'foreach' ;
 THEONLY : 'theonly' ;
-ISCLOSED: 'isClosable';
-DERIVABLE : 'derivable';
 INDENT : '{' ;
 DEDENT : '}' ;
 SEMICOLON : ';' ;
diff --git a/src/main/java/edu/kit/formal/gui/controls/WelcomePane.java b/src/main/java/edu/kit/formal/gui/controls/WelcomePane.java
index dc18a07c25af01f3bae4c3f05c1e9bd4ac6aee71..df9e3a04857b410663da7959a297d94d0c5e5e07 100644
--- a/src/main/java/edu/kit/formal/gui/controls/WelcomePane.java
+++ b/src/main/java/edu/kit/formal/gui/controls/WelcomePane.java
@@ -21,7 +21,7 @@ public class WelcomePane extends AnchorPane {
         proofScriptDebugger.getWelcomePaneDock().close();
         proofScriptDebugger.showActiveInspector(null);
         proofScriptDebugger.openScript(
-                new File("src/test/resources/edu/kit/formal/interpreter/contraposition/wo_branching.kps")
+                new File("src/test/resources/edu/kit/formal/interpreter/contraposition/w_branching.kps")
         );
 
         proofScriptDebugger.openKeyFile(
diff --git a/src/main/java/edu/kit/formal/interpreter/Evaluator.java b/src/main/java/edu/kit/formal/interpreter/Evaluator.java
index 4d2eb3b531311412f05788fc9ebabfbba5c89903..4dabdaad40bece610edd89f67a6c77b0d00fae97 100644
--- a/src/main/java/edu/kit/formal/interpreter/Evaluator.java
+++ b/src/main/java/edu/kit/formal/interpreter/Evaluator.java
@@ -54,7 +54,7 @@ public class Evaluator<T> extends DefaultASTVisitor<Value> implements ScopeObser
     }
 
     /**
-     * TODO Connect with KeY
+     * Visit a match expression and evaluate expression using matcher
      *
      * @param match
      * @return
@@ -64,16 +64,18 @@ public class Evaluator<T> extends DefaultASTVisitor<Value> implements ScopeObser
         if (match.getSignature() != null && !match.getSignature().isEmpty()) {
             throw new IllegalStateException("not supported");
         }
-
-        Value pattern = (Value) match.getPattern().accept(this);
-
         List<VariableAssignment> va = null;
-        if (pattern.getType() == Type.STRING) {
-            va = matcher.matchLabel(goal, (String) pattern.getData());
-        } else if (pattern.getType() == Type.TERM) {
-            va = matcher.matchSeq(goal, (String) pattern.getData(), match.getSignature());
+        Value pattern = (Value) match.getPattern().accept(this);
+        if (match.isDerivable()) {
+        } else {
+            if (pattern.getType() == Type.STRING) {
+                va = matcher.matchLabel(goal, (String) pattern.getData());
+            } else if (pattern.getType() == Type.TERM) {
+                va = matcher.matchSeq(goal, (String) pattern.getData(), match.getSignature());
+            }
         }
 
+
         return va != null && va.size() > 0 ? Value.TRUE : Value.FALSE;
     }
 
diff --git a/src/main/java/edu/kit/formal/interpreter/Interpreter.java b/src/main/java/edu/kit/formal/interpreter/Interpreter.java
index e9aed5eb92763d88d8c2cd2428cd04aa9d86b49b..8be113e1244896600a6ef51a979aff77426063f0 100644
--- a/src/main/java/edu/kit/formal/interpreter/Interpreter.java
+++ b/src/main/java/edu/kit/formal/interpreter/Interpreter.java
@@ -168,15 +168,19 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
         List<GoalNode<T>> goalsAfterCases = new ArrayList<>();
         //copy the list of goal nodes for keeping track of goals
         Set<GoalNode<T>> remainingGoalsSet = new HashSet<>(allGoalsBeforeCases);
-
+        //TODO
         //handle cases
         List<CaseStatement> cases = casesStatement.getCases();
         for (CaseStatement aCase : cases) {
-            Map<GoalNode<T>, VariableAssignment> matchedGoals =
-                    matchGoal(remainingGoalsSet, aCase);
-            if (matchedGoals != null) {
-                remainingGoalsSet.removeAll(matchedGoals.keySet());
-                goalsAfterCases.addAll(executeCase(aCase.getBody(), matchedGoals));
+            if (aCase.isClosedStmt) {
+                System.out.println("IsClosableStmt not implemented yet");
+            } else {
+                Map<GoalNode<T>, VariableAssignment> matchedGoals =
+                        matchGoal(remainingGoalsSet, (SimpleCaseStatement) aCase);
+                if (matchedGoals != null) {
+                    remainingGoalsSet.removeAll(matchedGoals.keySet());
+                    goalsAfterCases.addAll(executeCase(aCase.getBody(), matchedGoals));
+                }
             }
 
         }
@@ -219,11 +223,12 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
      * @param aCase
      * @return
      */
-    private Map<GoalNode<T>, VariableAssignment> matchGoal(Set<GoalNode<T>> allGoalsBeforeCases, CaseStatement aCase) {
+    private Map<GoalNode<T>, VariableAssignment> matchGoal(Set<GoalNode<T>> allGoalsBeforeCases, SimpleCaseStatement aCase) {
 
         HashMap<GoalNode<T>, VariableAssignment> matchedGoals = new HashMap<>();
         Expression matchExpression = aCase.getGuard();
 
+
         for (GoalNode<T> goal : allGoalsBeforeCases) {
             VariableAssignment va = evaluateMatchInGoal(matchExpression, goal);
             if (va != null) {
diff --git a/src/main/java/edu/kit/formal/interpreter/MatcherApi.java b/src/main/java/edu/kit/formal/interpreter/MatcherApi.java
index bb4854250291dcae75fc388431fa0646d3e50b82..6a82cd8073821c14ad88decc39a2d08a96371db8 100644
--- a/src/main/java/edu/kit/formal/interpreter/MatcherApi.java
+++ b/src/main/java/edu/kit/formal/interpreter/MatcherApi.java
@@ -13,4 +13,5 @@ import java.util.List;
 public interface MatcherApi<T> {
     List<VariableAssignment> matchLabel(GoalNode<T> currentState, String label);
     List<VariableAssignment> matchSeq(GoalNode<T> currentState, String data, Signature sig);
+
 }
diff --git a/src/main/java/edu/kit/formal/interpreter/dbg/Debugger.java b/src/main/java/edu/kit/formal/interpreter/dbg/Debugger.java
index cd2a991bbfdd8e822eef162c61d599ecb2b1e6de..ed1870df19bdc664e49be22ecb2e5b15966b3e77 100644
--- a/src/main/java/edu/kit/formal/interpreter/dbg/Debugger.java
+++ b/src/main/java/edu/kit/formal/interpreter/dbg/Debugger.java
@@ -221,7 +221,7 @@ public class Debugger {
         }
 
         @Override
-        public Void visit(CaseStatement caseStatement) {
+        public Void visit(SimpleCaseStatement caseStatement) {
             suffix(caseStatement);
             System.out.println("case " + Facade.prettyPrint(caseStatement.getGuard()));
             return super.visit(caseStatement);
diff --git a/src/main/java/edu/kit/formal/proofscriptparser/ASTChanger.java b/src/main/java/edu/kit/formal/proofscriptparser/ASTChanger.java
index 5783b53c1c2ebeed880f5cfe95a5fb897818629d..86c468284f666256dcd90e4cf8b58b76c61d47e2 100644
--- a/src/main/java/edu/kit/formal/proofscriptparser/ASTChanger.java
+++ b/src/main/java/edu/kit/formal/proofscriptparser/ASTChanger.java
@@ -110,11 +110,26 @@ public class ASTChanger extends DefaultASTVisitor<ASTNode> {
         return casesStatement;
     }
 
+    @Override
+    public IsClosableCase visit(IsClosableCase isClosableCase) {
+        isClosableCase.getBody().accept(this);
+        return isClosableCase;
+    }
+
+    @Override
+    public SimpleCaseStatement visit(SimpleCaseStatement simpleCaseStatement) {
+        simpleCaseStatement.getGuard().accept(this);
+        simpleCaseStatement.getBody().accept(this);
+        return simpleCaseStatement;
+    }
+
     @Override
     public CaseStatement visit(CaseStatement caseStatement) {
-        caseStatement.getGuard().accept(this);
-        caseStatement.getBody().accept(this);
+        //caseStatement.getGuard().accept(this);
+        //caseStatement.getBody().accept(this);
+        caseStatement.accept(this);
         return caseStatement;
+
     }
 
     @Override
diff --git a/src/main/java/edu/kit/formal/proofscriptparser/ASTTraversal.java b/src/main/java/edu/kit/formal/proofscriptparser/ASTTraversal.java
index 6908d5b66eb1293a864e15cdefd0f19b6a78193a..6557c4258b919d34457aa025e79540f802e278dc 100644
--- a/src/main/java/edu/kit/formal/proofscriptparser/ASTTraversal.java
+++ b/src/main/java/edu/kit/formal/proofscriptparser/ASTTraversal.java
@@ -104,8 +104,8 @@ public interface ASTTraversal<T> extends Visitor<T> {
 
     @Override
     default T visit(CaseStatement caseStatement) {
-        caseStatement.getGuard().accept(this);
-        caseStatement.getBody().accept(this);
+        //caseStatement.getBody().accept(this);
+        caseStatement.accept(this);
         return null;
     }
 
@@ -158,4 +158,17 @@ public interface ASTTraversal<T> extends Visitor<T> {
         e.getExpression().accept(this);
         return null;
     }
+
+    @Override
+    default T visit(IsClosableCase isClosableCase) {
+        isClosableCase.getBody().accept(this);
+        return null;
+    }
+
+    @Override
+    default T visit(SimpleCaseStatement simpleCaseStatement) {
+        simpleCaseStatement.getGuard().accept(this);
+        simpleCaseStatement.getBody().accept(this);
+        return null;
+    }
 }
diff --git a/src/main/java/edu/kit/formal/proofscriptparser/DefaultASTVisitor.java b/src/main/java/edu/kit/formal/proofscriptparser/DefaultASTVisitor.java
index 6f9d3a7a1651696209ba0b14245b1bab7098cf1f..3f4aecf4156ed4bd4f9a002a11bb20586fc4836e 100644
--- a/src/main/java/edu/kit/formal/proofscriptparser/DefaultASTVisitor.java
+++ b/src/main/java/edu/kit/formal/proofscriptparser/DefaultASTVisitor.java
@@ -128,5 +128,15 @@ public class DefaultASTVisitor<T> implements Visitor<T> {
     public T visit(UnaryExpression unaryExpression) {
         return defaultVisit(unaryExpression);
     }
+
+    @Override
+    public T visit(IsClosableCase isClosableCase) {
+        return defaultVisit(isClosableCase);
+    }
+
+    @Override
+    public T visit(SimpleCaseStatement simpleCaseStatement) {
+        return defaultVisit(simpleCaseStatement);
+    }
 }
 
diff --git a/src/main/java/edu/kit/formal/proofscriptparser/PrettyPrinter.java b/src/main/java/edu/kit/formal/proofscriptparser/PrettyPrinter.java
index bedb6a8de2e2876d9c9e13eccf988f115210b9ff..1b4b72381066f0ab8a048337ad6fc529d919d271 100644
--- a/src/main/java/edu/kit/formal/proofscriptparser/PrettyPrinter.java
+++ b/src/main/java/edu/kit/formal/proofscriptparser/PrettyPrinter.java
@@ -38,15 +38,13 @@ import java.util.Map;
  */
 public class PrettyPrinter extends DefaultASTVisitor<Void> {
 
+    private final StringBuilder s = new StringBuilder();
     @Getter
     @Setter
     private int maxWidth = 80;
-
     @Getter
     @Setter
     private boolean unicode = true;
-
-    private final StringBuilder s = new StringBuilder();
     private int indentation = 0;
 
     @Override
@@ -168,7 +166,7 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
     }
 
     @Override
-    public Void visit(CaseStatement caseStatement) {
+    public Void visit(SimpleCaseStatement caseStatement) {
         s.append("case ");
         caseStatement.getGuard().accept(this);
         s.append(" {");
diff --git a/src/main/java/edu/kit/formal/proofscriptparser/TransformAst.java b/src/main/java/edu/kit/formal/proofscriptparser/TransformAst.java
index 00602a5e02ceb195f29377e8f6dc1b44b4a49066..a86c17f7311c1f7afe108aba682172ab214a78dc 100644
--- a/src/main/java/edu/kit/formal/proofscriptparser/TransformAst.java
+++ b/src/main/java/edu/kit/formal/proofscriptparser/TransformAst.java
@@ -249,9 +249,16 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
     public Object visitMatchPattern(ScriptLanguageParser.MatchPatternContext ctx) {
         MatchExpression match = new MatchExpression();
         match.setRuleContext(ctx);
-        if (ctx.argList() != null)
-            match.setSignature((Signature) ctx.argList().accept(this));
-        match.setPattern((Expression) ctx.pattern.accept(this));
+
+        if (ctx.derivable != null) {
+            match.setDerivable(true);
+            match.setDerivableTerm((Expression) ctx.derivableExpression.accept(this));
+        } else {
+            if (ctx.argList() != null)
+                match.setSignature((Signature) ctx.argList().accept(this));
+            match.setPattern((Expression) ctx.pattern.accept(this));
+        }
+
         return match;
     }
 
@@ -283,12 +290,46 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
 
     @Override
     public Object visitCasesList(ScriptLanguageParser.CasesListContext ctx) {
-        CaseStatement caseStatement = new CaseStatement();
+
+        if (ctx.ISCLOSED() != null) {
+            IsClosableCase isClosableCase = new IsClosableCase();
+            isClosableCase.setRuleContext(ctx);
+            isClosableCase.setBody((Statements) ctx.stmtList().accept(this));
+            return isClosableCase;
+        } else {
+            SimpleCaseStatement caseStatement = new SimpleCaseStatement();
+            caseStatement.setRuleContext(ctx);
+            caseStatement.setGuard((Expression) ctx.expression().accept(this));
+            caseStatement.setBody((Statements) ctx.stmtList().accept(this));
+            return caseStatement;
+        }
+     /*   CaseStatement caseStatement = new CaseStatement();
+        caseStatement.setRuleContext(ctx);
+        caseStatement.setGuard((Expression) ctx.expression().accept(this));
+        caseStatement.setBody((Statements) ctx.stmtList().accept(this));
+        return caseStatement;*/
+
+    }
+
+/*
+    @Override
+    public Object visitSimpleCase(ScriptLanguageParser.SimpleCaseContext ctx) {
+        SimpleCaseStatement caseStatement = new SimpleCaseStatement();
         caseStatement.setRuleContext(ctx);
         caseStatement.setGuard((Expression) ctx.expression().accept(this));
         caseStatement.setBody((Statements) ctx.stmtList().accept(this));
         return caseStatement;
+
+    }
+
+    @Override
+    public Object visitClosableCase(ScriptLanguageParser.ClosableCaseContext ctx) {
+        IsClosableCase isClosableCase = new IsClosableCase();
+        isClosableCase.setRuleContext(ctx);
+        isClosableCase.setBody((Statements) ctx.stmtList().accept(this));
+        return isClosableCase;
     }
+*/
 
     @Override
     public Object visitForEachStmt(ScriptLanguageParser.ForEachStmtContext ctx) {
diff --git a/src/main/java/edu/kit/formal/proofscriptparser/Visitor.java b/src/main/java/edu/kit/formal/proofscriptparser/Visitor.java
index 309e472a229b1bbec41956908e1da545359a505f..b96612a7eedbecd077e4ef5a60a379ac4efcbc5f 100644
--- a/src/main/java/edu/kit/formal/proofscriptparser/Visitor.java
+++ b/src/main/java/edu/kit/formal/proofscriptparser/Visitor.java
@@ -53,7 +53,7 @@ public interface Visitor<T> {
 
     T visit(CasesStatement cases);
 
-    T visit(CaseStatement case_);
+    //T visit(CaseStatement case_);
 
     T visit(CallStatement call);
 
@@ -70,4 +70,9 @@ public interface Visitor<T> {
     T visit(UnaryExpression e);
 
 
+    T visit(IsClosableCase isClosableCase);
+
+    T visit(SimpleCaseStatement simpleCaseStatement);
+
+    T visit(CaseStatement caseStatement);
 }
diff --git a/src/main/java/edu/kit/formal/proofscriptparser/ast/CaseStatement.java b/src/main/java/edu/kit/formal/proofscriptparser/ast/CaseStatement.java
index a07e4e9f36b4d1407c8eda27128295997820004c..9d2217e3050bede5a300a8799014a08d346fd244 100644
--- a/src/main/java/edu/kit/formal/proofscriptparser/ast/CaseStatement.java
+++ b/src/main/java/edu/kit/formal/proofscriptparser/ast/CaseStatement.java
@@ -38,8 +38,8 @@ import lombok.NoArgsConstructor;
 @NoArgsConstructor
 @AllArgsConstructor
 public class CaseStatement extends Statement<ScriptLanguageParser.CasesListContext> {
-    private Expression guard;
-    private Statements body;
+    public boolean isClosedStmt;
+    protected Statements body;
 
     /**
      * {@inheritDoc}
@@ -52,6 +52,6 @@ public class CaseStatement extends Statement<ScriptLanguageParser.CasesListConte
      * {@inheritDoc}
      */
     @Override public CaseStatement copy() {
-        return new CaseStatement(guard.copy(), body.copy());
+        return new CaseStatement(body.copy(), isClosedStmt);
     }
 }
diff --git a/src/main/java/edu/kit/formal/proofscriptparser/ast/IsClosableCase.java b/src/main/java/edu/kit/formal/proofscriptparser/ast/IsClosableCase.java
new file mode 100644
index 0000000000000000000000000000000000000000..ead9b851fa2c8c671749f722593ce4db1e9ff687
--- /dev/null
+++ b/src/main/java/edu/kit/formal/proofscriptparser/ast/IsClosableCase.java
@@ -0,0 +1,34 @@
+package edu.kit.formal.proofscriptparser.ast;
+
+import edu.kit.formal.proofscriptparser.Visitor;
+import lombok.Data;
+import lombok.NoArgsConstructor;
+
+/**
+ * Object representing  a "match isClosable{ Commands}" block
+ */
+@Data
+@NoArgsConstructor
+public class IsClosableCase extends CaseStatement {
+    private boolean isClosedStmt = true;
+
+    public IsClosableCase(Statements body) {
+        this.body = body;
+    }
+
+    /**
+     * {@inheritDoc}
+     */
+    @Override
+    public <T> T accept(Visitor<T> visitor) {
+        return visitor.visit(this);
+    }
+
+    /**
+     * {@inheritDoc}
+     */
+    @Override
+    public IsClosableCase copy() {
+        return new IsClosableCase(body.copy());
+    }
+}
diff --git a/src/main/java/edu/kit/formal/proofscriptparser/ast/MatchExpression.java b/src/main/java/edu/kit/formal/proofscriptparser/ast/MatchExpression.java
index 1a0e6b31fb99563f2158749e79559d91eae235f1..abc52cac832fe54436dde9b40ad4abb791374e58 100644
--- a/src/main/java/edu/kit/formal/proofscriptparser/ast/MatchExpression.java
+++ b/src/main/java/edu/kit/formal/proofscriptparser/ast/MatchExpression.java
@@ -27,6 +27,8 @@ import edu.kit.formal.proofscriptparser.NotWelldefinedException;
 import edu.kit.formal.proofscriptparser.ScriptLanguageParser;
 import edu.kit.formal.proofscriptparser.Visitor;
 import lombok.Data;
+import lombok.Getter;
+import lombok.Setter;
 
 /**
  * A match expression contains an argument and a uses clause.
@@ -38,6 +40,12 @@ import lombok.Data;
 public class MatchExpression extends Expression<ScriptLanguageParser.MatchPatternContext> {
     private Signature signature = new Signature();
     private Expression pattern;
+    @Getter
+    @Setter
+    private boolean isDerivable;
+    @Getter
+    @Setter
+    private Expression derivableTerm;
 
     /**
      * {@inheritDoc}
diff --git a/src/main/java/edu/kit/formal/proofscriptparser/ast/SimpleCaseStatement.java b/src/main/java/edu/kit/formal/proofscriptparser/ast/SimpleCaseStatement.java
new file mode 100644
index 0000000000000000000000000000000000000000..e7f411b367431b69e2ad0c06c0c90a825fcf5753
--- /dev/null
+++ b/src/main/java/edu/kit/formal/proofscriptparser/ast/SimpleCaseStatement.java
@@ -0,0 +1,40 @@
+package edu.kit.formal.proofscriptparser.ast;
+
+import edu.kit.formal.proofscriptparser.Visitor;
+import lombok.AllArgsConstructor;
+import lombok.Data;
+import lombok.NoArgsConstructor;
+
+/**
+ * Created by sarah on 7/17/17.
+ */
+@Data
+@NoArgsConstructor
+@AllArgsConstructor
+public class SimpleCaseStatement extends CaseStatement {
+    private Expression guard;
+    private boolean isClosedStmt = false;
+
+    public SimpleCaseStatement(Expression guard, Statements body) {
+        this.guard = guard;
+        this.body = body;
+    }
+
+    /**
+     * {@inheritDoc}
+     */
+    @Override
+    public <T> T accept(Visitor<T> visitor) {
+        return visitor.visit(this);
+    }
+
+    /**
+     * {@inheritDoc}
+     */
+    @Override
+    public SimpleCaseStatement copy() {
+        return new SimpleCaseStatement(guard.copy(), body.copy());
+    }
+
+
+}
diff --git a/src/test/resources/edu/kit/formal/interpreter/contraposition/isClosable.kps b/src/test/resources/edu/kit/formal/interpreter/contraposition/isClosable.kps
new file mode 100644
index 0000000000000000000000000000000000000000..bed6a5ed257039cc67b2c132b5358918b3240215
--- /dev/null
+++ b/src/test/resources/edu/kit/formal/interpreter/contraposition/isClosable.kps
@@ -0,0 +1,18 @@
+
+script test(){
+    impRight;
+    impRight;
+    cases{
+        case match isCloseable:{
+            notLeft;
+            notRight;
+            replace_known_left occ='2';
+            concrete_impl_1;
+            close;
+        }
+
+        default:{
+            auto;
+        }
+    }
+}
\ No newline at end of file