Образец соответствия экзистенциальной цели в Изабель

Question

Мне было интересно, есть ли способ написать следующее сопоставление с образцом:

have "∃ q1 q2 q3 q4.
        b0^2 - a1^2 = 
            q1*(-1 + a0^2 + b0^2 - t^2 * a0^2 * b0^2) +
            q2*(-1 + a1^2 + b1^2 - t^2 * a1^2 * b1^2) +
            q3*(a0 * b0 - a1 * b1) +
            q4*(a1 * b0 + a0 * b1)"   
    (is "∃ q1 q2 q3 q4. ?a = ?b")      

В настоящее время я получаю сбой сопоставления с образцом, у меня есть опасение, что это может быть вообще невозможно. ..

Answer 1

Если вы напишите это так, ?a и ?b являются константами типа bool, т.е. они не должны зависеть от q1 до q4. Поскольку, в вашем случае, оператор зависит от них, сопоставление с образцом завершится неудачно.

Вы должны записать его как

(is "∃ q1 q2 q3 q4. ?a q1 q2 q3 q4 = ?b q1 q2 q3 q4")

, и тогда оно будет работать.

В противном случае что бы использовать ?a вне экзистенциального квантификатора? Это будет относиться к переменным q1 до q4, которые нигде не связаны.