nns シリーズ
maxima 上の QE パッケージである qepmax の周辺関数を幾つか公開します．
各関数の入力と出力とは等価な式です．
・dnf,cnf
選言，連言形に変換
・ncond
変数の個数の低減（大規模な式も扱えるように map から for ループに変更しました）
・nns,nnscan,nnscand
式の個数の低減（アルゴリズムを再考し，かなり高速になりました）
・nnss
式の次数の低減（上記３つの関数の組合せによる nns シリーズの中核です）
・nnsolve,nnsolvex,nnsolvexx
式の次数の低減（ nnsolve は連立方程式，nnsolvex は連立方程式・不等式，nnsolvexx は半代数系に対して nnss と同等の処理を maxima の solve コマンドを利用して実行しますが，低速な上，後の２つは結果がQ上でないと破綻します）
・s2e,s2t
sqrt,abs,max2,min2 を消去して，存在量化，半代数系に変換（ etf_root のように精密な指定は出来ませんが，通常の数学と同じ書式が使えます）
load(qepmax)$
showtime:on$
display2d:false$
prt(x):=null$
prt(x):=print(x)$
/* compare length function */
comparelength(f,g):=length(f)<=length(g)$
comparelength2(f,g):=length(g)<=length(f)$
/* cnf dnf */
infix(Or,60,40)$
infix(And,60,40)$
matchdeclare([aa,bb,cc,dd,ee,ff,gg,aa1,bb1,cc1,dd1,ee1,ff1,gg1],true)$
defrule(ru05r, (aa) Or ((bb) And (cc)),
((aa) Or (bb)) And ((aa) Or (cc)))$
defrule(ru08r, ((bb) And (cc)) Or (aa),
((aa) Or (bb)) And ((aa) Or (cc)))$
defrule(ru05a, (aa) And ((bb) Or (cc)),
((aa) And (bb)) Or ((aa) And (cc)))$
defrule(ru08a, ((bb) Or (cc)) And (aa),
((aa) And (bb)) Or ((aa) And (cc)))$
defrule(ru00r, (aa) Or (bb), (aa) %or (bb))$
defrule(ru00a, (aa) And (bb), (aa) %and (bb))$
orand2orand(f):=block([g],g:f,
if atom(g) then return(g),
if op(g)="%or" then g:xreduce("Or",args(g)),
if op(g)="%and" then g:xreduce("And",args(g)),g)$
cnf(f):=applyb2(applyb2(scanmap(orand2orand,f),ru05r,ru08r),ru00r,ru00a)$
dnf(f):=applyb2(applyb2(scanmap(orand2orand,f),ru05a,ru08a),ru00r,ru00a)$
/* necessary condition */
ncond(f):=block([exs,L],L:[],
exs:fullmap(lambda([x],[E,x]),
sort(rest(full_listify(powerset(setify(listofvars(f))))),comparelength)),
for k:1 thru length(exs) do
(q:dnf(qe(part(exs,k),f)),prt(q),L:append(L,[q])),
return((substpart("%and",L,0))%and(f))
)$
/* non-nonsense */
nns(f):=block([F,L,M],
if atom(f) then return(f)
elseif op(f)="%and" then
(F:sort(args(f),comparelength2),L:setify(F),
for k:1 thru length(f) do
(M:disjoin(part(F,k),L),print(M),
if qe([],(substpart("%and",M,0))%implies(f))=true then L:M),
return(substpart("%and",L,0)))
elseif op(f)="%or" then
(F:sort(args(f),comparelength2),L:setify(F),
for k:1 thru length(f) do
(M:disjoin(part(F,k),L),print(M),
if qe([],(f)%implies(substpart("%or",M,0)))=true then L:M),
return(substpart("%or",L,0)))
else f)$
/*
f:qe([],(a^2=1)%and(b^2=1));
nns(f);
nns(cnf(f));
*/
/* non-nonsense scan */
nnscan(f):=scanmap(nns,f)$
/* non-nonsense scan to dnf */
nnscand(f):=scanmap(nns,dnf(f))$
/* non-nonsense set */
nnss(f):=block([f1,f2,f3,q,nns4],
if mode=d then nns4(g):=nnscand(g) else nns4(g):=nns(g),
prt("pre-simplified formula"),f1: dnf (qe ([],f) ) ,
if atom(f1) then return(f1),
prt(length(f1)),prt(f1),prt("necessary condition"),
if op(f1)="%or" then
(f2:[],
for k:1 thru length(f1) do
(q:ncond(part(f1,k)),prt(k),prt(q),f2:append(f2,[q])),
f2:substpart("%or",f2,0))
else
(f2:dnf(ncond(f1)),prt(f2)),
prt("simplifing..."),
if op(f2)="%or" then
(f3:[],
for k:1 thru length(f2) do
(q:qe([],part(f2,k)),prt(k),prt(q),f3:append(f3,[q])),
prt("nnscanning..."),f3:substpart("%or",f3,0),prt(f3),return(nns4(f3)))
else q:qe([],f2),prt(q),prt("nnscanning..."),return(nns4(q))
)$
/* nnss with double negation */
nnssdn(f):=qe([],%not(nnss(%not(f))))$
/*
qe([],x^2=1);nnss(%);
qe([[X2,x]],x^2+a*x+1=0);nnss(%);
(((x>=0)%and(x=0))%or((x>=1)%and(x=1)))%and((y>=0)%and(y=0));nnss(%);
qe([[A,x]],(x=1)%eq(x^2+a*x+b=0));nnss(%);
qe([[A,x]],(x^2+x=1)%implies(x^2+a*x=b^2))%and(b<0);nnss(%);
a^2+b^2+c^2+d^2=0;nnss(%);
((x-1/x)^2+(y^2-4*y+5)^3+(z+1)^2/z^4<=1)%and(x<0);nnss(%);
qe([[E,x]],"%and"(0<=x,x<=1,y=x^2-2*a*x));nnss(%);
(x^2-1)*(x^2-4)<0;nnss(%);
(x^2-1)*(x^2-4)*(x^2-9)<0;nnss(%);
x^3+y^3+z^3=3*x*y*z;nnss(%);
x^3+y^3+z^3>=3*x*y*z;nnss(%);
x^3+y^3+z^3<=3*x*y*z;nnss(%);
x^3+y^3+z^3>3*x*y*z;nnssdn(%);
x^3+y^3+z^3<3*x*y*z;nnssdn(%);
qe([[A,x]],(x^2+x-1=0)%eq(a*x^2+b*x+c=0));nnss(%);
(a^2+b^2<=2)%and(a*b>=1);nnss(%);
(a^2+b^2+c^2<=3)%and(a*b*c>=1);nnss(%);
*/
/* nnsolvexx */
nnsolve(f):=block([g,len,q,org],
[linsolvewarn]:false,
if nnsqesolve=false then linsolve_params:true else linsolve_params:false,
if f=true then return(f),
if op(f)="%and" then fs:f else fs:flatten([f,0]),
prt("solving..."),prt(fs),
%rnum_list:[],
g:map(lambda([l],substpart("%and",l,0)),
solve(args(fs),listofvars(fs))),
len:length(%rnum_list),
if len#0 then
(for k:1 thru len do g:subst(concat(s,k),part(%rnum_list,k),g),
q:makelist([E,concat(s,k)],k,len),
if listp(g) and length(g)#0 then
(org:substpart("%or",g,0),
return( ev(qe(q,org),noeval) )) else f)
else
if listp(g) and length(g)#0 then
return( substpart("%or",g,0) ) else f
)$
defrule(ru000, (aa) # (bb), true)$
defrule(ru001, (aa) > (bb), true)$
defrule(ru002, (aa) >= (bb), true)$
defrule(ru003, (aa) < (bb), true)$
defrule(ru004, (aa) <= (bb), true)$
defrule(ru006, (aa) = (bb), true)$
nnsolvex0(f):=
(qe([],applyb1(f,ru006)))%and(nnsolve(
(applyb2(f,ru000,ru001,ru002,ru003,ru004))
))$
nnsolvex1(f):=nns(qe([],
ev(
(qe([],applyb1(f,ru006)))%and(nnsolve(
(applyb2(f,ru000,ru001,ru002,ru003,ru004))
)),eval)
))$
nnsolvex(f):=
if nnsqesolve=false then nnsolvex0(f) else nnsolvex1(f)$
nnsolvexx(f):=block([g,gg],
prt("pre-simplified formula"),g:dnf(qe([],f)),prt(g),
if atom(g) then return(g)
else prt("necessary condition"),g:dnf(ncond(g)),prt(length(g)),prt(g),
if op(g)="%or" then (prt("simplifing..."),gg:dnf(map(ncond,g)),prt(length(gg)),prt(gg),map(nnsolvex,gg))
else nnsolvex(ncond(g))
)$
/*
nnsolvexx(x^3+y^3+z^3=3*x*y*z);
nnsolvexx((a^2+b^2<=2)%and(a*b>=1));
nnsolvexx((a^2+b^2+c^2<=3)%and(a*b*c>=1));
*/
/* sqrt to existential, Tarski formulas */
defrule(sqrt2rtk, sqrt(aa), makertk(aa))$
defrule(sqrt2rtk2, 1/sqrt(aa), 1/makertk(aa))$
defrule(sqrt2rtk3, abs(aa), makertk(aa^2))$
defrule(sqrt2rtk4, max2(aa,bb), (aa+bb+makertk((aa-bb)^2))/2)$
defrule(sqrt2rtk5, min2(aa,bb), (aa+bb-makertk((aa-bb)^2))/2)$
s2e(f):=block([L,makertk,g,q,gg],L:[],
makertk(x):=block([rtk],rtk:concat(rt,length(L)+1),
L:append(L,[(rtk^2=x)%and(rtk>=0)]),rtk),
g:applyb2(f,sqrt2rtk,sqrt2rtk2,sqrt2rtk3,sqrt2rtk4,sqrt2rtk5),
q:makelist([E,concat(rt,k)],k,length(L)),
gg:(substpart("%and",L,0))%and(g),
ev(qe(q,gg),noeval)
)$
s2t(f):=block([L,makertk,g],L:[],
makertk(x):=block([rtk],rtk:concat(rt,length(L)+1),
L:append(L,[(rtk^2=x)%and(rtk>=0)]),rtk),
g:applyb2(f,sqrt2rtk,sqrt2rtk2,sqrt2rtk3,sqrt2rtk4,sqrt2rtk5),
qe(makelist([E,concat(rt,k)],k,length(L)),(substpart("%and",L,0))%and(g))
)$
/*
nnsolve(x^2=3*y^2);s2e(%);ev(%);
qe([[X1,x]],s2t(x+k=sqrt(2-x^2)));nnss(%);
s2t(max2(a,b)=x);nnss(%);
s2t(max2(a,max2(b,c))=x);nnss(%);
s2t(abs(x-a) = abs(x-b)+c);qe([[E,x]],%);qe([],s2t((%) %eq (abs(c)<=abs(a-b))));
s2t(x=(-b+sqrt(b^2-4*a*c))/(2*a));nnss(%);
*/
LK の健全性の証明
各言語の任意の論理式は，証明論においては，証明系で証明できる式，すなわち，定理式か否かに，モデル論においては，任意の構造，任意の変数への個体割り当てに対して真となる式，すなわち，恒真式か否かに，それぞれ分類されますが，その分類が同じ結果となるという性質を，証明系の健全性と完全性と呼びます．
ここでの「健全性（soundness），および，完全性（completeness）」とは，現実の数学に正しさの基準を置くモデル論から見て，証明系が「恒真でない式を証明してしまわない（健全である）こと，および，恒真な式を漏らさず証明できる（完全である）こと」を表したものです．
勿論，pvs が基づく証明系 LK も健全かつ完全であり，例えば，ある式が証明できないことは，カウンターモデル（その式の否定のモデル，いわゆる反例）の存在と等価であり，証明可能な式は，数学のどんな分野に戻しても正しい主張になります．
そのことは，任意の閉論理式の集合Σ，任意の閉論理式φに対して
１．Σ|-φ
２．Σ∪{¬φ}|-⊥
３．Σ∪{¬φ}にモデルはない
４．任意の構造に対して
Σ∪{¬φ}には偽の式が属する，つまり
Σに属する任意の式が真ならば，φは真
５．Σ|=φ
が等価であることから判ります．
なお，健全性（１から５）を導くことは容易で，LK の各推論規則から恒真の含意が得られることを確かめれば充分です，つまり，Σの全ての要素と¬⊥の連言を∧Σ，Δの全ての要素と⊥の選言を∨Δとして（一般結合則を見た上で），シーケントΣ⇒Δに含意の全称閉包∀(∧Σ⊃∨Δ)を対応させ，LKの推論規則のうち，Σ⇒ΔからΣ'⇒Δ'という形のものに対しては
∀(∧Σ⊃∨Δ)⊃∀(∧Σ'⊃∨Δ')
が，同じく，Σ_1⇒Δ_1とΣ_2⇒Δ_2からΣ'⇒Δ'という形のものに対しては
∀(∧Σ_1⊃∨Δ_1)∧∀(∧Σ_2⊃∨Δ_2)⊃∀(∧Σ'⊃∨Δ')
が，それぞれ恒真ならば，始式の恒真性と推論の個数についての帰納法から，証明図の最下式（終式？）も恒真という訳です．
例えば，MESON で確かめると．．．
(* !L *)
MESON[] `!p r:A->bool q:A->A->bool t:A->A. (
(!y.( (p y /\ q (t y) y) ==> (r y) ))
==>
(!y.( (p y /\ (!x. q x y)) ==> (r y) ))
)` ;;
0..0..1..2..solved at 6
val it : thm =
|- !p r q t.
(!y. p y /\ q (t y) y ==> r y) ==> (!y. p y /\ (!x. q x y) ==> r y)
#
(* ?L *)
MESON[] `!p r:A->bool q:A->A->bool. (
(!x y.( (p y /\ q x y) ==> (r y) ))
==>
(!y.( (p y /\ (?x. q x y)) ==> (r y) ))
)` ;;
0..0..1..2..solved at 6
val it : thm =
|- !p r q.
(!x y. p y /\ q x y ==> r y) ==> (!y. p y /\ (?x. q x y) ==> r y)
#
(* cut *)
MESON[] `!p q r:A->bool. (
(!x.( (p x /\ q x) ==> (r x) )) /\ (!x.( (p x) ==> (q x \/ r x) ))
==>
(!x.( (p x) ==> (r x) ))
)` ;;
0..0..1..2..7..12..solved at 18
val it : thm =
|- !p q r.
(!x. p x /\ q x ==> r x) /\ (!x. p x ==> q x \/ r x)
==> (!x. p x ==> r x)
となります．
「開いた式」
「開いた式」とは「変数の自由出現（あるいは自由変数）を含む論理式」のことで，その真理値の定め方には幾つかの立場があります．
言語，構造を固定した上で，伝統的（？）なのは，変数への個体割り当てを用いて
立場１ 割り当て毎に真偽を与える
立場２ 割り当て毎には充足性（＝立場１での真偽）を与え，任意の割り当てが充足する式に真を与える（ただし，偽は否定した式が真のこととするので，その式も否定も真とならないことがある）
というものです．
恒真性の定義では，構造，割り当てともに動くので（証明可能性が全称閉包をとっても変わらないことに対応），どちらの立場でも構いませんし，閉じた式（変数の自由出現を含まない論理式，いわゆる文）なら尚更ですから，変数への個体割り当てを用いずに，最初から
立場３ 全称閉包を評価する
のが簡明です．
というわけで，pvs に
x,y:var real f1:lemma x=y => (x=y or x<y)
と入力すると，黙って
f1 :
|-------
{1} FORALL (x, y: real): x = y => (x = y OR x < y)
から始まりますし，高階なので
p,q:var [[real,real]->bool] f2:lemma p(x, y) => (p(x, y) or q(x, y))
でも
f2 :
|-------
{1} FORALL (p, q: [[real, real] -> bool], x, y: real):
p(x, y) => (p(x, y) OR q(x, y))
から始まります．
また，立場３と同じく，変数への個体割り当てを用いない方法として，言語を拡張し
立場４ 新たな定数を導入，変数に代入して，閉じさせる
という，自由変数への割り当てを構造の定数の解釈で賄うものもあり，pvs のスコーレム定数はそれと見做すこともできます．
f1 :
|-------
{1} FORALL (x, y: real): x = y => (x = y OR x < y)
Rule? (skolem!)
Skolemizing,
this simplifies to:
f1 :
|-------
{1} x!1 = y!1 => (x!1 = y!1 OR x!1 < y!1)
f2 :
|-------
{1} FORALL (p, q: [[real, real] -> bool], x, y: real):
p(x, y) => (p(x, y) OR q(x, y))
Rule? (skolem!)
Skolemizing,
this simplifies to:
f2 :
|-------
{1} p!1(x!1, y!1) => (p!1(x!1, y!1) OR q!1(x!1, y!1))
なお，Shoenfield辺りでは，解釈が各個体となる新たな定数（いわゆる名前name）を導入，代入して，その任意のインスタンスが真となることを恒真としていますが．．．
Empty domain
古典的（？）な一階の古典論理の意味論では，ドメインAは空でないとされ，その理由として，Aが空では，∀x.p(x)，つまり「任意のxについて，x∈Aならばp(x)」が真，∃x.p(x)つまり「あるxについて，x∈Aかつp(x)」が偽，したがって，定理式
∀x.p(x)→∃x.p(x)
が偽となることが挙げられます．
一方，PVSでのドメインの宣言には
A:TYPE
と
A:TYPE+ 略さないなら A:NONEMPTY_TYPE
とがあり前者はAが空でも構いません．その場合，健全性を破棄しない以上，上記の含意は証明できない筈であり，実際
A:TYPE x,y:var A p:[A->bool]
としても
f01 :
|-------
{1} (FORALL (x): p(x)) => (EXISTS (x): p(x))
Rule? (flatten)
Applying disjunctive simplification to flatten sequent,
this simplifies to:
f01 :
{-1} (FORALL (x): p(x))
|-------
{1} (EXISTS (x): p(x))
Rule? (inst - "y" )
The supplied terms should not contain free variables.
The following irrelevant free variables occur in the terms: (y)
No change on: (inst - "y")
のように弾かれます．つまり，instantiate できるのは，宣言済みのドメインに属する定数，または，例えば
q:[A->bool]
とした上での
f02 :
|-------
{1} ((EXISTS (x): q(x)) AND (FORALL (x): p(x))) => (EXISTS (x): p(x))
Rule? (flatten)
Applying disjunctive simplification to flatten sequent,
this simplifies to:
f02 :
{-1} (EXISTS (x): q(x))
{-2} (FORALL (x): p(x))
|-------
{1} (EXISTS (x): p(x))
Rule? (skosimp*)
Repeatedly Skolemizing and flattening,
this simplifies to:
f02 :
{-1} q(x!1)
[-2] (FORALL (x): p(x))
|-------
[1] (EXISTS (x): p(x))
Rule? (inst - "x!1" )
Instantiating the top quantifier in - with the terms:
x!1,
this simplifies to:
f02 :
[-1] q(x!1)
{-2} p(x!1)
|-------
[1] (EXISTS (x): p(x))
Rule? (inst + "x!1" )
Instantiating the top quantifier in + with the terms:
x!1,
Q.E.D.
のようなスコーレム定数から構成された，いわゆる「閉項」のみという訳です．これは，代入する項に既に式内で量化されている変数が含まれている可能性を排したもので，例えば「∀x. ∃y. p(x, y) の x を y に inst して，∃y. p(y, y) を得る」といった事態を回避できます．
HOL Light だと，この辺りは，普通に
# g `(!x:A. ?y:A. p x y) ==> q` ;; Warning: Free variables in goal: p, q val it : goalstack = 1 subgoal (1 total) `(!x. ?y. p x y) ==> q` # e( STRIP_TAC );; val it : goalstack = 1 subgoal (1 total) 0 [`!x. ?y. p x y`] `q` # e( FIRST_X_ASSUM (ASSUME_TAC o (SPEC `y:A`) ) );; val it : goalstack = 1 subgoal (1 total) 0 [`?y'. p y y'`] `q`
と束縛変数が逃げてくれます（α変換ではなく，最初から，束縛変数と自由変数を使い分けるのが穏健ですが）．
PVSの使い方
今更ですが，使い方です．端末から
pvs
とすると，emacsが起動し
M-x nf
でNew file name:と尋ねられ，例えばdemoe20160519と適当に入力すれば，demo20160519.pvsが
demo20160519 % [ parameters ] : THEORY BEGIN % ASSUMING % assuming declarations % ENDASSUMING END demo20160519
のような初期内容で生成されます．そこで，例えば
demo20160519 % [ parameters ] : THEORY BEGIN % ASSUMING % assuming declarations A:TYPE+ a:A x,y:var A p:[A->bool] % ENDASSUMING f01:lemma exists(x):(p(x)=>(forall(y):(p(y)))) END demo20160519
のように宣言とステートメントと書き込み（type,var,lemmaといった予約語はcase insensitive）
M-x pr
とすれば
Installing rewrite rule sets.singleton_rew (all instances)
f01 :
|-------
{1} EXISTS (x): (p(x) => (FORALL (y): (p(y))))
Rule?
のような＊pvs＊バッファが開くので，以下のように順次入力する（実際には，TABの後に，fでflatten，iでinstなどのバインドを用います．キーバインド一覧はTAB h，また，コマンドの一覧はTABのみの連打，＊pvs＊ への復帰はq）と
f01 :
|-------
{1} EXISTS (x): (p(x) => (FORALL (y): (p(y))))
Rerunning step: (inst-cp 1 "a")
Instantiating (with copying) the top quantifier in 1 with the terms:
a,
this simplifies to:
f01 :
|-------
[1] EXISTS (x): (p(x) => (FORALL (y): (p(y))))
{2} (p(a) => (FORALL (y): (p(y))))
Rerunning step: (flatten)
Applying disjunctive simplification to flatten sequent,
this simplifies to:
f01 :
{-1} p(a)
|-------
[1] EXISTS (x): (p(x) => (FORALL (y): (p(y))))
{2} (FORALL (y): (p(y)))
Rerunning step: (skeep*)
Iterating skeep in '*,
this simplifies to:
f01 :
{-1} p(a)
|-------
{1} EXISTS (x): (p(x) => (FORALL (y): (p(y))))
{2} (p(y))
Rerunning step: (inst 1 "y")
Instantiating the top quantifier in 1 with the terms:
y,
this simplifies to:
f01 :
[-1] p(a)
|-------
{1} (p(y) => (FORALL (y): (p(y))))
[2] (p(y))
Rerunning step: (flatten)
Applying disjunctive simplification to flatten sequent,
Q.E.D.
となり，先のバッファに戻るので，ポインターをf01上に置き
C-c 2 p
とすれば
demo20160519 % [ parameters ] : THEORY BEGIN % ASSUMING % assuming declarations A:TYPE+ a:A x,y:var A p:[A->bool] % ENDASSUMING f01:lemma exists(x):(p(x)=>(forall(y):(p(y)))) %|- f01 : PROOF %|- (then (inst-cp 1 "a") (flatten) (skeep*) (inst 1 "y") (flatten)) %|- QED END demo20160519
のようにプルーフスクリプトが書き込まれます．手を加えたい場合は，先度，M-x pr，もしくは直接
%|- f01 : PROOF %|- (then (inst-cp + "a") (flatten) (skeep*) (inst + "y") (flatten)) %|- QED
C-c ! p
とすれば，インストールされます．なお，コメントアウトには，C-c ; が使えます．
また，＊pvs＊上での一般の操作でよく用いるのは
クイットは，q，または，C-z z （grindが帰ってこないときなどに便利な）インタラプトは，C-c C-c で，LISPに入ってしまった場合の復帰は，(restore) コマンドの前後に括弧を付して実行は，C-j コマンド履歴は．M-s，または，C-上下矢印
辺りでしょう．
skeep
PVSのskeepコマンドは，本来は x!1 などのように新規に導入すべきスコーレム定数を，衝突がない限り束縛されていた変数と同じ名前で導入してくれます．
f1 :
|-------
{1} (EXISTS (x: A): (p(x))) AND (EXISTS (x: A): (q(x))) =>
(EXISTS (x: A): (p(x) AND (EXISTS (x: A): (q(x)))))
Rule? (flatten)
Applying disjunctive simplification to flatten sequent,
this simplifies to:
f1 :
{-1} (EXISTS (x: A): (p(x)))
{-2} (EXISTS (x: A): (q(x)))
|-------
{1} (EXISTS (x: A): (p(x) AND (EXISTS (x: A): (q(x)))))
Rule? (skeep*)
Iterating skeep in '*,
this simplifies to:
f1 :
{-1} (p(x))
{-2} (q(x!1))
|-------
{1} (EXISTS (x: A): (p(x) AND (EXISTS (x: A): (q(x)))))
Rule? (inst + "x")
Instantiating the top quantifier in + with the terms:
x,
this simplifies to:
f1 :
[-1] (p(x))
[-2] (q(x!1))
|-------
{1} (p(x) AND (EXISTS (x: A): (q(x))))
Rule? (split)
Splitting conjunctions,
this yields 2 subgoals:
f1.1 :
[-1] (p(x))
[-2] (q(x!1))
|-------
{1} p(x)
which is trivially true.
This completes the proof of f1.1.
f1.2 :
[-1] (p(x))
[-2] (q(x!1))
|-------
{1} (EXISTS (x: A): (q(x)))
Rule? (inst + "x!1")
Instantiating the top quantifier in + with the terms:
x!1,
This completes the proof of f1.2.
Q.E.D.
HOL Light vs PVS (3)
g `!n. 8 <= n ==> (?x y. n = 3 * x + 5 * y)` ;; e( INDUCT_TAC );; e( ARITH_TAC );; e( REWRITE_TAC [LE] THEN REPEAT STRIP_TAC );; e( EXISTS_TAC `1` THEN EXISTS_TAC `1` THEN ASM_ARITH_TAC );; e( FIRST_X_ASSUM (fun t -> FIRST_ASSUM (MP_TAC o (MATCH_MP t))) THEN STRIP_TAC );; e( ASM_CASES_TAC `y = 0` );; e( EXISTS_TAC `x - 3` THEN EXISTS_TAC `2` THEN ASM_ARITH_TAC );; e( EXISTS_TAC `x + 2` THEN EXISTS_TAC `y - 1` THEN ASM_ARITH_TAC );;
f01:lemma forall(n:nat): 8 <= n => exists(x,y:nat): n = 3 * x + 5 * y %|- f01 : PROOF %|- (spread (induct "n" 1) %|- ((ground) %|- (then (skeep*) %|- (spread (split) %|- ((then (skeep*) %|- (spread (case "y = 0") %|- ((spread (inst + "x - 3" "2") ((ground) (ground))) %|- (spread (inst + "x + 2" "y - 1") ((ground) (ground)))))) %|- (then (inst 2 "1" "1") (ground))))))) %|- QED
カットオフされない為の場合分け（y=0 のとき3<=x，および，not(y=0) のとき1<=y）について，HOL Light は黙って判ってくれますが，PVSは
f01.2.1.1.2 (TCC):
[-1] y = 0
[-2] j = 3 * x + 5 * y
[-3] 8 <= j + 1
|-------
{1} x - 3 >= 0
f01.2.1.2.2 (TCC):
[-1] j = 3 * x + 5 * y
[-2] 8 <= j + 1
|-------
{1} y - 1 >= 0
[2] y = 0
のように確認してきます．
