return true
	}
}
func rewriteValueLOONG64_OpDiv8u(v *Value) bool {
	v_1 := v.Args[1]
	v_0 := v.Args[0]
	b := v.Block
	typ := &b.Func.Config.Types
	// match: (Div8u x y)
	// result: (DIVVU (ZeroExt8to64 x) (ZeroExt8to64 y))
	for {
		x := v_0
		y := v_1
		v.reset(OpLOONG64DIVVU)
		v0 := b.NewValue0(v.Pos, OpZeroExt8to64, typ.UInt64)
		v0.AddArg(x)

	return blk, rem
}

func rshu(x, y uint) int {
	z := x >> y
	if z <= x { // ERROR "Proved Leq64U$"
		return 1
	}
	return 0
}

func divu(x, y uint) int {
	z := x / y
	if z <= x { // ERROR "Proved Leq64U$"
		return 1
	}
	return 0
}

func modu1(x, y uint) int {
	z := x % y
	if z < y { // ERROR "Proved Less64U$"

(Div16  (Const16 [c])  (Const16 [d])) && d != 0 => (Const16 [c/d])
(Div32  (Const32 [c])  (Const32 [d])) && d != 0 => (Const32 [c/d])
(Div64  (Const64 [c])  (Const64 [d])) && d != 0 => (Const64 [c/d])
(Div8u  (Const8  [c])  (Const8  [d])) && d != 0 => (Const8  [int8(uint8(c)/uint8(d))])
(Div16u (Const16 [c])  (Const16 [d])) && d != 0 => (Const16 [int16(uint16(c)/uint16(d))])

	// For Div16, Div32 and Div64, AuxInt non-zero means that the divisor has been proved to be not -1
	// or that the dividend is not the most negative value.
	{name: "Div8", argLength: 2},  // arg0 / arg1, signed
	{name: "Div8u", argLength: 2}, // arg0 / arg1, unsigned
	{name: "Div16", argLength: 2, aux: "Bool"},
	{name: "Div16u", argLength: 2},
	{name: "Div32", argLength: 2, aux: "Bool"},
	{name: "Div32u", argLength: 2},

		v.AddArg2(v0, v1)
		return true
	}
}
func rewriteValuePPC64_OpDiv8u(v *Value) bool {
	v_1 := v.Args[1]
	v_0 := v.Args[0]
	b := v.Block
	typ := &b.Func.Config.Types
	// match: (Div8u x y)
	// result: (DIVWU (ZeroExt8to32 x) (ZeroExt8to32 y))
	for {
		x := v_0
		y := v_1
		v.reset(OpPPC64DIVWU)
		v0 := b.NewValue0(v.Pos, OpZeroExt8to32, typ.UInt32)
		v0.AddArg(x)

		v.AddArg2(v0, v1)
		return true
	}
}
func rewriteValueS390X_OpDiv8u(v *Value) bool {
	v_1 := v.Args[1]
	v_0 := v.Args[0]
	b := v.Block
	typ := &b.Func.Config.Types
	// match: (Div8u x y)
	// result: (DIVWU (MOVBZreg x) (MOVBZreg y))
	for {
		x := v_0
		y := v_1
		v.reset(OpS390XDIVWU)
		v0 := b.NewValue0(v.Pos, OpS390XMOVBZreg, typ.UInt64)
		v0.AddArg(x)

		v.AddArg2(v0, v1)
		return true
	}
}
func rewriteValueWasm_OpDiv8u(v *Value) bool {
	v_1 := v.Args[1]
	v_0 := v.Args[0]
	b := v.Block
	typ := &b.Func.Config.Types
	// match: (Div8u x y)
	// result: (I64DivU (ZeroExt8to64 x) (ZeroExt8to64 y))
	for {
		x := v_0
		y := v_1
		v.reset(OpWasmI64DivU)
		v0 := b.NewValue0(v.Pos, OpZeroExt8to64, typ.UInt64)
		v0.AddArg(x)

(Div32u x y) => (Select0 <typ.UInt32> (CALLudiv x y))
(Div16 x y) => (Div32 (SignExt16to32 x) (SignExt16to32 y))
(Div16u x y) => (Div32u (ZeroExt16to32 x) (ZeroExt16to32 y))
(Div8 x y) => (Div32 (SignExt8to32 x) (SignExt8to32 y))
(Div8u x y) => (Div32u (ZeroExt8to32 x) (ZeroExt8to32 y))
(Div(32|64)F ...) => (DIV(F|D) ...)

(Mod32 x y) =>
	(SUB (XOR <typ.UInt32>                                                        // negate the result if x is negative

(Div32 [false] x y) => (DIVW x y)
(Div16 [false] x y) => (DIVW (SignExt16to32 x) (SignExt16to32 y))
(Div16u x y) => (UDIVW (ZeroExt16to32 x) (ZeroExt16to32 y))
(Div8   x y) => (DIVW  (SignExt8to32  x) (SignExt8to32  y))
(Div8u  x y) => (UDIVW (ZeroExt8to32  x) (ZeroExt8to32  y))
(Div64u ...) => (UDIV  ...)
(Div32u ...) => (UDIVW ...)
(Div32F ...) => (FDIVS ...)
(Div64F ...) => (FDIVD ...)

(Mod64 x y) => (MOD x y)
(Mod32 x y) => (MODW x y)

		v.AddArg2(v0, v1)
		return true
	}
}
func rewriteValue386_OpDiv8u(v *Value) bool {
	v_1 := v.Args[1]
	v_0 := v.Args[0]
	b := v.Block
	typ := &b.Func.Config.Types
	// match: (Div8u x y)
	// result: (DIVWU (ZeroExt8to16 x) (ZeroExt8to16 y))
	for {
		x := v_0
		y := v_1
		v.reset(Op386DIVWU)
		v0 := b.NewValue0(v.Pos, OpZeroExt8to16, typ.UInt16)
		v0.AddArg(x)