Added lhs conjunct to avoid matching loop

marcoeilers · marcoeilers · commit 895279b9ec1d · 2024-12-05T23:20:16.000+01:00
diff --git a/src/main/resources/dafny_axioms/sequences.vpr b/src/main/resources/dafny_axioms/sequences.vpr
@@ -123,7 +123,7 @@ domain $Seq[E] {
     axiom {
         forall s: $Seq[E], t: $Seq[E], n: Int ::
         { Seq_take(Seq_append(s, t), n) }
-        n > 0 && n > Seq_length(s) ==> Seq_add(Seq_sub(n, Seq_length(s)), Seq_length(s)) == n && Seq_take(Seq_append(s, t), n) == Seq_append(s, Seq_take(t, Seq_sub(n, Seq_length(s))))
+        n > 0 && n > Seq_length(s) && n < Seq_length(Seq_append(s, t)) ==> Seq_add(Seq_sub(n, Seq_length(s)), Seq_length(s)) == n && Seq_take(Seq_append(s, t), n) == Seq_append(s, Seq_take(t, Seq_sub(n, Seq_length(s))))
     }
     axiom {
         forall s: $Seq[E], t: $Seq[E], n: Int ::

Original file line number	Diff line number	Diff line change
`@@ -123,7 +123,7 @@ domain $Seq[E] {`
`123`	`123`	`axiom {`
`124`	`124`	`forall s: $Seq[E], t: $Seq[E], n: Int ::`
`125`	`125`	`{ Seq_take(Seq_append(s, t), n) }`
`126`		`- n > 0 && n > Seq_length(s) ==> Seq_add(Seq_sub(n, Seq_length(s)), Seq_length(s)) == n && Seq_take(Seq_append(s, t), n) == Seq_append(s, Seq_take(t, Seq_sub(n, Seq_length(s))))`
	`126`	`+ n > 0 && n > Seq_length(s) && n < Seq_length(Seq_append(s, t)) ==> Seq_add(Seq_sub(n, Seq_length(s)), Seq_length(s)) == n && Seq_take(Seq_append(s, t), n) == Seq_append(s, Seq_take(t, Seq_sub(n, Seq_length(s))))`
`127`	`127`	`}`
`128`	`128`	`axiom {`
`129`	`129`	`forall s: $Seq[E], t: $Seq[E], n: Int ::`