diff --git a/src/main/java/de/tlc4b/analysis/MachineContext.java b/src/main/java/de/tlc4b/analysis/MachineContext.java
index 837641969cbfd6bec11394dec15b160206ef3fd0..7e4b87cdafe6320a9e6b47395483c7872fc8a5ff 100644
--- a/src/main/java/de/tlc4b/analysis/MachineContext.java
+++ b/src/main/java/de/tlc4b/analysis/MachineContext.java
@@ -81,7 +81,7 @@ public class MachineContext extends DepthFirstAdapter {
 	private final ArrayList<LTLFormulaVisitor> ltlVisitors;
 	private final PPredicate constantsSetup;
 
-	private boolean originallyHadConstants = false;
+	private boolean constantSetupInTraceFile = false;
 	// machine identifier
 	private final LinkedHashMap<String, Node> setParameter;
 	private final LinkedHashMap<String, Node> scalarParameter;
@@ -476,7 +476,7 @@ public class MachineContext extends DepthFirstAdapter {
 
 	@Override
 	public void caseAConstantsMachineClause(AConstantsMachineClause node) {
-		originallyHadConstants = true;
+		constantSetupInTraceFile = true;
 		List<PExpression> copy = new ArrayList<PExpression>(
 				node.getIdentifiers());
 		for (PExpression e : copy) {
@@ -490,7 +490,7 @@ public class MachineContext extends DepthFirstAdapter {
 	@Override
 	public void caseAAbstractConstantsMachineClause(
 			AAbstractConstantsMachineClause node) {
-		originallyHadConstants = true;
+		constantSetupInTraceFile = true;
 		List<PExpression> copy = new ArrayList<PExpression>(
 				node.getIdentifiers());
 		for (PExpression e : copy) {
@@ -593,7 +593,7 @@ public class MachineContext extends DepthFirstAdapter {
 	@Override
 	public void caseAPropertiesMachineClause(APropertiesMachineClause node) {
 		this.propertiesMachineClause = node;
-
+		constantSetupInTraceFile = true;
 		/**
 		 * check identifier scope in properties clauses
 		 */
@@ -1109,8 +1109,8 @@ public class MachineContext extends DepthFirstAdapter {
 		return constantsSetup;
 	}
 
-	public boolean originallyHadConstants() {
-		return originallyHadConstants;
+	public boolean constantSetupInTraceFile() {
+		return constantSetupInTraceFile;
 	}
 }
 
diff --git a/src/main/java/de/tlc4b/analysis/StandardMadules.java b/src/main/java/de/tlc4b/analysis/StandardMadules.java
index 1eefd1275e9a2c87bd2e812502b54922c8b77522..5d8ae042d3bf2763eb2359d98ad0782d3d9e1a29 100644
--- a/src/main/java/de/tlc4b/analysis/StandardMadules.java
+++ b/src/main/java/de/tlc4b/analysis/StandardMadules.java
@@ -148,7 +148,9 @@ public final class StandardMadules {
 	public static final String IS_REL_SEQUENCE_1 = "isRelSeq1";
 	public static final String REL_SEQUENCE_1_SET = "RelSeqSet1";
 	public static final String REL_INJECTIVE_SEQUENCE = "RelISeq";
+	public static final String REL_INJECTIVE_SEQUENCE_ELEMENT_OF = "RelISeqEleOf";
 	public static final String REL_INJECTIVE_SEQUENCE_1 = "RelISeq1";
+	public static final String REL_INJECTIVE_SEQUENCE_1_ELEMENT_OF = "RelISeq1EleOf";
 	public static final String REL_SEQUENCE_Concat = "RelSeqConcat";
 	public static final String REL_SEQUENCE_PREPAND = "RelSeqPrepand";
 	public static final String REL_SEQUENCE_APPEND = "RelSeqAppend";
diff --git a/src/main/java/de/tlc4b/analysis/UsedStandardModules.java b/src/main/java/de/tlc4b/analysis/UsedStandardModules.java
index 6ae2ca1753166ebc4dc70dc1273e7e376e850f62..19497f212c3037ee1e800a2dacdf6569f55cc507 100644
--- a/src/main/java/de/tlc4b/analysis/UsedStandardModules.java
+++ b/src/main/java/de/tlc4b/analysis/UsedStandardModules.java
@@ -532,11 +532,16 @@ public class UsedStandardModules extends DepthFirstAdapter {
 	 */
 
 	public void inASeqExpression(ASeqExpression node) {
-		evalSequenceOrRelation(node);
+		SetType type = (SetType) typechecker.getType(node);
+		if (type.getSubtype() instanceof FunctionType) {
+			usedStandardModules.add(STANDARD_MODULES.Sequences);
+		} else {
+			usedStandardModules.add(STANDARD_MODULES.SequencesAsRelations);
+		}
 	}
 
 	public void inASizeExpression(ASizeExpression node) {
-		evalSequenceOrRelation(node);
+		evalSequenceOrRelation(node.getExpression());
 	}
 
 	public void inAConcatExpression(AConcatExpression node) {
@@ -553,11 +558,11 @@ public class UsedStandardModules extends DepthFirstAdapter {
 	}
 
 	public void inAFirstExpression(AFirstExpression node) {
-		evalSequenceOrRelation(node);
+		evalSequenceOrRelation(node.getExpression());
 	}
 
 	public void inATailExpression(ATailExpression node) {
-		evalSequenceOrRelation(node);
+		evalSequenceOrRelation(node.getExpression());
 	}
 
 	/**
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index e0e5b6e7f9693aaf694c7cde7dd408a3255fa657..f07ed67e7e8aca5c7b609bb7a538a4fd3707bdd9 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -173,11 +173,13 @@ public class TLAPrinter extends DepthFirstAdapter {
 
 	private void printLTLFormulas() {
 		ArrayList<LTLFormulaVisitor> visitors = machineContext.getLTLFormulas();
-		for (int i = 0; i < visitors.size(); i++) {
-			LTLFormulaVisitor visitor = visitors.get(i);
-			tlaModuleString.append(visitor.getName() + " == ");
-			visitor.printLTLFormula(this, typeRestrictor);
-			tlaModuleString.append("\n");
+		if (TLC4BGlobals.isCheckltl()) {
+			for (int i = 0; i < visitors.size(); i++) {
+				LTLFormulaVisitor visitor = visitors.get(i);
+				tlaModuleString.append(visitor.getName() + " == ");
+				visitor.printLTLFormula(this, typeRestrictor);
+				tlaModuleString.append("\n");
+			}
 		}
 	}
 
@@ -304,7 +306,7 @@ public class TLAPrinter extends DepthFirstAdapter {
 		ArrayList<Node> list = this.tlaModule.getAssume();
 		if (list.size() == 0)
 			return;
-		
+
 		for (int i = 0; i < list.size(); i++) {
 			tlaModuleString.append("ASSUME ");
 			list.get(i).apply(this);
@@ -1716,7 +1718,8 @@ public class TLAPrinter extends DepthFirstAdapter {
 		} else {
 			if (node.parent() instanceof AMemberPredicate
 					&& !typeRestrictor.isARemovedNode(node.parent())
-					&& !this.tlaModule.getInitPredicates().contains(node.parent())) {
+					&& !this.tlaModule.getInitPredicates().contains(
+							node.parent())) {
 				tlaModuleString.append(REL_TOTAL_FUNCTION_ELEMENT_OF);
 			} else {
 				tlaModuleString.append(REL_TOTAL_FUNCTION);
@@ -2537,7 +2540,12 @@ public class TLAPrinter extends DepthFirstAdapter {
 	public void caseAIseqExpression(AIseqExpression node) {
 		SetType set = (SetType) typechecker.getType(node);
 		if (set.getSubtype() instanceof SetType) {
-			tlaModuleString.append(REL_INJECTIVE_SEQUENCE);
+			if (node.parent() instanceof AMemberPredicate
+					&& !typeRestrictor.isARemovedNode(node.parent())) {
+				tlaModuleString.append(REL_INJECTIVE_SEQUENCE_ELEMENT_OF);
+			} else {
+				tlaModuleString.append(REL_INJECTIVE_SEQUENCE);
+			}
 		} else {
 			if (node.parent() instanceof AMemberPredicate
 					&& !typeRestrictor.isARemovedNode(node.parent())) {
@@ -2555,7 +2563,12 @@ public class TLAPrinter extends DepthFirstAdapter {
 	public void caseAIseq1Expression(AIseq1Expression node) {
 		SetType set = (SetType) typechecker.getType(node);
 		if (set.getSubtype() instanceof SetType) {
-			tlaModuleString.append(REL_INJECTIVE_SEQUENCE_1);
+			if (node.parent() instanceof AMemberPredicate
+					&& !typeRestrictor.isARemovedNode(node.parent())) {
+				tlaModuleString.append(REL_INJECTIVE_SEQUENCE_1_ELEMENT_OF);
+			} else {
+				tlaModuleString.append(REL_INJECTIVE_SEQUENCE_1);
+			}
 		} else {
 			if (node.parent() instanceof AMemberPredicate
 					&& !typeRestrictor.isARemovedNode(node.parent())) {
diff --git a/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java b/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
index 6be0cea9aba6182e073cfd20aab9e4aaf3011737..1e3932fc013238b145b612ab1de6cf3efcb0f35a 100644
--- a/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
+++ b/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
@@ -55,7 +55,7 @@ public class TLCOutputInfo {
 		this.constants = machineContext.getConstants().keySet();
 		this.hasInit = tlaModule.getInitPredicates().size() > 0;
 
-		if (machineContext.originallyHadConstants()) {
+		if (machineContext.constantSetupInTraceFile()) {
 			this.constantSetup = true;
 		}
 
diff --git a/src/main/resources/standardModules/SequencesAsRelations.tla b/src/main/resources/standardModules/SequencesAsRelations.tla
index e97b03587cf0749bd29f37eeb2818d50ba62134f..af607c3260863615e06de4b01625bd58f79e01f7 100644
--- a/src/main/resources/standardModules/SequencesAsRelations.tla
+++ b/src/main/resources/standardModules/SequencesAsRelations.tla
@@ -28,10 +28,23 @@ LOCAL ISeq(S) == UNION { {x \in [(1..n) -> S]: Cardinality(Range(x)) = Cardinali
                         
 RelISeq(S) == {{<<n, x[n]>>:n \in 1..Len(x)} :x \in ISeq(S)}
  \* The set of all injective sequences with elements of S
+
+RelISeqEleOf(S) == {p \in SUBSET(Nat \times S): 
+    LET d == {q[1] : q \in p} 
+    IN /\ Cardinality(p) = Cardinality(d)
+       /\ d = 1..Cardinality(d)
+       /\ Cardinality(p) = Cardinality(RelRange(p))}
  
 RelISeq1(S) == RelISeq(S) \ {{}}
  \* The set of all non-empty injective sequences with elements of S
 
+RelISeq1EleOf(S) == {p \in SUBSET(Nat \times S): 
+    LET d == {q[1] : q \in p} 
+    IN /\ Cardinality(p) > 0
+       /\ Cardinality(p) = Cardinality(d)
+       /\ d = 1..Cardinality(d)
+       /\ Cardinality(p) = Cardinality(RelRange(p))}
+
 LOCAL SeqTest(s) == RelDomain(s) = 1..Cardinality(s)
  \* Testing if s is a sequence