if a <= b {
		if b > a {
			if b == a { // ERROR "Disproved Eq64$"
				return 112
			}
			return 114
		}
		if b >= a { // ERROR "Proved Leq64$"
			if b == a { // ERROR "Proved Eq64$"
				return 118
			}
			return 120
		}
		return 122
	}
	return 124
}

func f5(a, b uint) int {
	if a == b {
		if a <= b { // ERROR "Proved Leq64U$"
			return 130
		}
		return 132
	}

// some such cases, we can redirect the predecessor If block to the
// corresponding successor block directly. For example:
//
//	p:
//	  v11 = Less64 <bool> v10 v8
//	  If v11 goto b else u
//	b: <- p ...
//	  v17 = Leq64 <bool> v10 v8
//	  If v17 goto s else o
//
// We can redirect p to s directly.
//
// The implementation here borrows the framework of the prove pass.
//
//	1, Traverse all blocks of function f to find If blocks.

(Less(64|32|16|8)U (Const(64|32|16|8) <t> [-2]) x) => (Eq(64|32|16|8) x (Const(64|32|16|8) <t> [-1]))
(Leq64 x c:(Const64 [math.MinInt64])) => (Eq64 x c)
(Leq32 x c:(Const32 [math.MinInt32])) => (Eq32 x c)
(Leq16 x c:(Const16 [math.MinInt16])) => (Eq16 x c)
(Leq8  x c:(Const8  [math.MinInt8 ])) => (Eq8  x c)
(Leq64 c:(Const64 [math.MaxInt64]) x) => (Eq64 x c)
(Leq32 c:(Const32 [math.MaxInt32]) x) => (Eq32 x c)

			(Less32U (Int64Lo x) (Int64Lo y))))

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

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

(Leq64 x y) =>
	(OrB
		(Less32 (Int64Hi x) (Int64Hi y))
		(AndB

(Less8U  x y) => (I64LtU (ZeroExt8to64  x) (ZeroExt8to64  y))
(Less(64|32)F ...) => (F(64|32)Lt ...)

(Leq64  ...) => (I64LeS ...)
(Leq32  x y) => (I64LeS (SignExt32to64 x) (SignExt32to64 y))
(Leq16  x y) => (I64LeS (SignExt16to64 x) (SignExt16to64 y))
(Leq8   x y) => (I64LeS (SignExt8to64  x) (SignExt8to64  y))
(Leq64U ...) => (I64LeU ...)
(Leq32U x y) => (I64LeU (ZeroExt32to64 x) (ZeroExt32to64 y))

(Leq32U x y) => (XOR (MOVVconst [1]) (SGTU (ZeroExt32to64 x) (ZeroExt32to64 y)))
(Leq64U x y) => (XOR (MOVVconst [1]) (SGTU x y))

(OffPtr [off] ptr:(SP)) => (MOVVaddr [int32(off)] ptr)
(OffPtr [off] ptr) => (ADDVconst [off] ptr)

(Addr {sym} base) => (MOVVaddr {sym} base)
(LocalAddr <t> {sym} base mem) && t.Elem().HasPointers() => (MOVVaddr {sym} (SPanchored base mem))

	{name: "Leq16U", argLength: 2, typ: "Bool"},
	{name: "Leq32", argLength: 2, typ: "Bool"},
	{name: "Leq32U", argLength: 2, typ: "Bool"},
	{name: "Leq64", argLength: 2, typ: "Bool"},
	{name: "Leq64U", argLength: 2, typ: "Bool"},
	{name: "Leq32F", argLength: 2, typ: "Bool"},
	{name: "Leq64F", argLength: 2, typ: "Bool"},

	// the type of a CondSelect is the same as the type of its first

		return true
	}
	// match: (Leq64U x c:(Const64 [0]))
	// result: (Eq64 x c)
	for {
		x := v_0
		c := v_1
		if c.Op != OpConst64 || auxIntToInt64(c.AuxInt) != 0 {
			break
		}
		v.reset(OpEq64)
		v.AddArg2(x, c)
		return true
	}
	// match: (Leq64U c:(Const64 [-1]) x)
	// result: (Eq64 x c)
	for {
		c := v_0

(Leq32U x y) => (XOR (MOVVconst [1]) (SGTU (ZeroExt32to64 x) (ZeroExt32to64 y)))
(Leq64U x y) => (XOR (MOVVconst [1]) (SGTU x y))

(OffPtr [off] ptr:(SP)) && is32Bit(off) => (MOVVaddr [int32(off)] ptr)
(OffPtr [off] ptr) => (ADDVconst [off] ptr)

(Addr {sym} base) => (MOVVaddr {sym} base)
(LocalAddr <t> {sym} base mem) && t.Elem().HasPointers() => (MOVVaddr {sym} (SPanchored base mem))

(Leq64      x y) => (LOCGR {s390x.LessOrEqual} (MOVDconst [0]) (MOVDconst [1]) (CMP x y))
(Leq32      x y) => (LOCGR {s390x.LessOrEqual} (MOVDconst [0]) (MOVDconst [1]) (CMPW x y))
(Leq(16|8)  x y) => (LOCGR {s390x.LessOrEqual} (MOVDconst [0]) (MOVDconst [1]) (CMPW (MOV(H|B)reg x) (MOV(H|B)reg y)))
(Leq64U     x y) => (LOCGR {s390x.LessOrEqual} (MOVDconst [0]) (MOVDconst [1]) (CMPU x y))