问题标签 [leon]

我正在尝试使用 Welder 通过双重感应来证明一个属性。定义取自这里。可以在此处找到提供该理论更多细节的相关问题。无论如何，我只需要一些部分来显示我的问题：

基本上，我正在使用整数形式的表达式，POP(i,p)并且POW(i,p,q). 它们有一个正态性，称为 n。我想证明 if n(x) && n(y)then n(x+y)。

我们来看看具体的情况x = POP(i,p)，y = POP(j,q)然后x+y定义如下：

wherepop是一个模拟POP具有一些细微差异的构造的函数。

我在 Welder 中通过双重归纳进行证明如下：

我要关注的相关案例如下：

这里normpop1Lemma指出，为了拥有n(pop(i,p))你需要i自然和p正常。但是，我发现第二种情况没有得到证明。事实上，我需要将第二个属性概括为

但那我不是在打破感应吗？我真的可以解决这些案件i > j吗i < j？（在我实验的时候还有更多）

编辑

目前，我可以先在 y 上感应，然后在 x 上感应，对于 POP-POP 案例，我可以显示哪些情况i = j，i > j但i < j不是。我认为它可以通过使用它来工作，POP(j-i,q) + p = p + POP(j-i,q)但事实并非如此。

相反，现在我试图证明两个不同的属性，假设其中一个案例不能成立（要么 thei < j要么 the i > j）。