z3 - 关于在线使用 Z3Py 应用 Routh-Hurwitz 定理的问题

Question

示例 1：

我们使用以下代码应用 RH 定理

K = Real('K')
print simplify(And(12 - 3*K >0 , 20 + 0.25*K >0))

输出是：

¬(K ≥ 4) ∧ ¬(K ≤ -80)

示例 2：

我们使用以下代码应用 RH 定理

K, a1, a2, a3 = Reals('K a1 a2 a3')
a1 = 20 + 1.5*K
a2 = 4
a3 = 4*K -100
print simplify(And(a1 > 0 , a3 > 0, a1*a2 > a3))

输出是

¬(K ≤ -40/3) ∧ ¬(K ≤ 25) ∧ ¬(K ≤ -90)

示例 3：

我们使用以下代码应用 RH 定理

K = Real('K')
a1 = 10
a2 = 30 - 2.4*K
a3 =  2
a4 = 100 + 5*K
print simplify(And(a4 > 0, a1*a2*a3 > a3**2 + a4*a1**2))

输出是

¬(K ≤ -20) ∧ ¬(K ≥ -2351/137)

示例 4：

我们使用以下代码应用 RH 定理

u, s, d, g, N, b , a = Reals('u s d g N b a')
c1 = 2*u + s + d + g
prove(Implies(And(u > 0, s > 0, d >0, g >0), c1 > 0))
c2 = u*g + u**2 + s*u + 2*d*u + s*d + s*g + d*g
c3 = d*u**2 - N*a*b*s + d*u*g + s*d*u + s*d*g
prove(Implies(And(u > 0, s > 0, d >0, g >0, a >0, b > 0, N >0), c1*c2 > c3))

输出是：

proved
proved

剩余相对湿度条件：c3 > 0 导致

示例 5：

我们使用以下代码应用 RH 定理

u, s1, s2, d, g, N, b , a = Reals('u s1 s2 d g N b a')
c1 = d + 3*u + s1 + g + s2
prove(Implies(And(u > 0, s1 > 0, s2 > 0, d >0, g >0), c1 > 0))
c2 = s2*g + 3*d*u + d*g + d*s1+ s1*s2 + 3*u**2 + 2*s2*u + 2*s1*u+ s1*g + 2*u*g + d*s2 
c3 = 2*d*u*g + s1*u*g + 2*d*s2*u + 3*d*u**2 + d*g*s1 + s1*s2*g + u**3 + u*s2*g +  2*d*s1*u + s1*s2*u + g*u**2 + d*g*s2 + s1*u**2 + d*s1*s2 + s2*u**2
prove(Implies(And(u > 0, s1 > 0, s2 >0, d >0, g >0, a >0, b > 0, N >0), c3 > 0))
c4 = d*g*u**2 + d*s2*u**2 + s1*d*u*g + s1*d*s2*u + s1*d*s2*g - N*a*b*s1*s2 + d*u**3 +  s1*d*u**2 + d*u*s2*g
prove(Implies(And(u > 0, s1 > 0, s2 >0, d >0, g >0, a >0, b > 0, N >0), c1*c2*c3 >  c3**2 + c4*c1**2))

输出是：

proved
proved
proved

它也可以在这里在线试用。

剩余相对湿度条件：c4 > 0 导致

问题：

1. 如果您知道针对此类问题的更有效代码，请告诉我

2. 如何简化示例 1、2 和 3 的输出。

3. 对于示例 4，如何使用 Z3Py 求解关于 b 的 c3 > 0，然后获得 Ro 的公式

4. 对于示例 5，如何使用 Z3Py 求解关于 b 的 c4 > 0，然后获得 Ro 的公式

非常感谢。