diff --git a/src/cmd/compile/fmt_test.go b/src/cmd/compile/fmt_test.go
index 8af7cced6a7..5dd2fa50be8 100644
--- a/src/cmd/compile/fmt_test.go
+++ b/src/cmd/compile/fmt_test.go
@@ -646,6 +646,7 @@ var knownFormats = map[string]string{
 	"cmd/compile/internal/ssa.Op %s":                  "",
 	"cmd/compile/internal/ssa.Op %v":                  "",
 	"cmd/compile/internal/ssa.ValAndOff %s":           "",
+	"cmd/compile/internal/ssa.domain %v":              "",
 	"cmd/compile/internal/ssa.posetNode %v":           "",
 	"cmd/compile/internal/ssa.posetTestOp %v":         "",
 	"cmd/compile/internal/ssa.rbrank %d":              "",
diff --git a/src/cmd/compile/internal/ssa/loopbce.go b/src/cmd/compile/internal/ssa/loopbce.go
index a96d98717da..7f2da4870e4 100644
--- a/src/cmd/compile/internal/ssa/loopbce.go
+++ b/src/cmd/compile/internal/ssa/loopbce.go
@@ -137,7 +137,7 @@ nextb:
 			}
 		}
 
-		if f.pass.debug > 1 {
+		if f.pass.debug >= 1 {
 			if min.Op == OpConst64 {
 				b.Func.Warnl(b.Pos, "Induction variable with minimum %d and increment %d", min.AuxInt, inc.AuxInt)
 			} else {
diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index 371009a57d4..536cfcebf0c 100644
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/src/cmd/compile/internal/ssa/prove.go
@@ -388,6 +388,77 @@ func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
 			}
 		}
 	}
+
+	// Process: x+delta > w    (with delta,w constants)
+	//
+	// We want to derive: x+delta > w  ⇒  x > w-delta
+	//
+	// We do this for signed numbers for now, as that allows to prove many
+	// accesses to slices in loops.
+	//
+	// From x+delta > w, we compute (using integers of the correct size):
+	//    min = w - delta
+	//    max = MaxInt - delta
+	//
+	// And we prove that:
+	//    if min<max: min < x AND x <= max
+	//    if min>max: min < x OR  x <= max
+	//
+	// This is always correct, even in case of overflow.
+	//
+	// If the initial fact is x+delta >= w instead, the derived conditions are:
+	//    if min<max: min <= x AND x <= max
+	//    if min>max: min <= x OR  x <= max
+	//
+	// Notice the conditions for max are still <=, as they handle overflows.
+	if r == gt || r == gt|eq {
+		if x, delta := isConstDelta(v); x != nil && w.isGenericIntConst() && d == signed {
+			if parent.Func.pass.debug > 1 {
+				parent.Func.Warnl(parent.Pos, "x+d >= w; x:%v %v delta:%v w:%v d:%v", x, parent.String(), delta, w.AuxInt, d)
+			}
+
+			var min, max int64
+			var vmin, vmax *Value
+			switch x.Type.Size() {
+			case 8:
+				min = w.AuxInt - delta
+				max = int64(^uint64(0)>>1) - delta
+
+				vmin = parent.NewValue0I(parent.Pos, OpConst64, parent.Func.Config.Types.Int64, min)
+				vmax = parent.NewValue0I(parent.Pos, OpConst64, parent.Func.Config.Types.Int64, max)
+
+			case 4:
+				min = int64(int32(w.AuxInt) - int32(delta))
+				max = int64(int32(^uint32(0)>>1) - int32(delta))
+
+				vmin = parent.NewValue0I(parent.Pos, OpConst32, parent.Func.Config.Types.Int32, min)
+				vmax = parent.NewValue0I(parent.Pos, OpConst32, parent.Func.Config.Types.Int32, max)
+
+			default:
+				panic("unimplemented")
+			}
+
+			if min < max {
+				// Record that x > min and max >= x
+				ft.update(parent, x, vmin, d, r)
+				ft.update(parent, vmax, x, d, r|eq)
+			} else {
+				// We know that either x>min OR x<=max. factsTable cannot record OR conditions,
+				// so let's see if we can already prove that one of them is false, in which case
+				// the other must be true
+				if l, has := ft.limits[x.ID]; has {
+					if l.max <= min {
+						// x>min is impossible, so it must be x<=max
+						ft.update(parent, vmax, x, d, r|eq)
+					} else if l.min > max {
+						// x<=max is impossible, so it must be x>min
+						ft.update(parent, x, vmin, d, r)
+					}
+				}
+			}
+		}
+	}
+
 }
 
 var opMin = map[Op]int64{
@@ -405,8 +476,25 @@ func (ft *factsTable) isNonNegative(v *Value) bool {
 	if isNonNegative(v) {
 		return true
 	}
-	l, has := ft.limits[v.ID]
-	return has && (l.min >= 0 || l.umax <= math.MaxInt64)
+
+	// Check if the recorded limits can prove that the value is positive
+	if l, has := ft.limits[v.ID]; has && (l.min >= 0 || l.umax <= math.MaxInt64) {
+		return true
+	}
+
+	// Check if v = x+delta, and we can use x's limits to prove that it's positive
+	if x, delta := isConstDelta(v); x != nil {
+		if l, has := ft.limits[x.ID]; has {
+			if delta > 0 && l.min >= -delta && l.max <= math.MaxInt64-delta {
+				return true
+			}
+			if delta < 0 && l.min >= -delta {
+				return true
+			}
+		}
+	}
+
+	return false
 }
 
 // checkpoint saves the current state of known relations.
@@ -595,6 +683,16 @@ func prove(f *Func) {
 		}
 	}
 
+	// Find induction variables. Currently, findIndVars
+	// is limited to one induction variable per block.
+	var indVars map[*Block]indVar
+	for _, v := range findIndVar(f) {
+		if indVars == nil {
+			indVars = make(map[*Block]indVar)
+		}
+		indVars[v.entry] = v
+	}
+
 	// current node state
 	type walkState int
 	const (
@@ -634,6 +732,10 @@ func prove(f *Func) {
 		switch node.state {
 		case descend:
 			ft.checkpoint()
+			if iv, ok := indVars[node.block]; ok {
+				addIndVarRestrictions(ft, parent, iv)
+			}
+
 			if branch != unknown {
 				addBranchRestrictions(ft, parent, branch)
 				if ft.unsat {
@@ -688,6 +790,19 @@ func getBranch(sdom SparseTree, p *Block, b *Block) branch {
 	return unknown
 }
 
+// addIndVarRestrictions updates the factsTables ft with the facts
+// learned from the induction variable indVar which drives the loop
+// starting in Block b.
+func addIndVarRestrictions(ft *factsTable, b *Block, iv indVar) {
+	d := signed
+	if isNonNegative(iv.min) && isNonNegative(iv.max) {
+		d |= unsigned
+	}
+
+	addRestrictions(b, ft, d, iv.min, iv.ind, lt|eq)
+	addRestrictions(b, ft, d, iv.ind, iv.max, lt)
+}
+
 // addBranchRestrictions updates the factsTables ft with the facts learned when
 // branching from Block b in direction br.
 func addBranchRestrictions(ft *factsTable, b *Block, br branch) {
diff --git a/test/loopbce.go b/test/loopbce.go
index 857cf2442b6..c742df7e60c 100644
--- a/test/loopbce.go
+++ b/test/loopbce.go
@@ -1,12 +1,12 @@
 // +build amd64
-// errorcheck -0 -d=ssa/loopbce/debug=3
+// errorcheck -0 -d=ssa/prove/debug=1
 
 package main
 
 func f0a(a []int) int {
 	x := 0
 	for i := range a { // ERROR "Induction variable with minimum 0 and increment 1$"
-		x += a[i] // ERROR "Found redundant IsInBounds$"
+		x += a[i] // ERROR "Proved IsInBounds$"
 	}
 	return x
 }
@@ -14,7 +14,7 @@ func f0a(a []int) int {
 func f0b(a []int) int {
 	x := 0
 	for i := range a { // ERROR "Induction variable with minimum 0 and increment 1$"
-		b := a[i:] // ERROR "Found redundant IsSliceInBounds$"
+		b := a[i:] // ERROR "Proved IsSliceInBounds$"
 		x += b[0]
 	}
 	return x
@@ -23,7 +23,7 @@ func f0b(a []int) int {
 func f0c(a []int) int {
 	x := 0
 	for i := range a { // ERROR "Induction variable with minimum 0 and increment 1$"
-		b := a[:i+1] // ERROR "Found redundant IsSliceInBounds \(len promoted to cap\)$"
+		b := a[:i+1] // ERROR "Proved IsSliceInBounds$"
 		x += b[0]
 	}
 	return x
@@ -40,7 +40,7 @@ func f1(a []int) int {
 func f2(a []int) int {
 	x := 0
 	for i := 1; i < len(a); i++ { // ERROR "Induction variable with minimum 1 and increment 1$"
-		x += a[i] // ERROR "Found redundant IsInBounds$"
+		x += a[i] // ERROR "Proved IsInBounds$"
 	}
 	return x
 }
@@ -48,7 +48,7 @@ func f2(a []int) int {
 func f4(a [10]int) int {
 	x := 0
 	for i := 0; i < len(a); i += 2 { // ERROR "Induction variable with minimum 0 and increment 2$"
-		x += a[i] // ERROR "Found redundant IsInBounds$"
+		x += a[i] // ERROR "Proved IsInBounds$"
 	}
 	return x
 }
@@ -63,7 +63,7 @@ func f5(a [10]int) int {
 
 func f6(a []int) {
 	for i := range a { // ERROR "Induction variable with minimum 0 and increment 1$"
-		b := a[0:i] // ERROR "Found redundant IsSliceInBounds \(len promoted to cap\)$"
+		b := a[0:i] // ERROR "Proved IsSliceInBounds$"
 		f6(b)
 	}
 }
@@ -71,7 +71,7 @@ func f6(a []int) {
 func g0a(a string) int {
 	x := 0
 	for i := 0; i < len(a); i++ { // ERROR "Induction variable with minimum 0 and increment 1$"
-		x += int(a[i]) // ERROR "Found redundant IsInBounds$"
+		x += int(a[i]) // ERROR "Proved IsInBounds$"
 	}
 	return x
 }
@@ -79,7 +79,7 @@ func g0a(a string) int {
 func g0b(a string) int {
 	x := 0
 	for i := 0; len(a) > i; i++ { // ERROR "Induction variable with minimum 0 and increment 1$"
-		x += int(a[i]) // ERROR "Found redundant IsInBounds$"
+		x += int(a[i]) // ERROR "Proved IsInBounds$"
 	}
 	return x
 }
@@ -88,7 +88,7 @@ func g1() int {
 	a := "evenlength"
 	x := 0
 	for i := 0; i < len(a); i += 2 { // ERROR "Induction variable with minimum 0 and increment 2$"
-		x += int(a[i]) // ERROR "Found redundant IsInBounds$"
+		x += int(a[i]) // ERROR "Proved IsInBounds$"
 	}
 	return x
 }
@@ -98,7 +98,7 @@ func g2() int {
 	x := 0
 	for i := 0; i < len(a); i += 2 { // ERROR "Induction variable with minimum 0 and increment 2$"
 		j := i
-		if a[i] == 'e' { // ERROR "Found redundant IsInBounds$"
+		if a[i] == 'e' { // ERROR "Proved IsInBounds$"
 			j = j + 1
 		}
 		x += int(a[j])
@@ -109,27 +109,27 @@ func g2() int {
 func g3a() {
 	a := "this string has length 25"
 	for i := 0; i < len(a); i += 5 { // ERROR "Induction variable with minimum 0 and increment 5$"
-		useString(a[i:]) // ERROR "Found redundant IsSliceInBounds$"
+		useString(a[i:]) // ERROR "Proved IsSliceInBounds$"
 		useString(a[:i+3])
 	}
 }
 
 func g3b(a string) {
 	for i := 0; i < len(a); i++ { // ERROR "Induction variable with minimum 0 and increment 1$"
-		useString(a[i+1:]) // ERROR "Found redundant IsSliceInBounds$"
+		useString(a[i+1:]) // ERROR "Proved IsSliceInBounds$"
 	}
 }
 
 func g3c(a string) {
 	for i := 0; i < len(a); i++ { // ERROR "Induction variable with minimum 0 and increment 1$"
-		useString(a[:i+1]) // ERROR "Found redundant IsSliceInBounds$"
+		useString(a[:i+1]) // ERROR "Proved IsSliceInBounds$"
 	}
 }
 
 func h1(a []byte) {
 	c := a[:128]
 	for i := range c { // ERROR "Induction variable with minimum 0 and increment 1$"
-		c[i] = byte(i) // ERROR "Found redundant IsInBounds$"
+		c[i] = byte(i) // ERROR "Proved IsInBounds$"
 	}
 }
 
@@ -142,11 +142,11 @@ func h2(a []byte) {
 func k0(a [100]int) [100]int {
 	for i := 10; i < 90; i++ { // ERROR "Induction variable with minimum 10 and increment 1$"
 		a[i-11] = i
-		a[i-10] = i // ERROR "Found redundant \(IsInBounds ind 100\), ind < 80$"
-		a[i-5] = i  // ERROR "Found redundant \(IsInBounds ind 100\), ind < 85$"
-		a[i] = i    // ERROR "Found redundant \(IsInBounds ind 100\), ind < 90$"
-		a[i+5] = i  // ERROR "Found redundant \(IsInBounds ind 100\), ind < 95$"
-		a[i+10] = i // ERROR "Found redundant \(IsInBounds ind 100\), ind < 100$"
+		a[i-10] = i // ERROR "Proved IsInBounds$"
+		a[i-5] = i  // ERROR "Proved IsInBounds$"
+		a[i] = i    // ERROR "Proved IsInBounds$"
+		a[i+5] = i  // ERROR "Proved IsInBounds$"
+		a[i+10] = i // ERROR "Proved IsInBounds$"
 		a[i+11] = i
 	}
 	return a
@@ -155,12 +155,13 @@ func k0(a [100]int) [100]int {
 func k1(a [100]int) [100]int {
 	for i := 10; i < 90; i++ { // ERROR "Induction variable with minimum 10 and increment 1$"
 		useSlice(a[:i-11])
-		useSlice(a[:i-10]) // ERROR "Found redundant \(IsSliceInBounds ind 100\), ind < 80$"
-		useSlice(a[:i-5])  // ERROR "Found redundant \(IsSliceInBounds ind 100\), ind < 85$"
-		useSlice(a[:i])    // ERROR "Found redundant \(IsSliceInBounds ind 100\), ind < 90$"
-		useSlice(a[:i+5])  // ERROR "Found redundant \(IsSliceInBounds ind 100\), ind < 95$"
-		useSlice(a[:i+10]) // ERROR "Found redundant \(IsSliceInBounds ind 100\), ind < 100$"
-		useSlice(a[:i+11]) // ERROR "Found redundant \(IsSliceInBounds ind 100\), ind < 101$"
+		useSlice(a[:i-10]) // ERROR "Proved IsSliceInBounds$"
+		useSlice(a[:i-5])  // ERROR "Proved IsSliceInBounds$"
+		useSlice(a[:i])    // ERROR "Proved IsSliceInBounds$"
+		useSlice(a[:i+5])  // ERROR "Proved IsSliceInBounds$"
+		useSlice(a[:i+10]) // ERROR "Proved IsSliceInBounds$"
+		useSlice(a[:i+11]) // ERROR "Proved IsSliceInBounds$"
+		useSlice(a[:i+12])
 
 	}
 	return a
@@ -169,19 +170,22 @@ func k1(a [100]int) [100]int {
 func k2(a [100]int) [100]int {
 	for i := 10; i < 90; i++ { // ERROR "Induction variable with minimum 10 and increment 1$"
 		useSlice(a[i-11:])
-		useSlice(a[i-10:]) // ERROR "Found redundant \(IsSliceInBounds ind 100\), ind < 80$"
-		useSlice(a[i-5:])  // ERROR "Found redundant \(IsSliceInBounds ind 100\), ind < 85$"
-		useSlice(a[i:])    // ERROR "Found redundant \(IsSliceInBounds ind 100\), ind < 90$"
-		useSlice(a[i+5:])  // ERROR "Found redundant \(IsSliceInBounds ind 100\), ind < 95$"
-		useSlice(a[i+10:]) // ERROR "Found redundant \(IsSliceInBounds ind 100\), ind < 100$"
-		useSlice(a[i+11:]) // ERROR "Found redundant \(IsSliceInBounds ind 100\), ind < 101$"
+		useSlice(a[i-10:]) // ERROR "Proved IsSliceInBounds$"
+		useSlice(a[i-5:])  // ERROR "Proved IsSliceInBounds$"
+		useSlice(a[i:])    // ERROR "Proved IsSliceInBounds$"
+		useSlice(a[i+5:])  // ERROR "Proved IsSliceInBounds$"
+		useSlice(a[i+10:]) // ERROR "Proved IsSliceInBounds$"
+		useSlice(a[i+11:]) // ERROR "Proved IsSliceInBounds$"
+		useSlice(a[i+12:])
 	}
 	return a
 }
 
 func k3(a [100]int) [100]int {
 	for i := -10; i < 90; i++ { // ERROR "Induction variable with minimum -10 and increment 1$"
-		a[i+10] = i // ERROR "Found redundant \(IsInBounds ind 100\), ind < 100$"
+		a[i+9] = i
+		a[i+10] = i // ERROR "Proved IsInBounds$"
+		a[i+11] = i
 	}
 	return a
 }
@@ -189,7 +193,7 @@ func k3(a [100]int) [100]int {
 func k4(a [100]int) [100]int {
 	min := (-1) << 63
 	for i := min; i < min+50; i++ { // ERROR "Induction variable with minimum -9223372036854775808 and increment 1$"
-		a[i-min] = i // ERROR "Found redundant \(IsInBounds ind 100\), ind < 50$"
+		a[i-min] = i // ERROR "Proved IsInBounds$"
 	}
 	return a
 }
@@ -197,8 +201,8 @@ func k4(a [100]int) [100]int {
 func k5(a [100]int) [100]int {
 	max := (1 << 63) - 1
 	for i := max - 50; i < max; i++ { // ERROR "Induction variable with minimum 9223372036854775757 and increment 1$"
-		a[i-max+50] = i   // ERROR "Found redundant \(IsInBounds ind 100\), ind < 50$"
-		a[i-(max-70)] = i // ERROR "Found redundant \(IsInBounds ind 100\), ind < 70$"
+		a[i-max+50] = i   // ERROR "Proved IsInBounds$"
+		a[i-(max-70)] = i // ERROR "Proved IsInBounds$"
 	}
 	return a
 }
@@ -221,10 +225,10 @@ func nobce1() {
 
 func nobce2(a string) {
 	for i := int64(0); i < int64(len(a)); i++ { // ERROR "Induction variable with minimum 0 and increment 1$"
-		useString(a[i:]) // ERROR "Found redundant IsSliceInBounds$"
+		useString(a[i:]) // ERROR "Proved IsSliceInBounds$"
 	}
 	for i := int64(0); i < int64(len(a))-31337; i++ { // ERROR "Induction variable with minimum 0 and increment 1$"
-		useString(a[i:]) // ERROR "Found redundant IsSliceInBounds$"
+		useString(a[i:]) // ERROR "Proved IsSliceInBounds$"
 	}
 	for i := int64(0); i < int64(len(a))+int64(-1<<63); i++ { // ERROR "Induction variable with minimum 0 and increment 1$"
 		// tests an overflow of StringLen-MinInt64
diff --git a/test/prove.go b/test/prove.go
index f7b3ef0847b..a4eedbb717b 100644
--- a/test/prove.go
+++ b/test/prove.go
@@ -62,7 +62,7 @@ func f1c(a []int, i int64) int {
 }
 
 func f2(a []int) int {
-	for i := range a {
+	for i := range a { // ERROR "Induction variable with minimum 0 and increment 1"
 		a[i+1] = i
 		a[i+1] = i // ERROR "Proved IsInBounds$"
 	}
@@ -464,8 +464,7 @@ func f16(s []int) []int {
 }
 
 func f17(b []int) {
-	for i := 0; i < len(b); i++ {
-		useSlice(b[i:]) // Learns i <= len
+	for i := 0; i < len(b); i++ { // ERROR "Induction variable with minimum 0 and increment 1"
 		// This tests for i <= cap, which we can only prove
 		// using the derived relation between len and cap.
 		// This depends on finding the contradiction, since we