func lim1(x, y, z int) {
	// Test relations between signed and unsigned limits.
	if x > 5 {
		if uint(x) > 5 { // ERROR "Proved Less64U$"
			return
		}
	}
	if y >= 0 && y < 4 {
		if uint(y) > 4 { // ERROR "Disproved Less64U$"
			return
		}
		if uint(y) < 5 { // ERROR "Proved Less64U$"
			return
		}
	}
	if z < 4 {
		if uint(z) > 4 { // Not provable without disjunctions.
			return
		}
	}
}

(Eq64 x y) =>
	(AndB
		(Eq32 (Int64Hi x) (Int64Hi y))
		(Eq32 (Int64Lo x) (Int64Lo y)))

(Neq64 x y) =>
	(OrB
		(Neq32 (Int64Hi x) (Int64Hi y))
		(Neq32 (Int64Lo x) (Int64Lo y)))

(Less64U x y) =>
	(OrB
		(Less32U (Int64Hi x) (Int64Hi y))
		(AndB
			(Eq32 (Int64Hi x) (Int64Hi y))
			(Less32U (Int64Lo x) (Int64Lo y))))

(Leq64U x y) =>
	(OrB
		(Less32U (Int64Hi x) (Int64Hi y))

(Less64  ...) => (I64LtS ...)
(Less32  x y) => (I64LtS (SignExt32to64 x) (SignExt32to64 y))
(Less16  x y) => (I64LtS (SignExt16to64 x) (SignExt16to64 y))
(Less8   x y) => (I64LtS (SignExt8to64  x) (SignExt8to64  y))
(Less64U ...) => (I64LtU ...)
(Less32U x y) => (I64LtU (ZeroExt32to64 x) (ZeroExt32to64 y))
(Less16U x y) => (I64LtU (ZeroExt16to64 x) (ZeroExt16to64 y))
(Less8U  x y) => (I64LtU (ZeroExt8to64  x) (ZeroExt8to64  y))

(Less64  ...) => (SLT  ...)
(Less32  x y) => (SLT  (SignExt32to64 x) (SignExt32to64 y))
(Less16  x y) => (SLT  (SignExt16to64 x) (SignExt16to64 y))
(Less8   x y) => (SLT  (SignExt8to64  x) (SignExt8to64  y))
(Less64U ...) => (SLTU ...)
(Less32U x y) => (SLTU (ZeroExt32to64 x) (ZeroExt32to64 y))
(Less16U x y) => (SLTU (ZeroExt16to64 x) (ZeroExt16to64 y))
(Less8U  x y) => (SLTU (ZeroExt8to64  x) (ZeroExt8to64  y))

(Less8U x y)  => (SGTU (ZeroExt8to64 y) (ZeroExt8to64 x))
(Less16U x y) => (SGTU (ZeroExt16to64 y) (ZeroExt16to64 x))
(Less32U x y) => (SGTU (ZeroExt32to64 y) (ZeroExt32to64 x))
(Less64U x y) => (SGTU y x)

(Leq8 x y)  => (XOR (MOVVconst [1]) (SGT (SignExt8to64 x) (SignExt8to64 y)))
(Leq16 x y) => (XOR (MOVVconst [1]) (SGT (SignExt16to64 x) (SignExt16to64 y)))

			v2.AuxInt = int8ToAuxInt(d - c)
			v.AddArg2(v0, v2)
			return true
		}
		break
	}
	// match: (AndB (Less64U (Const64 [c]) x) (Less64U x (Const64 [d])))
	// cond: uint64(d) >= uint64(c+1) && uint64(c+1) > uint64(c)
	// result: (Less64U (Sub64 <x.Type> x (Const64 <x.Type> [c+1])) (Const64 <x.Type> [d-c-1]))
	for {
		for _i0 := 0; _i0 <= 1; _i0, v_0, v_1 = _i0+1, v_1, v_0 {

// unsigned integer range: ( c < x && x (<|<=) d ) -> ( x-(c+1) (<|<=) d-(c+1) )
(AndB (Less64U (Const64 [c]) x) ((Less|Leq)64U x (Const64 [d]))) && uint64(d) >= uint64(c+1) && uint64(c+1) > uint64(c) => ((Less|Leq)64U (Sub64 <x.Type> x (Const64 <x.Type> [c+1])) (Const64 <x.Type> [d-c-1]))

(Less8U x y)  => (SGTU (ZeroExt8to64 y) (ZeroExt8to64 x))
(Less16U x y) => (SGTU (ZeroExt16to64 y) (ZeroExt16to64 x))
(Less32U x y) => (SGTU (ZeroExt32to64 y) (ZeroExt32to64 x))
(Less64U x y) => (SGTU y x)

(Leq8 x y)  => (XOR (MOVVconst [1]) (SGT (SignExt8to64 x) (SignExt8to64 y)))
(Leq16 x y) => (XOR (MOVVconst [1]) (SGT (SignExt16to64 x) (SignExt16to64 y)))

	{name: "Less16U", argLength: 2, typ: "Bool"},
	{name: "Less32", argLength: 2, typ: "Bool"},
	{name: "Less32U", argLength: 2, typ: "Bool"},
	{name: "Less64", argLength: 2, typ: "Bool"},
	{name: "Less64U", argLength: 2, typ: "Bool"},
	{name: "Less32F", argLength: 2, typ: "Bool"},
	{name: "Less64F", argLength: 2, typ: "Bool"},

	{name: "Leq8", argLength: 2, typ: "Bool"},  // arg0 <= arg1, signed

		v.AddArg2(v0, v3)
		return true
	}
}
func rewriteValuedec64_OpLess64U(v *Value) bool {
	v_1 := v.Args[1]
	v_0 := v.Args[0]
	b := v.Block
	typ := &b.Func.Config.Types
	// match: (Less64U x y)
	// result: (OrB (Less32U (Int64Hi x) (Int64Hi y)) (AndB (Eq32 (Int64Hi x) (Int64Hi y)) (Less32U (Int64Lo x) (Int64Lo y))))
	for {
		x := v_0
		y := v_1
		v.reset(OpOrB)