}
	return x
}

// The 4 xxxxExtNto64 functions below test whether prove is looking
// through value-preserving sign/zero extensions of index values (issue #26292).

// Look through all extensions
func signExtNto64(x []int, j8 int8, j16 int16, j32 int32) int {
	if len(x) < 22 {
		return 0
	}
	if j8 >= 0 && j8 < 22 {
		return x[j8] // ERROR "Proved IsInBounds$"
	}
	if j16 >= 0 && j16 < 22 {

(Div64 [false] x y) => (I64DivS x y)
(Div32 [false] x y) => (I64DivS (SignExt32to64 x) (SignExt32to64 y))
(Div16 [false] x y) => (I64DivS (SignExt16to64 x) (SignExt16to64 y))
(Div8          x y) => (I64DivS (SignExt8to64 x) (SignExt8to64 y))
(Div64u ...) => (I64DivU ...)
(Div32u x y) => (I64DivU (ZeroExt32to64 x) (ZeroExt32to64 y))
(Div16u x y) => (I64DivU (ZeroExt16to64 x) (ZeroExt16to64 y))
(Div8u  x y) => (I64DivU (ZeroExt8to64 x) (ZeroExt8to64 y))

(Rsh8x64 <t> x y) => (SRAV (SignExt8to64 x) (OR <t> (NEGV <t> (SGTU y (MOVVconst <typ.UInt64> [63]))) y))
(Rsh8x32 <t> x y) => (SRAV (SignExt8to64 x) (OR <t> (NEGV <t> (SGTU (ZeroExt32to64 y) (MOVVconst <typ.UInt64> [63]))) (ZeroExt32to64 y)))
(Rsh8x16 <t> x y) => (SRAV (SignExt8to64 x) (OR <t> (NEGV <t> (SGTU (ZeroExt16to64 y) (MOVVconst <typ.UInt64> [63]))) (ZeroExt16to64 y)))

(Rsh8x64 <t> x y) => (SRAV (SignExt8to64 x) (OR <t> (NEGV <t> (SGTU y (MOVVconst <typ.UInt64> [63]))) y))
(Rsh8x32 <t> x y) => (SRAV (SignExt8to64 x) (OR <t> (NEGV <t> (SGTU (ZeroExt32to64 y) (MOVVconst <typ.UInt64> [63]))) (ZeroExt32to64 y)))
(Rsh8x16 <t> x y) => (SRAV (SignExt8to64 x) (OR <t> (NEGV <t> (SGTU (ZeroExt16to64 y) (MOVVconst <typ.UInt64> [63]))) (ZeroExt16to64 y)))

(Rsh8x8   <t> x y) && !shiftIsBounded(v) => (SRA  <t> (SignExt8to64  x) (OR <y.Type> y (ADDI <y.Type> [-1] (SLTIU <y.Type> [64] (ZeroExt8to64  y)))))
(Rsh8x16  <t> x y) && !shiftIsBounded(v) => (SRA  <t> (SignExt8to64  x) (OR <y.Type> y (ADDI <y.Type> [-1] (SLTIU <y.Type> [64] (ZeroExt16to64 y)))))
(Rsh8x32  <t> x y) && !shiftIsBounded(v) => (SRA  <t> (SignExt8to64  x) (OR <y.Type> y (ADDI <y.Type> [-1] (SLTIU <y.Type> [64] (ZeroExt32to64 y)))))

	return false
}
func rewriteValueWasm_OpDiv8(v *Value) bool {
	v_1 := v.Args[1]
	v_0 := v.Args[0]
	b := v.Block
	typ := &b.Func.Config.Types
	// match: (Div8 x y)
	// result: (I64DivS (SignExt8to64 x) (SignExt8to64 y))
	for {
		x := v_0
		y := v_1
		v.reset(OpWasmI64DivS)
		v0 := b.NewValue0(v.Pos, OpSignExt8to64, typ.Int64)
		v0.AddArg(x)
		v1 := b.NewValue0(v.Pos, OpSignExt8to64, typ.Int64)

	}
}
func rewriteValueLOONG64_OpDiv8(v *Value) bool {
	v_1 := v.Args[1]
	v_0 := v.Args[0]
	b := v.Block
	typ := &b.Func.Config.Types
	// match: (Div8 x y)
	// result: (DIVV (SignExt8to64 x) (SignExt8to64 y))
	for {
		x := v_0
		y := v_1
		v.reset(OpLOONG64DIVV)
		v0 := b.NewValue0(v.Pos, OpSignExt8to64, typ.Int64)
		v0.AddArg(x)
		v1 := b.NewValue0(v.Pos, OpSignExt8to64, typ.Int64)

(Bswap64 x) =>
	(Int64Make
		(Bswap32 <typ.UInt32> (Int64Lo x))
		(Bswap32 <typ.UInt32> (Int64Hi x)))

(SignExt32to64 x) => (Int64Make (Signmask x) x)
(SignExt16to64 x) => (SignExt32to64 (SignExt16to32 x))
(SignExt8to64 x) => (SignExt32to64 (SignExt8to32 x))

(ZeroExt32to64 x) => (Int64Make (Const32 <typ.UInt32> [0]) x)
(ZeroExt16to64 x) => (ZeroExt32to64 (ZeroExt16to32 x))
(ZeroExt8to64 x) => (ZeroExt32to64 (ZeroExt8to32 x))

	}
}
func rewriteValueMIPS64_OpDiv8(v *Value) bool {
	v_1 := v.Args[1]
	v_0 := v.Args[0]
	b := v.Block
	typ := &b.Func.Config.Types
	// match: (Div8 x y)
	// result: (Select1 (DIVV (SignExt8to64 x) (SignExt8to64 y)))
	for {
		x := v_0
		y := v_1
		v.reset(OpSelect1)
		v0 := b.NewValue0(v.Pos, OpMIPS64DIVV, types.NewTuple(typ.Int64, typ.Int64))
		v1 := b.NewValue0(v.Pos, OpSignExt8to64, typ.Int64)

(Trunc32to8  (SignExt8to32  x)) => x
(Trunc32to16 (SignExt8to32  x)) => (SignExt8to16  x)
(Trunc32to16 (SignExt16to32 x)) => x
(Trunc64to8  (SignExt8to64  x)) => x
(Trunc64to16 (SignExt8to64  x)) => (SignExt8to16  x)
(Trunc64to16 (SignExt16to64 x)) => x
(Trunc64to32 (SignExt8to64  x)) => (SignExt8to32  x)
(Trunc64to32 (SignExt16to64 x)) => (SignExt16to32 x)
(Trunc64to32 (SignExt32to64 x)) => x