ACL2 で鳩の巣の原理を使ってみた
目次
投稿日: 2022-03-26 土
1. 注意
この記事はいま思うとあまりよく分かっていなかったときに書いたものなので参考にしない方がいいです。 近々、本当に役に立つ初心者向けの記事を書く予定なので作成しだいここにリンクを張る予定です。
2. はじめに
本記事では ACL2 で鳩の巣の原理を使った証明ができることを確認します。
この記事は ACL2 を実際に使って定理証明をする作業がどんな感じなのかがよく分かるようになっていると思います。 そのような記事は日本語圏において現在のところ一つもないと思うので大変貴重なものだと思います(自画自賛)。
ACL2 による自動定理証明って少し気になるけどなんか学習コスト高そうだしやめとこうかなーって感じの人に是非見てもらいたいです。 ただし、ACL2 の使い方の説明として十分なものとはとても言えません。 実際に ACL2 を使うには ACL2 - ACL2-tutorial を読まないと路頭に迷う可能性が高いので注意してください。
本記事は過去に私が書いた acl2-theorems/pigeonhole.lisp というコードをベースにしてます。 「じゃあそのコード読めばよくね？この記事意味あるの？」って考えられると予想していますが、 正直なところ ACL2 のうまくいっているコードってなんでそうなっているのかまるで意味不明なんですよね。 何故かというと ACL2 で定理の証明に失敗したときに得られる情報を使って補助定理やヒントを書いているので、 結果だけ見てもその過程が失われてしまうからです。 なお、目的を明確にして書き直しているので関数や定理の名前や形は元のコードから多少変わっていることに注意してください。
org-mode から ACL2 を動かしてそのまま文書を作成してサイトに投稿する仕組みが整ったので、 ACL2 で色々証明して投稿していくという個人的な企画をやっているので、 これからも ACL2 で何かを証明してみた系の記事は続く予定です。
本記事中のプログラムのライセンスは acl2-theorems/pigeonhole.lisp と同様に3条項BSDライセンスとします。
3. そもそも鳩の巣の原理って何？
鳩の巣の原理とは以下のようなものです。
鳩を入れる箱が n 個あったときに鳩が m 羽いたとします。
ここで n < m のとき、鳩を全ていずれかの箱に入れると、
必ず1つの箱に2羽以上入っている箱が少なくとも1つはあります。
鳩を箱に入れようとする人は私が知っている範囲だと実験的行動分析の人くらいしかいない気がするというのはおいておいて、 ともかく上記のように定式化できるものを鳩の巣の原理と呼ぶのです。
たとえば、 367 人以上の生徒が集まる全校集会では必ず生徒の誕生日が重複するということが鳩の巣の原理を使うといえるので結構身近な問題です。
4. pigeonhole の定理の紹介
というわけで鳩の巣の原理を Lisp 的に表現した下記の定理を証明したいと思います。
下記の用に pigeonhole の定理を定義します。
(defthm pigeonhole
(implies (and (subsetp x s)
(< (len s) (len x))
(no-duplicatesp s))
(not (no-duplicatesp x))))
証明失敗: 出力を確認する
ACL2 Warning [Free] in ( DEFTHM PIGEONHOLE ...): A :REWRITE rule generated
from PIGEONHOLE contains the free variable S. This variable will be
chosen by searching for an instance of (SUBSETP-EQUAL X S) in the context
of the term being rewritten. This is generally a severe restriction
on the applicability of a :REWRITE rule. See :DOC free-variables.
Goal'
([ A key checkpoint:
Goal'
(IMPLIES (AND (SUBSETP-EQUAL X S)
(< (LEN S) (LEN X))
(NO-DUPLICATESP-EQUAL S))
(NOT (NO-DUPLICATESP-EQUAL X)))
*1 (Goal') is pushed for proof by induction.
])
Perhaps we can prove *1 by induction. Five induction schemes are suggested
by this conjecture. These merge into two derived induction schemes.
However, one of these is flawed and so we are left with one viable
candidate.
We will induct according to a scheme suggested by (NO-DUPLICATESP-EQUAL X),
but modified to accommodate (LEN X) and (SUBSETP-EQUAL X S). These
suggestions were produced using the :induction rules LEN,
NO-DUPLICATESP-EQUAL and SUBSETP-EQUAL. If we let (:P S X) denote
*1 above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X))
(NOT (MEMBER-EQUAL (CAR X) (CDR X)))
(:P S (CDR X)))
(:P S X))
(IMPLIES (AND (NOT (ENDP X))
(MEMBER-EQUAL (CAR X) (CDR X)))
(:P S X))
(IMPLIES (ENDP X) (:P S X))).
This induction is justified by the same argument used to admit
NO-DUPLICATESP-EQUAL. When applied to the goal at hand the above induction
scheme produces five nontautological subgoals.
Subgoal *1/5
Subgoal *1/5'
Subgoal *1/4
Subgoal *1/4'
Subgoal *1/4''
Subgoal *1/4'''
Subgoal *1/4'4'
Subgoal *1/4'5'
Subgoal *1/4'6'
Subgoal *1/4'7'
Subgoal *1/4'8'
Subgoal *1/4'9'
Subgoal *1/4'10'
([ A key checkpoint while proving *1 (descended from Goal'):
Subgoal *1/4'4'
(IMPLIES (AND (EQUAL (LEN (CDR X)) (LEN S))
(CONSP X)
(NOT (MEMBER-EQUAL (CAR X) (CDR X)))
(<= (LEN S) (LEN S))
(MEMBER-EQUAL (CAR X) S)
(SUBSETP-EQUAL (CDR X) S)
(< (LEN S) (+ 1 (LEN S)))
(NO-DUPLICATESP-EQUAL S))
(NOT (NO-DUPLICATESP-EQUAL (CDR X))))
*1.1 (Subgoal *1/4'10') is pushed for proof by induction.
])
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/1
Subgoal *1/1'
So we now return to *1.1, which is
(IMPLIES (AND (NOT (MEMBER-EQUAL X1 X2))
(MEMBER-EQUAL X1 S)
(SUBSETP-EQUAL X2 S)
(NO-DUPLICATESP-EQUAL S))
(NOT (NO-DUPLICATESP-EQUAL X2))).
Subgoal *1.1/5
Subgoal *1.1/5'
Subgoal *1.1/4
Subgoal *1.1/4'
Subgoal *1.1/3
Subgoal *1.1/3'
Subgoal *1.1/2
Subgoal *1.1/2'
Subgoal *1.1/1
Subgoal *1.1/1'
Subgoal *1.1/1''
Subgoal *1.1/1'''
*1.1.1 (Subgoal *1.1/1''') is pushed for proof by induction.
So we now return to *1.1.1, which is
(IMPLIES (MEMBER-EQUAL X1 S)
(NOT (NO-DUPLICATESP-EQUAL S))).
Subgoal *1.1.1/4
Subgoal *1.1.1/4'
Subgoal *1.1.1/3
Subgoal *1.1.1/3'
Subgoal *1.1.1/3''
Subgoal *1.1.1/3'''
Subgoal *1.1.1/3'4'
Subgoal *1.1.1/3'5'
*1.1.1.1 (Subgoal *1.1.1/3'5') is pushed for proof by induction.
Subgoal *1.1.1/2
Subgoal *1.1.1/2'
Subgoal *1.1.1/2''
Subgoal *1.1.1/1
Subgoal *1.1.1/1'
So we now return to *1.1.1.1, which is
(IMPLIES (NOT (MEMBER-EQUAL S1 S2))
(NOT (NO-DUPLICATESP-EQUAL S2))).
Subgoal *1.1.1.1/4
Subgoal *1.1.1.1/4'
Subgoal *1.1.1.1/3
Subgoal *1.1.1.1/3'
Subgoal *1.1.1.1/2
Subgoal *1.1.1.1/2'
Subgoal *1.1.1.1/1
Subgoal *1.1.1.1/1'
Subgoal *1.1.1.1/1''
Subgoal *1.1.1.1/1'''
A goal of NIL, Subgoal *1.1.1.1/1''', has been generated! Obviously,
the proof attempt has failed.
Summary
Form: ( DEFTHM PIGEONHOLE ...)
Rules: ((:DEFINITION ENDP)
(:DEFINITION LEN)
(:DEFINITION MEMBER-EQUAL)
(:DEFINITION NO-DUPLICATESP-EQL-EXEC$GUARD-CHECK)
(:DEFINITION NO-DUPLICATESP-EQUAL)
(:DEFINITION NOT)
(:DEFINITION RETURN-LAST)
(:DEFINITION SUBSETP-EQL-EXEC$GUARD-CHECK)
(:DEFINITION SUBSETP-EQUAL)
(:ELIM CAR-CDR-ELIM)
(:FAKE-RUNE-FOR-LINEAR NIL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION LEN)
(:INDUCTION MEMBER-EQUAL)
(:INDUCTION NO-DUPLICATESP-EQUAL)
(:INDUCTION SUBSETP-EQUAL)
(:TYPE-PRESCRIPTION LEN)
(:TYPE-PRESCRIPTION MEMBER-EQUAL))
Warnings: Free
Time: 0.03 seconds (prove: 0.02, print: 0.00, other: 0.00)
Prover steps counted: 6708
---
The key checkpoint goals, below, may help you to debug this failure.
See :DOC failure and see :DOC set-checkpoint-summary-limit.
---
*** Key checkpoint at the top level: ***
Goal'
(IMPLIES (AND (SUBSETP-EQUAL X S)
(< (LEN S) (LEN X))
(NO-DUPLICATESP-EQUAL S))
(NOT (NO-DUPLICATESP-EQUAL X)))
*** Key checkpoint under a top-level induction
before generating a goal of NIL (see :DOC nil-goal): ***
Subgoal *1/4'4'
(IMPLIES (AND (EQUAL (LEN (CDR X)) (LEN S))
(CONSP X)
(NOT (MEMBER-EQUAL (CAR X) (CDR X)))
(<= (LEN S) (LEN S))
(MEMBER-EQUAL (CAR X) S)
(SUBSETP-EQUAL (CDR X) S)
(< (LEN S) (+ 1 (LEN S)))
(NO-DUPLICATESP-EQUAL S))
(NOT (NO-DUPLICATESP-EQUAL (CDR X))))
ACL2 Error in ( DEFTHM PIGEONHOLE ...): See :DOC failure.
******** FAILED ********
当然のように定理の証明に失敗していますが、 その解説の前にこの定理が何を表現しているのかについて説明します。
s は巣箱の ID のリストです。
ID が具体的にどう表現されているかは重要ではありません。
no-duplicatesp はリストに重複がないことを調べる関数なのですが、
これを使って s に重複がないことを確認します。
x は鳩が実際に入っている巣箱のIDのリストを表現しています。
イメージとしては鳩を0羽目の鳩、1羽目の鳩、2羽目の鳩……と横に並べていると思ってください。
x はそれらの鳩が入っている巣箱IDを鳩と同じ順番に並べたものです。
たとえば (nth 5 x) が、 A であったとしましょう。
これは 5 羽目の鳩が A という巣箱に入っているということを意味します。
1つ目の仮定である (subsetp x s) とは x の要素が全て巣箱 ID であるということを表現しています。
なお、 subsetp 関数はリストの中身に重複があってもなくても機能するということは重要なので気をつけてください。
2つ目の仮定である (< (len s) (len x)) についてですが、
s が重複のない巣箱IDのリストなので (len s) とは巣箱の数を表現しています。
x は鳩が入っている巣箱IDのリストなので (len x) は鳩の数を表現しています。
よって (< (len s) (len x)) とは巣箱の数よりも鳩の数が多いということを意味します。
3つ目の仮定である (no-duplicatesp s) は巣箱の ID に重複がないことを確認しています。
この定理の帰結の (not (no-duplicatesp x)) は x には重複があるということを意味します。
x は鳩が入っている巣箱 ID のリストのため、これに重複があるということは同じ巣箱に二羽以上入っている巣箱が存在することを示しています。
no-duplicatesp は重複がないことを確認する関数でその結果を否定することで重複の存在を確認しています。二重否定になっていて分かりにくいですが我慢してください。
この定理を日本語で簡潔に説明すると次のようになります。
- 定理: pigeonhole
- 仮定
- リスト
xの要素は全てリストsの要素である - リスト
sよりもリストxの方が長い(多くの要素がある) - リスト
sに重複がない
- リスト
- 帰結
- リスト
xには重複がある
- リスト
- 仮定
長々と説明してきましたがこれだけのことです。
定理 pigeonhole が鳩の巣の原理を表現していると伝わりましたか？
正直ちょっと不安です。
5. pigeonhole はそのままだと証明できる気配がない件について
では、 pigeonhole 定理の意味が伝わったところで証明を試みましょう。
(defthm pigeonhole
(implies (and (subsetp x s)
(< (len s) (len x))
(no-duplicatesp s))
(not (no-duplicatesp x))))
証明失敗: 出力を確認する
ACL2 Warning [Free] in ( DEFTHM PIGEONHOLE ...): A :REWRITE rule generated
from PIGEONHOLE contains the free variable S. This variable will be
chosen by searching for an instance of (SUBSETP-EQUAL X S) in the context
of the term being rewritten. This is generally a severe restriction
on the applicability of a :REWRITE rule. See :DOC free-variables.
Goal'
([ A key checkpoint:
Goal'
(IMPLIES (AND (SUBSETP-EQUAL X S)
(< (LEN S) (LEN X))
(NO-DUPLICATESP-EQUAL S))
(NOT (NO-DUPLICATESP-EQUAL X)))
*1 (Goal') is pushed for proof by induction.
])
Perhaps we can prove *1 by induction. Five induction schemes are suggested
by this conjecture. These merge into two derived induction schemes.
However, one of these is flawed and so we are left with one viable
candidate.
We will induct according to a scheme suggested by (NO-DUPLICATESP-EQUAL X),
but modified to accommodate (LEN X) and (SUBSETP-EQUAL X S). These
suggestions were produced using the :induction rules LEN,
NO-DUPLICATESP-EQUAL and SUBSETP-EQUAL. If we let (:P S X) denote
*1 above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X))
(NOT (MEMBER-EQUAL (CAR X) (CDR X)))
(:P S (CDR X)))
(:P S X))
(IMPLIES (AND (NOT (ENDP X))
(MEMBER-EQUAL (CAR X) (CDR X)))
(:P S X))
(IMPLIES (ENDP X) (:P S X))).
This induction is justified by the same argument used to admit
NO-DUPLICATESP-EQUAL. When applied to the goal at hand the above induction
scheme produces five nontautological subgoals.
Subgoal *1/5
Subgoal *1/5'
Subgoal *1/4
Subgoal *1/4'
Subgoal *1/4''
Subgoal *1/4'''
Subgoal *1/4'4'
Subgoal *1/4'5'
Subgoal *1/4'6'
Subgoal *1/4'7'
Subgoal *1/4'8'
Subgoal *1/4'9'
Subgoal *1/4'10'
([ A key checkpoint while proving *1 (descended from Goal'):
Subgoal *1/4'4'
(IMPLIES (AND (EQUAL (LEN (CDR X)) (LEN S))
(CONSP X)
(NOT (MEMBER-EQUAL (CAR X) (CDR X)))
(<= (LEN S) (LEN S))
(MEMBER-EQUAL (CAR X) S)
(SUBSETP-EQUAL (CDR X) S)
(< (LEN S) (+ 1 (LEN S)))
(NO-DUPLICATESP-EQUAL S))
(NOT (NO-DUPLICATESP-EQUAL (CDR X))))
*1.1 (Subgoal *1/4'10') is pushed for proof by induction.
])
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/1
Subgoal *1/1'
So we now return to *1.1, which is
(IMPLIES (AND (NOT (MEMBER-EQUAL X1 X2))
(MEMBER-EQUAL X1 S)
(SUBSETP-EQUAL X2 S)
(NO-DUPLICATESP-EQUAL S))
(NOT (NO-DUPLICATESP-EQUAL X2))).
Subgoal *1.1/5
Subgoal *1.1/5'
Subgoal *1.1/4
Subgoal *1.1/4'
Subgoal *1.1/3
Subgoal *1.1/3'
Subgoal *1.1/2
Subgoal *1.1/2'
Subgoal *1.1/1
Subgoal *1.1/1'
Subgoal *1.1/1''
Subgoal *1.1/1'''
*1.1.1 (Subgoal *1.1/1''') is pushed for proof by induction.
So we now return to *1.1.1, which is
(IMPLIES (MEMBER-EQUAL X1 S)
(NOT (NO-DUPLICATESP-EQUAL S))).
Subgoal *1.1.1/4
Subgoal *1.1.1/4'
Subgoal *1.1.1/3
Subgoal *1.1.1/3'
Subgoal *1.1.1/3''
Subgoal *1.1.1/3'''
Subgoal *1.1.1/3'4'
Subgoal *1.1.1/3'5'
*1.1.1.1 (Subgoal *1.1.1/3'5') is pushed for proof by induction.
Subgoal *1.1.1/2
Subgoal *1.1.1/2'
Subgoal *1.1.1/2''
Subgoal *1.1.1/1
Subgoal *1.1.1/1'
So we now return to *1.1.1.1, which is
(IMPLIES (NOT (MEMBER-EQUAL S1 S2))
(NOT (NO-DUPLICATESP-EQUAL S2))).
Subgoal *1.1.1.1/4
Subgoal *1.1.1.1/4'
Subgoal *1.1.1.1/3
Subgoal *1.1.1.1/3'
Subgoal *1.1.1.1/2
Subgoal *1.1.1.1/2'
Subgoal *1.1.1.1/1
Subgoal *1.1.1.1/1'
Subgoal *1.1.1.1/1''
Subgoal *1.1.1.1/1'''
A goal of NIL, Subgoal *1.1.1.1/1''', has been generated! Obviously,
the proof attempt has failed.
Summary
Form: ( DEFTHM PIGEONHOLE ...)
Rules: ((:DEFINITION ENDP)
(:DEFINITION LEN)
(:DEFINITION MEMBER-EQUAL)
(:DEFINITION NO-DUPLICATESP-EQL-EXEC$GUARD-CHECK)
(:DEFINITION NO-DUPLICATESP-EQUAL)
(:DEFINITION NOT)
(:DEFINITION RETURN-LAST)
(:DEFINITION SUBSETP-EQL-EXEC$GUARD-CHECK)
(:DEFINITION SUBSETP-EQUAL)
(:ELIM CAR-CDR-ELIM)
(:FAKE-RUNE-FOR-LINEAR NIL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION LEN)
(:INDUCTION MEMBER-EQUAL)
(:INDUCTION NO-DUPLICATESP-EQUAL)
(:INDUCTION SUBSETP-EQUAL)
(:TYPE-PRESCRIPTION LEN)
(:TYPE-PRESCRIPTION MEMBER-EQUAL))
Warnings: Free
Time: 0.02 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted: 6708
---
The key checkpoint goals, below, may help you to debug this failure.
See :DOC failure and see :DOC set-checkpoint-summary-limit.
---
*** Key checkpoint at the top level: ***
Goal'
(IMPLIES (AND (SUBSETP-EQUAL X S)
(< (LEN S) (LEN X))
(NO-DUPLICATESP-EQUAL S))
(NOT (NO-DUPLICATESP-EQUAL X)))
*** Key checkpoint under a top-level induction
before generating a goal of NIL (see :DOC nil-goal): ***
Subgoal *1/4'4'
(IMPLIES (AND (EQUAL (LEN (CDR X)) (LEN S))
(CONSP X)
(NOT (MEMBER-EQUAL (CAR X) (CDR X)))
(<= (LEN S) (LEN S))
(MEMBER-EQUAL (CAR X) S)
(SUBSETP-EQUAL (CDR X) S)
(< (LEN S) (+ 1 (LEN S)))
(NO-DUPLICATESP-EQUAL S))
(NOT (NO-DUPLICATESP-EQUAL (CDR X))))
ACL2 Error in ( DEFTHM PIGEONHOLE ...): See :DOC failure.
******** FAILED ********
自動証明には失敗します。
そもそも ACL2 は下記の帰納法を試みています。
:P は証明しようとしている定理のことです。
(AND (IMPLIES (AND (NOT (ENDP X))
(NOT (MEMBER-EQUAL (CAR X) (CDR X)))
(:P S (CDR X)))
(:P S X))
(IMPLIES (AND (NOT (ENDP X))
(MEMBER-EQUAL (CAR X) (CDR X)))
(:P S X))
(IMPLIES (ENDP X) (:P S X))).
これは len, no-duplicatesp-equal, subsetp-equal
の3つの関数から自動生成した帰納法なのですが、
この帰納法ではどうやったって鳩の巣の原理は証明できそうにありません。
ではヒントを与えて別の帰納法を教えてあげればいいのではないかと思うのですが、 この定理を直接帰納法で証明する良い方法は思いつきません。 というわけでここで詰みです。 ……とそんなわけはなく、もしそうであればこの記事を作成していません。
鳩の巣の原理を表現する別の定理を証明し、その定理が意味していることと
pigeonhole が意味していることが等しいということが証明できればよいのです。
というわけで別の方法で pigeonhole と同様の定理を証明します。
5.1. 警告 Free について
pigeonhole の定理の証明を試みる際に Free という警告がでています。
これは、帰結部にない変数 s が使われているけど書き換え時に s
をマッチするときの処理をどうすればいいか指定して欲しいって感じの警告です。
挙動は :once と :all から選ぶことができて、ACL2 の起動時に特に何も設定せずに警告を無視した場合には :all が使われるようです(:doc Set-match-free-default を参照)。
:once の場合は最初の仮定のみを、
:all の場合はバックトラックを駆使して全ての仮定を使ってマッチをしてくれるようです。
本記事を書くために調べて始めて知ったのですが、
:all を設定している場合でも最初の仮定から試行するようなので、仮定を書く順番には意味があるということになります。
重要な仮定を先に置くことが Rewriter の効率からみても重要なようです。
詳細については :doc free-variables を参照してください。
組み合せ爆発みたいなことが起きて証明がいつになっても終わらないということが起きない限りは、 :all を選択するのが良さそうです。
というわけで、本記事ではとりあえず :all を選択しようかと考えています。
:match-free :all を指定して、 pigeonhole を再度定義します。
(defthm pigeonhole
(implies (and (subsetp x s)
(< (len s) (len x))
(no-duplicatesp s))
(not (no-duplicatesp x)))
:rule-classes ((:rewrite :match-free :all)))
証明失敗: 出力を確認する
Goal'
([ A key checkpoint:
Goal'
(IMPLIES (AND (SUBSETP-EQUAL X S)
(< (LEN S) (LEN X))
(NO-DUPLICATESP-EQUAL S))
(NOT (NO-DUPLICATESP-EQUAL X)))
*1 (Goal') is pushed for proof by induction.
])
Perhaps we can prove *1 by induction. Five induction schemes are suggested
by this conjecture. These merge into two derived induction schemes.
However, one of these is flawed and so we are left with one viable
candidate.
We will induct according to a scheme suggested by (NO-DUPLICATESP-EQUAL X),
but modified to accommodate (LEN X) and (SUBSETP-EQUAL X S). These
suggestions were produced using the :induction rules LEN,
NO-DUPLICATESP-EQUAL and SUBSETP-EQUAL. If we let (:P S X) denote
*1 above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X))
(NOT (MEMBER-EQUAL (CAR X) (CDR X)))
(:P S (CDR X)))
(:P S X))
(IMPLIES (AND (NOT (ENDP X))
(MEMBER-EQUAL (CAR X) (CDR X)))
(:P S X))
(IMPLIES (ENDP X) (:P S X))).
This induction is justified by the same argument used to admit
NO-DUPLICATESP-EQUAL. When applied to the goal at hand the above induction
scheme produces five nontautological subgoals.
Subgoal *1/5
Subgoal *1/5'
Subgoal *1/4
Subgoal *1/4'
Subgoal *1/4''
Subgoal *1/4'''
Subgoal *1/4'4'
Subgoal *1/4'5'
Subgoal *1/4'6'
Subgoal *1/4'7'
Subgoal *1/4'8'
Subgoal *1/4'9'
Subgoal *1/4'10'
([ A key checkpoint while proving *1 (descended from Goal'):
Subgoal *1/4'4'
(IMPLIES (AND (EQUAL (LEN (CDR X)) (LEN S))
(CONSP X)
(NOT (MEMBER-EQUAL (CAR X) (CDR X)))
(<= (LEN S) (LEN S))
(MEMBER-EQUAL (CAR X) S)
(SUBSETP-EQUAL (CDR X) S)
(< (LEN S) (+ 1 (LEN S)))
(NO-DUPLICATESP-EQUAL S))
(NOT (NO-DUPLICATESP-EQUAL (CDR X))))
*1.1 (Subgoal *1/4'10') is pushed for proof by induction.
])
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/1
Subgoal *1/1'
So we now return to *1.1, which is
(IMPLIES (AND (NOT (MEMBER-EQUAL X1 X2))
(MEMBER-EQUAL X1 S)
(SUBSETP-EQUAL X2 S)
(NO-DUPLICATESP-EQUAL S))
(NOT (NO-DUPLICATESP-EQUAL X2))).
Subgoal *1.1/5
Subgoal *1.1/5'
Subgoal *1.1/4
Subgoal *1.1/4'
Subgoal *1.1/3
Subgoal *1.1/3'
Subgoal *1.1/2
Subgoal *1.1/2'
Subgoal *1.1/1
Subgoal *1.1/1'
Subgoal *1.1/1''
Subgoal *1.1/1'''
*1.1.1 (Subgoal *1.1/1''') is pushed for proof by induction.
So we now return to *1.1.1, which is
(IMPLIES (MEMBER-EQUAL X1 S)
(NOT (NO-DUPLICATESP-EQUAL S))).
Subgoal *1.1.1/4
Subgoal *1.1.1/4'
Subgoal *1.1.1/3
Subgoal *1.1.1/3'
Subgoal *1.1.1/3''
Subgoal *1.1.1/3'''
Subgoal *1.1.1/3'4'
Subgoal *1.1.1/3'5'
*1.1.1.1 (Subgoal *1.1.1/3'5') is pushed for proof by induction.
Subgoal *1.1.1/2
Subgoal *1.1.1/2'
Subgoal *1.1.1/2''
Subgoal *1.1.1/1
Subgoal *1.1.1/1'
So we now return to *1.1.1.1, which is
(IMPLIES (NOT (MEMBER-EQUAL S1 S2))
(NOT (NO-DUPLICATESP-EQUAL S2))).
Subgoal *1.1.1.1/4
Subgoal *1.1.1.1/4'
Subgoal *1.1.1.1/3
Subgoal *1.1.1.1/3'
Subgoal *1.1.1.1/2
Subgoal *1.1.1.1/2'
Subgoal *1.1.1.1/1
Subgoal *1.1.1.1/1'
Subgoal *1.1.1.1/1''
Subgoal *1.1.1.1/1'''
A goal of NIL, Subgoal *1.1.1.1/1''', has been generated! Obviously,
the proof attempt has failed.
Summary
Form: ( DEFTHM PIGEONHOLE ...)
Rules: ((:DEFINITION ENDP)
(:DEFINITION LEN)
(:DEFINITION MEMBER-EQUAL)
(:DEFINITION NO-DUPLICATESP-EQL-EXEC$GUARD-CHECK)
(:DEFINITION NO-DUPLICATESP-EQUAL)
(:DEFINITION NOT)
(:DEFINITION RETURN-LAST)
(:DEFINITION SUBSETP-EQL-EXEC$GUARD-CHECK)
(:DEFINITION SUBSETP-EQUAL)
(:ELIM CAR-CDR-ELIM)
(:FAKE-RUNE-FOR-LINEAR NIL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION LEN)
(:INDUCTION MEMBER-EQUAL)
(:INDUCTION NO-DUPLICATESP-EQUAL)
(:INDUCTION SUBSETP-EQUAL)
(:TYPE-PRESCRIPTION LEN)
(:TYPE-PRESCRIPTION MEMBER-EQUAL))
Time: 0.02 seconds (prove: 0.02, print: 0.00, other: 0.00)
Prover steps counted: 6708
---
The key checkpoint goals, below, may help you to debug this failure.
See :DOC failure and see :DOC set-checkpoint-summary-limit.
---
*** Key checkpoint at the top level: ***
Goal'
(IMPLIES (AND (SUBSETP-EQUAL X S)
(< (LEN S) (LEN X))
(NO-DUPLICATESP-EQUAL S))
(NOT (NO-DUPLICATESP-EQUAL X)))
*** Key checkpoint under a top-level induction
before generating a goal of NIL (see :DOC nil-goal): ***
Subgoal *1/4'4'
(IMPLIES (AND (EQUAL (LEN (CDR X)) (LEN S))
(CONSP X)
(NOT (MEMBER-EQUAL (CAR X) (CDR X)))
(<= (LEN S) (LEN S))
(MEMBER-EQUAL (CAR X) S)
(SUBSETP-EQUAL (CDR X) S)
(< (LEN S) (+ 1 (LEN S)))
(NO-DUPLICATESP-EQUAL S))
(NOT (NO-DUPLICATESP-EQUAL (CDR X))))
ACL2 Error in ( DEFTHM PIGEONHOLE ...): See :DOC failure.
******** FAILED ********
これで警告 Free が消えました。
6. 数的な鳩の巣の原理: numeric-pigeonhole
さて、別の方法で鳩の巣の原理を表現するといってもどうすればいいのでしょうか？ 残念なことにさっぱり分からなかったので鳩の巣の原理を既に証明している人いないかなーと思って探したところ、Coq で鳩の巣の原理を証明する方法について紹介されている方を発見しました。
プログラミング Coq [研究活動] IIJ Innovation Institute の「新しい型の定義」にて次のように記載されています。
Coq で鳩の巣原理を表現するには少し工夫が要ります。Coq で表現するために、ここでは「m 個の箱の列」を「長さ m のリスト」、「i 番目の箱に n 個の物が入っている」ということを「リストの i 番目の要素は n である」と置き換えます。
— https://www.iij-ii.co.jp/activities/programming-coq/coqt4.html (2022/3/24 現在)
この表現方法であれば ACL2 でも証明できるかもしれません。 ACL2 でこの表現を用いた鳩の巣の原理の定理を書くためには、1 より大きい要素が一つ以上存在することを調べる関数と、リストの要素の総和を求める関数が必要なためまずはこれらを用意します。
(defun member-if-over-1 (x) (cond ((endp x) nil) ((< 1 (car x)) x) (t (member-if-over-1 (cdr x)))))
出力を確認する
The admission of MEMBER-IF-OVER-1 is trivial, using the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X). We observe that the type of MEMBER-IF-OVER-1 is described by the theorem (OR (CONSP (MEMBER-IF-OVER-1 X)) (EQUAL (MEMBER-IF-OVER-1 X) NIL)). Summary Form: ( DEFUN MEMBER-IF-OVER-1 ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) MEMBER-IF-OVER-1
member-if-over-1 のテスト
(thm (equal (list (member-if-over-1 '(1 1 1 1 1))
(member-if-over-1 '(1 1 2 3 1)))
'(nil (2 3 1))))
証明成功: 出力を確認する
Q.E.D.
Summary
Form: ( THM ...)
Rules: ((:EXECUTABLE-COUNTERPART CONS)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART MEMBER-IF-OVER-1))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 9
Proof succeeded.
(defun sum (x) (if (endp x) 0 (+ (car x) (sum (cdr x)))))
出力を確認する
The admission of SUM is trivial, using the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X). We observe that the type of SUM is described by the theorem (ACL2-NUMBERP (SUM X)). We used primitive type reasoning. Summary Form: ( DEFUN SUM ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) SUM
sum のテスト
(thm (equal (sum '(1 2 3 4 5)) 15))
証明成功: 出力を確認する
Q.E.D.
Summary
Form: ( THM ...)
Rules: ((:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART SUM))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 4
Proof succeeded.
上記の関数を用いて numeric-pigeonhole 定理を定義します。
(defthm numeric-pigeonhole
(implies (< (len x) (sum x))
(member-if-over-1 x)))
証明成功: 出力を確認する
*1 (the initial Goal, a key checkpoint) is pushed for proof by induction.
Perhaps we can prove *1 by induction. Three induction schemes are
suggested by this conjecture. Subsumption reduces that number to two.
These merge into one derived induction scheme.
We will induct according to a scheme suggested by (MEMBER-IF-OVER-1 X).
This suggestion was produced using the :induction rules LEN, MEMBER-IF-OVER-1
and SUM. If we let (:P X) denote *1 above then the induction scheme
we'll use is
(AND (IMPLIES (AND (NOT (ENDP X))
(<= (CAR X) 1)
(:P (CDR X)))
(:P X))
(IMPLIES (AND (NOT (ENDP X)) (< 1 (CAR X)))
(:P X))
(IMPLIES (ENDP X) (:P X))).
This induction is justified by the same argument used to admit
MEMBER-IF-OVER-1. When applied to the goal at hand the above induction
scheme produces four nontautological subgoals.
Subgoal *1/4
Subgoal *1/4'
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/1
Subgoal *1/1'
*1 is COMPLETED!
Thus key checkpoint Goal is COMPLETED!
Q.E.D.
Summary
Form: ( DEFTHM NUMERIC-PIGEONHOLE ...)
Rules: ((:DEFINITION ENDP)
(:DEFINITION LEN)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NOT)
(:DEFINITION SUM)
(:EXECUTABLE-COUNTERPART <)
(:INDUCTION LEN)
(:INDUCTION MEMBER-IF-OVER-1)
(:INDUCTION SUM)
(:TYPE-PRESCRIPTION MEMBER-IF-OVER-1))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 606
NUMERIC-PIGEONHOLE
自動証明に成功しました。
numeric-pigeonhole について解説します。
x は巣箱のリストでありそれぞれの要素に巣箱に入っている鳩の数が入っていると考えてください。 (len x) は巣箱の数 (sum x) は巣箱に入っている鳩の総和を求めていることから鳩の数を表わしています。
この定理の仮定部分は巣箱の数 (len x) より鳩の数 (sum x) の方が大きいと言っています。
帰結部分の (member-if-over-1 x) では x の中に1 より大きい数が少なくとも一つあるといっています。
よって、 numeric-pigeonhole は下記のように書き下せます。
- 定理: numeric-pigeonhole
- 仮定
(len x)より(sum x)の方が大きい
- 帰結
xには1より大きい数が1つ以上存在する
- 仮定
これで鳩の巣の原理の証明は完了です！ 補助定理やヒントなしに成功した定理の証明についてあれこれ考えないのが ACL2 とうまく付き合うコツです。
めでたしめでたし。ではありません。私は元々考えていた pigeonhole の定理を示したいのです。
やはり Lisper なら List で語るのが一興なのではないでしょうか？
7. numeric-pigeonhole から pigeonhole へ繋ぐ定理の証明
さて、 numeric-pigeonhole を使って pigeonhole を証明する方法について考えてみましょう。
それぞれの定理を再掲します。
(defthm pigeonhole
(implies (and (no-duplicatesp s)
(subsetp x s)
(< (len s) (len x)))
(not (no-duplicatesp x))))
(defthm numeric-pigeonhole
(implies (< (len x) (sum x))
(member-if-over-1 x)))
pigenhole の x を変換して numeric-pigeonhole の x の形に変形することができれば、
numeric-pigenhole を使うことができそうです。
pigeonhole の x は鳩ごとの巣箱IDのリストなので、これを巣箱ごとの鳩の数に変換する関数を書きましょう。
この関数のために list-count というリストから要素を数える補助関数を定義します。
ACL2 には count という関数が既にあるのですが list ではなくて sequence を対象にするものでちょっと扱いにくいため自分で書きます。
(defun list-count (e x) (cond ((endp x) 0) ((equal e (car x)) (+ 1 (list-count e (cdr x)))) (t (list-count e (cdr x)))))
出力を確認する
The admission of LIST-COUNT is trivial, using the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X). We observe that the type of LIST-COUNT is described by the theorem (AND (INTEGERP (LIST-COUNT E X)) (<= 0 (LIST-COUNT E X))). We used primitive type reasoning. Summary Form: ( DEFUN LIST-COUNT ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) LIST-COUNT
list-count のテスト
(thm (equal (list-count 'a '(a b c a b c a)) 3))
証明成功: 出力を確認する
Q.E.D.
Summary
Form: ( THM ...)
Rules: ((:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART LIST-COUNT))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 5
Proof succeeded.
map-list-count の説明を追記: map-list-count は pegionhole の x, s
を numeric-pigenhole の表現の x に変換する関数です。
それぞれのリストの要素を list-count に写すため map-list-count と命名しています。
(defun map-list-count (x s) (if (endp s) nil (cons (list-count (car s) x) (map-list-count x (cdr s)))))
出力を確認する
The admission of MAP-LIST-COUNT is trivial, using the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT S). We observe that the type of MAP-LIST-COUNT is described by the theorem (TRUE-LISTP (MAP-LIST-COUNT X S)). We used primitive type reasoning. Summary Form: ( DEFUN MAP-LIST-COUNT ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) MAP-LIST-COUNT
正しく書けているか確認してみます。
(thm (equal (map-list-count '(a b c c c d c d a e) '(a b c d e))
'(2 1 4 2 1)))
証明成功: 出力を確認する
Q.E.D.
Summary
Form: ( THM ...)
Rules: ((:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART MAP-LIST-COUNT))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 5
Proof succeeded.
7.1. member-if-over-1-map-list-count-is-duplicated の定理
これで次の定理 member-if-over-1-map-list-count-is-duplicated を証明してみましょう。
この定理は、もしも (map-list-count x s) に 1 より大きい値があったら必ず x に重複があるといっています。
この定理によって numeric-pigeonhole と pigeonhole を繋ぐことができます。
(defthm member-if-over-1-map-list-count-is-duplicated
(implies (and (no-duplicatesp s)
(subsetp x s)
(member-if-over-1 (map-list-count x s)))
(not (no-duplicatesp x)))
:rule-classes ((:rewrite :match-free :all)))
証明失敗: 出力を確認する
Goal'
([ A key checkpoint:
Goal'
(IMPLIES (AND (NO-DUPLICATESP-EQUAL S)
(SUBSETP-EQUAL X S)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT X S)))
(NOT (NO-DUPLICATESP-EQUAL X)))
*1 (Goal') is pushed for proof by induction.
])
Perhaps we can prove *1 by induction. Four induction schemes are suggested
by this conjecture. These merge into two derived induction schemes.
We will choose arbitrarily among these.
We will induct according to a scheme suggested by (MAP-LIST-COUNT X S).
This suggestion was produced using the :induction rules MAP-LIST-COUNT
and NO-DUPLICATESP-EQUAL. If we let (:P S X) denote *1 above then
the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP S)) (:P (CDR S) X))
(:P S X))
(IMPLIES (ENDP S) (:P S X))).
This induction is justified by the same argument used to admit
MAP-LIST-COUNT. When applied to the goal at hand the above induction
scheme produces four nontautological subgoals.
Subgoal *1/4
Subgoal *1/4'
Subgoal *1/4''
Subgoal *1/4'''
Subgoal *1/4'4'
Subgoal *1/4'5'
([ A key checkpoint while proving *1 (descended from Goal'):
Subgoal *1/4''
(IMPLIES (AND (CONSP S)
(NOT (MEMBER-IF-OVER-1 (MAP-LIST-COUNT X (CDR S))))
(NOT (MEMBER-EQUAL (CAR S) (CDR S)))
(NO-DUPLICATESP-EQUAL (CDR S))
(SUBSETP-EQUAL X S)
(< 1 (LIST-COUNT (CAR S) X))
(CONS (LIST-COUNT (CAR S) X)
(MAP-LIST-COUNT X (CDR S))))
(NOT (NO-DUPLICATESP-EQUAL X)))
*1.1 (Subgoal *1/4'5') is pushed for proof by induction.
])
Subgoal *1/3
Subgoal *1/3'
Splitter note (see :DOC splitter) for Subgoal *1/3' (2 subgoals).
if-intro: ((:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL))
Subgoal *1/3.2
Subgoal *1/3.2'
Subgoal *1/3.2''
Subgoal *1/3.2'''
([ A key checkpoint while proving *1 (descended from Goal'):
Subgoal *1/3.2
(IMPLIES (AND (CONSP S)
(NOT (SUBSETP-EQUAL X (CDR S)))
(NOT (MEMBER-EQUAL (CAR S) (CDR S)))
(NO-DUPLICATESP-EQUAL (CDR S))
(SUBSETP-EQUAL X S)
(< 1 (LIST-COUNT (CAR S) X))
(CONS (LIST-COUNT (CAR S) X)
(MAP-LIST-COUNT X (CDR S))))
(NOT (NO-DUPLICATESP-EQUAL X)))
*1.2 (Subgoal *1/3.2''') is pushed for proof by induction.
])
Subgoal *1/3.1
Subgoal *1/3.1'
Subgoal *1/3.1''
([ A key checkpoint while proving *1 (descended from Goal'):
Subgoal *1/3.1
(IMPLIES (AND (CONSP S)
(NOT (SUBSETP-EQUAL X (CDR S)))
(NOT (MEMBER-EQUAL (CAR S) (CDR S)))
(NO-DUPLICATESP-EQUAL (CDR S))
(SUBSETP-EQUAL X S)
(<= (LIST-COUNT (CAR S) X) 1)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT X (CDR S))))
(NOT (NO-DUPLICATESP-EQUAL X)))
*1.3 (Subgoal *1/3.1'') is pushed for proof by induction.
])
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/1
Subgoal *1/1'
So we now return to *1.3, which is
(IMPLIES (AND (NOT (SUBSETP-EQUAL X S2))
(NOT (MEMBER-EQUAL S1 S2))
(NO-DUPLICATESP-EQUAL S2)
(SUBSETP-EQUAL X (CONS S1 S2))
(<= (LIST-COUNT S1 X) 1)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT X S2)))
(NOT (NO-DUPLICATESP-EQUAL X))).
Subgoal *1.3/7
Subgoal *1.3/7'
Subgoal *1.3/6
Subgoal *1.3/6'
Splitter note (see :DOC splitter) for Subgoal *1.3/6' (3 subgoals).
if-intro: ((:DEFINITION MEMBER-EQUAL)
(:DEFINITION NO-DUPLICATESP-EQUAL)
(:DEFINITION SUBSETP-EQUAL))
Subgoal *1.3/6.3
Subgoal *1.3/6.3'
Subgoal *1.3/6.3''
Subgoal *1.3/6.3'''
*1.3.1 (Subgoal *1.3/6.3''') is pushed for proof by induction.
Subgoal *1.3/6.2
Subgoal *1.3/6.2'
Subgoal *1.3/6.2''
Subgoal *1.3/6.2'''
*1.3.2 (Subgoal *1.3/6.2''') is pushed for proof by induction.
Subgoal *1.3/6.1
Subgoal *1.3/6.1'
Subgoal *1.3/6.1''
*1.3.3 (Subgoal *1.3/6.1'') is pushed for proof by induction.
Subgoal *1.3/5
Subgoal *1.3/5'
Subgoal *1.3/4
Subgoal *1.3/4'
Subgoal *1.3/3
Subgoal *1.3/3'
Subgoal *1.3/3''
Subgoal *1.3/3'''
Subgoal *1.3/3'4'
Subgoal *1.3/3'5'
*1.3.4 (Subgoal *1.3/3'5') is pushed for proof by induction.
Subgoal *1.3/2
Subgoal *1.3/2'
Splitter note (see :DOC splitter) for Subgoal *1.3/2' (2 subgoals).
if-intro: ((:DEFINITION MEMBER-EQUAL)
(:DEFINITION NO-DUPLICATESP-EQUAL)
(:DEFINITION SUBSETP-EQUAL))
Subgoal *1.3/2.2
Subgoal *1.3/2.1
Subgoal *1.3/1
Subgoal *1.3/1'
So we now return to *1.3.4, which is
(IMPLIES (AND (EQUAL (LIST-COUNT X1 X2) 0)
(SUBSETP-EQUAL X2 S2)
(NOT (MEMBER-EQUAL X1 S2))
(NO-DUPLICATESP-EQUAL S2)
(CONS X1 S2)
(SUBSETP-EQUAL X2 (CONS X1 S2))
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT (CONS X1 X2) S2))
(NOT (MEMBER-EQUAL X1 X2)))
(NOT (NO-DUPLICATESP-EQUAL X2))).
Subgoal *1.3.4/8
Subgoal *1.3.4/8'
Subgoal *1.3.4/7
Subgoal *1.3.4/7'
Subgoal *1.3.4/6
Subgoal *1.3.4/6'
Subgoal *1.3.4/6''
Subgoal *1.3.4/6'''
Subgoal *1.3.4/6'4'
*1.3.4.1 (Subgoal *1.3.4/6'4') is pushed for proof by induction.
Subgoal *1.3.4/5
Subgoal *1.3.4/5'
Subgoal *1.3.4/4
Subgoal *1.3.4/4'
Subgoal *1.3.4/3
Subgoal *1.3.4/3'
Subgoal *1.3.4/2
Subgoal *1.3.4/2'
Subgoal *1.3.4/1
Subgoal *1.3.4/1'
Subgoal *1.3.4/1''
*1.3.4.2 (Subgoal *1.3.4/1'') is pushed for proof by induction.
So we now return to *1.3.4.2, which is
(IMPLIES (AND (NOT (CONSP X2))
(NOT (MEMBER-EQUAL X1 S2))
(NO-DUPLICATESP-EQUAL S2)
(CONS X1 S2))
(NOT (MEMBER-IF-OVER-1 (MAP-LIST-COUNT (CONS X1 X2) S2)))).
Subgoal *1.3.4.2/6
Subgoal *1.3.4.2/6'
Subgoal *1.3.4.2/5
Subgoal *1.3.4.2/4
Subgoal *1.3.4.2/4'
Subgoal *1.3.4.2/3
Subgoal *1.3.4.2/3'
Subgoal *1.3.4.2/2
Subgoal *1.3.4.2/2'
Subgoal *1.3.4.2/1
Subgoal *1.3.4.2/1'
*1.3.4.2 is COMPLETED!
We therefore turn our attention to *1.3.4.1, which is
(IMPLIES (AND (NOT (MEMBER-EQUAL X3 X4))
(NOT (MEMBER-IF-OVER-1 (MAP-LIST-COUNT (CONS X1 X4) S2)))
(NOT (EQUAL X1 X3))
(EQUAL (LIST-COUNT X1 X4) 0)
(MEMBER-EQUAL X3 S2)
(SUBSETP-EQUAL X4 S2)
(NOT (MEMBER-EQUAL X1 S2))
(NO-DUPLICATESP-EQUAL S2)
(CONS X1 S2)
(SUBSETP-EQUAL X4 (CONS X1 S2))
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT (LIST* X1 X3 X4) S2))
(NOT (MEMBER-EQUAL X1 X4)))
(NOT (NO-DUPLICATESP-EQUAL X4))).
Subgoal *1.3.4.1/10
Subgoal *1.3.4.1/10'
Subgoal *1.3.4.1/9
Subgoal *1.3.4.1/9'
Subgoal *1.3.4.1/8
Subgoal *1.3.4.1/8'
Subgoal *1.3.4.1/8''
Subgoal *1.3.4.1/8'''
Subgoal *1.3.4.1/8'4'
*1.3.4.1.1 (Subgoal *1.3.4.1/8'4') is pushed for proof by induction.
Subgoal *1.3.4.1/7
Subgoal *1.3.4.1/7'
Subgoal *1.3.4.1/6
Subgoal *1.3.4.1/6'
Subgoal *1.3.4.1/5
Subgoal *1.3.4.1/5'
Subgoal *1.3.4.1/4
Subgoal *1.3.4.1/4'
Subgoal *1.3.4.1/4''
Subgoal *1.3.4.1/4'''
Subgoal *1.3.4.1/4'4'
*1.3.4.1.2 (Subgoal *1.3.4.1/4'4') is pushed for proof by induction.
Subgoal *1.3.4.1/3
Subgoal *1.3.4.1/3'
Subgoal *1.3.4.1/2
Subgoal *1.3.4.1/2'
Subgoal *1.3.4.1/1
Subgoal *1.3.4.1/1'
Subgoal *1.3.4.1/1''
*1.3.4.1.3 (Subgoal *1.3.4.1/1'') is pushed for proof by induction.
So we now return to *1.3.4.1.3, which is
(IMPLIES (AND (NOT (CONSP X4))
(NOT (MEMBER-IF-OVER-1 (MAP-LIST-COUNT (CONS X1 X4) S2)))
(NOT (EQUAL X1 X3))
(MEMBER-EQUAL X3 S2)
(NOT (MEMBER-EQUAL X1 S2))
(NO-DUPLICATESP-EQUAL S2)
(CONS X1 S2))
(NOT (MEMBER-IF-OVER-1 (MAP-LIST-COUNT (LIST* X1 X3 X4) S2)))).
Subgoal *1.3.4.1.3/8
Subgoal *1.3.4.1.3/8'
Subgoal *1.3.4.1.3/7
Subgoal *1.3.4.1.3/6
Subgoal *1.3.4.1.3/6'
Subgoal *1.3.4.1.3/5
Subgoal *1.3.4.1.3/5'
Subgoal *1.3.4.1.3/4
Subgoal *1.3.4.1.3/4'
Subgoal *1.3.4.1.3/4''
Subgoal *1.3.4.1.3/4'''
Subgoal *1.3.4.1.3/4'4'
Subgoal *1.3.4.1.3/4'5'
*1.3.4.1.3.1 (Subgoal *1.3.4.1.3/4'5') is pushed for proof by induction.
Subgoal *1.3.4.1.3/3
Subgoal *1.3.4.1.3/3'
Subgoal *1.3.4.1.3/2
Subgoal *1.3.4.1.3/2'
Subgoal *1.3.4.1.3/2''
Subgoal *1.3.4.1.3/1
Subgoal *1.3.4.1.3/1'
So we now return to *1.3.4.1.3.1, which is
(IMPLIES (AND (NOT (MEMBER-EQUAL S3 S4))
(NOT (CONSP X4))
(NOT (MEMBER-IF-OVER-1 (MAP-LIST-COUNT (CONS X1 X4) S4)))
(NOT (EQUAL X1 S3))
(NOT (MEMBER-EQUAL X1 S4))
(NO-DUPLICATESP-EQUAL S4)
(LIST* X1 S3 S4))
(NOT (MEMBER-IF-OVER-1 (MAP-LIST-COUNT (LIST* X1 S3 X4) S4)))).
Subgoal *1.3.4.1.3.1/8
Subgoal *1.3.4.1.3.1/8'
Subgoal *1.3.4.1.3.1/7
Subgoal *1.3.4.1.3.1/6
Subgoal *1.3.4.1.3.1/6'
Subgoal *1.3.4.1.3.1/5
Subgoal *1.3.4.1.3.1/5'
Subgoal *1.3.4.1.3.1/4
Subgoal *1.3.4.1.3.1/4'
Subgoal *1.3.4.1.3.1/3
Subgoal *1.3.4.1.3.1/3'
Subgoal *1.3.4.1.3.1/2
Subgoal *1.3.4.1.3.1/2'
Subgoal *1.3.4.1.3.1/1
Subgoal *1.3.4.1.3.1/1'
*1.3.4.1.3.1 and *1.3.4.1.3 are COMPLETED!
We therefore turn our attention to *1.3.4.1.2, which is
(IMPLIES (AND (NOT (MEMBER-EQUAL X5 X6))
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT (CONS X1 X6) S2))
(NOT (EQUAL X3 X5))
(NOT (MEMBER-EQUAL X3 X6))
(NOT (MEMBER-IF-OVER-1 (MAP-LIST-COUNT (LIST* X1 X5 X6) S2)))
(NOT (EQUAL X1 X3))
(NOT (EQUAL X1 X5))
(EQUAL (LIST-COUNT X1 X6) 0)
(MEMBER-EQUAL X3 S2)
(MEMBER-EQUAL X5 S2)
(SUBSETP-EQUAL X6 S2)
(NOT (MEMBER-EQUAL X1 S2))
(NO-DUPLICATESP-EQUAL S2)
(CONS X1 S2)
(SUBSETP-EQUAL X6 (CONS X1 S2))
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT (LIST* X1 X3 X5 X6) S2))
(NOT (MEMBER-EQUAL X1 X6)))
(NOT (NO-DUPLICATESP-EQUAL X6))).
The formula above is subsumed by one of its parents, *1.3.4, which
we're in the process of trying to prove by induction. When an inductive
proof pushes a subgoal for induction that is less general than the
original goal, it may be a sign that either an inappropriate induction
was chosen or that the original goal is insufficiently general. In
any case, our proof attempt has failed.
Summary
Form: ( DEFTHM MEMBER-IF-OVER-1-MAP-LIST-COUNT-IS-DUPLICATED ...)
Rules: ((:DEFINITION ENDP)
(:DEFINITION LIST-COUNT)
(:DEFINITION MAP-LIST-COUNT)
(:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQL-EXEC$GUARD-CHECK)
(:DEFINITION NO-DUPLICATESP-EQUAL)
(:DEFINITION NOT)
(:DEFINITION RETURN-LAST)
(:DEFINITION SUBSETP-EQL-EXEC$GUARD-CHECK)
(:DEFINITION SUBSETP-EQUAL)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART <)
(:EXECUTABLE-COUNTERPART BINARY-+)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART MEMBER-IF-OVER-1)
(:FAKE-RUNE-FOR-LINEAR NIL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION LIST-COUNT)
(:INDUCTION MAP-LIST-COUNT)
(:INDUCTION MEMBER-EQUAL)
(:INDUCTION NO-DUPLICATESP-EQUAL)
(:INDUCTION SUBSETP-EQUAL)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:TYPE-PRESCRIPTION LIST-COUNT)
(:TYPE-PRESCRIPTION MAP-LIST-COUNT)
(:TYPE-PRESCRIPTION MEMBER-EQUAL)
(:TYPE-PRESCRIPTION MEMBER-IF-OVER-1)
(:TYPE-PRESCRIPTION SUBSETP-EQUAL))
Splitter rules (see :DOC splitter):
if-intro: ((:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL)
(:DEFINITION SUBSETP-EQUAL))
Time: 0.11 seconds (prove: 0.10, print: 0.01, other: 0.00)
Prover steps counted: 56958
---
The key checkpoint goals, below, may help you to debug this failure.
See :DOC failure and see :DOC set-checkpoint-summary-limit.
---
*** Key checkpoint at the top level: ***
Goal'
(IMPLIES (AND (NO-DUPLICATESP-EQUAL S)
(SUBSETP-EQUAL X S)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT X S)))
(NOT (NO-DUPLICATESP-EQUAL X)))
*** Key checkpoints under a top-level induction: ***
Subgoal *1/4''
(IMPLIES (AND (CONSP S)
(NOT (MEMBER-IF-OVER-1 (MAP-LIST-COUNT X (CDR S))))
(NOT (MEMBER-EQUAL (CAR S) (CDR S)))
(NO-DUPLICATESP-EQUAL (CDR S))
(SUBSETP-EQUAL X S)
(< 1 (LIST-COUNT (CAR S) X))
(CONS (LIST-COUNT (CAR S) X)
(MAP-LIST-COUNT X (CDR S))))
(NOT (NO-DUPLICATESP-EQUAL X)))
Subgoal *1/3.2
(IMPLIES (AND (CONSP S)
(NOT (SUBSETP-EQUAL X (CDR S)))
(NOT (MEMBER-EQUAL (CAR S) (CDR S)))
(NO-DUPLICATESP-EQUAL (CDR S))
(SUBSETP-EQUAL X S)
(< 1 (LIST-COUNT (CAR S) X))
(CONS (LIST-COUNT (CAR S) X)
(MAP-LIST-COUNT X (CDR S))))
(NOT (NO-DUPLICATESP-EQUAL X)))
Subgoal *1/3.1
(IMPLIES (AND (CONSP S)
(NOT (SUBSETP-EQUAL X (CDR S)))
(NOT (MEMBER-EQUAL (CAR S) (CDR S)))
(NO-DUPLICATESP-EQUAL (CDR S))
(SUBSETP-EQUAL X S)
(<= (LIST-COUNT (CAR S) X) 1)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT X (CDR S))))
(NOT (NO-DUPLICATESP-EQUAL X)))
ACL2 Error in ( DEFTHM MEMBER-IF-OVER-1-MAP-LIST-COUNT-IS-DUPLICATED
...): See :DOC failure.
******** FAILED ********
証明に失敗しました。原因について考えましょう。
下記のような帰納法を用いています。
(AND (IMPLIES (AND (NOT (ENDP S)) (:P (CDR S) X)) (:P S X)) (IMPLIES (ENDP S) (:P S X)))
この帰納法には問題があります(実際にこの時点で問題に気づけたわけではなく、色々先に進めてから気づいたのですが、その色々を書くと冗長だしここで気づいた方が良いのであえてその内容は書きません。ACL2 が意味のある帰納法を使っているかを確認することは大切です)。
定理の帰結には、 X しか出現しないのに S で帰納法を試みています。
これでは無意味なので帰納段階の仮定のところで X の式が変わるようにしなければこの定理を証明するのは無理です。
どうすればいいかしばらく悩んだのですが、
帰納段階の仮定では (cdr s) としていて (car s) のことを考慮していないので、
x の方も (car s) のことを考えなくてよい形、すなわち x から (car s) を除去した形にすべきであると考えました。
ということでリストから特定の要素を除去する関数 remove を使用して、
帰納段階の仮定を (:P (CDR S) (REMOVE (CAR S) X)) のようにすれば帰納法を使って証明できそうな感じがします。
map-list-count 関数で再帰をするときも x の式はそのままなのに s の式は (cdr s) に変えていましたが、
上記の帰納法を用いることを考慮すると map-list-count でも再帰するときに x を (remove (car s) x)
に変えた方がよさそうです。
計算量は増大しますがこの関数はそもそも定理を証明するための補助なので関数の使用した場合について考える必要はありません。
:ubt! というコマンドを使って map-list-count を定義する前の時点まで ACL2 の状態を巻き戻して定義しなおしましょう。
:ubt! map-list-count
出力を確認する
L 4:x(DEFUN LIST-COUNT (E X) ...)
(defun map-list-count (x s) (if (endp s) nil (cons (list-count (car s) x) (map-list-count (remove (car s) x) (cdr s)))))
出力を確認する
The admission of MAP-LIST-COUNT is trivial, using the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT S). We observe that the type of MAP-LIST-COUNT is described by the theorem (TRUE-LISTP (MAP-LIST-COUNT X S)). We used primitive type reasoning. Summary Form: ( DEFUN MAP-LIST-COUNT ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) MAP-LIST-COUNT
では、再度証明を試みましょう。
(defthm member-if-over-1-map-list-count-is-duplicated
(implies (and (no-duplicatesp s)
(subsetp x s)
(member-if-over-1 (map-list-count x s)))
(not (no-duplicatesp x)))
:rule-classes ((:rewrite :match-free :all)))
証明失敗: 出力を確認する
Goal'
([ A key checkpoint:
Goal'
(IMPLIES (AND (NO-DUPLICATESP-EQUAL S)
(SUBSETP-EQUAL X S)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT X S)))
(NOT (NO-DUPLICATESP-EQUAL X)))
*1 (Goal') is pushed for proof by induction.
])
Perhaps we can prove *1 by induction. Four induction schemes are suggested
by this conjecture. These merge into two derived induction schemes.
However, one of these is flawed and so we are left with one viable
candidate.
We will induct according to a scheme suggested by (NO-DUPLICATESP-EQUAL X),
but modified to accommodate (SUBSETP-EQUAL X S). These suggestions
were produced using the :induction rules NO-DUPLICATESP-EQUAL and
SUBSETP-EQUAL. If we let (:P S X) denote *1 above then the induction
scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X))
(NOT (MEMBER-EQUAL (CAR X) (CDR X)))
(:P S (CDR X)))
(:P S X))
(IMPLIES (AND (NOT (ENDP X))
(MEMBER-EQUAL (CAR X) (CDR X)))
(:P S X))
(IMPLIES (ENDP X) (:P S X))).
This induction is justified by the same argument used to admit
NO-DUPLICATESP-EQUAL. When applied to the goal at hand the above induction
scheme produces five nontautological subgoals.
Subgoal *1/5
Subgoal *1/5'
Subgoal *1/4
Subgoal *1/4'
Subgoal *1/4''
Subgoal *1/4'''
Subgoal *1/4'4'
([ A key checkpoint while proving *1 (descended from Goal'):
Subgoal *1/4''
(IMPLIES (AND (CONSP X)
(NOT (MEMBER-EQUAL (CAR X) (CDR X)))
(NOT (MEMBER-IF-OVER-1 (MAP-LIST-COUNT (CDR X) S)))
(NO-DUPLICATESP-EQUAL S)
(MEMBER-EQUAL (CAR X) S)
(SUBSETP-EQUAL (CDR X) S)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT X S)))
(NOT (NO-DUPLICATESP-EQUAL (CDR X))))
*1.1 (Subgoal *1/4'4') is pushed for proof by induction.
])
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/1
Subgoal *1/1'
Subgoal *1/1''
([ A key checkpoint while proving *1 (descended from Goal'):
Subgoal *1/1''
(IMPLIES (AND (NOT (CONSP X))
(NO-DUPLICATESP-EQUAL S))
(NOT (MEMBER-IF-OVER-1 (MAP-LIST-COUNT X S))))
*1.2 (Subgoal *1/1'') is pushed for proof by induction.
])
So we now return to *1.2, which is
(IMPLIES (AND (NOT (CONSP X))
(NO-DUPLICATESP-EQUAL S))
(NOT (MEMBER-IF-OVER-1 (MAP-LIST-COUNT X S)))).
Subgoal *1.2/4
Subgoal *1.2/4'
Subgoal *1.2/3
Subgoal *1.2/3'
Subgoal *1.2/2
Subgoal *1.2/2'
Subgoal *1.2/1
Subgoal *1.2/1'
*1.2 is COMPLETED!
Thus key checkpoint Subgoal *1/1'' is COMPLETED!
We therefore turn our attention to *1.1, which is
(IMPLIES (AND (NOT (MEMBER-EQUAL X1 X2))
(NOT (MEMBER-IF-OVER-1 (MAP-LIST-COUNT X2 S)))
(NO-DUPLICATESP-EQUAL S)
(MEMBER-EQUAL X1 S)
(SUBSETP-EQUAL X2 S)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT (CONS X1 X2) S)))
(NOT (NO-DUPLICATESP-EQUAL X2))).
Subgoal *1.1/7
Subgoal *1.1/7'
Subgoal *1.1/6
Subgoal *1.1/6'
Subgoal *1.1/6''
Subgoal *1.1/6'''
Subgoal *1.1/6'4'
*1.1.1 (Subgoal *1.1/6'4') is pushed for proof by induction.
Subgoal *1.1/5
Subgoal *1.1/5'
Subgoal *1.1/4
Subgoal *1.1/4'
Subgoal *1.1/4''
Subgoal *1.1/4'''
Subgoal *1.1/4'4'
*1.1.2 (Subgoal *1.1/4'4') is pushed for proof by induction.
Subgoal *1.1/3
Subgoal *1.1/3'
Subgoal *1.1/2
Subgoal *1.1/2'
Subgoal *1.1/1
Subgoal *1.1/1'
Subgoal *1.1/1''
*1.1.3 (Subgoal *1.1/1'') is pushed for proof by induction.
So we now return to *1.1.3, which is
(IMPLIES (AND (NOT (CONSP X2))
(NOT (MEMBER-IF-OVER-1 (MAP-LIST-COUNT X2 S)))
(NO-DUPLICATESP-EQUAL S)
(MEMBER-EQUAL X1 S))
(NOT (MEMBER-IF-OVER-1 (MAP-LIST-COUNT (CONS X1 X2) S)))).
Subgoal *1.1.3/7
Subgoal *1.1.3/7'
Subgoal *1.1.3/7''
Subgoal *1.1.3/6
Subgoal *1.1.3/6'
Subgoal *1.1.3/5
Subgoal *1.1.3/5'
Subgoal *1.1.3/4
Subgoal *1.1.3/4'
Subgoal *1.1.3/3
Subgoal *1.1.3/3'
Subgoal *1.1.3/2
Subgoal *1.1.3/2'
Subgoal *1.1.3/2''
Subgoal *1.1.3/2'''
Subgoal *1.1.3/1
Subgoal *1.1.3/1'
*1.1.3 is COMPLETED!
We therefore turn our attention to *1.1.2, which is
(IMPLIES (AND (NOT (MEMBER-EQUAL X3 X4))
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT X4 S))
(NOT (EQUAL X1 X3))
(NOT (MEMBER-EQUAL X1 X4))
(NOT (MEMBER-IF-OVER-1 (MAP-LIST-COUNT (CONS X3 X4) S)))
(NO-DUPLICATESP-EQUAL S)
(MEMBER-EQUAL X1 S)
(MEMBER-EQUAL X3 S)
(SUBSETP-EQUAL X4 S)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT (LIST* X1 X3 X4) S)))
(NOT (NO-DUPLICATESP-EQUAL X4))).
The formula above is subsumed by one of its parents, *1, which we're
in the process of trying to prove by induction. When an inductive
proof pushes a subgoal for induction that is less general than the
original goal, it may be a sign that either an inappropriate induction
was chosen or that the original goal is insufficiently general. In
any case, our proof attempt has failed.
Summary
Form: ( DEFTHM MEMBER-IF-OVER-1-MAP-LIST-COUNT-IS-DUPLICATED ...)
Rules: ((:DEFINITION ENDP)
(:DEFINITION LIST-COUNT)
(:DEFINITION MAP-LIST-COUNT)
(:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQL-EXEC$GUARD-CHECK)
(:DEFINITION NO-DUPLICATESP-EQUAL)
(:DEFINITION NOT)
(:DEFINITION REMOVE-EQUAL)
(:DEFINITION RETURN-LAST)
(:DEFINITION SUBSETP-EQL-EXEC$GUARD-CHECK)
(:DEFINITION SUBSETP-EQUAL)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART <)
(:EXECUTABLE-COUNTERPART BINARY-+)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART MEMBER-IF-OVER-1)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION MAP-LIST-COUNT)
(:INDUCTION MEMBER-EQUAL)
(:INDUCTION NO-DUPLICATESP-EQUAL)
(:INDUCTION SUBSETP-EQUAL)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:TYPE-PRESCRIPTION MAP-LIST-COUNT)
(:TYPE-PRESCRIPTION MEMBER-EQUAL)
(:TYPE-PRESCRIPTION MEMBER-IF-OVER-1))
Time: 0.04 seconds (prove: 0.03, print: 0.00, other: 0.00)
Prover steps counted: 23107
---
The key checkpoint goals, below, may help you to debug this failure.
See :DOC failure and see :DOC set-checkpoint-summary-limit.
---
*** Key checkpoint at the top level: ***
Goal'
(IMPLIES (AND (NO-DUPLICATESP-EQUAL S)
(SUBSETP-EQUAL X S)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT X S)))
(NOT (NO-DUPLICATESP-EQUAL X)))
*** Key checkpoint under a top-level induction: ***
Subgoal *1/4''
(IMPLIES (AND (CONSP X)
(NOT (MEMBER-EQUAL (CAR X) (CDR X)))
(NOT (MEMBER-IF-OVER-1 (MAP-LIST-COUNT (CDR X) S)))
(NO-DUPLICATESP-EQUAL S)
(MEMBER-EQUAL (CAR X) S)
(SUBSETP-EQUAL (CDR X) S)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT X S)))
(NOT (NO-DUPLICATESP-EQUAL (CDR X))))
ACL2 Error in ( DEFTHM MEMBER-IF-OVER-1-MAP-LIST-COUNT-IS-DUPLICATED
...): See :DOC failure.
******** FAILED ********
失敗しました。 ACL2 が自動的に採用した帰納法を確認してみましょう。
We will induct according to a scheme suggested by (NO-DUPLICATESP-EQUAL X),
but modified to accommodate (SUBSETP-EQUAL X S). These suggestions
were produced using the :induction rules NO-DUPLICATESP-EQUAL and
SUBSETP-EQUAL. If we let (:P S X) denote *1 above then the induction
scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X))
(NOT (MEMBER-EQUAL (CAR X) (CDR X)))
(:P S (CDR X)))
(:P S X))
(IMPLIES (AND (NOT (ENDP X))
(MEMBER-EQUAL (CAR X) (CDR X)))
(:P S X))
(IMPLIES (ENDP X) (:P S X))).
This induction is justified by the same argument used to admit
NO-DUPLICATESP-EQUAL. When applied to the goal at hand the above induction
scheme produces five nontautological subgoals.
Induction scheme として map-list-count が選ばれていないようです。
map-list-count を induction scheme にして帰納法の主張を生成して欲しいので下記のようにヒントを与えます。
(defthm member-if-over-1-map-list-count-is-duplicated
(implies (and (member-if-over-1 (map-list-count x s))
(no-duplicatesp s)
(subsetp x s))
(not (no-duplicatesp x)))
:hints (("Goal" :induct (map-list-count x s)))
:rule-classes ((:rewrite :match-free :all)))
証明失敗: 出力を確認する
*1 (the initial Goal, a key checkpoint) is pushed for proof by induction.
We have been told to use induction. One induction scheme is suggested
by the induction hint.
We will induct according to a scheme suggested by (MAP-LIST-COUNT X S).
This suggestion was produced using the :induction rule MAP-LIST-COUNT.
If we let (:P S X) denote *1 above then the induction scheme we'll
use is
(AND (IMPLIES (AND (NOT (ENDP S))
(:P (CDR S) (REMOVE-EQUAL (CAR S) X)))
(:P S X))
(IMPLIES (ENDP S) (:P S X))).
This induction is justified by the same argument used to admit
MAP-LIST-COUNT. Note, however, that the unmeasured variable X is being
instantiated. When applied to the goal at hand the above induction
scheme produces two nontautological subgoals.
Subgoal *1/2
Subgoal *1/2'
Splitter note (see :DOC splitter) for Subgoal *1/2' (5 subgoals).
if-intro: ((:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL)
(:DEFINITION NOT))
Subgoal *1/2.5
Subgoal *1/2.5'
Subgoal *1/2.5''
Subgoal *1/2.5'''
Subgoal *1/2.5'4'
Subgoal *1/2.5'5'
([ A key checkpoint while proving *1 (descended from Goal):
Subgoal *1/2.5
(IMPLIES (AND (CONSP S)
(NOT (MEMBER-IF-OVER-1 (MAP-LIST-COUNT (REMOVE-EQUAL (CAR S) X)
(CDR S))))
(< 1 (LIST-COUNT (CAR S) X))
(CONS (LIST-COUNT (CAR S) X)
(MAP-LIST-COUNT (REMOVE-EQUAL (CAR S) X)
(CDR S)))
(NOT (MEMBER-EQUAL (CAR S) (CDR S)))
(NO-DUPLICATESP-EQUAL (CDR S))
(SUBSETP-EQUAL X S))
(NOT (NO-DUPLICATESP-EQUAL X)))
*1.1 (Subgoal *1/2.5'5') is pushed for proof by induction.
])
Subgoal *1/2.4
Subgoal *1/2.4'
Subgoal *1/2.4''
Subgoal *1/2.4'''
([ A key checkpoint while proving *1 (descended from Goal):
Subgoal *1/2.4
(IMPLIES (AND (CONSP S)
(NOT (SUBSETP-EQUAL (REMOVE-EQUAL (CAR S) X)
(CDR S)))
(< 1 (LIST-COUNT (CAR S) X))
(CONS (LIST-COUNT (CAR S) X)
(MAP-LIST-COUNT (REMOVE-EQUAL (CAR S) X)
(CDR S)))
(NOT (MEMBER-EQUAL (CAR S) (CDR S)))
(NO-DUPLICATESP-EQUAL (CDR S))
(SUBSETP-EQUAL X S))
(NOT (NO-DUPLICATESP-EQUAL X)))
*1.2 (Subgoal *1/2.4''') is pushed for proof by induction.
])
Subgoal *1/2.3
Subgoal *1/2.3'
Subgoal *1/2.3''
Subgoal *1/2.3'''
([ A key checkpoint while proving *1 (descended from Goal):
Subgoal *1/2.3
(IMPLIES (AND (CONSP S)
(NOT (SUBSETP-EQUAL (REMOVE-EQUAL (CAR S) X)
(CDR S)))
(<= (LIST-COUNT (CAR S) X) 1)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT (REMOVE-EQUAL (CAR S) X)
(CDR S)))
(NOT (MEMBER-EQUAL (CAR S) (CDR S)))
(NO-DUPLICATESP-EQUAL (CDR S))
(SUBSETP-EQUAL X S))
(NOT (NO-DUPLICATESP-EQUAL X)))
*1.3 (Subgoal *1/2.3''') is pushed for proof by induction.
])
Subgoal *1/2.2
Subgoal *1/2.2'
Subgoal *1/2.2''
Subgoal *1/2.2'''
([ A key checkpoint while proving *1 (descended from Goal):
Subgoal *1/2.2
(IMPLIES (AND (CONSP S)
(NOT (NO-DUPLICATESP-EQUAL (REMOVE-EQUAL (CAR S) X)))
(< 1 (LIST-COUNT (CAR S) X))
(CONS (LIST-COUNT (CAR S) X)
(MAP-LIST-COUNT (REMOVE-EQUAL (CAR S) X)
(CDR S)))
(NOT (MEMBER-EQUAL (CAR S) (CDR S)))
(NO-DUPLICATESP-EQUAL (CDR S))
(SUBSETP-EQUAL X S))
(NOT (NO-DUPLICATESP-EQUAL X)))
*1.4 (Subgoal *1/2.2''') is pushed for proof by induction.
])
Subgoal *1/2.1
Subgoal *1/2.1'
Subgoal *1/2.1''
Subgoal *1/2.1'''
([ A key checkpoint while proving *1 (descended from Goal):
Subgoal *1/2.1
(IMPLIES (AND (CONSP S)
(NOT (NO-DUPLICATESP-EQUAL (REMOVE-EQUAL (CAR S) X)))
(<= (LIST-COUNT (CAR S) X) 1)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT (REMOVE-EQUAL (CAR S) X)
(CDR S)))
(NOT (MEMBER-EQUAL (CAR S) (CDR S)))
(NO-DUPLICATESP-EQUAL (CDR S))
(SUBSETP-EQUAL X S))
(NOT (NO-DUPLICATESP-EQUAL X)))
*1.5 (Subgoal *1/2.1''') is pushed for proof by induction.
])
Subgoal *1/1
Subgoal *1/1'
So we now return to *1.5, which is
(IMPLIES (AND (TRUE-LISTP REL)
(NOT (NO-DUPLICATESP-EQUAL REL))
(<= (LIST-COUNT S1 X) 1)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT REL S2))
(NOT (MEMBER-EQUAL S1 S2))
(NO-DUPLICATESP-EQUAL S2)
(SUBSETP-EQUAL X (CONS S1 S2)))
(NOT (NO-DUPLICATESP-EQUAL X))).
Subgoal *1.5/8
Subgoal *1.5/8'
Splitter note (see :DOC splitter) for Subgoal *1.5/8' (2 subgoals).
if-intro: ((:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1))
Subgoal *1.5/8.2
Subgoal *1.5/8.2'
Subgoal *1.5/8.2''
Subgoal *1.5/8.2'''
*1.5.1 (Subgoal *1.5/8.2''') is pushed for proof by induction.
Subgoal *1.5/8.1
Subgoal *1.5/8.1'
Subgoal *1.5/8.1''
*1.5.2 (Subgoal *1.5/8.1'') is pushed for proof by induction.
Subgoal *1.5/7
Subgoal *1.5/7'
Subgoal *1.5/6
Subgoal *1.5/6'
Subgoal *1.5/5
Subgoal *1.5/5'
Subgoal *1.5/5''
Subgoal *1.5/5'''
Subgoal *1.5/5'4'
Subgoal *1.5/5'5'
Subgoal *1.5/5'6'
Subgoal *1.5/5'7'
*1.5.3 (Subgoal *1.5/5'7') is pushed for proof by induction.
Subgoal *1.5/4
Subgoal *1.5/4'
Splitter note (see :DOC splitter) for Subgoal *1.5/4' (2 subgoals).
if-intro: ((:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1))
Subgoal *1.5/4.2
Subgoal *1.5/4.2'
Subgoal *1.5/4.2''
Subgoal *1.5/4.2'''
*1.5.4 (Subgoal *1.5/4.2''') is pushed for proof by induction.
Subgoal *1.5/4.1
Subgoal *1.5/4.1'
Subgoal *1.5/4.1''
Subgoal *1.5/4.1'''
*1.5.5 (Subgoal *1.5/4.1''') is pushed for proof by induction.
Subgoal *1.5/3
Subgoal *1.5/2
Subgoal *1.5/2'
Subgoal *1.5/1
Subgoal *1.5/1'
So we now return to *1.5.5, which is
(IMPLIES (AND (TRUE-LISTP REL0)
(NOT (MEMBER-EQUAL S3 S4))
(NO-DUPLICATESP-EQUAL REL0)
(TRUE-LISTP REL)
(NOT (NO-DUPLICATESP-EQUAL REL))
(<= (LIST-COUNT S1 X) 1)
(<= (LIST-COUNT S3 REL) 1)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT REL0 S4))
(NOT (EQUAL S1 S3))
(NOT (MEMBER-EQUAL S1 S4))
(NO-DUPLICATESP-EQUAL S4)
(SUBSETP-EQUAL X (LIST* S1 S3 S4)))
(NOT (NO-DUPLICATESP-EQUAL X))).
Subgoal *1.5.5/9
Subgoal *1.5.5/9'
Splitter note (see :DOC splitter) for Subgoal *1.5.5/9' (2 subgoals).
if-intro: ((:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL))
Subgoal *1.5.5/9.2
Subgoal *1.5.5/9.2'
Subgoal *1.5.5/9.2''
Subgoal *1.5.5/9.2'''
*1.5.5.1 (Subgoal *1.5.5/9.2''') is pushed for proof by induction.
Subgoal *1.5.5/9.1
Subgoal *1.5.5/9.1'
Subgoal *1.5.5/9.1''
*1.5.5.2 (Subgoal *1.5.5/9.1'') is pushed for proof by induction.
Subgoal *1.5.5/8
Subgoal *1.5.5/8'
Subgoal *1.5.5/7
Subgoal *1.5.5/7'
Subgoal *1.5.5/6
Subgoal *1.5.5/6'
Subgoal *1.5.5/6''
Subgoal *1.5.5/6'''
Subgoal *1.5.5/6'4'
Subgoal *1.5.5/6'5'
Subgoal *1.5.5/6'6'
Subgoal *1.5.5/6'7'
*1.5.5.3 (Subgoal *1.5.5/6'7') is pushed for proof by induction.
Subgoal *1.5.5/5
Subgoal *1.5.5/5'
Splitter note (see :DOC splitter) for Subgoal *1.5.5/5' (2 subgoals).
if-intro: ((:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL))
Subgoal *1.5.5/5.2
Subgoal *1.5.5/5.2'
Subgoal *1.5.5/5.2''
Subgoal *1.5.5/5.2'''
*1.5.5.4 (Subgoal *1.5.5/5.2''') is pushed for proof by induction.
Subgoal *1.5.5/5.1
Subgoal *1.5.5/5.1'
Subgoal *1.5.5/5.1''
Subgoal *1.5.5/5.1'''
*1.5.5.5 (Subgoal *1.5.5/5.1''') is pushed for proof by induction.
Subgoal *1.5.5/4
Subgoal *1.5.5/4'
Subgoal *1.5.5/3
Subgoal *1.5.5/2
Subgoal *1.5.5/2'
Subgoal *1.5.5/1
Subgoal *1.5.5/1'
So we now return to *1.5.5.5, which is
(IMPLIES (AND (TRUE-LISTP REL1)
(NOT (EQUAL S3 S5))
(NOT (NO-DUPLICATESP-EQUAL REL1))
(TRUE-LISTP REL0)
(NOT (MEMBER-EQUAL S3 S6))
(NO-DUPLICATESP-EQUAL REL0)
(TRUE-LISTP REL)
(NOT (NO-DUPLICATESP-EQUAL REL))
(<= (LIST-COUNT S1 X) 1)
(<= (LIST-COUNT S3 REL) 1)
(<= (LIST-COUNT S5 REL0) 1)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT REL1 S6))
(NOT (EQUAL S1 S3))
(NOT (EQUAL S1 S5))
(NOT (MEMBER-EQUAL S1 S6))
(NOT (MEMBER-EQUAL S5 S6))
(NO-DUPLICATESP-EQUAL S6)
(SUBSETP-EQUAL X (LIST* S1 S3 S5 S6)))
(NOT (NO-DUPLICATESP-EQUAL X))).
Subgoal *1.5.5.5/10
Subgoal *1.5.5.5/10'
Splitter note (see :DOC splitter) for Subgoal *1.5.5.5/10' (2 subgoals).
if-intro: ((:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL))
Subgoal *1.5.5.5/10.2
Subgoal *1.5.5.5/10.2'
Subgoal *1.5.5.5/10.2''
Subgoal *1.5.5.5/10.2'''
*1.5.5.5.1 (Subgoal *1.5.5.5/10.2''') is pushed for proof by induction.
Subgoal *1.5.5.5/10.1
Subgoal *1.5.5.5/10.1'
Subgoal *1.5.5.5/10.1''
*1.5.5.5.2 (Subgoal *1.5.5.5/10.1'') is pushed for proof by induction.
Subgoal *1.5.5.5/9
Subgoal *1.5.5.5/9'
Subgoal *1.5.5.5/8
Subgoal *1.5.5.5/8'
Subgoal *1.5.5.5/7
Subgoal *1.5.5.5/7'
Subgoal *1.5.5.5/6
Subgoal *1.5.5.5/6'
Subgoal *1.5.5.5/6''
Subgoal *1.5.5.5/6'''
Subgoal *1.5.5.5/6'4'
Subgoal *1.5.5.5/6'5'
Subgoal *1.5.5.5/6'6'
Subgoal *1.5.5.5/6'7'
*1.5.5.5.3 (Subgoal *1.5.5.5/6'7') is pushed for proof by induction.
Subgoal *1.5.5.5/5
Subgoal *1.5.5.5/5'
Subgoal *1.5.5.5/4
Subgoal *1.5.5.5/4'
Splitter note (see :DOC splitter) for Subgoal *1.5.5.5/4' (2 subgoals).
if-intro: ((:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL))
Subgoal *1.5.5.5/4.2
Subgoal *1.5.5.5/4.2'
Subgoal *1.5.5.5/4.2''
Subgoal *1.5.5.5/4.2'''
*1.5.5.5.4 (Subgoal *1.5.5.5/4.2''') is pushed for proof by induction.
Subgoal *1.5.5.5/4.1
Subgoal *1.5.5.5/4.1'
Subgoal *1.5.5.5/4.1''
Subgoal *1.5.5.5/4.1'''
*1.5.5.5.5 (Subgoal *1.5.5.5/4.1''') is pushed for proof by induction.
Subgoal *1.5.5.5/3
Subgoal *1.5.5.5/2
Subgoal *1.5.5.5/2'
Subgoal *1.5.5.5/1
Subgoal *1.5.5.5/1'
So we now return to *1.5.5.5.5, which is
(IMPLIES (AND (TRUE-LISTP REL2)
(NOT (EQUAL S3 S7))
(NO-DUPLICATESP-EQUAL REL2)
(TRUE-LISTP REL1)
(NOT (EQUAL S3 S5))
(NOT (NO-DUPLICATESP-EQUAL REL1))
(TRUE-LISTP REL0)
(NOT (MEMBER-EQUAL S3 S8))
(NO-DUPLICATESP-EQUAL REL0)
(TRUE-LISTP REL)
(NOT (NO-DUPLICATESP-EQUAL REL))
(<= (LIST-COUNT S1 X) 1)
(<= (LIST-COUNT S3 REL) 1)
(<= (LIST-COUNT S5 REL0) 1)
(<= (LIST-COUNT S7 REL1) 1)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT REL2 S8))
(NOT (EQUAL S1 S3))
(NOT (EQUAL S1 S5))
(NOT (EQUAL S1 S7))
(NOT (MEMBER-EQUAL S1 S8))
(NOT (EQUAL S5 S7))
(NOT (MEMBER-EQUAL S5 S8))
(NOT (MEMBER-EQUAL S7 S8))
(NO-DUPLICATESP-EQUAL S8)
(SUBSETP-EQUAL X (LIST* S1 S3 S5 S7 S8)))
(NOT (NO-DUPLICATESP-EQUAL X))).
Subgoal *1.5.5.5.5/11
Subgoal *1.5.5.5.5/11'
Splitter note (see :DOC splitter) for Subgoal *1.5.5.5.5/11' (2 subgoals).
if-intro: ((:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL))
Subgoal *1.5.5.5.5/11.2
Subgoal *1.5.5.5.5/11.2'
Subgoal *1.5.5.5.5/11.2''
Subgoal *1.5.5.5.5/11.2'''
*1.5.5.5.5.1 (Subgoal *1.5.5.5.5/11.2''') is pushed for proof by induction.
Subgoal *1.5.5.5.5/11.1
Subgoal *1.5.5.5.5/11.1'
Subgoal *1.5.5.5.5/11.1''
*1.5.5.5.5.2 (Subgoal *1.5.5.5.5/11.1'') is pushed for proof by induction.
Subgoal *1.5.5.5.5/10
Subgoal *1.5.5.5.5/10'
Subgoal *1.5.5.5.5/9
Subgoal *1.5.5.5.5/9'
Subgoal *1.5.5.5.5/8
Subgoal *1.5.5.5.5/8'
Subgoal *1.5.5.5.5/7
Subgoal *1.5.5.5.5/7'
Subgoal *1.5.5.5.5/6
Subgoal *1.5.5.5.5/6'
Subgoal *1.5.5.5.5/6''
Subgoal *1.5.5.5.5/6'''
Subgoal *1.5.5.5.5/6'4'
Subgoal *1.5.5.5.5/6'5'
Subgoal *1.5.5.5.5/6'6'
Subgoal *1.5.5.5.5/6'7'
*1.5.5.5.5.3 (Subgoal *1.5.5.5.5/6'7') is pushed for proof by induction.
Subgoal *1.5.5.5.5/5
Subgoal *1.5.5.5.5/5'
Subgoal *1.5.5.5.5/4
Subgoal *1.5.5.5.5/4'
Splitter note (see :DOC splitter) for Subgoal *1.5.5.5.5/4' (2 subgoals).
if-intro: ((:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL))
Subgoal *1.5.5.5.5/4.2
Subgoal *1.5.5.5.5/4.2'
Subgoal *1.5.5.5.5/4.2''
Subgoal *1.5.5.5.5/4.2'''
*1.5.5.5.5.4 (Subgoal *1.5.5.5.5/4.2''') is pushed for proof by induction.
Subgoal *1.5.5.5.5/4.1
Subgoal *1.5.5.5.5/4.1'
Subgoal *1.5.5.5.5/4.1''
Subgoal *1.5.5.5.5/4.1'''
*1.5.5.5.5.5 (Subgoal *1.5.5.5.5/4.1''') is pushed for proof by induction.
Subgoal *1.5.5.5.5/3
Subgoal *1.5.5.5.5/2
Subgoal *1.5.5.5.5/2'
Subgoal *1.5.5.5.5/1
Subgoal *1.5.5.5.5/1'
So we now return to *1.5.5.5.5.5, which is
(IMPLIES (AND (TRUE-LISTP REL3)
(NOT (EQUAL S3 S9))
(NOT (NO-DUPLICATESP-EQUAL REL3))
(TRUE-LISTP REL2)
(NOT (EQUAL S3 S7))
(NO-DUPLICATESP-EQUAL REL2)
(TRUE-LISTP REL1)
(NOT (EQUAL S3 S5))
(NOT (NO-DUPLICATESP-EQUAL REL1))
(TRUE-LISTP REL0)
(NOT (MEMBER-EQUAL S3 S10))
(NO-DUPLICATESP-EQUAL REL0)
(TRUE-LISTP REL)
(NOT (NO-DUPLICATESP-EQUAL REL))
(<= (LIST-COUNT S1 X) 1)
(<= (LIST-COUNT S3 REL) 1)
(<= (LIST-COUNT S5 REL0) 1)
(<= (LIST-COUNT S7 REL1) 1)
(<= (LIST-COUNT S9 REL2) 1)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT REL3 S10))
(NOT (EQUAL S1 S3))
(NOT (EQUAL S1 S5))
(NOT (EQUAL S1 S7))
(NOT (EQUAL S1 S9))
(NOT (MEMBER-EQUAL S1 S10))
(NOT (EQUAL S5 S7))
(NOT (EQUAL S5 S9))
(NOT (MEMBER-EQUAL S5 S10))
(NOT (EQUAL S7 S9))
(NOT (MEMBER-EQUAL S7 S10))
(NOT (MEMBER-EQUAL S9 S10))
(NO-DUPLICATESP-EQUAL S10)
(SUBSETP-EQUAL X (LIST* S1 S3 S5 S7 S9 S10)))
(NOT (NO-DUPLICATESP-EQUAL X))).
Subgoal *1.5.5.5.5.5/12
Subgoal *1.5.5.5.5.5/12'
Splitter note (see :DOC splitter) for Subgoal *1.5.5.5.5.5/12' (2 subgoals).
if-intro: ((:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL))
Subgoal *1.5.5.5.5.5/12.2
Subgoal *1.5.5.5.5.5/12.2'
Subgoal *1.5.5.5.5.5/12.2''
Subgoal *1.5.5.5.5.5/12.2'''
*1.5.5.5.5.5.1 (Subgoal *1.5.5.5.5.5/12.2''') is pushed for proof by
induction.
Subgoal *1.5.5.5.5.5/12.1
Subgoal *1.5.5.5.5.5/12.1'
Subgoal *1.5.5.5.5.5/12.1''
*1.5.5.5.5.5.2 (Subgoal *1.5.5.5.5.5/12.1'') is pushed for proof by
induction.
Subgoal *1.5.5.5.5.5/11
Subgoal *1.5.5.5.5.5/11'
Subgoal *1.5.5.5.5.5/10
Subgoal *1.5.5.5.5.5/10'
Subgoal *1.5.5.5.5.5/9
Subgoal *1.5.5.5.5.5/9'
Subgoal *1.5.5.5.5.5/8
Subgoal *1.5.5.5.5.5/8'
Subgoal *1.5.5.5.5.5/7
Subgoal *1.5.5.5.5.5/7'
Subgoal *1.5.5.5.5.5/6
Subgoal *1.5.5.5.5.5/6'
Subgoal *1.5.5.5.5.5/6''
Subgoal *1.5.5.5.5.5/6'''
Subgoal *1.5.5.5.5.5/6'4'
Subgoal *1.5.5.5.5.5/6'5'
Subgoal *1.5.5.5.5.5/6'6'
Subgoal *1.5.5.5.5.5/6'7'
*1.5.5.5.5.5.3 (Subgoal *1.5.5.5.5.5/6'7') is pushed for proof by induction.
Subgoal *1.5.5.5.5.5/5
Subgoal *1.5.5.5.5.5/5'
Subgoal *1.5.5.5.5.5/4
Subgoal *1.5.5.5.5.5/4'
Splitter note (see :DOC splitter) for Subgoal *1.5.5.5.5.5/4' (2 subgoals).
if-intro: ((:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL))
Subgoal *1.5.5.5.5.5/4.2
Subgoal *1.5.5.5.5.5/4.2'
Subgoal *1.5.5.5.5.5/4.2''
Subgoal *1.5.5.5.5.5/4.2'''
*1.5.5.5.5.5.4 (Subgoal *1.5.5.5.5.5/4.2''') is pushed for proof by
induction.
Subgoal *1.5.5.5.5.5/4.1
Subgoal *1.5.5.5.5.5/4.1'
Subgoal *1.5.5.5.5.5/4.1''
Subgoal *1.5.5.5.5.5/4.1'''
*1.5.5.5.5.5.5 (Subgoal *1.5.5.5.5.5/4.1''') is pushed for proof by
induction.
Subgoal *1.5.5.5.5.5/3
Subgoal *1.5.5.5.5.5/2
Subgoal *1.5.5.5.5.5/2'
Subgoal *1.5.5.5.5.5/1
Subgoal *1.5.5.5.5.5/1'
So we now return to *1.5.5.5.5.5.5, which is
(IMPLIES (AND (TRUE-LISTP REL4)
(NOT (EQUAL S3 S11))
(NO-DUPLICATESP-EQUAL REL4)
(TRUE-LISTP REL3)
(NOT (EQUAL S3 S9))
(NOT (NO-DUPLICATESP-EQUAL REL3))
(TRUE-LISTP REL2)
(NOT (EQUAL S3 S7))
(NO-DUPLICATESP-EQUAL REL2)
(TRUE-LISTP REL1)
(NOT (EQUAL S3 S5))
(NOT (NO-DUPLICATESP-EQUAL REL1))
(TRUE-LISTP REL0)
(NOT (MEMBER-EQUAL S3 S12))
(NO-DUPLICATESP-EQUAL REL0)
(TRUE-LISTP REL)
(NOT (NO-DUPLICATESP-EQUAL REL))
(<= (LIST-COUNT S1 X) 1)
(<= (LIST-COUNT S3 REL) 1)
(<= (LIST-COUNT S5 REL0) 1)
(<= (LIST-COUNT S7 REL1) 1)
(<= (LIST-COUNT S9 REL2) 1)
(<= (LIST-COUNT S11 REL3) 1)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT REL4 S12))
(NOT (EQUAL S1 S3))
(NOT (EQUAL S1 S5))
(NOT (EQUAL S1 S7))
(NOT (EQUAL S1 S9))
(NOT (EQUAL S1 S11))
(NOT (MEMBER-EQUAL S1 S12))
(NOT (EQUAL S5 S7))
(NOT (EQUAL S5 S9))
(NOT (EQUAL S5 S11))
(NOT (MEMBER-EQUAL S5 S12))
(NOT (EQUAL S7 S9))
(NOT (EQUAL S7 S11))
(NOT (MEMBER-EQUAL S7 S12))
(NOT (EQUAL S9 S11))
(NOT (MEMBER-EQUAL S9 S12))
(NOT (MEMBER-EQUAL S11 S12))
(NO-DUPLICATESP-EQUAL S12)
(SUBSETP-EQUAL X (LIST* S1 S3 S5 S7 S9 S11 S12)))
(NOT (NO-DUPLICATESP-EQUAL X))).
Subgoal *1.5.5.5.5.5.5/13
Subgoal *1.5.5.5.5.5.5/13'
Splitter note (see :DOC splitter) for Subgoal *1.5.5.5.5.5.5/13' (2
subgoals).
if-intro: ((:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL))
Subgoal *1.5.5.5.5.5.5/13.2
Subgoal *1.5.5.5.5.5.5/13.2'
Subgoal *1.5.5.5.5.5.5/13.2''
Subgoal *1.5.5.5.5.5.5/13.2'''
*1.5.5.5.5.5.5.1 (Subgoal *1.5.5.5.5.5.5/13.2''') is pushed for proof
by induction.
Subgoal *1.5.5.5.5.5.5/13.1
Subgoal *1.5.5.5.5.5.5/13.1'
Subgoal *1.5.5.5.5.5.5/13.1''
*1.5.5.5.5.5.5.2 (Subgoal *1.5.5.5.5.5.5/13.1'') is pushed for proof
by induction.
Subgoal *1.5.5.5.5.5.5/12
Subgoal *1.5.5.5.5.5.5/12'
Subgoal *1.5.5.5.5.5.5/11
Subgoal *1.5.5.5.5.5.5/11'
Subgoal *1.5.5.5.5.5.5/10
Subgoal *1.5.5.5.5.5.5/10'
Subgoal *1.5.5.5.5.5.5/9
Subgoal *1.5.5.5.5.5.5/9'
Subgoal *1.5.5.5.5.5.5/8
Subgoal *1.5.5.5.5.5.5/8'
Subgoal *1.5.5.5.5.5.5/7
Subgoal *1.5.5.5.5.5.5/7'
Subgoal *1.5.5.5.5.5.5/6
Subgoal *1.5.5.5.5.5.5/6'
Subgoal *1.5.5.5.5.5.5/6''
Subgoal *1.5.5.5.5.5.5/6'''
Subgoal *1.5.5.5.5.5.5/6'4'
Subgoal *1.5.5.5.5.5.5/6'5'
Subgoal *1.5.5.5.5.5.5/6'6'
Subgoal *1.5.5.5.5.5.5/6'7'
*1.5.5.5.5.5.5.3 (Subgoal *1.5.5.5.5.5.5/6'7') is pushed for proof
by induction.
Subgoal *1.5.5.5.5.5.5/5
Subgoal *1.5.5.5.5.5.5/5'
Subgoal *1.5.5.5.5.5.5/4
Subgoal *1.5.5.5.5.5.5/4'
Splitter note (see :DOC splitter) for Subgoal *1.5.5.5.5.5.5/4' (2
subgoals).
if-intro: ((:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL))
Subgoal *1.5.5.5.5.5.5/4.2
Subgoal *1.5.5.5.5.5.5/4.2'
Subgoal *1.5.5.5.5.5.5/4.2''
Subgoal *1.5.5.5.5.5.5/4.2'''
*1.5.5.5.5.5.5.4 (Subgoal *1.5.5.5.5.5.5/4.2''') is pushed for proof
by induction.
Subgoal *1.5.5.5.5.5.5/4.1
Subgoal *1.5.5.5.5.5.5/4.1'
Subgoal *1.5.5.5.5.5.5/4.1''
Subgoal *1.5.5.5.5.5.5/4.1'''
*1.5.5.5.5.5.5.5 (Subgoal *1.5.5.5.5.5.5/4.1''') is pushed for proof
by induction.
Subgoal *1.5.5.5.5.5.5/3
Subgoal *1.5.5.5.5.5.5/2
Subgoal *1.5.5.5.5.5.5/2'
Subgoal *1.5.5.5.5.5.5/1
Subgoal *1.5.5.5.5.5.5/1'
So we now return to *1.5.5.5.5.5.5.5, which is
(IMPLIES (AND (TRUE-LISTP REL5)
(NOT (EQUAL S3 S13))
(NOT (NO-DUPLICATESP-EQUAL REL5))
(TRUE-LISTP REL4)
(NOT (EQUAL S3 S11))
(NO-DUPLICATESP-EQUAL REL4)
(TRUE-LISTP REL3)
(NOT (EQUAL S3 S9))
(NOT (NO-DUPLICATESP-EQUAL REL3))
(TRUE-LISTP REL2)
(NOT (EQUAL S3 S7))
(NO-DUPLICATESP-EQUAL REL2)
(TRUE-LISTP REL1)
(NOT (EQUAL S3 S5))
(NOT (NO-DUPLICATESP-EQUAL REL1))
(TRUE-LISTP REL0)
(NOT (MEMBER-EQUAL S3 S14))
(NO-DUPLICATESP-EQUAL REL0)
(TRUE-LISTP REL)
(NOT (NO-DUPLICATESP-EQUAL REL))
(<= (LIST-COUNT S1 X) 1)
(<= (LIST-COUNT S3 REL) 1)
(<= (LIST-COUNT S5 REL0) 1)
(<= (LIST-COUNT S7 REL1) 1)
(<= (LIST-COUNT S9 REL2) 1)
(<= (LIST-COUNT S11 REL3) 1)
(<= (LIST-COUNT S13 REL4) 1)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT REL5 S14))
(NOT (EQUAL S1 S3))
(NOT (EQUAL S1 S5))
(NOT (EQUAL S1 S7))
(NOT (EQUAL S1 S9))
(NOT (EQUAL S1 S11))
(NOT (EQUAL S1 S13))
(NOT (MEMBER-EQUAL S1 S14))
(NOT (EQUAL S5 S7))
(NOT (EQUAL S5 S9))
(NOT (EQUAL S5 S11))
(NOT (EQUAL S5 S13))
(NOT (MEMBER-EQUAL S5 S14))
(NOT (EQUAL S7 S9))
(NOT (EQUAL S7 S11))
(NOT (EQUAL S7 S13))
(NOT (MEMBER-EQUAL S7 S14))
(NOT (EQUAL S9 S11))
(NOT (EQUAL S9 S13))
(NOT (MEMBER-EQUAL S9 S14))
(NOT (EQUAL S11 S13))
(NOT (MEMBER-EQUAL S11 S14))
(NOT (MEMBER-EQUAL S13 S14))
(NO-DUPLICATESP-EQUAL S14)
(SUBSETP-EQUAL X (LIST* S1 S3 S5 S7 S9 S11 S13 S14)))
(NOT (NO-DUPLICATESP-EQUAL X))).
Subgoal *1.5.5.5.5.5.5.5/14
Subgoal *1.5.5.5.5.5.5.5/14'
Splitter note (see :DOC splitter) for Subgoal *1.5.5.5.5.5.5.5/14'
(2 subgoals).
if-intro: ((:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL))
Subgoal *1.5.5.5.5.5.5.5/14.2
Subgoal *1.5.5.5.5.5.5.5/14.2'
Subgoal *1.5.5.5.5.5.5.5/14.2''
Subgoal *1.5.5.5.5.5.5.5/14.2'''
*1.5.5.5.5.5.5.5.1 (Subgoal *1.5.5.5.5.5.5.5/14.2''') is pushed for
proof by induction.
Subgoal *1.5.5.5.5.5.5.5/14.1
Subgoal *1.5.5.5.5.5.5.5/14.1'
Subgoal *1.5.5.5.5.5.5.5/14.1''
*1.5.5.5.5.5.5.5.2 (Subgoal *1.5.5.5.5.5.5.5/14.1'') is pushed for
proof by induction.
Subgoal *1.5.5.5.5.5.5.5/13
Subgoal *1.5.5.5.5.5.5.5/13'
Subgoal *1.5.5.5.5.5.5.5/12
Subgoal *1.5.5.5.5.5.5.5/12'
Subgoal *1.5.5.5.5.5.5.5/11
Subgoal *1.5.5.5.5.5.5.5/11'
Subgoal *1.5.5.5.5.5.5.5/10
Subgoal *1.5.5.5.5.5.5.5/10'
Subgoal *1.5.5.5.5.5.5.5/9
Subgoal *1.5.5.5.5.5.5.5/9'
Subgoal *1.5.5.5.5.5.5.5/8
Subgoal *1.5.5.5.5.5.5.5/8'
Subgoal *1.5.5.5.5.5.5.5/7
Subgoal *1.5.5.5.5.5.5.5/7'
Subgoal *1.5.5.5.5.5.5.5/6
Subgoal *1.5.5.5.5.5.5.5/6'
Subgoal *1.5.5.5.5.5.5.5/6''
Subgoal *1.5.5.5.5.5.5.5/6'''
Subgoal *1.5.5.5.5.5.5.5/6'4'
Subgoal *1.5.5.5.5.5.5.5/6'5'
Subgoal *1.5.5.5.5.5.5.5/6'6'
Subgoal *1.5.5.5.5.5.5.5/6'7'
*1.5.5.5.5.5.5.5.3 (Subgoal *1.5.5.5.5.5.5.5/6'7') is pushed for proof
by induction.
Subgoal *1.5.5.5.5.5.5.5/5
Subgoal *1.5.5.5.5.5.5.5/5'
Subgoal *1.5.5.5.5.5.5.5/4
Subgoal *1.5.5.5.5.5.5.5/4'
Splitter note (see :DOC splitter) for Subgoal *1.5.5.5.5.5.5.5/4' (2
subgoals).
if-intro: ((:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL))
Subgoal *1.5.5.5.5.5.5.5/4.2
Subgoal *1.5.5.5.5.5.5.5/4.2'
Subgoal *1.5.5.5.5.5.5.5/4.2''
Subgoal *1.5.5.5.5.5.5.5/4.2'''
*1.5.5.5.5.5.5.5.4 (Subgoal *1.5.5.5.5.5.5.5/4.2''') is pushed for
proof by induction.
Subgoal *1.5.5.5.5.5.5.5/4.1
Subgoal *1.5.5.5.5.5.5.5/4.1'
Subgoal *1.5.5.5.5.5.5.5/4.1''
Subgoal *1.5.5.5.5.5.5.5/4.1'''
*1.5.5.5.5.5.5.5.5 (Subgoal *1.5.5.5.5.5.5.5/4.1''') is pushed for
proof by induction.
Subgoal *1.5.5.5.5.5.5.5/3
Subgoal *1.5.5.5.5.5.5.5/2
Subgoal *1.5.5.5.5.5.5.5/2'
Subgoal *1.5.5.5.5.5.5.5/1
Subgoal *1.5.5.5.5.5.5.5/1'
So we now return to *1.5.5.5.5.5.5.5.5, which is
(IMPLIES (AND (TRUE-LISTP REL6)
(NOT (EQUAL S3 S15))
(NO-DUPLICATESP-EQUAL REL6)
(TRUE-LISTP REL5)
(NOT (EQUAL S3 S13))
(NOT (NO-DUPLICATESP-EQUAL REL5))
(TRUE-LISTP REL4)
(NOT (EQUAL S3 S11))
(NO-DUPLICATESP-EQUAL REL4)
(TRUE-LISTP REL3)
(NOT (EQUAL S3 S9))
(NOT (NO-DUPLICATESP-EQUAL REL3))
(TRUE-LISTP REL2)
(NOT (EQUAL S3 S7))
(NO-DUPLICATESP-EQUAL REL2)
(TRUE-LISTP REL1)
(NOT (EQUAL S3 S5))
(NOT (NO-DUPLICATESP-EQUAL REL1))
(TRUE-LISTP REL0)
(NOT (MEMBER-EQUAL S3 S16))
(NO-DUPLICATESP-EQUAL REL0)
(TRUE-LISTP REL)
(NOT (NO-DUPLICATESP-EQUAL REL))
(<= (LIST-COUNT S1 X) 1)
(<= (LIST-COUNT S3 REL) 1)
(<= (LIST-COUNT S5 REL0) 1)
(<= (LIST-COUNT S7 REL1) 1)
(<= (LIST-COUNT S9 REL2) 1)
(<= (LIST-COUNT S11 REL3) 1)
(<= (LIST-COUNT S13 REL4) 1)
(<= (LIST-COUNT S15 REL5) 1)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT REL6 S16))
(NOT (EQUAL S1 S3))
(NOT (EQUAL S1 S5))
(NOT (EQUAL S1 S7))
(NOT (EQUAL S1 S9))
(NOT (EQUAL S1 S11))
(NOT (EQUAL S1 S13))
(NOT (EQUAL S1 S15))
(NOT (MEMBER-EQUAL S1 S16))
(NOT (EQUAL S5 S7))
(NOT (EQUAL S5 S9))
(NOT (EQUAL S5 S11))
(NOT (EQUAL S5 S13))
(NOT (EQUAL S5 S15))
(NOT (MEMBER-EQUAL S5 S16))
(NOT (EQUAL S7 S9))
(NOT (EQUAL S7 S11))
(NOT (EQUAL S7 S13))
(NOT (EQUAL S7 S15))
(NOT (MEMBER-EQUAL S7 S16))
(NOT (EQUAL S9 S11))
(NOT (EQUAL S9 S13))
(NOT (EQUAL S9 S15))
(NOT (MEMBER-EQUAL S9 S16))
(NOT (EQUAL S11 S13))
(NOT (EQUAL S11 S15))
(NOT (MEMBER-EQUAL S11 S16))
(NOT (EQUAL S13 S15))
(NOT (MEMBER-EQUAL S13 S16))
(NOT (MEMBER-EQUAL S15 S16))
(NO-DUPLICATESP-EQUAL S16)
(SUBSETP-EQUAL X
(LIST* S1 S3 S5 S7 S9 S11 S13 S15 S16)))
(NOT (NO-DUPLICATESP-EQUAL X))).
Subgoal *1.5.5.5.5.5.5.5.5/15
Subgoal *1.5.5.5.5.5.5.5.5/15'
Splitter note (see :DOC splitter) for Subgoal *1.5.5.5.5.5.5.5.5/15'
(2 subgoals).
if-intro: ((:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL))
Subgoal *1.5.5.5.5.5.5.5.5/15.2
Subgoal *1.5.5.5.5.5.5.5.5/15.2'
Subgoal *1.5.5.5.5.5.5.5.5/15.2''
Subgoal *1.5.5.5.5.5.5.5.5/15.2'''
Normally we would attempt to prove Subgoal *1.5.5.5.5.5.5.5.5/15.2'''
by induction. However, that would cause the induction-depth-limit
of 9 to be exceeded. See :DOC induction-depth-limit.
Summary
Form: ( DEFTHM MEMBER-IF-OVER-1-MAP-LIST-COUNT-IS-DUPLICATED ...)
Rules: ((:DEFINITION ENDP)
(:DEFINITION MAP-LIST-COUNT)
(:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL)
(:DEFINITION NOT)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART MEMBER-IF-OVER-1)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION MAP-LIST-COUNT)
(:INDUCTION MEMBER-EQUAL)
(:INDUCTION NO-DUPLICATESP-EQUAL)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:TYPE-PRESCRIPTION LIST-COUNT)
(:TYPE-PRESCRIPTION MAP-LIST-COUNT)
(:TYPE-PRESCRIPTION MEMBER-EQUAL)
(:TYPE-PRESCRIPTION REMOVE-EQUAL))
Splitter rules (see :DOC splitter):
if-intro: ((:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL)
(:DEFINITION NOT))
Time: 1.50 seconds (prove: 1.48, print: 0.02, other: 0.00)
Prover steps counted: 332938
---
The key checkpoint goals, below, may help you to debug this failure.
See :DOC failure and see :DOC set-checkpoint-summary-limit.
---
*** Key checkpoint at the top level: ***
Goal
(IMPLIES
(AND (MEMBER-IF-OVER-1 (MAP-LIST-COUNT X S))
(LET ((X S))
(MBE :LOGIC (PROG2$ (NO-DUPLICATESP-EQL-EXEC$GUARD-CHECK X)
(NO-DUPLICATESP-EQUAL X))
:EXEC (NO-DUPLICATESP-EQL-EXEC X)))
(LET ((Y S))
(MBE :LOGIC (PROG2$ (SUBSETP-EQL-EXEC$GUARD-CHECK X Y)
(SUBSETP-EQUAL X Y))
:EXEC (SUBSETP-EQL-EXEC X Y))))
(NOT (LET NIL
(MBE :LOGIC (PROG2$ (NO-DUPLICATESP-EQL-EXEC$GUARD-CHECK X)
(NO-DUPLICATESP-EQUAL X))
:EXEC (NO-DUPLICATESP-EQL-EXEC X)))))
*** Key checkpoints under a top-level induction
before the induction-depth-limit stopped the proof attempt: ***
Subgoal *1/2.5
(IMPLIES (AND (CONSP S)
(NOT (MEMBER-IF-OVER-1 (MAP-LIST-COUNT (REMOVE-EQUAL (CAR S) X)
(CDR S))))
(< 1 (LIST-COUNT (CAR S) X))
(CONS (LIST-COUNT (CAR S) X)
(MAP-LIST-COUNT (REMOVE-EQUAL (CAR S) X)
(CDR S)))
(NOT (MEMBER-EQUAL (CAR S) (CDR S)))
(NO-DUPLICATESP-EQUAL (CDR S))
(SUBSETP-EQUAL X S))
(NOT (NO-DUPLICATESP-EQUAL X)))
Subgoal *1/2.4
(IMPLIES (AND (CONSP S)
(NOT (SUBSETP-EQUAL (REMOVE-EQUAL (CAR S) X)
(CDR S)))
(< 1 (LIST-COUNT (CAR S) X))
(CONS (LIST-COUNT (CAR S) X)
(MAP-LIST-COUNT (REMOVE-EQUAL (CAR S) X)
(CDR S)))
(NOT (MEMBER-EQUAL (CAR S) (CDR S)))
(NO-DUPLICATESP-EQUAL (CDR S))
(SUBSETP-EQUAL X S))
(NOT (NO-DUPLICATESP-EQUAL X)))
Subgoal *1/2.3
(IMPLIES (AND (CONSP S)
(NOT (SUBSETP-EQUAL (REMOVE-EQUAL (CAR S) X)
(CDR S)))
(<= (LIST-COUNT (CAR S) X) 1)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT (REMOVE-EQUAL (CAR S) X)
(CDR S)))
(NOT (MEMBER-EQUAL (CAR S) (CDR S)))
(NO-DUPLICATESP-EQUAL (CDR S))
(SUBSETP-EQUAL X S))
(NOT (NO-DUPLICATESP-EQUAL X)))
Note: There are two additional key checkpoints under a top-level induction.
See :DOC set-checkpoint-summary-limit to change the number printed.
ACL2 Error in ( DEFTHM MEMBER-IF-OVER-1-MAP-LIST-COUNT-IS-DUPLICATED
...): See :DOC failure.
******** FAILED ********
証明に失敗しました。 しかし、下記のように帰納法は意図したものになりました。
(AND (IMPLIES (AND (NOT (ENDP S))
(:P (CDR S) (REMOVE-EQUAL (CAR S) X)))
(:P S X))
(IMPLIES (ENDP S) (:P S X)))
失敗の原因を探すため Keycheck points を確認します。
下記のメッセージ以下に Subgoal というのが表示されています。
これをみてどんな補助定理が必要かについて考えます。
*** Key checkpoints under a top-level induction
before the induction-depth-limit stopped the proof attempt: ***
Subgoal *1/2.5 と Subgoal *1/2.4 に着目してみましょう。
よくみると仮定に (< 1 (LIST-COUNT (CAR S) X)) があります。
このケースでは、明らかに X の中に重複があります。
なぜなら、 これは X の中に (CAR S) が二つ以上あることを意味するからです。
よって、これを示す定理 not-no-duplicatesp-list-count を証明します。
(defthm not-no-duplicatesp-list-count
(implies (< 1 (list-count e x))
(not (no-duplicatesp x)))
:rule-classes ((:rewrite :match-free :all)))
証明成功: 出力を確認する
Goal'
([ A key checkpoint:
Goal'
(IMPLIES (< 1 (LIST-COUNT E X))
(NOT (NO-DUPLICATESP-EQUAL X)))
*1 (Goal') is pushed for proof by induction.
])
Perhaps we can prove *1 by induction. Two induction schemes are suggested
by this conjecture. These merge into one derived induction scheme.
We will induct according to a scheme suggested by (NO-DUPLICATESP-EQUAL X),
but modified to accommodate (LIST-COUNT E X). These suggestions were
produced using the :induction rules LIST-COUNT and NO-DUPLICATESP-EQUAL.
If we let (:P E X) denote *1 above then the induction scheme we'll
use is
(AND (IMPLIES (AND (NOT (ENDP X))
(NOT (MEMBER-EQUAL (CAR X) (CDR X)))
(:P E (CDR X)))
(:P E X))
(IMPLIES (AND (NOT (ENDP X))
(MEMBER-EQUAL (CAR X) (CDR X)))
(:P E X))
(IMPLIES (ENDP X) (:P E X))).
This induction is justified by the same argument used to admit
NO-DUPLICATESP-EQUAL. When applied to the goal at hand the above induction
scheme produces four nontautological subgoals.
Subgoal *1/4
Subgoal *1/4'
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/3''
Subgoal *1/3'''
Subgoal *1/3'4'
Subgoal *1/3'5'
([ A key checkpoint while proving *1 (descended from Goal'):
Subgoal *1/3'''
(IMPLIES (AND (EQUAL (LIST-COUNT (CAR X) (CDR X)) 1)
(CONSP X)
(NOT (MEMBER-EQUAL (CAR X) (CDR X))))
(NOT (NO-DUPLICATESP-EQUAL (CDR X))))
*1.1 (Subgoal *1/3'5') is pushed for proof by induction.
])
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/2''
Subgoal *1/1
Subgoal *1/1'
So we now return to *1.1, which is
(IMPLIES (AND (EQUAL (LIST-COUNT X1 X2) 1)
(NOT (MEMBER-EQUAL X1 X2)))
(NOT (NO-DUPLICATESP-EQUAL X2))).
Subgoal *1.1/5
Subgoal *1.1/5'
Subgoal *1.1/4
Subgoal *1.1/4'
Subgoal *1.1/3
Subgoal *1.1/3'
Subgoal *1.1/2
Subgoal *1.1/2'
Subgoal *1.1/1
Subgoal *1.1/1'
*1.1 and *1 are COMPLETED!
Thus key checkpoints Subgoal *1/3''' and Goal' are COMPLETED!
Q.E.D.
Summary
Form: ( DEFTHM NOT-NO-DUPLICATESP-LIST-COUNT ...)
Rules: ((:DEFINITION ENDP)
(:DEFINITION LIST-COUNT)
(:DEFINITION MEMBER-EQUAL)
(:DEFINITION NO-DUPLICATESP-EQL-EXEC$GUARD-CHECK)
(:DEFINITION NO-DUPLICATESP-EQUAL)
(:DEFINITION NOT)
(:DEFINITION RETURN-LAST)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART <)
(:EXECUTABLE-COUNTERPART BINARY-+)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART NOT)
(:FAKE-RUNE-FOR-LINEAR NIL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION LIST-COUNT)
(:INDUCTION MEMBER-EQUAL)
(:INDUCTION NO-DUPLICATESP-EQUAL)
(:TYPE-PRESCRIPTION LIST-COUNT)
(:TYPE-PRESCRIPTION MEMBER-EQUAL))
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted: 2241
NOT-NO-DUPLICATESP-LIST-COUNT
(defthm member-if-over-1-map-list-count-is-duplicated
(implies (and (no-duplicatesp s)
(subsetp x s)
(member-if-over-1 (map-list-count x s)))
(not (no-duplicatesp x)))
:hints (("Goal" :induct (map-list-count x s)))
:rule-classes ((:rewrite :match-free :all)))
証明失敗: 出力を確認する
*1 (the initial Goal, a key checkpoint) is pushed for proof by induction.
We have been told to use induction. One induction scheme is suggested
by the induction hint.
We will induct according to a scheme suggested by (MAP-LIST-COUNT X S).
This suggestion was produced using the :induction rule MAP-LIST-COUNT.
If we let (:P S X) denote *1 above then the induction scheme we'll
use is
(AND (IMPLIES (AND (NOT (ENDP S))
(:P (CDR S) (REMOVE-EQUAL (CAR S) X)))
(:P S X))
(IMPLIES (ENDP S) (:P S X))).
This induction is justified by the same argument used to admit
MAP-LIST-COUNT. Note, however, that the unmeasured variable X is being
instantiated. When applied to the goal at hand the above induction
scheme produces two nontautological subgoals.
Subgoal *1/2
Subgoal *1/2'
Splitter note (see :DOC splitter) for Subgoal *1/2' (2 subgoals).
if-intro: ((:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL)
(:DEFINITION NOT))
Subgoal *1/2.2
Subgoal *1/2.2'
Subgoal *1/2.2''
Subgoal *1/2.2'''
([ A key checkpoint while proving *1 (descended from Goal):
Subgoal *1/2.2
(IMPLIES (AND (CONSP S)
(NOT (SUBSETP-EQUAL (REMOVE-EQUAL (CAR S) X)
(CDR S)))
(NOT (MEMBER-EQUAL (CAR S) (CDR S)))
(NO-DUPLICATESP-EQUAL (CDR S))
(SUBSETP-EQUAL X S)
(<= (LIST-COUNT (CAR S) X) 1)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT (REMOVE-EQUAL (CAR S) X)
(CDR S))))
(NOT (NO-DUPLICATESP-EQUAL X)))
*1.1 (Subgoal *1/2.2''') is pushed for proof by induction.
])
Subgoal *1/2.1
Subgoal *1/2.1'
Subgoal *1/2.1''
Subgoal *1/2.1'''
([ A key checkpoint while proving *1 (descended from Goal):
Subgoal *1/2.1
(IMPLIES (AND (CONSP S)
(NOT (NO-DUPLICATESP-EQUAL (REMOVE-EQUAL (CAR S) X)))
(NOT (MEMBER-EQUAL (CAR S) (CDR S)))
(NO-DUPLICATESP-EQUAL (CDR S))
(SUBSETP-EQUAL X S)
(<= (LIST-COUNT (CAR S) X) 1)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT (REMOVE-EQUAL (CAR S) X)
(CDR S))))
(NOT (NO-DUPLICATESP-EQUAL X)))
*1.2 (Subgoal *1/2.1''') is pushed for proof by induction.
])
Subgoal *1/1
Subgoal *1/1'
So we now return to *1.2, which is
(IMPLIES (AND (TRUE-LISTP REL)
(NOT (NO-DUPLICATESP-EQUAL REL))
(NOT (MEMBER-EQUAL S1 S2))
(NO-DUPLICATESP-EQUAL S2)
(SUBSETP-EQUAL X (CONS S1 S2))
(<= (LIST-COUNT S1 X) 1)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT REL S2)))
(NOT (NO-DUPLICATESP-EQUAL X))).
Subgoal *1.2/7
Subgoal *1.2/7'
Subgoal *1.2/7''
Subgoal *1.2/7'''
Subgoal *1.2/7'4'
Subgoal *1.2/7'5'
Subgoal *1.2/7'6'
Subgoal *1.2/7'7'
Subgoal *1.2/7'8'
*1.2.1 (Subgoal *1.2/7'8') is pushed for proof by induction.
Subgoal *1.2/6
Subgoal *1.2/6'
Splitter note (see :DOC splitter) for Subgoal *1.2/6' (2 subgoals).
if-intro: ((:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL))
Subgoal *1.2/6.2
Subgoal *1.2/6.2'
Subgoal *1.2/6.2''
Subgoal *1.2/6.2'''
Subgoal *1.2/6.2'4'
*1.2.2 (Subgoal *1.2/6.2'4') is pushed for proof by induction.
Subgoal *1.2/6.1
Subgoal *1.2/6.1'
Subgoal *1.2/6.1''
*1.2.3 (Subgoal *1.2/6.1'') is pushed for proof by induction.
Subgoal *1.2/5
Subgoal *1.2/5'
Subgoal *1.2/4
Subgoal *1.2/4'
Subgoal *1.2/3
Subgoal *1.2/3'
Splitter note (see :DOC splitter) for Subgoal *1.2/3' (2 subgoals).
if-intro: ((:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL))
Subgoal *1.2/3.2
Subgoal *1.2/3.2'
Subgoal *1.2/3.2''
Subgoal *1.2/3.2'''
Subgoal *1.2/3.2'4'
Subgoal *1.2/3.2'5'
*1.2.4 (Subgoal *1.2/3.2'5') is pushed for proof by induction.
Subgoal *1.2/3.1
Subgoal *1.2/3.1'
Subgoal *1.2/3.1''
Subgoal *1.2/3.1'''
*1.2.5 (Subgoal *1.2/3.1''') is pushed for proof by induction.
Subgoal *1.2/2
Subgoal *1.2/1
Subgoal *1.2/1'
So we now return to *1.2.5, which is
(IMPLIES (AND (TRUE-LISTP REL0)
(NO-DUPLICATESP-EQUAL REL0)
(TRUE-LISTP REL)
(NOT (NO-DUPLICATESP-EQUAL REL))
(NOT (EQUAL S1 S3))
(NOT (MEMBER-EQUAL S1 S4))
(NOT (MEMBER-EQUAL S3 S4))
(NO-DUPLICATESP-EQUAL S4)
(SUBSETP-EQUAL X (LIST* S1 S3 S4))
(<= (LIST-COUNT S1 X) 1)
(<= (LIST-COUNT S3 REL) 1)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT REL0 S4)))
(NOT (NO-DUPLICATESP-EQUAL X))).
Subgoal *1.2.5/9
Subgoal *1.2.5/9'
Subgoal *1.2.5/9''
Subgoal *1.2.5/8
Subgoal *1.2.5/8'
Splitter note (see :DOC splitter) for Subgoal *1.2.5/8' (2 subgoals).
if-intro: ((:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL))
Subgoal *1.2.5/8.2
Subgoal *1.2.5/8.1
Subgoal *1.2.5/8.1'
Subgoal *1.2.5/8.1''
*1.2.5.1 (Subgoal *1.2.5/8.1'') is pushed for proof by induction.
Subgoal *1.2.5/7
Subgoal *1.2.5/7'
Subgoal *1.2.5/6
Subgoal *1.2.5/6'
Subgoal *1.2.5/5
Subgoal *1.2.5/5'
Subgoal *1.2.5/4
Subgoal *1.2.5/4'
Splitter note (see :DOC splitter) for Subgoal *1.2.5/4' (2 subgoals).
if-intro: ((:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL))
Subgoal *1.2.5/4.2
Subgoal *1.2.5/4.1
Subgoal *1.2.5/4.1'
Subgoal *1.2.5/4.1''
Subgoal *1.2.5/4.1'''
*1.2.5.2 (Subgoal *1.2.5/4.1''') is pushed for proof by induction.
Subgoal *1.2.5/3
Subgoal *1.2.5/2
Subgoal *1.2.5/2'
Subgoal *1.2.5/1
Subgoal *1.2.5/1'
So we now return to *1.2.5.2, which is
(IMPLIES (AND (TRUE-LISTP REL1)
(NOT (EQUAL S1 S5))
(NOT (NO-DUPLICATESP-EQUAL REL1))
(TRUE-LISTP REL0)
(NO-DUPLICATESP-EQUAL REL0)
(TRUE-LISTP REL)
(NOT (NO-DUPLICATESP-EQUAL REL))
(NOT (EQUAL S1 S3))
(NOT (MEMBER-EQUAL S1 S6))
(NOT (EQUAL S3 S5))
(NOT (MEMBER-EQUAL S3 S6))
(NOT (MEMBER-EQUAL S5 S6))
(NO-DUPLICATESP-EQUAL S6)
(SUBSETP-EQUAL X (LIST* S1 S3 S5 S6))
(<= (LIST-COUNT S1 X) 1)
(<= (LIST-COUNT S3 REL) 1)
(<= (LIST-COUNT S5 REL0) 1)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT REL1 S6)))
(NOT (NO-DUPLICATESP-EQUAL X))).
Subgoal *1.2.5.2/10
Subgoal *1.2.5.2/10'
Subgoal *1.2.5.2/10''
Subgoal *1.2.5.2/10'''
Subgoal *1.2.5.2/10'4'
Subgoal *1.2.5.2/10'5'
Subgoal *1.2.5.2/10'6'
Subgoal *1.2.5.2/10'7'
Subgoal *1.2.5.2/10'8'
*1.2.5.2.1 (Subgoal *1.2.5.2/10'8') is pushed for proof by induction.
Subgoal *1.2.5.2/9
Subgoal *1.2.5.2/9'
Splitter note (see :DOC splitter) for Subgoal *1.2.5.2/9' (2 subgoals).
if-intro: ((:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL))
Subgoal *1.2.5.2/9.2
Subgoal *1.2.5.2/9.2'
Subgoal *1.2.5.2/9.2''
Subgoal *1.2.5.2/9.2'''
Subgoal *1.2.5.2/9.2'4'
*1.2.5.2.2 (Subgoal *1.2.5.2/9.2'4') is pushed for proof by induction.
Subgoal *1.2.5.2/9.1
Subgoal *1.2.5.2/9.1'
Subgoal *1.2.5.2/9.1''
*1.2.5.2.3 (Subgoal *1.2.5.2/9.1'') is pushed for proof by induction.
Subgoal *1.2.5.2/8
Subgoal *1.2.5.2/8'
Subgoal *1.2.5.2/7
Subgoal *1.2.5.2/7'
Subgoal *1.2.5.2/6
Subgoal *1.2.5.2/6'
Subgoal *1.2.5.2/5
Subgoal *1.2.5.2/5'
Subgoal *1.2.5.2/4
Subgoal *1.2.5.2/4'
Splitter note (see :DOC splitter) for Subgoal *1.2.5.2/4' (2 subgoals).
if-intro: ((:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL))
Subgoal *1.2.5.2/4.2
Subgoal *1.2.5.2/4.2'
Subgoal *1.2.5.2/4.2''
Subgoal *1.2.5.2/4.2'''
Subgoal *1.2.5.2/4.2'4'
Subgoal *1.2.5.2/4.2'5'
*1.2.5.2.4 (Subgoal *1.2.5.2/4.2'5') is pushed for proof by induction.
Subgoal *1.2.5.2/4.1
Subgoal *1.2.5.2/4.1'
Subgoal *1.2.5.2/4.1''
Subgoal *1.2.5.2/4.1'''
*1.2.5.2.5 (Subgoal *1.2.5.2/4.1''') is pushed for proof by induction.
Subgoal *1.2.5.2/3
Subgoal *1.2.5.2/2
Subgoal *1.2.5.2/2'
Subgoal *1.2.5.2/1
Subgoal *1.2.5.2/1'
So we now return to *1.2.5.2.5, which is
(IMPLIES (AND (TRUE-LISTP REL2)
(NOT (EQUAL S1 S7))
(NO-DUPLICATESP-EQUAL REL2)
(TRUE-LISTP REL1)
(NOT (EQUAL S1 S5))
(NOT (NO-DUPLICATESP-EQUAL REL1))
(TRUE-LISTP REL0)
(NO-DUPLICATESP-EQUAL REL0)
(TRUE-LISTP REL)
(NOT (NO-DUPLICATESP-EQUAL REL))
(NOT (EQUAL S1 S3))
(NOT (MEMBER-EQUAL S1 S8))
(NOT (EQUAL S3 S5))
(NOT (EQUAL S3 S7))
(NOT (MEMBER-EQUAL S3 S8))
(NOT (EQUAL S5 S7))
(NOT (MEMBER-EQUAL S5 S8))
(NOT (MEMBER-EQUAL S7 S8))
(NO-DUPLICATESP-EQUAL S8)
(SUBSETP-EQUAL X (LIST* S1 S3 S5 S7 S8))
(<= (LIST-COUNT S1 X) 1)
(<= (LIST-COUNT S3 REL) 1)
(<= (LIST-COUNT S5 REL0) 1)
(<= (LIST-COUNT S7 REL1) 1)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT REL2 S8)))
(NOT (NO-DUPLICATESP-EQUAL X))).
Subgoal *1.2.5.2.5/11
Subgoal *1.2.5.2.5/11'
Subgoal *1.2.5.2.5/11''
Subgoal *1.2.5.2.5/10
Subgoal *1.2.5.2.5/10'
Splitter note (see :DOC splitter) for Subgoal *1.2.5.2.5/10' (2 subgoals).
if-intro: ((:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL))
Subgoal *1.2.5.2.5/10.2
Subgoal *1.2.5.2.5/10.1
Subgoal *1.2.5.2.5/10.1'
Subgoal *1.2.5.2.5/10.1''
*1.2.5.2.5.1 (Subgoal *1.2.5.2.5/10.1'') is pushed for proof by induction.
Subgoal *1.2.5.2.5/9
Subgoal *1.2.5.2.5/9'
Subgoal *1.2.5.2.5/8
Subgoal *1.2.5.2.5/8'
Subgoal *1.2.5.2.5/7
Subgoal *1.2.5.2.5/7'
Subgoal *1.2.5.2.5/6
Subgoal *1.2.5.2.5/6'
Subgoal *1.2.5.2.5/5
Subgoal *1.2.5.2.5/5'
Subgoal *1.2.5.2.5/4
Subgoal *1.2.5.2.5/4'
Splitter note (see :DOC splitter) for Subgoal *1.2.5.2.5/4' (2 subgoals).
if-intro: ((:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL))
Subgoal *1.2.5.2.5/4.2
Subgoal *1.2.5.2.5/4.1
Subgoal *1.2.5.2.5/4.1'
Subgoal *1.2.5.2.5/4.1''
Subgoal *1.2.5.2.5/4.1'''
*1.2.5.2.5.2 (Subgoal *1.2.5.2.5/4.1''') is pushed for proof by induction.
Subgoal *1.2.5.2.5/3
Subgoal *1.2.5.2.5/2
Subgoal *1.2.5.2.5/2'
Subgoal *1.2.5.2.5/1
Subgoal *1.2.5.2.5/1'
So we now return to *1.2.5.2.5.2, which is
(IMPLIES (AND (TRUE-LISTP REL3)
(NOT (EQUAL S1 S9))
(NOT (NO-DUPLICATESP-EQUAL REL3))
(TRUE-LISTP REL2)
(NOT (EQUAL S1 S7))
(NO-DUPLICATESP-EQUAL REL2)
(TRUE-LISTP REL1)
(NOT (EQUAL S1 S5))
(NOT (NO-DUPLICATESP-EQUAL REL1))
(TRUE-LISTP REL0)
(NO-DUPLICATESP-EQUAL REL0)
(TRUE-LISTP REL)
(NOT (NO-DUPLICATESP-EQUAL REL))
(NOT (EQUAL S1 S3))
(NOT (MEMBER-EQUAL S1 S10))
(NOT (EQUAL S3 S5))
(NOT (EQUAL S3 S7))
(NOT (EQUAL S3 S9))
(NOT (MEMBER-EQUAL S3 S10))
(NOT (EQUAL S5 S7))
(NOT (EQUAL S5 S9))
(NOT (MEMBER-EQUAL S5 S10))
(NOT (EQUAL S7 S9))
(NOT (MEMBER-EQUAL S7 S10))
(NOT (MEMBER-EQUAL S9 S10))
(NO-DUPLICATESP-EQUAL S10)
(SUBSETP-EQUAL X (LIST* S1 S3 S5 S7 S9 S10))
(<= (LIST-COUNT S1 X) 1)
(<= (LIST-COUNT S3 REL) 1)
(<= (LIST-COUNT S5 REL0) 1)
(<= (LIST-COUNT S7 REL1) 1)
(<= (LIST-COUNT S9 REL2) 1)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT REL3 S10)))
(NOT (NO-DUPLICATESP-EQUAL X))).
Subgoal *1.2.5.2.5.2/12
Subgoal *1.2.5.2.5.2/12'
Subgoal *1.2.5.2.5.2/12''
Subgoal *1.2.5.2.5.2/12'''
Subgoal *1.2.5.2.5.2/12'4'
Subgoal *1.2.5.2.5.2/12'5'
Subgoal *1.2.5.2.5.2/12'6'
Subgoal *1.2.5.2.5.2/12'7'
Subgoal *1.2.5.2.5.2/12'8'
*1.2.5.2.5.2.1 (Subgoal *1.2.5.2.5.2/12'8') is pushed for proof by
induction.
Subgoal *1.2.5.2.5.2/11
Subgoal *1.2.5.2.5.2/11'
Splitter note (see :DOC splitter) for Subgoal *1.2.5.2.5.2/11' (2 subgoals).
if-intro: ((:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL))
Subgoal *1.2.5.2.5.2/11.2
Subgoal *1.2.5.2.5.2/11.2'
Subgoal *1.2.5.2.5.2/11.2''
Subgoal *1.2.5.2.5.2/11.2'''
Subgoal *1.2.5.2.5.2/11.2'4'
*1.2.5.2.5.2.2 (Subgoal *1.2.5.2.5.2/11.2'4') is pushed for proof by
induction.
Subgoal *1.2.5.2.5.2/11.1
Subgoal *1.2.5.2.5.2/11.1'
Subgoal *1.2.5.2.5.2/11.1''
*1.2.5.2.5.2.3 (Subgoal *1.2.5.2.5.2/11.1'') is pushed for proof by
induction.
Subgoal *1.2.5.2.5.2/10
Subgoal *1.2.5.2.5.2/10'
Subgoal *1.2.5.2.5.2/9
Subgoal *1.2.5.2.5.2/9'
Subgoal *1.2.5.2.5.2/8
Subgoal *1.2.5.2.5.2/8'
Subgoal *1.2.5.2.5.2/7
Subgoal *1.2.5.2.5.2/7'
Subgoal *1.2.5.2.5.2/6
Subgoal *1.2.5.2.5.2/6'
Subgoal *1.2.5.2.5.2/5
Subgoal *1.2.5.2.5.2/5'
Subgoal *1.2.5.2.5.2/4
Subgoal *1.2.5.2.5.2/4'
Splitter note (see :DOC splitter) for Subgoal *1.2.5.2.5.2/4' (2 subgoals).
if-intro: ((:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL))
Subgoal *1.2.5.2.5.2/4.2
Subgoal *1.2.5.2.5.2/4.2'
Subgoal *1.2.5.2.5.2/4.2''
Subgoal *1.2.5.2.5.2/4.2'''
Subgoal *1.2.5.2.5.2/4.2'4'
Subgoal *1.2.5.2.5.2/4.2'5'
*1.2.5.2.5.2.4 (Subgoal *1.2.5.2.5.2/4.2'5') is pushed for proof by
induction.
Subgoal *1.2.5.2.5.2/4.1
Subgoal *1.2.5.2.5.2/4.1'
Subgoal *1.2.5.2.5.2/4.1''
Subgoal *1.2.5.2.5.2/4.1'''
*1.2.5.2.5.2.5 (Subgoal *1.2.5.2.5.2/4.1''') is pushed for proof by
induction.
Subgoal *1.2.5.2.5.2/3
Subgoal *1.2.5.2.5.2/2
Subgoal *1.2.5.2.5.2/2'
Subgoal *1.2.5.2.5.2/1
Subgoal *1.2.5.2.5.2/1'
So we now return to *1.2.5.2.5.2.5, which is
(IMPLIES (AND (TRUE-LISTP REL4)
(NOT (EQUAL S1 S11))
(NO-DUPLICATESP-EQUAL REL4)
(TRUE-LISTP REL3)
(NOT (EQUAL S1 S9))
(NOT (NO-DUPLICATESP-EQUAL REL3))
(TRUE-LISTP REL2)
(NOT (EQUAL S1 S7))
(NO-DUPLICATESP-EQUAL REL2)
(TRUE-LISTP REL1)
(NOT (EQUAL S1 S5))
(NOT (NO-DUPLICATESP-EQUAL REL1))
(TRUE-LISTP REL0)
(NO-DUPLICATESP-EQUAL REL0)
(TRUE-LISTP REL)
(NOT (NO-DUPLICATESP-EQUAL REL))
(NOT (EQUAL S1 S3))
(NOT (MEMBER-EQUAL S1 S12))
(NOT (EQUAL S3 S5))
(NOT (EQUAL S3 S7))
(NOT (EQUAL S3 S9))
(NOT (EQUAL S3 S11))
(NOT (MEMBER-EQUAL S3 S12))
(NOT (EQUAL S5 S7))
(NOT (EQUAL S5 S9))
(NOT (EQUAL S5 S11))
(NOT (MEMBER-EQUAL S5 S12))
(NOT (EQUAL S7 S9))
(NOT (EQUAL S7 S11))
(NOT (MEMBER-EQUAL S7 S12))
(NOT (EQUAL S9 S11))
(NOT (MEMBER-EQUAL S9 S12))
(NOT (MEMBER-EQUAL S11 S12))
(NO-DUPLICATESP-EQUAL S12)
(SUBSETP-EQUAL X (LIST* S1 S3 S5 S7 S9 S11 S12))
(<= (LIST-COUNT S1 X) 1)
(<= (LIST-COUNT S3 REL) 1)
(<= (LIST-COUNT S5 REL0) 1)
(<= (LIST-COUNT S7 REL1) 1)
(<= (LIST-COUNT S9 REL2) 1)
(<= (LIST-COUNT S11 REL3) 1)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT REL4 S12)))
(NOT (NO-DUPLICATESP-EQUAL X))).
Subgoal *1.2.5.2.5.2.5/13
Subgoal *1.2.5.2.5.2.5/13'
Subgoal *1.2.5.2.5.2.5/13''
Subgoal *1.2.5.2.5.2.5/12
Subgoal *1.2.5.2.5.2.5/12'
Splitter note (see :DOC splitter) for Subgoal *1.2.5.2.5.2.5/12' (2
subgoals).
if-intro: ((:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL))
Subgoal *1.2.5.2.5.2.5/12.2
Subgoal *1.2.5.2.5.2.5/12.1
Subgoal *1.2.5.2.5.2.5/12.1'
Subgoal *1.2.5.2.5.2.5/12.1''
*1.2.5.2.5.2.5.1 (Subgoal *1.2.5.2.5.2.5/12.1'') is pushed for proof
by induction.
Subgoal *1.2.5.2.5.2.5/11
Subgoal *1.2.5.2.5.2.5/11'
Subgoal *1.2.5.2.5.2.5/10
Subgoal *1.2.5.2.5.2.5/10'
Subgoal *1.2.5.2.5.2.5/9
Subgoal *1.2.5.2.5.2.5/9'
Subgoal *1.2.5.2.5.2.5/8
Subgoal *1.2.5.2.5.2.5/8'
Subgoal *1.2.5.2.5.2.5/7
Subgoal *1.2.5.2.5.2.5/7'
Subgoal *1.2.5.2.5.2.5/6
Subgoal *1.2.5.2.5.2.5/6'
Subgoal *1.2.5.2.5.2.5/5
Subgoal *1.2.5.2.5.2.5/5'
Subgoal *1.2.5.2.5.2.5/4
Subgoal *1.2.5.2.5.2.5/4'
Splitter note (see :DOC splitter) for Subgoal *1.2.5.2.5.2.5/4' (2
subgoals).
if-intro: ((:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL))
Subgoal *1.2.5.2.5.2.5/4.2
Subgoal *1.2.5.2.5.2.5/4.1
Subgoal *1.2.5.2.5.2.5/4.1'
Subgoal *1.2.5.2.5.2.5/4.1''
Subgoal *1.2.5.2.5.2.5/4.1'''
*1.2.5.2.5.2.5.2 (Subgoal *1.2.5.2.5.2.5/4.1''') is pushed for proof
by induction.
Subgoal *1.2.5.2.5.2.5/3
Subgoal *1.2.5.2.5.2.5/2
Subgoal *1.2.5.2.5.2.5/2'
Subgoal *1.2.5.2.5.2.5/1
Subgoal *1.2.5.2.5.2.5/1'
So we now return to *1.2.5.2.5.2.5.2, which is
(IMPLIES (AND (TRUE-LISTP REL5)
(NOT (EQUAL S1 S13))
(NOT (NO-DUPLICATESP-EQUAL REL5))
(TRUE-LISTP REL4)
(NOT (EQUAL S1 S11))
(NO-DUPLICATESP-EQUAL REL4)
(TRUE-LISTP REL3)
(NOT (EQUAL S1 S9))
(NOT (NO-DUPLICATESP-EQUAL REL3))
(TRUE-LISTP REL2)
(NOT (EQUAL S1 S7))
(NO-DUPLICATESP-EQUAL REL2)
(TRUE-LISTP REL1)
(NOT (EQUAL S1 S5))
(NOT (NO-DUPLICATESP-EQUAL REL1))
(TRUE-LISTP REL0)
(NO-DUPLICATESP-EQUAL REL0)
(TRUE-LISTP REL)
(NOT (NO-DUPLICATESP-EQUAL REL))
(NOT (EQUAL S1 S3))
(NOT (MEMBER-EQUAL S1 S14))
(NOT (EQUAL S3 S5))
(NOT (EQUAL S3 S7))
(NOT (EQUAL S3 S9))
(NOT (EQUAL S3 S11))
(NOT (EQUAL S3 S13))
(NOT (MEMBER-EQUAL S3 S14))
(NOT (EQUAL S5 S7))
(NOT (EQUAL S5 S9))
(NOT (EQUAL S5 S11))
(NOT (EQUAL S5 S13))
(NOT (MEMBER-EQUAL S5 S14))
(NOT (EQUAL S7 S9))
(NOT (EQUAL S7 S11))
(NOT (EQUAL S7 S13))
(NOT (MEMBER-EQUAL S7 S14))
(NOT (EQUAL S9 S11))
(NOT (EQUAL S9 S13))
(NOT (MEMBER-EQUAL S9 S14))
(NOT (EQUAL S11 S13))
(NOT (MEMBER-EQUAL S11 S14))
(NOT (MEMBER-EQUAL S13 S14))
(NO-DUPLICATESP-EQUAL S14)
(SUBSETP-EQUAL X (LIST* S1 S3 S5 S7 S9 S11 S13 S14))
(<= (LIST-COUNT S1 X) 1)
(<= (LIST-COUNT S3 REL) 1)
(<= (LIST-COUNT S5 REL0) 1)
(<= (LIST-COUNT S7 REL1) 1)
(<= (LIST-COUNT S9 REL2) 1)
(<= (LIST-COUNT S11 REL3) 1)
(<= (LIST-COUNT S13 REL4) 1)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT REL5 S14)))
(NOT (NO-DUPLICATESP-EQUAL X))).
Subgoal *1.2.5.2.5.2.5.2/14
Subgoal *1.2.5.2.5.2.5.2/14'
Subgoal *1.2.5.2.5.2.5.2/14''
Subgoal *1.2.5.2.5.2.5.2/14'''
Subgoal *1.2.5.2.5.2.5.2/14'4'
Subgoal *1.2.5.2.5.2.5.2/14'5'
Subgoal *1.2.5.2.5.2.5.2/14'6'
Subgoal *1.2.5.2.5.2.5.2/14'7'
Subgoal *1.2.5.2.5.2.5.2/14'8'
*1.2.5.2.5.2.5.2.1 (Subgoal *1.2.5.2.5.2.5.2/14'8') is pushed for proof
by induction.
Subgoal *1.2.5.2.5.2.5.2/13
Subgoal *1.2.5.2.5.2.5.2/13'
Splitter note (see :DOC splitter) for Subgoal *1.2.5.2.5.2.5.2/13'
(2 subgoals).
if-intro: ((:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL))
Subgoal *1.2.5.2.5.2.5.2/13.2
Subgoal *1.2.5.2.5.2.5.2/13.2'
Subgoal *1.2.5.2.5.2.5.2/13.2''
Subgoal *1.2.5.2.5.2.5.2/13.2'''
Subgoal *1.2.5.2.5.2.5.2/13.2'4'
*1.2.5.2.5.2.5.2.2 (Subgoal *1.2.5.2.5.2.5.2/13.2'4') is pushed for
proof by induction.
Subgoal *1.2.5.2.5.2.5.2/13.1
Subgoal *1.2.5.2.5.2.5.2/13.1'
Subgoal *1.2.5.2.5.2.5.2/13.1''
*1.2.5.2.5.2.5.2.3 (Subgoal *1.2.5.2.5.2.5.2/13.1'') is pushed for
proof by induction.
Subgoal *1.2.5.2.5.2.5.2/12
Subgoal *1.2.5.2.5.2.5.2/12'
Subgoal *1.2.5.2.5.2.5.2/11
Subgoal *1.2.5.2.5.2.5.2/11'
Subgoal *1.2.5.2.5.2.5.2/10
Subgoal *1.2.5.2.5.2.5.2/10'
Subgoal *1.2.5.2.5.2.5.2/9
Subgoal *1.2.5.2.5.2.5.2/9'
Subgoal *1.2.5.2.5.2.5.2/8
Subgoal *1.2.5.2.5.2.5.2/8'
Subgoal *1.2.5.2.5.2.5.2/7
Subgoal *1.2.5.2.5.2.5.2/7'
Subgoal *1.2.5.2.5.2.5.2/6
Subgoal *1.2.5.2.5.2.5.2/6'
Subgoal *1.2.5.2.5.2.5.2/5
Subgoal *1.2.5.2.5.2.5.2/5'
Subgoal *1.2.5.2.5.2.5.2/4
Subgoal *1.2.5.2.5.2.5.2/4'
Splitter note (see :DOC splitter) for Subgoal *1.2.5.2.5.2.5.2/4' (2
subgoals).
if-intro: ((:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL))
Subgoal *1.2.5.2.5.2.5.2/4.2
Subgoal *1.2.5.2.5.2.5.2/4.2'
Subgoal *1.2.5.2.5.2.5.2/4.2''
Subgoal *1.2.5.2.5.2.5.2/4.2'''
Subgoal *1.2.5.2.5.2.5.2/4.2'4'
Subgoal *1.2.5.2.5.2.5.2/4.2'5'
*1.2.5.2.5.2.5.2.4 (Subgoal *1.2.5.2.5.2.5.2/4.2'5') is pushed for
proof by induction.
Subgoal *1.2.5.2.5.2.5.2/4.1
Subgoal *1.2.5.2.5.2.5.2/4.1'
Subgoal *1.2.5.2.5.2.5.2/4.1''
Subgoal *1.2.5.2.5.2.5.2/4.1'''
*1.2.5.2.5.2.5.2.5 (Subgoal *1.2.5.2.5.2.5.2/4.1''') is pushed for
proof by induction.
Subgoal *1.2.5.2.5.2.5.2/3
Subgoal *1.2.5.2.5.2.5.2/2
Subgoal *1.2.5.2.5.2.5.2/2'
Subgoal *1.2.5.2.5.2.5.2/1
Subgoal *1.2.5.2.5.2.5.2/1'
So we now return to *1.2.5.2.5.2.5.2.5, which is
(IMPLIES (AND (TRUE-LISTP REL6)
(NOT (EQUAL S1 S15))
(NO-DUPLICATESP-EQUAL REL6)
(TRUE-LISTP REL5)
(NOT (EQUAL S1 S13))
(NOT (NO-DUPLICATESP-EQUAL REL5))
(TRUE-LISTP REL4)
(NOT (EQUAL S1 S11))
(NO-DUPLICATESP-EQUAL REL4)
(TRUE-LISTP REL3)
(NOT (EQUAL S1 S9))
(NOT (NO-DUPLICATESP-EQUAL REL3))
(TRUE-LISTP REL2)
(NOT (EQUAL S1 S7))
(NO-DUPLICATESP-EQUAL REL2)
(TRUE-LISTP REL1)
(NOT (EQUAL S1 S5))
(NOT (NO-DUPLICATESP-EQUAL REL1))
(TRUE-LISTP REL0)
(NO-DUPLICATESP-EQUAL REL0)
(TRUE-LISTP REL)
(NOT (NO-DUPLICATESP-EQUAL REL))
(NOT (EQUAL S1 S3))
(NOT (MEMBER-EQUAL S1 S16))
(NOT (EQUAL S3 S5))
(NOT (EQUAL S3 S7))
(NOT (EQUAL S3 S9))
(NOT (EQUAL S3 S11))
(NOT (EQUAL S3 S13))
(NOT (EQUAL S3 S15))
(NOT (MEMBER-EQUAL S3 S16))
(NOT (EQUAL S5 S7))
(NOT (EQUAL S5 S9))
(NOT (EQUAL S5 S11))
(NOT (EQUAL S5 S13))
(NOT (EQUAL S5 S15))
(NOT (MEMBER-EQUAL S5 S16))
(NOT (EQUAL S7 S9))
(NOT (EQUAL S7 S11))
(NOT (EQUAL S7 S13))
(NOT (EQUAL S7 S15))
(NOT (MEMBER-EQUAL S7 S16))
(NOT (EQUAL S9 S11))
(NOT (EQUAL S9 S13))
(NOT (EQUAL S9 S15))
(NOT (MEMBER-EQUAL S9 S16))
(NOT (EQUAL S11 S13))
(NOT (EQUAL S11 S15))
(NOT (MEMBER-EQUAL S11 S16))
(NOT (EQUAL S13 S15))
(NOT (MEMBER-EQUAL S13 S16))
(NOT (MEMBER-EQUAL S15 S16))
(NO-DUPLICATESP-EQUAL S16)
(SUBSETP-EQUAL X
(LIST* S1 S3 S5 S7 S9 S11 S13 S15 S16))
(<= (LIST-COUNT S1 X) 1)
(<= (LIST-COUNT S3 REL) 1)
(<= (LIST-COUNT S5 REL0) 1)
(<= (LIST-COUNT S7 REL1) 1)
(<= (LIST-COUNT S9 REL2) 1)
(<= (LIST-COUNT S11 REL3) 1)
(<= (LIST-COUNT S13 REL4) 1)
(<= (LIST-COUNT S15 REL5) 1)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT REL6 S16)))
(NOT (NO-DUPLICATESP-EQUAL X))).
Subgoal *1.2.5.2.5.2.5.2.5/15
Subgoal *1.2.5.2.5.2.5.2.5/15'
Subgoal *1.2.5.2.5.2.5.2.5/15''
Subgoal *1.2.5.2.5.2.5.2.5/14
Subgoal *1.2.5.2.5.2.5.2.5/14'
Splitter note (see :DOC splitter) for Subgoal *1.2.5.2.5.2.5.2.5/14'
(2 subgoals).
if-intro: ((:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL))
Subgoal *1.2.5.2.5.2.5.2.5/14.2
Subgoal *1.2.5.2.5.2.5.2.5/14.1
Subgoal *1.2.5.2.5.2.5.2.5/14.1'
Subgoal *1.2.5.2.5.2.5.2.5/14.1''
Normally we would attempt to prove Subgoal *1.2.5.2.5.2.5.2.5/14.1''
by induction. However, that would cause the induction-depth-limit
of 9 to be exceeded. See :DOC induction-depth-limit.
Summary
Form: ( DEFTHM MEMBER-IF-OVER-1-MAP-LIST-COUNT-IS-DUPLICATED ...)
Rules: ((:DEFINITION ENDP)
(:DEFINITION MAP-LIST-COUNT)
(:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL)
(:DEFINITION NOT)
(:DEFINITION SUBSETP-EQUAL)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART MEMBER-IF-OVER-1)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION MAP-LIST-COUNT)
(:INDUCTION MEMBER-EQUAL)
(:INDUCTION NO-DUPLICATESP-EQUAL)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE NOT-NO-DUPLICATESP-LIST-COUNT)
(:TYPE-PRESCRIPTION LIST-COUNT)
(:TYPE-PRESCRIPTION MAP-LIST-COUNT)
(:TYPE-PRESCRIPTION MEMBER-EQUAL)
(:TYPE-PRESCRIPTION REMOVE-EQUAL))
Splitter rules (see :DOC splitter):
if-intro: ((:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL)
(:DEFINITION NOT))
Time: 1.36 seconds (prove: 1.34, print: 0.02, other: 0.00)
Prover steps counted: 270544
---
The key checkpoint goals, below, may help you to debug this failure.
See :DOC failure and see :DOC set-checkpoint-summary-limit.
---
*** Key checkpoint at the top level: ***
Goal
(IMPLIES
(AND (LET ((X S))
(MBE :LOGIC (PROG2$ (NO-DUPLICATESP-EQL-EXEC$GUARD-CHECK X)
(NO-DUPLICATESP-EQUAL X))
:EXEC (NO-DUPLICATESP-EQL-EXEC X)))
(LET ((Y S))
(MBE :LOGIC (PROG2$ (SUBSETP-EQL-EXEC$GUARD-CHECK X Y)
(SUBSETP-EQUAL X Y))
:EXEC (SUBSETP-EQL-EXEC X Y)))
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT X S)))
(NOT (LET NIL
(MBE :LOGIC (PROG2$ (NO-DUPLICATESP-EQL-EXEC$GUARD-CHECK X)
(NO-DUPLICATESP-EQUAL X))
:EXEC (NO-DUPLICATESP-EQL-EXEC X)))))
*** Key checkpoints under a top-level induction
before the induction-depth-limit stopped the proof attempt: ***
Subgoal *1/2.2
(IMPLIES (AND (CONSP S)
(NOT (SUBSETP-EQUAL (REMOVE-EQUAL (CAR S) X)
(CDR S)))
(NOT (MEMBER-EQUAL (CAR S) (CDR S)))
(NO-DUPLICATESP-EQUAL (CDR S))
(SUBSETP-EQUAL X S)
(<= (LIST-COUNT (CAR S) X) 1)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT (REMOVE-EQUAL (CAR S) X)
(CDR S))))
(NOT (NO-DUPLICATESP-EQUAL X)))
Subgoal *1/2.1
(IMPLIES (AND (CONSP S)
(NOT (NO-DUPLICATESP-EQUAL (REMOVE-EQUAL (CAR S) X)))
(NOT (MEMBER-EQUAL (CAR S) (CDR S)))
(NO-DUPLICATESP-EQUAL (CDR S))
(SUBSETP-EQUAL X S)
(<= (LIST-COUNT (CAR S) X) 1)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT (REMOVE-EQUAL (CAR S) X)
(CDR S))))
(NOT (NO-DUPLICATESP-EQUAL X)))
ACL2 Error in ( DEFTHM MEMBER-IF-OVER-1-MAP-LIST-COUNT-IS-DUPLICATED
...): See :DOC failure.
******** FAILED ********
期待どおり、 (car s) が x に複数ある場合の Subgoal は消えていますね。
Subgoal *1/2.1 についてですが、 (NOT (NO-DUPLICATESP-EQUAL (REMOVE-EQUAL (CAR S) X))) であれば、
(NOT (NO-DUPLICATESP-EQUAL X)) であるのってよく考えたら当然ですよね。
x から (car s) を取り除いた、すなわち x から要素が一つ以上減ったリストに重複があるわけなので、 x には必ず重複があります。
というわけで次の not-no-duplicatesp-remove を証明しましょう。
(defthm not-no-duplicatesp-remove
(implies (not (no-duplicatesp (remove e x)))
(not (no-duplicatesp x)))
:rule-classes ((:rewrite :match-free :all)))
証明失敗: 出力を確認する
Goal'
([ A key checkpoint:
Goal'
(IMPLIES (NOT (NO-DUPLICATESP-EQUAL (REMOVE-EQUAL E X)))
(NOT (NO-DUPLICATESP-EQUAL X)))
*1 (Goal') is pushed for proof by induction.
])
Perhaps we can prove *1 by induction. Two induction schemes are suggested
by this conjecture. These merge into one derived induction scheme.
We will induct according to a scheme suggested by (NO-DUPLICATESP-EQUAL X),
but modified to accommodate (REMOVE-EQUAL E X). These suggestions
were produced using the :induction rules NO-DUPLICATESP-EQUAL and
REMOVE-EQUAL. If we let (:P E X) denote *1 above then the induction
scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X))
(NOT (MEMBER-EQUAL (CAR X) (CDR X)))
(:P E (CDR X)))
(:P E X))
(IMPLIES (AND (NOT (ENDP X))
(MEMBER-EQUAL (CAR X) (CDR X)))
(:P E X))
(IMPLIES (ENDP X) (:P E X))).
This induction is justified by the same argument used to admit
NO-DUPLICATESP-EQUAL. When applied to the goal at hand the above induction
scheme produces four nontautological subgoals.
Subgoal *1/4
Subgoal *1/4'
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/3''
Subgoal *1/3'''
Subgoal *1/3'4'
Subgoal *1/3'5'
Subgoal *1/3'6'
([ A key checkpoint while proving *1 (descended from Goal'):
Subgoal *1/3'''
(IMPLIES (AND (CONSP X)
(NOT (MEMBER-EQUAL (CAR X) (CDR X)))
(NO-DUPLICATESP-EQUAL (REMOVE-EQUAL E (CDR X)))
(NOT (EQUAL E (CAR X)))
(MEMBER-EQUAL (CAR X)
(REMOVE-EQUAL E (CDR X))))
(NOT (NO-DUPLICATESP-EQUAL (CDR X))))
*1.1 (Subgoal *1/3'6') is pushed for proof by induction.
])
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/2''
Subgoal *1/1
Subgoal *1/1'
So we now return to *1.1, which is
(IMPLIES (AND (TRUE-LISTP REL)
(NOT (MEMBER-EQUAL X1 X2))
(NO-DUPLICATESP-EQUAL REL)
(NOT (EQUAL E X1))
(MEMBER-EQUAL X1 REL))
(NOT (NO-DUPLICATESP-EQUAL X2))).
Subgoal *1.1/5
Subgoal *1.1/5'
Subgoal *1.1/4
Subgoal *1.1/4'
Subgoal *1.1/3
Subgoal *1.1/2
Subgoal *1.1/2'
Subgoal *1.1/2''
Subgoal *1.1/2'''
Subgoal *1.1/2'4'
*1.1.1 (Subgoal *1.1/2'4') is pushed for proof by induction.
Subgoal *1.1/1
Subgoal *1.1/1'
So we now return to *1.1.1, which is
(IMPLIES (AND (TRUE-LISTP REL2)
(NOT (MEMBER-EQUAL REL1 X2))
(NOT (MEMBER-EQUAL REL1 REL2))
(NO-DUPLICATESP-EQUAL REL2)
(NOT (EQUAL E REL1)))
(NOT (NO-DUPLICATESP-EQUAL X2))).
Subgoal *1.1.1/5
Subgoal *1.1.1/5'
Subgoal *1.1.1/4
Subgoal *1.1.1/4'
Subgoal *1.1.1/3
Subgoal *1.1.1/2
Subgoal *1.1.1/2'
Subgoal *1.1.1/1
Subgoal *1.1.1/1'
Subgoal *1.1.1/1''
Subgoal *1.1.1/1'''
*1.1.1.1 (Subgoal *1.1.1/1''') is pushed for proof by induction.
So we now return to *1.1.1.1, which is
(IMPLIES (AND (NOT (MEMBER-EQUAL REL1 X2))
(NOT (EQUAL E REL1)))
(NOT (NO-DUPLICATESP-EQUAL X2))).
Subgoal *1.1.1.1/4
Subgoal *1.1.1.1/4'
Subgoal *1.1.1.1/3
Subgoal *1.1.1.1/3'
Subgoal *1.1.1.1/2
Subgoal *1.1.1.1/2'
Subgoal *1.1.1.1/1
Subgoal *1.1.1.1/1'
Subgoal *1.1.1.1/1''
Subgoal *1.1.1.1/1'''
A goal of NIL, Subgoal *1.1.1.1/1''', has been generated! Obviously,
the proof attempt has failed.
Summary
Form: ( DEFTHM NOT-NO-DUPLICATESP-REMOVE ...)
Rules: ((:DEFINITION ENDP)
(:DEFINITION MEMBER-EQUAL)
(:DEFINITION NO-DUPLICATESP-EQL-EXEC$GUARD-CHECK)
(:DEFINITION NO-DUPLICATESP-EQUAL)
(:DEFINITION NOT)
(:DEFINITION REMOVE-EQL-EXEC$GUARD-CHECK)
(:DEFINITION REMOVE-EQUAL)
(:DEFINITION RETURN-LAST)
(:DEFINITION TRUE-LISTP)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART NO-DUPLICATESP-EQUAL)
(:EXECUTABLE-COUNTERPART NOT)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION MEMBER-EQUAL)
(:INDUCTION NO-DUPLICATESP-EQUAL)
(:INDUCTION REMOVE-EQUAL)
(:INDUCTION TRUE-LISTP)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:TYPE-PRESCRIPTION MEMBER-EQUAL)
(:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL)
(:TYPE-PRESCRIPTION REMOVE-EQUAL))
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted: 5254
---
The key checkpoint goals, below, may help you to debug this failure.
See :DOC failure and see :DOC set-checkpoint-summary-limit.
---
*** Key checkpoint at the top level: ***
Goal'
(IMPLIES (NOT (NO-DUPLICATESP-EQUAL (REMOVE-EQUAL E X)))
(NOT (NO-DUPLICATESP-EQUAL X)))
*** Key checkpoint under a top-level induction
before generating a goal of NIL (see :DOC nil-goal): ***
Subgoal *1/3'''
(IMPLIES (AND (CONSP X)
(NOT (MEMBER-EQUAL (CAR X) (CDR X)))
(NO-DUPLICATESP-EQUAL (REMOVE-EQUAL E (CDR X)))
(NOT (EQUAL E (CAR X)))
(MEMBER-EQUAL (CAR X)
(REMOVE-EQUAL E (CDR X))))
(NOT (NO-DUPLICATESP-EQUAL (CDR X))))
ACL2 Error in ( DEFTHM NOT-NO-DUPLICATESP-REMOVE ...): See :DOC failure.
******** FAILED ********
Subgoal *1/3''' の仮定に (NOT (EQUAL E (CAR X))) と (MEMBER-EQUAL (CAR X) (REMOVE-EQUAL E (CDR X))) があるのが気になりますね。
E と (CAR X) は異なるのですから、 (member (car x) (remove e (cdr x))) は、
(member (car x) (cdr x)) と真偽が一致するはずです。
これには member-remove という名前をつけて証明しましょう。
(defthm member-remove
(implies (not (equal x y))
(iff (member x (remove y z))
(member x z))))
証明成功: 出力を確認する
Goal'
Subgoal 2
([ A key checkpoint:
Subgoal 2
(IMPLIES (AND (NOT (EQUAL X Y))
(NOT (MEMBER-EQUAL X (REMOVE-EQUAL Y Z))))
(NOT (MEMBER-EQUAL X Z)))
*1 (Subgoal 2) is pushed for proof by induction.
])
Subgoal 1
([ A key checkpoint:
Subgoal 1
(IMPLIES (AND (NOT (EQUAL X Y))
(MEMBER-EQUAL X (REMOVE-EQUAL Y Z)))
(MEMBER-EQUAL X Z))
Normally we would attempt to prove Subgoal 1 by induction. However,
we prefer in this instance to focus on the original input conjecture
rather than this simplified special case. We therefore abandon our
previous work on this conjecture and reassign the name *1 to the original
conjecture. (See :DOC otf-flg.)
])
Perhaps we can prove *1 by induction. Two induction schemes are suggested
by this conjecture. These merge into one derived induction scheme.
We will induct according to a scheme suggested by (MEMBER-EQUAL X Z),
but modified to accommodate (REMOVE-EQUAL Y Z). These suggestions
were produced using the :induction rules MEMBER-EQUAL and REMOVE-EQUAL.
If we let (:P X Y Z) denote *1 above then the induction scheme we'll
use is
(AND (IMPLIES (AND (NOT (ENDP Z))
(NOT (EQUAL X (CAR Z)))
(:P X Y (CDR Z)))
(:P X Y Z))
(IMPLIES (AND (NOT (ENDP Z)) (EQUAL X (CAR Z)))
(:P X Y Z))
(IMPLIES (ENDP Z) (:P X Y Z))).
This induction is justified by the same argument used to admit MEMBER-EQUAL.
When applied to the goal at hand the above induction scheme produces
three nontautological subgoals.
Subgoal *1/3
Subgoal *1/3'
Splitter note (see :DOC splitter) for Subgoal *1/3' (2 subgoals).
if-intro: ((:DEFINITION REMOVE-EQUAL))
Subgoal *1/3.2
Subgoal *1/3.1
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/1
Subgoal *1/1'
*1 is COMPLETED!
Thus key checkpoint Goal is COMPLETED!
Q.E.D.
Summary
Form: ( DEFTHM MEMBER-REMOVE ...)
Rules: ((:DEFINITION ENDP)
(:DEFINITION IFF)
(:DEFINITION MEMBER-EQUAL)
(:DEFINITION NOT)
(:DEFINITION REMOVE-EQUAL)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART NOT)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION MEMBER-EQUAL)
(:INDUCTION REMOVE-EQUAL)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:TYPE-PRESCRIPTION MEMBER-EQUAL)
(:TYPE-PRESCRIPTION REMOVE-EQUAL))
Splitter rules (see :DOC splitter):
if-intro: ((:DEFINITION REMOVE-EQUAL))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 1487
MEMBER-REMOVE
ところで定理に iff を使っていますが、これは数学的には (and (implies x y) (implies y x)) と同じです。しかし ACL2 的には同じではありません。
どういうことかというと (iff x y) の場合は仮定部に x が出てきたときに y に書き換えてくれるんです。
implies の場合は書き変えてくれません。詳しくは ACL2 のチュートリアルを読んでください。
もう一つ、何故 (equal (member x (remove y z)) (member x z)) じゃないのかという当然の疑問が湧くかもしれません。
これは Lisper なら知っていることかと思いますが、
(member x z) の結果は t or nil ではありません。
(member x z) の結果は x が見つかった時点の z の部分リストを返します。
もしも何も見つからなかったら nil を返すという仕様です。
こういう述語として使えるけど真のときに t を返すわけではない関数のことを準述語と呼ぶのですが、
準述語で真偽が等しいということを調べるには equal ではなくて iff を使います(なお、ACL2 や Common Lisp において真とは nil 以外の値のことを意味します)。
真偽だけでなく値も一致するのであれば equal でよいです。
それでは再度 not-no-duplicatesp-remove を証明しましょう。
(defthm not-no-duplicatesp-remove
(implies (not (no-duplicatesp (remove e x)))
(not (no-duplicatesp x)))
:rule-classes ((:rewrite :match-free :all)))
証明成功: 出力を確認する
Goal'
([ A key checkpoint:
Goal'
(IMPLIES (NOT (NO-DUPLICATESP-EQUAL (REMOVE-EQUAL E X)))
(NOT (NO-DUPLICATESP-EQUAL X)))
*1 (Goal') is pushed for proof by induction.
])
Perhaps we can prove *1 by induction. Two induction schemes are suggested
by this conjecture. These merge into one derived induction scheme.
We will induct according to a scheme suggested by (NO-DUPLICATESP-EQUAL X),
but modified to accommodate (REMOVE-EQUAL E X). These suggestions
were produced using the :induction rules NO-DUPLICATESP-EQUAL and
REMOVE-EQUAL. If we let (:P E X) denote *1 above then the induction
scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X))
(NOT (MEMBER-EQUAL (CAR X) (CDR X)))
(:P E (CDR X)))
(:P E X))
(IMPLIES (AND (NOT (ENDP X))
(MEMBER-EQUAL (CAR X) (CDR X)))
(:P E X))
(IMPLIES (ENDP X) (:P E X))).
This induction is justified by the same argument used to admit
NO-DUPLICATESP-EQUAL. When applied to the goal at hand the above induction
scheme produces four nontautological subgoals.
Subgoal *1/4
Subgoal *1/4'
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/3''
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/2''
Subgoal *1/1
Subgoal *1/1'
*1 is COMPLETED!
Thus key checkpoint Goal' is COMPLETED!
Q.E.D.
Summary
Form: ( DEFTHM NOT-NO-DUPLICATESP-REMOVE ...)
Rules: ((:DEFINITION ENDP)
(:DEFINITION NO-DUPLICATESP-EQL-EXEC$GUARD-CHECK)
(:DEFINITION NO-DUPLICATESP-EQUAL)
(:DEFINITION NOT)
(:DEFINITION REMOVE-EQL-EXEC$GUARD-CHECK)
(:DEFINITION REMOVE-EQUAL)
(:DEFINITION RETURN-LAST)
(:EXECUTABLE-COUNTERPART NO-DUPLICATESP-EQUAL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION NO-DUPLICATESP-EQUAL)
(:INDUCTION REMOVE-EQUAL)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE MEMBER-REMOVE)
(:TYPE-PRESCRIPTION MEMBER-EQUAL)
(:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL)
(:TYPE-PRESCRIPTION REMOVE-EQUAL))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 1174
NOT-NO-DUPLICATESP-REMOVE
やりました！証明成功です。
では再度 member-if-over-1-map-list-count-is-duplicated の証明を試みましょう。
(defthm member-if-over-1-map-list-count-is-duplicated
(implies (and (no-duplicatesp s)
(subsetp x s)
(member-if-over-1 (map-list-count x s)))
(not (no-duplicatesp x)))
:hints (("Goal" :induct (map-list-count x s)))
:rule-classes ((:rewrite :match-free :all)))
証明失敗: 出力を確認する
*1 (the initial Goal, a key checkpoint) is pushed for proof by induction.
We have been told to use induction. One induction scheme is suggested
by the induction hint.
We will induct according to a scheme suggested by (MAP-LIST-COUNT X S).
This suggestion was produced using the :induction rule MAP-LIST-COUNT.
If we let (:P S X) denote *1 above then the induction scheme we'll
use is
(AND (IMPLIES (AND (NOT (ENDP S))
(:P (CDR S) (REMOVE-EQUAL (CAR S) X)))
(:P S X))
(IMPLIES (ENDP S) (:P S X))).
This induction is justified by the same argument used to admit
MAP-LIST-COUNT. Note, however, that the unmeasured variable X is being
instantiated. When applied to the goal at hand the above induction
scheme produces two nontautological subgoals.
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/2''
Subgoal *1/2'''
Subgoal *1/2'4'
Subgoal *1/2'5'
([ A key checkpoint while proving *1 (descended from Goal):
Subgoal *1/2''
(IMPLIES (AND (CONSP S)
(NOT (SUBSETP-EQUAL (REMOVE-EQUAL (CAR S) X)
(CDR S)))
(NOT (MEMBER-EQUAL (CAR S) (CDR S)))
(NO-DUPLICATESP-EQUAL (CDR S))
(SUBSETP-EQUAL X S)
(<= (LIST-COUNT (CAR S) X) 1)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT (REMOVE-EQUAL (CAR S) X)
(CDR S))))
(NOT (NO-DUPLICATESP-EQUAL X)))
*1.1 (Subgoal *1/2'5') is pushed for proof by induction.
])
Subgoal *1/1
Subgoal *1/1'
So we now return to *1.1, which is
(IMPLIES (AND (TRUE-LISTP REL)
(NOT (SUBSETP-EQUAL REL S2))
(NOT (MEMBER-EQUAL S1 S2))
(NO-DUPLICATESP-EQUAL S2)
(SUBSETP-EQUAL X (CONS S1 S2))
(<= (LIST-COUNT S1 X) 1)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT REL S2)))
(NOT (NO-DUPLICATESP-EQUAL X))).
Subgoal *1.1/5
Subgoal *1.1/5'
Subgoal *1.1/4
Subgoal *1.1/4'
Subgoal *1.1/3
Subgoal *1.1/3'
Subgoal *1.1/2
Subgoal *1.1/2'
Subgoal *1.1/2''
Subgoal *1.1/1
Subgoal *1.1/1'
Subgoal *1.1/1''
Subgoal *1.1/1'''
*1.1.1 (Subgoal *1.1/1''') is pushed for proof by induction.
So we now return to *1.1.1, which is
(IMPLIES (AND (TRUE-LISTP REL)
(NOT (SUBSETP-EQUAL REL S2))
(NOT (MEMBER-EQUAL S1 S2))
(NO-DUPLICATESP-EQUAL S2))
(NOT (MEMBER-IF-OVER-1 (MAP-LIST-COUNT REL S2)))).
Subgoal *1.1.1/5
Subgoal *1.1.1/5'
Subgoal *1.1.1/5''
Subgoal *1.1.1/5'''
Subgoal *1.1.1/5'4'
*1.1.1.1 (Subgoal *1.1.1/5'4') is pushed for proof by induction.
Subgoal *1.1.1/4
Subgoal *1.1.1/4'
Subgoal *1.1.1/4''
Subgoal *1.1.1/4'''
Subgoal *1.1.1/4'4'
*1.1.1.2 (Subgoal *1.1.1/4'4') is pushed for proof by induction.
Subgoal *1.1.1/3
Subgoal *1.1.1/3'
Subgoal *1.1.1/2
Subgoal *1.1.1/1
Subgoal *1.1.1/1'
So we now return to *1.1.1.2, which is
(IMPLIES (AND (MEMBER-EQUAL REL1 S2)
(NOT (MEMBER-IF-OVER-1 (MAP-LIST-COUNT REL2 S2)))
(TRUE-LISTP REL2)
(NOT (SUBSETP-EQUAL REL2 S2))
(NOT (MEMBER-EQUAL S1 S2))
(NO-DUPLICATESP-EQUAL S2))
(NOT (MEMBER-IF-OVER-1 (MAP-LIST-COUNT (CONS REL1 REL2) S2)))).
Subgoal *1.1.1.2/6
Subgoal *1.1.1.2/6'
Subgoal *1.1.1.2/6''
Subgoal *1.1.1.2/6'''
Subgoal *1.1.1.2/6'4'
*1.1.1.2.1 (Subgoal *1.1.1.2/6'4') is pushed for proof by induction.
Subgoal *1.1.1.2/5
Subgoal *1.1.1.2/5'
Subgoal *1.1.1.2/5''
Subgoal *1.1.1.2/5'''
Subgoal *1.1.1.2/5'4'
*1.1.1.2.2 (Subgoal *1.1.1.2/5'4') is pushed for proof by induction.
Subgoal *1.1.1.2/4
Subgoal *1.1.1.2/4'
Subgoal *1.1.1.2/3
Subgoal *1.1.1.2/2
Subgoal *1.1.1.2/2'
Subgoal *1.1.1.2/2''
Subgoal *1.1.1.2/2'''
Subgoal *1.1.1.2/2'4'
*1.1.1.2.3 (Subgoal *1.1.1.2/2'4') is pushed for proof by induction.
Subgoal *1.1.1.2/1
Subgoal *1.1.1.2/1'
So we now return to *1.1.1.2.3, which is
(IMPLIES (AND (MEMBER-EQUAL REL3 S2)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT REL4 S2))
(MEMBER-EQUAL REL1 S2)
(NOT (MEMBER-IF-OVER-1 (MAP-LIST-COUNT (CONS REL3 REL4) S2)))
(TRUE-LISTP REL4)
(NOT (SUBSETP-EQUAL REL4 S2))
(NOT (MEMBER-EQUAL S1 S2))
(NO-DUPLICATESP-EQUAL S2))
(NOT (MEMBER-IF-OVER-1 (MAP-LIST-COUNT (LIST* REL1 REL3 REL4)
S2)))).
The formula above is subsumed by one of its parents, *1.1.1, which
we're in the process of trying to prove by induction. When an inductive
proof pushes a subgoal for induction that is less general than the
original goal, it may be a sign that either an inappropriate induction
was chosen or that the original goal is insufficiently general. In
any case, our proof attempt has failed.
Summary
Form: ( DEFTHM MEMBER-IF-OVER-1-MAP-LIST-COUNT-IS-DUPLICATED ...)
Rules: ((:DEFINITION ENDP)
(:DEFINITION LIST-COUNT)
(:DEFINITION MAP-LIST-COUNT)
(:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL)
(:DEFINITION NOT)
(:DEFINITION SUBSETP-EQUAL)
(:DEFINITION TRUE-LISTP)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART <)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART MEMBER-IF-OVER-1)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION LIST-COUNT)
(:INDUCTION MAP-LIST-COUNT)
(:INDUCTION NO-DUPLICATESP-EQUAL)
(:INDUCTION SUBSETP-EQUAL)
(:INDUCTION TRUE-LISTP)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE NOT-NO-DUPLICATESP-LIST-COUNT)
(:REWRITE NOT-NO-DUPLICATESP-REMOVE)
(:TYPE-PRESCRIPTION LIST-COUNT)
(:TYPE-PRESCRIPTION MAP-LIST-COUNT)
(:TYPE-PRESCRIPTION MEMBER-EQUAL)
(:TYPE-PRESCRIPTION REMOVE-EQUAL)
(:TYPE-PRESCRIPTION SUBSETP-EQUAL))
Time: 0.04 seconds (prove: 0.04, print: 0.00, other: 0.00)
Prover steps counted: 26426
---
The key checkpoint goals, below, may help you to debug this failure.
See :DOC failure and see :DOC set-checkpoint-summary-limit.
---
*** Key checkpoint at the top level: ***
Goal
(IMPLIES
(AND (LET ((X S))
(MBE :LOGIC (PROG2$ (NO-DUPLICATESP-EQL-EXEC$GUARD-CHECK X)
(NO-DUPLICATESP-EQUAL X))
:EXEC (NO-DUPLICATESP-EQL-EXEC X)))
(LET ((Y S))
(MBE :LOGIC (PROG2$ (SUBSETP-EQL-EXEC$GUARD-CHECK X Y)
(SUBSETP-EQUAL X Y))
:EXEC (SUBSETP-EQL-EXEC X Y)))
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT X S)))
(NOT (LET NIL
(MBE :LOGIC (PROG2$ (NO-DUPLICATESP-EQL-EXEC$GUARD-CHECK X)
(NO-DUPLICATESP-EQUAL X))
:EXEC (NO-DUPLICATESP-EQL-EXEC X)))))
*** Key checkpoint under a top-level induction: ***
Subgoal *1/2''
(IMPLIES (AND (CONSP S)
(NOT (SUBSETP-EQUAL (REMOVE-EQUAL (CAR S) X)
(CDR S)))
(NOT (MEMBER-EQUAL (CAR S) (CDR S)))
(NO-DUPLICATESP-EQUAL (CDR S))
(SUBSETP-EQUAL X S)
(<= (LIST-COUNT (CAR S) X) 1)
(MEMBER-IF-OVER-1 (MAP-LIST-COUNT (REMOVE-EQUAL (CAR S) X)
(CDR S))))
(NOT (NO-DUPLICATESP-EQUAL X)))
ACL2 Error in ( DEFTHM MEMBER-IF-OVER-1-MAP-LIST-COUNT-IS-DUPLICATED
...): See :DOC failure.
******** FAILED ********
失敗しましたが、失敗するまでにかかる時間は短かくなりました。
Subgoal *1/2'' ですが、仮定の (NOT (SUBSETP-EQUAL (REMOVE-EQUAL (CAR S) X) (CDR S))) と (SUBSETP-EQUAL X S) の2つが気になりますね。
もしも、 (NOT (SUBSETP-EQUAL (REMOVE-EQUAL (CAR S) X) (CDR S))) が真であるとしたら、
(SUBSETP-EQUAL X S) が真であるはずがありません。
x から (car s) を除いたリストが (cdr s) の部分集合ではないのだとしたら、
(subsetp x s) は確実に偽です。これは (subsetp x s) を (subsetp x (cons (car s) (cdr s)))
と書きかえてみるとより明確になると思います。 (car s) を除いた x が (cdr s) の部分集合でないわけですから、 (subsetp x (cons (car s) (cdr s))) は偽です。
よって、 (NOT (SUBSETP-EQUAL (REMOVE-EQUAL (CAR S) X) (CDR S))) と (SUBSETP-EQUAL X S) が両立することはありえず矛盾しています。
仮定に矛盾があると分かったため Subgoal *1/2'' は真です。
ということで (not (subsetp (remove e x) s)) のとき (not (subsetp x (cons e s))) であることを証明すればよさそうです。
(subsetp (remove e x) s) と (subsetp x (cons e s) の関係についてもう少し深く考えてみましょう。 (subsetp (remove e x) s) は x から e 除去を除去したときに s の部分集合だといっています。 (subsetp x (cons e s)) は x は s に e という要素を追加した集合の部分集合だといっています。
これって、結局同じことをいっていませんか？ x が e という要素を含む場合と含まない場合について考えてみてください。
(subsetp x (cons e s)) も (subsetp (remove e x) s) も x に e が入っているかどうかで結果が変わりません。
であれば、そもそも (subsetp (remove e x) s) は (subsetp x (cons e s)) と同値だといえそうです。
これを subsetp-remove-cons という名前の定理として証明しましょう。
remove が再帰関数なのに対して cons は非再帰の関数なので remove を cons に書き換えるルールは強力です。
(defthm subsetp-remove-cons
(equal (subsetp (remove e x) s)
(subsetp x (cons e s))))
証明成功: 出力を確認する
Goal'
([ A key checkpoint:
Goal'
(EQUAL (SUBSETP-EQUAL (REMOVE-EQUAL E X) S)
(SUBSETP-EQUAL X (CONS E S)))
*1 (Goal') is pushed for proof by induction.
])
Perhaps we can prove *1 by induction. Two induction schemes are suggested
by this conjecture. These merge into one derived induction scheme.
We will induct according to a scheme suggested by
(SUBSETP-EQUAL X (CONS E S)), but modified to accommodate (REMOVE-EQUAL E X).
These suggestions were produced using the :induction rules REMOVE-EQUAL
and SUBSETP-EQUAL. If we let (:P E S X) denote *1 above then the induction
scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X))
(NOT (MEMBER-EQUAL (CAR X) (CONS E S))))
(:P E S X))
(IMPLIES (AND (NOT (ENDP X))
(MEMBER-EQUAL (CAR X) (CONS E S))
(:P E S (CDR X)))
(:P E S X))
(IMPLIES (ENDP X) (:P E S X))).
This induction is justified by the same argument used to admit SUBSETP-EQUAL.
When applied to the goal at hand the above induction scheme produces
three nontautological subgoals.
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/1
Subgoal *1/1'
*1 is COMPLETED!
Thus key checkpoint Goal' is COMPLETED!
Q.E.D.
Summary
Form: ( DEFTHM SUBSETP-REMOVE-CONS ...)
Rules: ((:DEFINITION ENDP)
(:DEFINITION MEMBER-EQUAL)
(:DEFINITION NOT)
(:DEFINITION REMOVE-EQL-EXEC$GUARD-CHECK)
(:DEFINITION REMOVE-EQUAL)
(:DEFINITION RETURN-LAST)
(:DEFINITION SUBSETP-EQL-EXEC$GUARD-CHECK)
(:DEFINITION SUBSETP-EQUAL)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION REMOVE-EQUAL)
(:INDUCTION SUBSETP-EQUAL)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:TYPE-PRESCRIPTION MEMBER-EQUAL)
(:TYPE-PRESCRIPTION REMOVE-EQUAL))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 954
SUBSETP-REMOVE-CONS
証明に成功しましたね。
それでは member-if-over-1-map-list-count-is-duplicated の証明を試みてみましょう。
(defthm member-if-over-1-map-list-count-is-duplicated
(implies (and (no-duplicatesp s)
(subsetp x s)
(member-if-over-1 (map-list-count x s)))
(not (no-duplicatesp x)))
:hints (("Goal" :induct (map-list-count x s)))
:rule-classes ((:rewrite :match-free :all)))
証明成功: 出力を確認する
*1 (the initial Goal, a key checkpoint) is pushed for proof by induction.
We have been told to use induction. One induction scheme is suggested
by the induction hint.
We will induct according to a scheme suggested by (MAP-LIST-COUNT X S).
This suggestion was produced using the :induction rule MAP-LIST-COUNT.
If we let (:P S X) denote *1 above then the induction scheme we'll
use is
(AND (IMPLIES (AND (NOT (ENDP S))
(:P (CDR S) (REMOVE-EQUAL (CAR S) X)))
(:P S X))
(IMPLIES (ENDP S) (:P S X))).
This induction is justified by the same argument used to admit
MAP-LIST-COUNT. Note, however, that the unmeasured variable X is being
instantiated. When applied to the goal at hand the above induction
scheme produces two nontautological subgoals.
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/1
Subgoal *1/1'
*1 is COMPLETED!
Thus key checkpoint Goal is COMPLETED!
Q.E.D.
Summary
Form: ( DEFTHM MEMBER-IF-OVER-1-MAP-LIST-COUNT-IS-DUPLICATED ...)
Rules: ((:DEFINITION ENDP)
(:DEFINITION MAP-LIST-COUNT)
(:DEFINITION MEMBER-EQUAL)
(:DEFINITION MEMBER-IF-OVER-1)
(:DEFINITION NO-DUPLICATESP-EQUAL)
(:DEFINITION NOT)
(:DEFINITION SUBSETP-EQUAL)
(:EXECUTABLE-COUNTERPART MEMBER-IF-OVER-1)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION MAP-LIST-COUNT)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE CONS-CAR-CDR)
(:REWRITE NOT-NO-DUPLICATESP-LIST-COUNT)
(:REWRITE NOT-NO-DUPLICATESP-REMOVE)
(:REWRITE SUBSETP-REMOVE-CONS)
(:TYPE-PRESCRIPTION LIST-COUNT)
(:TYPE-PRESCRIPTION MAP-LIST-COUNT)
(:TYPE-PRESCRIPTION SUBSETP-EQUAL))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 1242
MEMBER-IF-OVER-1-MAP-LIST-COUNT-IS-DUPLICATED
証明成功です！これで pigeonhole の証明に一歩近づきました！
7.2. map-list-count の長さと総和に関する定理
再度 pigeonhole と numeric-pigeonhole の定理を再掲します。
(defthm pigeonhole
(implies (and (subsetp x s)
(< (len s) (len x))
(no-duplicatesp s))
(not (no-duplicatesp x)))
:rule-classes ((:rewrite :match-free :all)))
(defthm numeric-pigeonhole
(implies (< (len x) (sum x))
(member-if-over-1 x)))
numeric-pigeonhole では (< (len x) (sum x)) を仮定しているため、
(map-list-count x s) の長さと総和に関する定理が必要です。
まずは、 (map-list-count x s) の長さが (len s) と一致することを証明しましょう。
(defthm len-map-list-count
(equal (len (map-list-count x s))
(len s)))
証明成功: 出力を確認する
*1 (the initial Goal, a key checkpoint) is pushed for proof by induction.
Perhaps we can prove *1 by induction. Two induction schemes are suggested
by this conjecture. These merge into one derived induction scheme.
We will induct according to a scheme suggested by (LEN S), but modified
to accommodate (MAP-LIST-COUNT X S). These suggestions were produced
using the :induction rules LEN and MAP-LIST-COUNT. If we let (:P S X)
denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP S)) (:P S X))
(IMPLIES (AND (CONSP S)
(:P (CDR S) (REMOVE-EQUAL (CAR S) X)))
(:P S X))).
This induction is justified by the same argument used to admit LEN.
Note, however, that the unmeasured variable X is being instantiated.
When applied to the goal at hand the above induction scheme produces
two nontautological subgoals.
Subgoal *1/2
Subgoal *1/1
*1 is COMPLETED!
Thus key checkpoint Goal is COMPLETED!
Q.E.D.
Summary
Form: ( DEFTHM LEN-MAP-LIST-COUNT ...)
Rules: ((:DEFINITION LEN)
(:DEFINITION MAP-LIST-COUNT)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART LEN)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION LEN)
(:INDUCTION MAP-LIST-COUNT)
(:REWRITE CDR-CONS)
(:TYPE-PRESCRIPTION MAP-LIST-COUNT))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 314
LEN-MAP-LIST-COUNT
では (map-count-list x s) の総和が鳩の総数である (len x) と同じになることを示します。
(map-list-count s) の総和が鳩の総数になるためには、=x= が s の部分集合であるという条件が必要です。
(defthm sum-map-count-list
(implies (subsetp x s)
(equal (sum (map-list-count x s))
(len x))))
証明失敗: 出力を確認する
Goal'
([ A key checkpoint:
Goal'
(IMPLIES (SUBSETP-EQUAL X S)
(EQUAL (SUM (MAP-LIST-COUNT X S))
(LEN X)))
*1 (Goal') is pushed for proof by induction.
])
Perhaps we can prove *1 by induction. Three induction schemes are
suggested by this conjecture. These merge into two derived induction
schemes. However, one of these is flawed and so we are left with one
viable candidate.
We will induct according to a scheme suggested by (LEN X), but modified
to accommodate (SUBSETP-EQUAL X S). These suggestions were produced
using the :induction rules LEN and SUBSETP-EQUAL. If we let (:P S X)
denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP X)) (:P S X))
(IMPLIES (AND (CONSP X) (:P S (CDR X)))
(:P S X))).
This induction is justified by the same argument used to admit LEN.
When applied to the goal at hand the above induction scheme produces
three nontautological subgoals.
Subgoal *1/3
Subgoal *1/3'
([ A key checkpoint while proving *1 (descended from Goal'):
Subgoal *1/3'
(IMPLIES (NOT (CONSP X))
(EQUAL (SUM (MAP-LIST-COUNT X S)) 0))
*1.1 (Subgoal *1/3') is pushed for proof by induction.
])
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/2''
Subgoal *1/2'''
Subgoal *1/2'4'
([ A key checkpoint while proving *1 (descended from Goal'):
Subgoal *1/2'
(IMPLIES (AND (CONSP X)
(EQUAL (SUM (MAP-LIST-COUNT (CDR X) S))
(LEN (CDR X)))
(MEMBER-EQUAL (CAR X) S)
(SUBSETP-EQUAL (CDR X) S))
(EQUAL (SUM (MAP-LIST-COUNT X S))
(+ 1 (LEN (CDR X)))))
*1.2 (Subgoal *1/2'4') is pushed for proof by induction.
])
Subgoal *1/1
So we now return to *1.2, which is
(IMPLIES (AND (MEMBER-EQUAL X1 S)
(SUBSETP-EQUAL X2 S))
(EQUAL (SUM (MAP-LIST-COUNT (CONS X1 X2) S))
(+ 1 (SUM (MAP-LIST-COUNT X2 S))))).
Subgoal *1.2/4
Subgoal *1.2/4'
Subgoal *1.2/3
Subgoal *1.2/3'
Subgoal *1.2/3''
Subgoal *1.2/3'''
Subgoal *1.2/3'4'
*1.2.1 (Subgoal *1.2/3'4') is pushed for proof by induction.
Subgoal *1.2/2
Subgoal *1.2/2'
Subgoal *1.2/1
Subgoal *1.2/1'
Subgoal *1.2/1''
*1.2.2 (Subgoal *1.2/1'') is pushed for proof by induction.
So we now return to *1.2.2, which is
(IMPLIES (AND (NOT (CONSP X2))
(MEMBER-EQUAL X1 S))
(EQUAL (SUM (MAP-LIST-COUNT (CONS X1 X2) S))
(+ 1 (SUM (MAP-LIST-COUNT X2 S))))).
Subgoal *1.2.2/4
Subgoal *1.2.2/4'
Splitter note (see :DOC splitter) for Subgoal *1.2.2/4' (3 subgoals).
if-intro: ((:DEFINITION LIST-COUNT)
(:DEFINITION MAP-LIST-COUNT)
(:DEFINITION MEMBER-EQUAL)
(:DEFINITION REMOVE-EQUAL)
(:DEFINITION SUM))
Subgoal *1.2.2/4.3
Subgoal *1.2.2/4.2
Subgoal *1.2.2/4.1
Subgoal *1.2.2/4.1'
Subgoal *1.2.2/3
Subgoal *1.2.2/3'
Subgoal *1.2.2/3''
Subgoal *1.2.2/2
Subgoal *1.2.2/2'
Subgoal *1.2.2/1
Subgoal *1.2.2/1'
*1.2.2 is COMPLETED!
We therefore turn our attention to *1.2.1, which is
(IMPLIES (AND (MEMBER-EQUAL X3 S)
(EQUAL (SUM (MAP-LIST-COUNT (CONS X1 X4) S))
(+ 1 (SUM (MAP-LIST-COUNT X4 S))))
(MEMBER-EQUAL X1 S)
(SUBSETP-EQUAL X4 S))
(EQUAL (SUM (MAP-LIST-COUNT (LIST* X1 X3 X4) S))
(+ 1
(SUM (MAP-LIST-COUNT (CONS X3 X4) S))))).
Subgoal *1.2.1/5
Subgoal *1.2.1/5'
Subgoal *1.2.1/4
Subgoal *1.2.1/4'
Subgoal *1.2.1/4''
Subgoal *1.2.1/4'''
Subgoal *1.2.1/4'4'
*1.2.1.1 (Subgoal *1.2.1/4'4') is pushed for proof by induction.
Subgoal *1.2.1/3
Subgoal *1.2.1/3'
Subgoal *1.2.1/2
Subgoal *1.2.1/2'
Subgoal *1.2.1/2''
Subgoal *1.2.1/2'''
Subgoal *1.2.1/2'4'
*1.2.1.2 (Subgoal *1.2.1/2'4') is pushed for proof by induction.
Subgoal *1.2.1/1
Subgoal *1.2.1/1'
Subgoal *1.2.1/1''
*1.2.1.3 (Subgoal *1.2.1/1'') is pushed for proof by induction.
So we now return to *1.2.1.3, which is
(IMPLIES (AND (NOT (CONSP X4))
(MEMBER-EQUAL X3 S)
(EQUAL (SUM (MAP-LIST-COUNT (CONS X1 X4) S))
(+ 1 (SUM (MAP-LIST-COUNT X4 S))))
(MEMBER-EQUAL X1 S))
(EQUAL (SUM (MAP-LIST-COUNT (LIST* X1 X3 X4) S))
(+ 1
(SUM (MAP-LIST-COUNT (CONS X3 X4) S))))).
Subgoal *1.2.1.3/7
Subgoal *1.2.1.3/7'
Splitter note (see :DOC splitter) for Subgoal *1.2.1.3/7' (3 subgoals).
if-intro: ((:DEFINITION LIST-COUNT)
(:DEFINITION MAP-LIST-COUNT)
(:DEFINITION MEMBER-EQUAL)
(:DEFINITION REMOVE-EQUAL)
(:DEFINITION SUM))
Subgoal *1.2.1.3/7.3
Subgoal *1.2.1.3/7.2
Subgoal *1.2.1.3/7.1
Subgoal *1.2.1.3/7.1'
Subgoal *1.2.1.3/6
Subgoal *1.2.1.3/6'
Subgoal *1.2.1.3/5
Subgoal *1.2.1.3/5'
Splitter note (see :DOC splitter) for Subgoal *1.2.1.3/5' (3 subgoals).
if-intro: ((:DEFINITION LIST-COUNT)
(:DEFINITION MAP-LIST-COUNT)
(:DEFINITION MEMBER-EQUAL)
(:DEFINITION REMOVE-EQUAL)
(:DEFINITION SUM))
Subgoal *1.2.1.3/5.3
Subgoal *1.2.1.3/5.2
Subgoal *1.2.1.3/5.1
Subgoal *1.2.1.3/5.1'
Subgoal *1.2.1.3/4
Subgoal *1.2.1.3/4'
Subgoal *1.2.1.3/4''
Subgoal *1.2.1.3/3
Subgoal *1.2.1.3/3'
Subgoal *1.2.1.3/2
Subgoal *1.2.1.3/2'
Splitter note (see :DOC splitter) for Subgoal *1.2.1.3/2' (3 subgoals).
if-intro: ((:DEFINITION LIST-COUNT)
(:DEFINITION MAP-LIST-COUNT)
(:DEFINITION MEMBER-EQUAL)
(:DEFINITION REMOVE-EQUAL)
(:DEFINITION SUM))
Subgoal *1.2.1.3/2.3
Subgoal *1.2.1.3/2.2
Subgoal *1.2.1.3/2.1
Subgoal *1.2.1.3/2.1'
Subgoal *1.2.1.3/1
Subgoal *1.2.1.3/1'
*1.2.1.3 is COMPLETED!
We therefore turn our attention to *1.2.1.2, which is
(IMPLIES (AND (MEMBER-EQUAL X5 S)
(NOT (EQUAL (SUM (MAP-LIST-COUNT (CONS X1 X6) S))
(+ 1 (SUM (MAP-LIST-COUNT X6 S)))))
(MEMBER-EQUAL X3 S)
(EQUAL (SUM (MAP-LIST-COUNT (LIST* X1 X5 X6) S))
(+ 1
(SUM (MAP-LIST-COUNT (CONS X5 X6) S))))
(MEMBER-EQUAL X1 S)
(SUBSETP-EQUAL X6 S))
(EQUAL (SUM (MAP-LIST-COUNT (LIST* X1 X3 X5 X6) S))
(+ 1
(SUM (MAP-LIST-COUNT (LIST* X3 X5 X6) S))))).
The formula above is subsumed by one of its parents, *1.2, which we're
in the process of trying to prove by induction. When an inductive
proof pushes a subgoal for induction that is less general than the
original goal, it may be a sign that either an inappropriate induction
was chosen or that the original goal is insufficiently general. In
any case, our proof attempt has failed.
Summary
Form: ( DEFTHM SUM-MAP-COUNT-LIST ...)
Rules: ((:DEFINITION ENDP)
(:DEFINITION FIX)
(:DEFINITION LEN)
(:DEFINITION LIST-COUNT)
(:DEFINITION MAP-LIST-COUNT)
(:DEFINITION MEMBER-EQUAL)
(:DEFINITION NOT)
(:DEFINITION REMOVE-EQUAL)
(:DEFINITION RETURN-LAST)
(:DEFINITION SUBSETP-EQL-EXEC$GUARD-CHECK)
(:DEFINITION SUBSETP-EQUAL)
(:DEFINITION SUM)
(:DEFINITION SYNP)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART BINARY-+)
(:EXECUTABLE-COUNTERPART CONSP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION LEN)
(:INDUCTION MAP-LIST-COUNT)
(:INDUCTION MEMBER-EQUAL)
(:INDUCTION SUBSETP-EQUAL)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE FOLD-CONSTS-IN-+)
(:REWRITE UNICITY-OF-0)
(:TYPE-PRESCRIPTION MAP-LIST-COUNT)
(:TYPE-PRESCRIPTION MEMBER-EQUAL)
(:TYPE-PRESCRIPTION SUM))
Splitter rules (see :DOC splitter):
if-intro: ((:DEFINITION LIST-COUNT)
(:DEFINITION MAP-LIST-COUNT)
(:DEFINITION MEMBER-EQUAL)
(:DEFINITION REMOVE-EQUAL)
(:DEFINITION SUM))
Time: 0.08 seconds (prove: 0.07, print: 0.01, other: 0.00)
Prover steps counted: 55803
---
The key checkpoint goals, below, may help you to debug this failure.
See :DOC failure and see :DOC set-checkpoint-summary-limit.
---
*** Key checkpoint at the top level: ***
Goal'
(IMPLIES (SUBSETP-EQUAL X S)
(EQUAL (SUM (MAP-LIST-COUNT X S))
(LEN X)))
*** Key checkpoints under a top-level induction: ***
Subgoal *1/3'
(IMPLIES (NOT (CONSP X))
(EQUAL (SUM (MAP-LIST-COUNT X S)) 0))
Subgoal *1/2'
(IMPLIES (AND (CONSP X)
(EQUAL (SUM (MAP-LIST-COUNT (CDR X) S))
(LEN (CDR X)))
(MEMBER-EQUAL (CAR X) S)
(SUBSETP-EQUAL (CDR X) S))
(EQUAL (SUM (MAP-LIST-COUNT X S))
(+ 1 (LEN (CDR X)))))
ACL2 Error in ( DEFTHM SUM-MAP-COUNT-LIST ...): See :DOC failure.
******** FAILED ********
証明に失敗しました。原因は下記の induction scheme のせいです。
(AND (IMPLIES (NOT (CONSP X)) (:P S X)) (IMPLIES (AND (CONSP X) (:P S (CDR X))) (:P S X)))
map-list-count を使ってもらうように修正します。
(defthm sum-map-count-list
(implies (subsetp x s)
(equal (sum (map-list-count x s))
(len x)))
:hints (("Goal" :induct (map-list-count x s))))
証明失敗: 出力を確認する
*1 (the initial Goal, a key checkpoint) is pushed for proof by induction.
We have been told to use induction. One induction scheme is suggested
by the induction hint.
We will induct according to a scheme suggested by (MAP-LIST-COUNT X S).
This suggestion was produced using the :induction rule MAP-LIST-COUNT.
If we let (:P S X) denote *1 above then the induction scheme we'll
use is
(AND (IMPLIES (AND (NOT (ENDP S))
(:P (CDR S) (REMOVE-EQUAL (CAR S) X)))
(:P S X))
(IMPLIES (ENDP S) (:P S X))).
This induction is justified by the same argument used to admit
MAP-LIST-COUNT. Note, however, that the unmeasured variable X is being
instantiated. When applied to the goal at hand the above induction
scheme produces two nontautological subgoals.
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/2''
Subgoal *1/2'''
Subgoal *1/2'4'
Subgoal *1/2'5'
([ A key checkpoint while proving *1 (descended from Goal):
Subgoal *1/2''
(IMPLIES (AND (CONSP S)
(EQUAL (SUM (MAP-LIST-COUNT (REMOVE-EQUAL (CAR S) X)
(CDR S)))
(LEN (REMOVE-EQUAL (CAR S) X)))
(SUBSETP-EQUAL X S))
(EQUAL (+ (LIST-COUNT (CAR S) X)
(LEN (REMOVE-EQUAL (CAR S) X)))
(LEN X)))
*1.1 (Subgoal *1/2'5') is pushed for proof by induction.
])
Subgoal *1/1
Subgoal *1/1'
So we now return to *1.1, which is
(IMPLIES (SUBSETP-EQUAL X (CONS S1 S2))
(EQUAL (+ (LIST-COUNT S1 X)
(SUM (MAP-LIST-COUNT (REMOVE-EQUAL S1 X)
S2)))
(LEN X))).
Subgoal *1.1/3
Subgoal *1.1/3'
Subgoal *1.1/3''
Subgoal *1.1/3'''
Subgoal *1.1/3'4'
Subgoal *1.1/3'5'
Subgoal *1.1/3'6'
Subgoal *1.1/3'7'
*1.1.1 (Subgoal *1.1/3'7') is pushed for proof by induction.
Subgoal *1.1/2
Subgoal *1.1/2'
Subgoal *1.1/2''
Subgoal *1.1/2'''
Subgoal *1.1/2'4'
*1.1.2 (Subgoal *1.1/2'4') is pushed for proof by induction.
Subgoal *1.1/1
Subgoal *1.1/1'
Subgoal *1.1/1''
*1.1.3 (Subgoal *1.1/1'') is pushed for proof by induction.
So we now return to *1.1.3, which is
(IMPLIES (AND (NOT (CONSP S2))
(SUBSETP-EQUAL X (CONS S1 S2)))
(EQUAL (LIST-COUNT S1 X) (LEN X))).
Subgoal *1.1.3/3
Subgoal *1.1.3/2
Subgoal *1.1.3/1
*1.1.3 is COMPLETED!
We therefore turn our attention to *1.1.2, which is
(IMPLIES (AND (NOT (SUBSETP-EQUAL X (CONS S1 S4)))
(SUBSETP-EQUAL X (LIST* S1 S3 S4)))
(EQUAL (+ (LIST-COUNT S1 X)
(LIST-COUNT S3 (REMOVE-EQUAL S1 X))
(SUM (MAP-LIST-COUNT (REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X))
S4)))
(LEN X))).
Subgoal *1.1.2/4
Subgoal *1.1.2/4'
Subgoal *1.1.2/4''
Subgoal *1.1.2/4'''
Subgoal *1.1.2/4'4'
Subgoal *1.1.2/4'5'
Subgoal *1.1.2/4'6'
Subgoal *1.1.2/4'7'
Subgoal *1.1.2/4'8'
Subgoal *1.1.2/4'9'
Subgoal *1.1.2/4'10'
*1.1.2.1 (Subgoal *1.1.2/4'10') is pushed for proof by induction.
Subgoal *1.1.2/3
Subgoal *1.1.2/3'
Subgoal *1.1.2/3''
Subgoal *1.1.2/3'''
Subgoal *1.1.2/3'4'
*1.1.2.2 (Subgoal *1.1.2/3'4') is pushed for proof by induction.
Subgoal *1.1.2/2
Subgoal *1.1.2/2'
Subgoal *1.1.2/2''
Subgoal *1.1.2/2'''
Subgoal *1.1.2/2'4'
*1.1.2.3 (Subgoal *1.1.2/2'4') is pushed for proof by induction.
Subgoal *1.1.2/1
Subgoal *1.1.2/1'
Subgoal *1.1.2/1''
*1.1.2.4 (Subgoal *1.1.2/1'') is pushed for proof by induction.
So we now return to *1.1.2.4, which is
(IMPLIES (AND (NOT (CONSP S4))
(NOT (SUBSETP-EQUAL X (CONS S1 S4)))
(SUBSETP-EQUAL X (LIST* S1 S3 S4)))
(EQUAL (+ (LIST-COUNT S1 X)
(LIST-COUNT S3 (REMOVE-EQUAL S1 X)))
(LEN X))).
Subgoal *1.1.2.4/4
Subgoal *1.1.2.4/3
Subgoal *1.1.2.4/2
Subgoal *1.1.2.4/1
Subgoal *1.1.2.4/1'
Subgoal *1.1.2.4/1''
Subgoal *1.1.2.4/1'''
Subgoal *1.1.2.4/1'4'
*1.1.2.4.1 (Subgoal *1.1.2.4/1'4') is pushed for proof by induction.
So we now return to *1.1.2.4.1, which is
(IMPLIES (AND (SUBSETP-EQUAL X2 (CONS S1 S4))
(NOT (CONSP S4))
(NOT (EQUAL X1 S1))
(CONS X1 S4)
(SUBSETP-EQUAL X2 (LIST* S1 X1 S4)))
(EQUAL (+ 1 (LIST-COUNT S1 X2)
(LIST-COUNT X1 (REMOVE-EQUAL S1 X2)))
(+ 1 (LEN X2)))).
Subgoal *1.1.2.4.1/4
Subgoal *1.1.2.4.1/3
Subgoal *1.1.2.4.1/2
Subgoal *1.1.2.4.1/1
*1.1.2.4.1 and *1.1.2.4 are COMPLETED!
We therefore turn our attention to *1.1.2.3, which is
(IMPLIES
(AND (SUBSETP-EQUAL X (CONS S1 S6))
(NOT (SUBSETP-EQUAL X (LIST* S1 S5 S6)))
(SUBSETP-EQUAL X (LIST* S1 S3 S5 S6)))
(EQUAL
(+
(LIST-COUNT S1 X)
(LIST-COUNT S3 (REMOVE-EQUAL S1 X))
(LIST-COUNT S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X)))
(SUM (MAP-LIST-COUNT (REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X)))
S6)))
(LEN X))).
Subgoal *1.1.2.3/5
Subgoal *1.1.2.3/5'
Subgoal *1.1.2.3/5''
Subgoal *1.1.2.3/5'''
Subgoal *1.1.2.3/5'4'
Subgoal *1.1.2.3/5'5'
Subgoal *1.1.2.3/5'6'
Subgoal *1.1.2.3/5'7'
Subgoal *1.1.2.3/5'8'
Subgoal *1.1.2.3/5'9'
Subgoal *1.1.2.3/5'10'
Subgoal *1.1.2.3/5'11'
Subgoal *1.1.2.3/5'12'
*1.1.2.3.1 (Subgoal *1.1.2.3/5'12') is pushed for proof by induction.
Subgoal *1.1.2.3/4
Subgoal *1.1.2.3/4'
Subgoal *1.1.2.3/4''
Subgoal *1.1.2.3/4'''
Subgoal *1.1.2.3/4'4'
*1.1.2.3.2 (Subgoal *1.1.2.3/4'4') is pushed for proof by induction.
Subgoal *1.1.2.3/3
Subgoal *1.1.2.3/3'
Subgoal *1.1.2.3/3''
Subgoal *1.1.2.3/3'''
Subgoal *1.1.2.3/3'4'
*1.1.2.3.3 (Subgoal *1.1.2.3/3'4') is pushed for proof by induction.
Subgoal *1.1.2.3/2
Subgoal *1.1.2.3/2'
Subgoal *1.1.2.3/2''
Subgoal *1.1.2.3/2'''
Subgoal *1.1.2.3/2'4'
*1.1.2.3.4 (Subgoal *1.1.2.3/2'4') is pushed for proof by induction.
Subgoal *1.1.2.3/1
Subgoal *1.1.2.3/1'
Subgoal *1.1.2.3/1''
*1.1.2.3.5 (Subgoal *1.1.2.3/1'') is pushed for proof by induction.
So we now return to *1.1.2.3.5, which is
(IMPLIES (AND (NOT (CONSP S6))
(SUBSETP-EQUAL X (CONS S1 S6))
(NOT (SUBSETP-EQUAL X (LIST* S1 S5 S6)))
(SUBSETP-EQUAL X (LIST* S1 S3 S5 S6)))
(EQUAL (+ (LIST-COUNT S1 X)
(LIST-COUNT S3 (REMOVE-EQUAL S1 X))
(LIST-COUNT S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X))))
(LEN X))).
Subgoal *1.1.2.3.5/5
Subgoal *1.1.2.3.5/4
Subgoal *1.1.2.3.5/3
Subgoal *1.1.2.3.5/2
Subgoal *1.1.2.3.5/1
*1.1.2.3.5 is COMPLETED!
We therefore turn our attention to *1.1.2.3.4, which is
(IMPLIES
(AND (NOT (SUBSETP-EQUAL X (CONS S1 S8)))
(SUBSETP-EQUAL X (LIST* S1 S7 S8))
(NOT (SUBSETP-EQUAL X (LIST* S1 S5 S7 S8)))
(SUBSETP-EQUAL X (LIST* S1 S3 S5 S7 S8)))
(EQUAL
(+
(LIST-COUNT S1 X)
(LIST-COUNT S3 (REMOVE-EQUAL S1 X))
(LIST-COUNT S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X)))
(LIST-COUNT S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X))))
(SUM
(MAP-LIST-COUNT
(REMOVE-EQUAL S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X))))
S8)))
(LEN X))).
Subgoal *1.1.2.3.4/6
Subgoal *1.1.2.3.4/6'
Subgoal *1.1.2.3.4/6''
Subgoal *1.1.2.3.4/6'''
Subgoal *1.1.2.3.4/6'4'
Subgoal *1.1.2.3.4/6'5'
Subgoal *1.1.2.3.4/6'6'
Subgoal *1.1.2.3.4/6'7'
Subgoal *1.1.2.3.4/6'8'
Subgoal *1.1.2.3.4/6'9'
Subgoal *1.1.2.3.4/6'10'
Subgoal *1.1.2.3.4/6'11'
Subgoal *1.1.2.3.4/6'12'
Subgoal *1.1.2.3.4/6'13'
Subgoal *1.1.2.3.4/6'14'
*1.1.2.3.4.1 (Subgoal *1.1.2.3.4/6'14') is pushed for proof by induction.
Subgoal *1.1.2.3.4/5
Subgoal *1.1.2.3.4/5'
Subgoal *1.1.2.3.4/5''
Subgoal *1.1.2.3.4/5'''
Subgoal *1.1.2.3.4/5'4'
*1.1.2.3.4.2 (Subgoal *1.1.2.3.4/5'4') is pushed for proof by induction.
Subgoal *1.1.2.3.4/4
Subgoal *1.1.2.3.4/4'
Subgoal *1.1.2.3.4/4''
Subgoal *1.1.2.3.4/4'''
Subgoal *1.1.2.3.4/4'4'
*1.1.2.3.4.3 (Subgoal *1.1.2.3.4/4'4') is pushed for proof by induction.
Subgoal *1.1.2.3.4/3
Subgoal *1.1.2.3.4/3'
Subgoal *1.1.2.3.4/3''
Subgoal *1.1.2.3.4/3'''
Subgoal *1.1.2.3.4/3'4'
*1.1.2.3.4.4 (Subgoal *1.1.2.3.4/3'4') is pushed for proof by induction.
Subgoal *1.1.2.3.4/2
Subgoal *1.1.2.3.4/2'
Subgoal *1.1.2.3.4/2''
Subgoal *1.1.2.3.4/2'''
Subgoal *1.1.2.3.4/2'4'
*1.1.2.3.4.5 (Subgoal *1.1.2.3.4/2'4') is pushed for proof by induction.
Subgoal *1.1.2.3.4/1
Subgoal *1.1.2.3.4/1'
Subgoal *1.1.2.3.4/1''
*1.1.2.3.4.6 (Subgoal *1.1.2.3.4/1'') is pushed for proof by induction.
So we now return to *1.1.2.3.4.6, which is
(IMPLIES
(AND (NOT (CONSP S8))
(NOT (SUBSETP-EQUAL X (CONS S1 S8)))
(SUBSETP-EQUAL X (LIST* S1 S7 S8))
(NOT (SUBSETP-EQUAL X (LIST* S1 S5 S7 S8)))
(SUBSETP-EQUAL X (LIST* S1 S3 S5 S7 S8)))
(EQUAL (+ (LIST-COUNT S1 X)
(LIST-COUNT S3 (REMOVE-EQUAL S1 X))
(LIST-COUNT S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X)))
(LIST-COUNT S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X)))))
(LEN X))).
Subgoal *1.1.2.3.4.6/6
Subgoal *1.1.2.3.4.6/5
Splitter note (see :DOC splitter) for Subgoal *1.1.2.3.4.6/5 (4 subgoals).
if-intro: ((:DEFINITION LIST-COUNT)
(:DEFINITION MEMBER-EQUAL)
(:DEFINITION REMOVE-EQUAL)
(:DEFINITION SUBSETP-EQUAL))
Subgoal *1.1.2.3.4.6/5.4
Subgoal *1.1.2.3.4.6/5.3
Splitter note (see :DOC splitter) for Subgoal *1.1.2.3.4.6/5.3 (2 subgoals).
if-intro: ((:DEFINITION LIST-COUNT)
(:DEFINITION REMOVE-EQUAL))
Subgoal *1.1.2.3.4.6/5.3.2
Subgoal *1.1.2.3.4.6/5.3.1
Subgoal *1.1.2.3.4.6/5.2
Subgoal *1.1.2.3.4.6/5.1
Splitter note (see :DOC splitter) for Subgoal *1.1.2.3.4.6/5.1 (2 subgoals).
if-intro: ((:DEFINITION LIST-COUNT)
(:DEFINITION REMOVE-EQUAL))
Subgoal *1.1.2.3.4.6/5.1.2
Subgoal *1.1.2.3.4.6/5.1.1
Subgoal *1.1.2.3.4.6/4
Subgoal *1.1.2.3.4.6/3
Subgoal *1.1.2.3.4.6/2
Subgoal *1.1.2.3.4.6/1
Splitter note (see :DOC splitter) for Subgoal *1.1.2.3.4.6/1 (2 subgoals).
if-intro: ((:DEFINITION LIST-COUNT)
(:DEFINITION MEMBER-EQUAL)
(:DEFINITION REMOVE-EQUAL)
(:DEFINITION SUBSETP-EQUAL))
Subgoal *1.1.2.3.4.6/1.2
Subgoal *1.1.2.3.4.6/1.2'
Subgoal *1.1.2.3.4.6/1.2''
Subgoal *1.1.2.3.4.6/1.2'''
Subgoal *1.1.2.3.4.6/1.2'4'
*1.1.2.3.4.6.1 (Subgoal *1.1.2.3.4.6/1.2'4') is pushed for proof by
induction.
Subgoal *1.1.2.3.4.6/1.1
Splitter note (see :DOC splitter) for Subgoal *1.1.2.3.4.6/1.1 (2 subgoals).
if-intro: ((:DEFINITION LIST-COUNT)
(:DEFINITION REMOVE-EQUAL))
Subgoal *1.1.2.3.4.6/1.1.2
Subgoal *1.1.2.3.4.6/1.1.2'
Subgoal *1.1.2.3.4.6/1.1.2''
Subgoal *1.1.2.3.4.6/1.1.2'''
Subgoal *1.1.2.3.4.6/1.1.2'4'
*1.1.2.3.4.6.2 (Subgoal *1.1.2.3.4.6/1.1.2'4') is pushed for proof
by induction.
Subgoal *1.1.2.3.4.6/1.1.1
Subgoal *1.1.2.3.4.6/1.1.1'
Subgoal *1.1.2.3.4.6/1.1.1''
Subgoal *1.1.2.3.4.6/1.1.1'''
*1.1.2.3.4.6.3 (Subgoal *1.1.2.3.4.6/1.1.1''') is pushed for proof
by induction.
So we now return to *1.1.2.3.4.6.3, which is
(IMPLIES
(AND (SUBSETP-EQUAL X2 (CONS S1 S8))
(NOT (CONSP S8))
(NOT (EQUAL X1 S1))
(CONS X1 S8)
(SUBSETP-EQUAL X2 (LIST* S1 X1 S8))
(NOT (SUBSETP-EQUAL X2 (LIST* S1 S5 X1 S8)))
(SUBSETP-EQUAL X2 (LIST* S1 S3 S5 X1 S8))
(NOT (EQUAL S3 X1))
(NOT (EQUAL S5 X1)))
(EQUAL
(+ 1 (LIST-COUNT S1 X2)
(LIST-COUNT S3 (REMOVE-EQUAL S1 X2))
(LIST-COUNT S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X2)))
(LIST-COUNT X1
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X2)))))
(+ 1 (LEN X2)))).
Subgoal *1.1.2.3.4.6.3/6
Subgoal *1.1.2.3.4.6.3/5
Subgoal *1.1.2.3.4.6.3/4
Subgoal *1.1.2.3.4.6.3/3
Subgoal *1.1.2.3.4.6.3/2
Subgoal *1.1.2.3.4.6.3/1
*1.1.2.3.4.6.3 is COMPLETED!
We therefore turn our attention to *1.1.2.3.4.6.2, which is
(IMPLIES
(AND (SUBSETP-EQUAL X2 (CONS S1 S8))
(NOT (CONSP S8))
(NOT (EQUAL X1 S1))
(CONS X1 S8)
(SUBSETP-EQUAL X2 (LIST* S1 X1 S8))
(NOT (SUBSETP-EQUAL X2 (LIST* S1 X1 X1 S8)))
(SUBSETP-EQUAL X2 (LIST* S1 S3 X1 X1 S8))
(NOT (EQUAL S3 X1)))
(EQUAL
(+ 1 (LIST-COUNT S1 X2)
(LIST-COUNT S3 (REMOVE-EQUAL S1 X2))
(LIST-COUNT X1
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X2)))
(LIST-COUNT X1
(REMOVE-EQUAL X1
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X2)))))
(+ 1 (LEN X2)))).
Subgoal *1.1.2.3.4.6.2/6
Subgoal *1.1.2.3.4.6.2/5
Subgoal *1.1.2.3.4.6.2/4
Subgoal *1.1.2.3.4.6.2/3
Subgoal *1.1.2.3.4.6.2/2
Subgoal *1.1.2.3.4.6.2/1
*1.1.2.3.4.6.2 is COMPLETED!
We therefore turn our attention to *1.1.2.3.4.6.1, which is
(IMPLIES
(AND (SUBSETP-EQUAL X2 (CONS S1 S8))
(NOT (CONSP S8))
(NOT (EQUAL X1 S1))
(CONS X1 S8)
(SUBSETP-EQUAL X2 (LIST* S1 X1 S8))
(NOT (SUBSETP-EQUAL X2 (LIST* S1 S5 X1 S8)))
(SUBSETP-EQUAL X2 (LIST* S1 X1 S5 X1 S8)))
(EQUAL
(+ 1 (LIST-COUNT S1 X2)
(LIST-COUNT X1 (REMOVE-EQUAL S1 X2))
(LIST-COUNT S5
(REMOVE-EQUAL X1 (REMOVE-EQUAL S1 X2)))
(LIST-COUNT X1
(REMOVE-EQUAL S5
(REMOVE-EQUAL X1 (REMOVE-EQUAL S1 X2)))))
(+ 1 (LEN X2)))).
Subgoal *1.1.2.3.4.6.1/6
Subgoal *1.1.2.3.4.6.1/5
Subgoal *1.1.2.3.4.6.1/4
Subgoal *1.1.2.3.4.6.1/3
Subgoal *1.1.2.3.4.6.1/2
Subgoal *1.1.2.3.4.6.1/1
*1.1.2.3.4.6.1 and *1.1.2.3.4.6 are COMPLETED!
We therefore turn our attention to *1.1.2.3.4.5, which is
(IMPLIES
(AND (SUBSETP-EQUAL X (CONS S1 S10))
(NOT (SUBSETP-EQUAL X (LIST* S1 S9 S10)))
(SUBSETP-EQUAL X (LIST* S1 S7 S9 S10))
(NOT (SUBSETP-EQUAL X (LIST* S1 S5 S7 S9 S10)))
(SUBSETP-EQUAL X (LIST* S1 S3 S5 S7 S9 S10)))
(EQUAL
(+
(LIST-COUNT S1 X)
(LIST-COUNT S3 (REMOVE-EQUAL S1 X))
(LIST-COUNT S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X)))
(LIST-COUNT S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X))))
(LIST-COUNT
S9
(REMOVE-EQUAL S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X)))))
(SUM
(MAP-LIST-COUNT
(REMOVE-EQUAL
S9
(REMOVE-EQUAL S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X)))))
S10)))
(LEN X))).
Subgoal *1.1.2.3.4.5/7
Subgoal *1.1.2.3.4.5/7'
Subgoal *1.1.2.3.4.5/7''
Subgoal *1.1.2.3.4.5/7'''
Subgoal *1.1.2.3.4.5/7'4'
Subgoal *1.1.2.3.4.5/7'5'
Subgoal *1.1.2.3.4.5/7'6'
Subgoal *1.1.2.3.4.5/7'7'
Subgoal *1.1.2.3.4.5/7'8'
Subgoal *1.1.2.3.4.5/7'9'
Subgoal *1.1.2.3.4.5/7'10'
Subgoal *1.1.2.3.4.5/7'11'
Subgoal *1.1.2.3.4.5/7'12'
Subgoal *1.1.2.3.4.5/7'13'
Subgoal *1.1.2.3.4.5/7'14'
Subgoal *1.1.2.3.4.5/7'15'
Subgoal *1.1.2.3.4.5/7'16'
*1.1.2.3.4.5.1 (Subgoal *1.1.2.3.4.5/7'16') is pushed for proof by
induction.
Subgoal *1.1.2.3.4.5/6
Subgoal *1.1.2.3.4.5/6'
Subgoal *1.1.2.3.4.5/6''
Subgoal *1.1.2.3.4.5/6'''
Subgoal *1.1.2.3.4.5/6'4'
*1.1.2.3.4.5.2 (Subgoal *1.1.2.3.4.5/6'4') is pushed for proof by induction.
Subgoal *1.1.2.3.4.5/5
Subgoal *1.1.2.3.4.5/5'
Subgoal *1.1.2.3.4.5/5''
Subgoal *1.1.2.3.4.5/5'''
Subgoal *1.1.2.3.4.5/5'4'
*1.1.2.3.4.5.3 (Subgoal *1.1.2.3.4.5/5'4') is pushed for proof by induction.
Subgoal *1.1.2.3.4.5/4
Subgoal *1.1.2.3.4.5/4'
Subgoal *1.1.2.3.4.5/4''
Subgoal *1.1.2.3.4.5/4'''
Subgoal *1.1.2.3.4.5/4'4'
*1.1.2.3.4.5.4 (Subgoal *1.1.2.3.4.5/4'4') is pushed for proof by induction.
Subgoal *1.1.2.3.4.5/3
Subgoal *1.1.2.3.4.5/3'
Subgoal *1.1.2.3.4.5/3''
Subgoal *1.1.2.3.4.5/3'''
Subgoal *1.1.2.3.4.5/3'4'
*1.1.2.3.4.5.5 (Subgoal *1.1.2.3.4.5/3'4') is pushed for proof by induction.
Subgoal *1.1.2.3.4.5/2
Subgoal *1.1.2.3.4.5/2'
Subgoal *1.1.2.3.4.5/2''
Subgoal *1.1.2.3.4.5/2'''
Subgoal *1.1.2.3.4.5/2'4'
*1.1.2.3.4.5.6 (Subgoal *1.1.2.3.4.5/2'4') is pushed for proof by induction.
Subgoal *1.1.2.3.4.5/1
Subgoal *1.1.2.3.4.5/1'
Subgoal *1.1.2.3.4.5/1''
*1.1.2.3.4.5.7 (Subgoal *1.1.2.3.4.5/1'') is pushed for proof by induction.
So we now return to *1.1.2.3.4.5.7, which is
(IMPLIES
(AND (NOT (CONSP S10))
(SUBSETP-EQUAL X (CONS S1 S10))
(NOT (SUBSETP-EQUAL X (LIST* S1 S9 S10)))
(SUBSETP-EQUAL X (LIST* S1 S7 S9 S10))
(NOT (SUBSETP-EQUAL X (LIST* S1 S5 S7 S9 S10)))
(SUBSETP-EQUAL X (LIST* S1 S3 S5 S7 S9 S10)))
(EQUAL
(+
(LIST-COUNT S1 X)
(LIST-COUNT S3 (REMOVE-EQUAL S1 X))
(LIST-COUNT S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X)))
(LIST-COUNT S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X))))
(LIST-COUNT
S9
(REMOVE-EQUAL S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X))))))
(LEN X))).
Subgoal *1.1.2.3.4.5.7/7
Subgoal *1.1.2.3.4.5.7/6
Subgoal *1.1.2.3.4.5.7/5
Subgoal *1.1.2.3.4.5.7/4
Subgoal *1.1.2.3.4.5.7/3
Subgoal *1.1.2.3.4.5.7/2
Subgoal *1.1.2.3.4.5.7/1
*1.1.2.3.4.5.7 is COMPLETED!
We therefore turn our attention to *1.1.2.3.4.5.6, which is
(IMPLIES
(AND (NOT (SUBSETP-EQUAL X (CONS S1 S12)))
(SUBSETP-EQUAL X (LIST* S1 S11 S12))
(NOT (SUBSETP-EQUAL X (LIST* S1 S9 S11 S12)))
(SUBSETP-EQUAL X (LIST* S1 S7 S9 S11 S12))
(NOT (SUBSETP-EQUAL X (LIST* S1 S5 S7 S9 S11 S12)))
(SUBSETP-EQUAL X (LIST* S1 S3 S5 S7 S9 S11 S12)))
(EQUAL
(+
(LIST-COUNT S1 X)
(LIST-COUNT S3 (REMOVE-EQUAL S1 X))
(LIST-COUNT S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X)))
(LIST-COUNT S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X))))
(LIST-COUNT
S9
(REMOVE-EQUAL S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X)))))
(LIST-COUNT
S11
(REMOVE-EQUAL
S9
(REMOVE-EQUAL S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X))))))
(SUM
(MAP-LIST-COUNT
(REMOVE-EQUAL
S11
(REMOVE-EQUAL
S9
(REMOVE-EQUAL S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X))))))
S12)))
(LEN X))).
Subgoal *1.1.2.3.4.5.6/8
Subgoal *1.1.2.3.4.5.6/8'
Subgoal *1.1.2.3.4.5.6/8''
Subgoal *1.1.2.3.4.5.6/8'''
Subgoal *1.1.2.3.4.5.6/8'4'
Subgoal *1.1.2.3.4.5.6/8'5'
Subgoal *1.1.2.3.4.5.6/8'6'
Subgoal *1.1.2.3.4.5.6/8'7'
Subgoal *1.1.2.3.4.5.6/8'8'
Subgoal *1.1.2.3.4.5.6/8'9'
Subgoal *1.1.2.3.4.5.6/8'10'
Subgoal *1.1.2.3.4.5.6/8'11'
Subgoal *1.1.2.3.4.5.6/8'12'
Subgoal *1.1.2.3.4.5.6/8'13'
Subgoal *1.1.2.3.4.5.6/8'14'
Subgoal *1.1.2.3.4.5.6/8'15'
Subgoal *1.1.2.3.4.5.6/8'16'
Subgoal *1.1.2.3.4.5.6/8'17'
Subgoal *1.1.2.3.4.5.6/8'18'
*1.1.2.3.4.5.6.1 (Subgoal *1.1.2.3.4.5.6/8'18') is pushed for proof
by induction.
Subgoal *1.1.2.3.4.5.6/7
Subgoal *1.1.2.3.4.5.6/7'
Subgoal *1.1.2.3.4.5.6/7''
Subgoal *1.1.2.3.4.5.6/7'''
Subgoal *1.1.2.3.4.5.6/7'4'
*1.1.2.3.4.5.6.2 (Subgoal *1.1.2.3.4.5.6/7'4') is pushed for proof
by induction.
Subgoal *1.1.2.3.4.5.6/6
Subgoal *1.1.2.3.4.5.6/6'
Subgoal *1.1.2.3.4.5.6/6''
Subgoal *1.1.2.3.4.5.6/6'''
Subgoal *1.1.2.3.4.5.6/6'4'
*1.1.2.3.4.5.6.3 (Subgoal *1.1.2.3.4.5.6/6'4') is pushed for proof
by induction.
Subgoal *1.1.2.3.4.5.6/5
Subgoal *1.1.2.3.4.5.6/5'
Subgoal *1.1.2.3.4.5.6/5''
Subgoal *1.1.2.3.4.5.6/5'''
Subgoal *1.1.2.3.4.5.6/5'4'
*1.1.2.3.4.5.6.4 (Subgoal *1.1.2.3.4.5.6/5'4') is pushed for proof
by induction.
Subgoal *1.1.2.3.4.5.6/4
Subgoal *1.1.2.3.4.5.6/4'
Subgoal *1.1.2.3.4.5.6/4''
Subgoal *1.1.2.3.4.5.6/4'''
Subgoal *1.1.2.3.4.5.6/4'4'
*1.1.2.3.4.5.6.5 (Subgoal *1.1.2.3.4.5.6/4'4') is pushed for proof
by induction.
Subgoal *1.1.2.3.4.5.6/3
Subgoal *1.1.2.3.4.5.6/3'
Subgoal *1.1.2.3.4.5.6/3''
Subgoal *1.1.2.3.4.5.6/3'''
Subgoal *1.1.2.3.4.5.6/3'4'
*1.1.2.3.4.5.6.6 (Subgoal *1.1.2.3.4.5.6/3'4') is pushed for proof
by induction.
Subgoal *1.1.2.3.4.5.6/2
Subgoal *1.1.2.3.4.5.6/2'
Subgoal *1.1.2.3.4.5.6/2''
Subgoal *1.1.2.3.4.5.6/2'''
Subgoal *1.1.2.3.4.5.6/2'4'
*1.1.2.3.4.5.6.7 (Subgoal *1.1.2.3.4.5.6/2'4') is pushed for proof
by induction.
Subgoal *1.1.2.3.4.5.6/1
Subgoal *1.1.2.3.4.5.6/1'
Subgoal *1.1.2.3.4.5.6/1''
*1.1.2.3.4.5.6.8 (Subgoal *1.1.2.3.4.5.6/1'') is pushed for proof by
induction.
So we now return to *1.1.2.3.4.5.6.8, which is
(IMPLIES
(AND (NOT (CONSP S12))
(NOT (SUBSETP-EQUAL X (CONS S1 S12)))
(SUBSETP-EQUAL X (LIST* S1 S11 S12))
(NOT (SUBSETP-EQUAL X (LIST* S1 S9 S11 S12)))
(SUBSETP-EQUAL X (LIST* S1 S7 S9 S11 S12))
(NOT (SUBSETP-EQUAL X (LIST* S1 S5 S7 S9 S11 S12)))
(SUBSETP-EQUAL X (LIST* S1 S3 S5 S7 S9 S11 S12)))
(EQUAL
(+
(LIST-COUNT S1 X)
(LIST-COUNT S3 (REMOVE-EQUAL S1 X))
(LIST-COUNT S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X)))
(LIST-COUNT S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X))))
(LIST-COUNT
S9
(REMOVE-EQUAL S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X)))))
(LIST-COUNT
S11
(REMOVE-EQUAL
S9
(REMOVE-EQUAL S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X)))))))
(LEN X))).
Subgoal *1.1.2.3.4.5.6.8/8
Subgoal *1.1.2.3.4.5.6.8/7
Splitter note (see :DOC splitter) for Subgoal *1.1.2.3.4.5.6.8/7 (4
subgoals).
if-intro: ((:DEFINITION LIST-COUNT)
(:DEFINITION MEMBER-EQUAL)
(:DEFINITION REMOVE-EQUAL)
(:DEFINITION SUBSETP-EQUAL))
Subgoal *1.1.2.3.4.5.6.8/7.4
Subgoal *1.1.2.3.4.5.6.8/7.4'
Subgoal *1.1.2.3.4.5.6.8/7.3
Splitter note (see :DOC splitter) for Subgoal *1.1.2.3.4.5.6.8/7.3
(2 subgoals).
if-intro: ((:DEFINITION LIST-COUNT)
(:DEFINITION REMOVE-EQUAL))
Subgoal *1.1.2.3.4.5.6.8/7.3.2
Subgoal *1.1.2.3.4.5.6.8/7.3.1
Splitter note (see :DOC splitter) for Subgoal *1.1.2.3.4.5.6.8/7.3.1
(2 subgoals).
if-intro: ((:DEFINITION LIST-COUNT)
(:DEFINITION REMOVE-EQUAL))
Subgoal *1.1.2.3.4.5.6.8/7.3.1.2
Subgoal *1.1.2.3.4.5.6.8/7.3.1.2'
Subgoal *1.1.2.3.4.5.6.8/7.3.1.1
Splitter note (see :DOC splitter) for Subgoal *1.1.2.3.4.5.6.8/7.3.1.1
(2 subgoals).
if-intro: ((:DEFINITION LIST-COUNT)
(:DEFINITION REMOVE-EQUAL))
Subgoal *1.1.2.3.4.5.6.8/7.3.1.1.2
Subgoal *1.1.2.3.4.5.6.8/7.3.1.1.2'
Subgoal *1.1.2.3.4.5.6.8/7.3.1.1.1
Subgoal *1.1.2.3.4.5.6.8/7.2
Subgoal *1.1.2.3.4.5.6.8/7.2'
Subgoal *1.1.2.3.4.5.6.8/7.1
Splitter note (see :DOC splitter) for Subgoal *1.1.2.3.4.5.6.8/7.1
(2 subgoals).
if-intro: ((:DEFINITION LIST-COUNT)
(:DEFINITION REMOVE-EQUAL))
Subgoal *1.1.2.3.4.5.6.8/7.1.2
Subgoal *1.1.2.3.4.5.6.8/7.1.1
Splitter note (see :DOC splitter) for Subgoal *1.1.2.3.4.5.6.8/7.1.1
(2 subgoals).
if-intro: ((:DEFINITION LIST-COUNT)
(:DEFINITION REMOVE-EQUAL))
Subgoal *1.1.2.3.4.5.6.8/7.1.1.2
Subgoal *1.1.2.3.4.5.6.8/7.1.1.2'
Subgoal *1.1.2.3.4.5.6.8/7.1.1.1
Splitter note (see :DOC splitter) for Subgoal *1.1.2.3.4.5.6.8/7.1.1.1
(2 subgoals).
if-intro: ((:DEFINITION LIST-COUNT)
(:DEFINITION REMOVE-EQUAL))
Subgoal *1.1.2.3.4.5.6.8/7.1.1.1.2
Subgoal *1.1.2.3.4.5.6.8/7.1.1.1.2'
Subgoal *1.1.2.3.4.5.6.8/7.1.1.1.1
Subgoal *1.1.2.3.4.5.6.8/6
Subgoal *1.1.2.3.4.5.6.8/5
Subgoal *1.1.2.3.4.5.6.8/4
Subgoal *1.1.2.3.4.5.6.8/3
Subgoal *1.1.2.3.4.5.6.8/2
Subgoal *1.1.2.3.4.5.6.8/1
Splitter note (see :DOC splitter) for Subgoal *1.1.2.3.4.5.6.8/1 (2
subgoals).
if-intro: ((:DEFINITION LIST-COUNT)
(:DEFINITION MEMBER-EQUAL)
(:DEFINITION REMOVE-EQUAL)
(:DEFINITION SUBSETP-EQUAL))
Subgoal *1.1.2.3.4.5.6.8/1.2
Subgoal *1.1.2.3.4.5.6.8/1.2'
Subgoal *1.1.2.3.4.5.6.8/1.2''
Subgoal *1.1.2.3.4.5.6.8/1.2'''
Subgoal *1.1.2.3.4.5.6.8/1.2'4'
*1.1.2.3.4.5.6.8.1 (Subgoal *1.1.2.3.4.5.6.8/1.2'4') is pushed for
proof by induction.
Subgoal *1.1.2.3.4.5.6.8/1.1
Splitter note (see :DOC splitter) for Subgoal *1.1.2.3.4.5.6.8/1.1
(2 subgoals).
if-intro: ((:DEFINITION LIST-COUNT)
(:DEFINITION REMOVE-EQUAL))
Subgoal *1.1.2.3.4.5.6.8/1.1.2
Subgoal *1.1.2.3.4.5.6.8/1.1.2'
Subgoal *1.1.2.3.4.5.6.8/1.1.2''
Subgoal *1.1.2.3.4.5.6.8/1.1.2'''
Subgoal *1.1.2.3.4.5.6.8/1.1.2'4'
*1.1.2.3.4.5.6.8.2 (Subgoal *1.1.2.3.4.5.6.8/1.1.2'4') is pushed for
proof by induction.
Subgoal *1.1.2.3.4.5.6.8/1.1.1
Splitter note (see :DOC splitter) for Subgoal *1.1.2.3.4.5.6.8/1.1.1
(2 subgoals).
if-intro: ((:DEFINITION LIST-COUNT)
(:DEFINITION REMOVE-EQUAL))
Subgoal *1.1.2.3.4.5.6.8/1.1.1.2
Subgoal *1.1.2.3.4.5.6.8/1.1.1.2'
Subgoal *1.1.2.3.4.5.6.8/1.1.1.2''
Subgoal *1.1.2.3.4.5.6.8/1.1.1.2'''
Subgoal *1.1.2.3.4.5.6.8/1.1.1.2'4'
*1.1.2.3.4.5.6.8.3 (Subgoal *1.1.2.3.4.5.6.8/1.1.1.2'4') is pushed
for proof by induction.
Subgoal *1.1.2.3.4.5.6.8/1.1.1.1
Splitter note (see :DOC splitter) for Subgoal *1.1.2.3.4.5.6.8/1.1.1.1
(2 subgoals).
if-intro: ((:DEFINITION LIST-COUNT)
(:DEFINITION REMOVE-EQUAL))
Subgoal *1.1.2.3.4.5.6.8/1.1.1.1.2
Subgoal *1.1.2.3.4.5.6.8/1.1.1.1.2'
Subgoal *1.1.2.3.4.5.6.8/1.1.1.1.2''
Subgoal *1.1.2.3.4.5.6.8/1.1.1.1.2'''
Subgoal *1.1.2.3.4.5.6.8/1.1.1.1.2'4'
*1.1.2.3.4.5.6.8.4 (Subgoal *1.1.2.3.4.5.6.8/1.1.1.1.2'4') is pushed
for proof by induction.
Subgoal *1.1.2.3.4.5.6.8/1.1.1.1.1
Subgoal *1.1.2.3.4.5.6.8/1.1.1.1.1'
Subgoal *1.1.2.3.4.5.6.8/1.1.1.1.1''
Subgoal *1.1.2.3.4.5.6.8/1.1.1.1.1'''
*1.1.2.3.4.5.6.8.5 (Subgoal *1.1.2.3.4.5.6.8/1.1.1.1.1''') is pushed
for proof by induction.
So we now return to *1.1.2.3.4.5.6.8.5, which is
(IMPLIES
(AND (SUBSETP-EQUAL X2 (CONS S1 S12))
(NOT (CONSP S12))
(NOT (EQUAL X1 S1))
(CONS X1 S12)
(SUBSETP-EQUAL X2 (LIST* S1 X1 S12))
(NOT (SUBSETP-EQUAL X2 (LIST* S1 S9 X1 S12)))
(SUBSETP-EQUAL X2 (LIST* S1 S7 S9 X1 S12))
(NOT (SUBSETP-EQUAL X2 (LIST* S1 S5 S7 S9 X1 S12)))
(SUBSETP-EQUAL X2 (LIST* S1 S3 S5 S7 S9 X1 S12))
(NOT (EQUAL S3 X1))
(NOT (EQUAL S5 X1))
(NOT (EQUAL S7 X1))
(NOT (EQUAL S9 X1)))
(EQUAL
(+
1 (LIST-COUNT S1 X2)
(LIST-COUNT S3 (REMOVE-EQUAL S1 X2))
(LIST-COUNT S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X2)))
(LIST-COUNT S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X2))))
(LIST-COUNT
S9
(REMOVE-EQUAL S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X2)))))
(LIST-COUNT
X1
(REMOVE-EQUAL
S9
(REMOVE-EQUAL S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X2)))))))
(+ 1 (LEN X2)))).
Subgoal *1.1.2.3.4.5.6.8.5/8
Subgoal *1.1.2.3.4.5.6.8.5/7
Subgoal *1.1.2.3.4.5.6.8.5/6
Subgoal *1.1.2.3.4.5.6.8.5/5
Subgoal *1.1.2.3.4.5.6.8.5/4
Subgoal *1.1.2.3.4.5.6.8.5/3
Subgoal *1.1.2.3.4.5.6.8.5/2
Subgoal *1.1.2.3.4.5.6.8.5/1
*1.1.2.3.4.5.6.8.5 is COMPLETED!
We therefore turn our attention to *1.1.2.3.4.5.6.8.4, which is
(IMPLIES
(AND (SUBSETP-EQUAL X2 (CONS S1 S12))
(NOT (CONSP S12))
(NOT (EQUAL X1 S1))
(CONS X1 S12)
(SUBSETP-EQUAL X2 (LIST* S1 X1 S12))
(NOT (SUBSETP-EQUAL X2 (LIST* S1 X1 X1 S12)))
(SUBSETP-EQUAL X2 (LIST* S1 S7 X1 X1 S12))
(NOT (SUBSETP-EQUAL X2 (LIST* S1 S5 S7 X1 X1 S12)))
(SUBSETP-EQUAL X2 (LIST* S1 S3 S5 S7 X1 X1 S12))
(NOT (EQUAL S3 X1))
(NOT (EQUAL S5 X1))
(NOT (EQUAL S7 X1)))
(EQUAL
(+
1 (LIST-COUNT S1 X2)
(LIST-COUNT S3 (REMOVE-EQUAL S1 X2))
(LIST-COUNT S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X2)))
(LIST-COUNT S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X2))))
(LIST-COUNT
X1
(REMOVE-EQUAL S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X2)))))
(LIST-COUNT
X1
(REMOVE-EQUAL
X1
(REMOVE-EQUAL S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X2)))))))
(+ 1 (LEN X2)))).
Subgoal *1.1.2.3.4.5.6.8.4/8
Subgoal *1.1.2.3.4.5.6.8.4/7
Subgoal *1.1.2.3.4.5.6.8.4/6
Subgoal *1.1.2.3.4.5.6.8.4/5
Subgoal *1.1.2.3.4.5.6.8.4/4
Subgoal *1.1.2.3.4.5.6.8.4/3
Subgoal *1.1.2.3.4.5.6.8.4/2
Subgoal *1.1.2.3.4.5.6.8.4/1
*1.1.2.3.4.5.6.8.4 is COMPLETED!
We therefore turn our attention to *1.1.2.3.4.5.6.8.3, which is
(IMPLIES
(AND (SUBSETP-EQUAL X2 (CONS S1 S12))
(NOT (CONSP S12))
(NOT (EQUAL X1 S1))
(CONS X1 S12)
(SUBSETP-EQUAL X2 (LIST* S1 X1 S12))
(NOT (SUBSETP-EQUAL X2 (LIST* S1 S9 X1 S12)))
(SUBSETP-EQUAL X2 (LIST* S1 X1 S9 X1 S12))
(NOT (SUBSETP-EQUAL X2 (LIST* S1 S5 X1 S9 X1 S12)))
(SUBSETP-EQUAL X2 (LIST* S1 S3 S5 X1 S9 X1 S12))
(NOT (EQUAL S3 X1))
(NOT (EQUAL S5 X1)))
(EQUAL
(+
1 (LIST-COUNT S1 X2)
(LIST-COUNT S3 (REMOVE-EQUAL S1 X2))
(LIST-COUNT S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X2)))
(LIST-COUNT X1
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X2))))
(LIST-COUNT
S9
(REMOVE-EQUAL X1
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X2)))))
(LIST-COUNT
X1
(REMOVE-EQUAL
S9
(REMOVE-EQUAL X1
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X2)))))))
(+ 1 (LEN X2)))).
Subgoal *1.1.2.3.4.5.6.8.3/8
Subgoal *1.1.2.3.4.5.6.8.3/7
Subgoal *1.1.2.3.4.5.6.8.3/6
Subgoal *1.1.2.3.4.5.6.8.3/5
Subgoal *1.1.2.3.4.5.6.8.3/4
Subgoal *1.1.2.3.4.5.6.8.3/3
Subgoal *1.1.2.3.4.5.6.8.3/2
Subgoal *1.1.2.3.4.5.6.8.3/1
*1.1.2.3.4.5.6.8.3 is COMPLETED!
We therefore turn our attention to *1.1.2.3.4.5.6.8.2, which is
(IMPLIES
(AND (SUBSETP-EQUAL X2 (CONS S1 S12))
(NOT (CONSP S12))
(NOT (EQUAL X1 S1))
(CONS X1 S12)
(SUBSETP-EQUAL X2 (LIST* S1 X1 S12))
(NOT (SUBSETP-EQUAL X2 (LIST* S1 S9 X1 S12)))
(SUBSETP-EQUAL X2 (LIST* S1 S7 S9 X1 S12))
(NOT (SUBSETP-EQUAL X2 (LIST* S1 X1 S7 S9 X1 S12)))
(SUBSETP-EQUAL X2 (LIST* S1 S3 X1 S7 S9 X1 S12))
(NOT (EQUAL S3 X1)))
(EQUAL
(+
1 (LIST-COUNT S1 X2)
(LIST-COUNT S3 (REMOVE-EQUAL S1 X2))
(LIST-COUNT X1
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X2)))
(LIST-COUNT S7
(REMOVE-EQUAL X1
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X2))))
(LIST-COUNT
S9
(REMOVE-EQUAL S7
(REMOVE-EQUAL X1
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X2)))))
(LIST-COUNT
X1
(REMOVE-EQUAL
S9
(REMOVE-EQUAL S7
(REMOVE-EQUAL X1
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X2)))))))
(+ 1 (LEN X2)))).
Subgoal *1.1.2.3.4.5.6.8.2/8
Subgoal *1.1.2.3.4.5.6.8.2/7
Subgoal *1.1.2.3.4.5.6.8.2/6
Subgoal *1.1.2.3.4.5.6.8.2/5
Subgoal *1.1.2.3.4.5.6.8.2/4
Subgoal *1.1.2.3.4.5.6.8.2/3
Subgoal *1.1.2.3.4.5.6.8.2/2
Subgoal *1.1.2.3.4.5.6.8.2/1
*1.1.2.3.4.5.6.8.2 is COMPLETED!
We therefore turn our attention to *1.1.2.3.4.5.6.8.1, which is
(IMPLIES
(AND (SUBSETP-EQUAL X2 (CONS S1 S12))
(NOT (CONSP S12))
(NOT (EQUAL X1 S1))
(CONS X1 S12)
(SUBSETP-EQUAL X2 (LIST* S1 X1 S12))
(NOT (SUBSETP-EQUAL X2 (LIST* S1 S9 X1 S12)))
(SUBSETP-EQUAL X2 (LIST* S1 S7 S9 X1 S12))
(NOT (SUBSETP-EQUAL X2 (LIST* S1 S5 S7 S9 X1 S12)))
(SUBSETP-EQUAL X2 (LIST* S1 X1 S5 S7 S9 X1 S12)))
(EQUAL
(+
1 (LIST-COUNT S1 X2)
(LIST-COUNT X1 (REMOVE-EQUAL S1 X2))
(LIST-COUNT S5
(REMOVE-EQUAL X1 (REMOVE-EQUAL S1 X2)))
(LIST-COUNT S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL X1 (REMOVE-EQUAL S1 X2))))
(LIST-COUNT
S9
(REMOVE-EQUAL S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL X1 (REMOVE-EQUAL S1 X2)))))
(LIST-COUNT
X1
(REMOVE-EQUAL
S9
(REMOVE-EQUAL S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL X1 (REMOVE-EQUAL S1 X2)))))))
(+ 1 (LEN X2)))).
Subgoal *1.1.2.3.4.5.6.8.1/8
Subgoal *1.1.2.3.4.5.6.8.1/7
Subgoal *1.1.2.3.4.5.6.8.1/6
Subgoal *1.1.2.3.4.5.6.8.1/5
Subgoal *1.1.2.3.4.5.6.8.1/4
Subgoal *1.1.2.3.4.5.6.8.1/3
Subgoal *1.1.2.3.4.5.6.8.1/2
Subgoal *1.1.2.3.4.5.6.8.1/1
*1.1.2.3.4.5.6.8.1 and *1.1.2.3.4.5.6.8 are COMPLETED!
We therefore turn our attention to *1.1.2.3.4.5.6.7, which is
(IMPLIES
(AND (SUBSETP-EQUAL X (CONS S1 S14))
(NOT (SUBSETP-EQUAL X (LIST* S1 S13 S14)))
(SUBSETP-EQUAL X (LIST* S1 S11 S13 S14))
(NOT (SUBSETP-EQUAL X (LIST* S1 S9 S11 S13 S14)))
(SUBSETP-EQUAL X (LIST* S1 S7 S9 S11 S13 S14))
(NOT (SUBSETP-EQUAL X (LIST* S1 S5 S7 S9 S11 S13 S14)))
(SUBSETP-EQUAL X (LIST* S1 S3 S5 S7 S9 S11 S13 S14)))
(EQUAL
(+
(LIST-COUNT S1 X)
(LIST-COUNT S3 (REMOVE-EQUAL S1 X))
(LIST-COUNT S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X)))
(LIST-COUNT S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X))))
(LIST-COUNT
S9
(REMOVE-EQUAL S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X)))))
(LIST-COUNT
S11
(REMOVE-EQUAL
S9
(REMOVE-EQUAL S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X))))))
(LIST-COUNT
S13
(REMOVE-EQUAL
S11
(REMOVE-EQUAL
S9
(REMOVE-EQUAL S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X)))))))
(SUM
(MAP-LIST-COUNT
(REMOVE-EQUAL
S13
(REMOVE-EQUAL
S11
(REMOVE-EQUAL
S9
(REMOVE-EQUAL
S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X)))))))
S14)))
(LEN X))).
Subgoal *1.1.2.3.4.5.6.7/9
Subgoal *1.1.2.3.4.5.6.7/9'
Subgoal *1.1.2.3.4.5.6.7/9''
Subgoal *1.1.2.3.4.5.6.7/9'''
Subgoal *1.1.2.3.4.5.6.7/9'4'
Subgoal *1.1.2.3.4.5.6.7/9'5'
Subgoal *1.1.2.3.4.5.6.7/9'6'
Subgoal *1.1.2.3.4.5.6.7/9'7'
Subgoal *1.1.2.3.4.5.6.7/9'8'
Subgoal *1.1.2.3.4.5.6.7/9'9'
Subgoal *1.1.2.3.4.5.6.7/9'10'
Subgoal *1.1.2.3.4.5.6.7/9'11'
Subgoal *1.1.2.3.4.5.6.7/9'12'
Subgoal *1.1.2.3.4.5.6.7/9'13'
Subgoal *1.1.2.3.4.5.6.7/9'14'
Subgoal *1.1.2.3.4.5.6.7/9'15'
Subgoal *1.1.2.3.4.5.6.7/9'16'
Subgoal *1.1.2.3.4.5.6.7/9'17'
Subgoal *1.1.2.3.4.5.6.7/9'18'
Subgoal *1.1.2.3.4.5.6.7/9'19'
Subgoal *1.1.2.3.4.5.6.7/9'20'
Subgoal *1.1.2.3.4.5.6.7/9'21'
*1.1.2.3.4.5.6.7.1 (Subgoal *1.1.2.3.4.5.6.7/9'21') is pushed for proof
by induction.
Subgoal *1.1.2.3.4.5.6.7/8
Subgoal *1.1.2.3.4.5.6.7/8'
Subgoal *1.1.2.3.4.5.6.7/8''
Subgoal *1.1.2.3.4.5.6.7/8'''
Subgoal *1.1.2.3.4.5.6.7/8'4'
*1.1.2.3.4.5.6.7.2 (Subgoal *1.1.2.3.4.5.6.7/8'4') is pushed for proof
by induction.
Subgoal *1.1.2.3.4.5.6.7/7
Subgoal *1.1.2.3.4.5.6.7/7'
Subgoal *1.1.2.3.4.5.6.7/7''
Subgoal *1.1.2.3.4.5.6.7/7'''
Subgoal *1.1.2.3.4.5.6.7/7'4'
*1.1.2.3.4.5.6.7.3 (Subgoal *1.1.2.3.4.5.6.7/7'4') is pushed for proof
by induction.
Subgoal *1.1.2.3.4.5.6.7/6
Subgoal *1.1.2.3.4.5.6.7/6'
Subgoal *1.1.2.3.4.5.6.7/6''
Subgoal *1.1.2.3.4.5.6.7/6'''
Subgoal *1.1.2.3.4.5.6.7/6'4'
*1.1.2.3.4.5.6.7.4 (Subgoal *1.1.2.3.4.5.6.7/6'4') is pushed for proof
by induction.
Subgoal *1.1.2.3.4.5.6.7/5
Subgoal *1.1.2.3.4.5.6.7/5'
Subgoal *1.1.2.3.4.5.6.7/5''
Subgoal *1.1.2.3.4.5.6.7/5'''
Subgoal *1.1.2.3.4.5.6.7/5'4'
*1.1.2.3.4.5.6.7.5 (Subgoal *1.1.2.3.4.5.6.7/5'4') is pushed for proof
by induction.
Subgoal *1.1.2.3.4.5.6.7/4
Subgoal *1.1.2.3.4.5.6.7/4'
Subgoal *1.1.2.3.4.5.6.7/4''
Subgoal *1.1.2.3.4.5.6.7/4'''
Subgoal *1.1.2.3.4.5.6.7/4'4'
*1.1.2.3.4.5.6.7.6 (Subgoal *1.1.2.3.4.5.6.7/4'4') is pushed for proof
by induction.
Subgoal *1.1.2.3.4.5.6.7/3
Subgoal *1.1.2.3.4.5.6.7/3'
Subgoal *1.1.2.3.4.5.6.7/3''
Subgoal *1.1.2.3.4.5.6.7/3'''
Subgoal *1.1.2.3.4.5.6.7/3'4'
*1.1.2.3.4.5.6.7.7 (Subgoal *1.1.2.3.4.5.6.7/3'4') is pushed for proof
by induction.
Subgoal *1.1.2.3.4.5.6.7/2
Subgoal *1.1.2.3.4.5.6.7/2'
Subgoal *1.1.2.3.4.5.6.7/2''
Subgoal *1.1.2.3.4.5.6.7/2'''
Subgoal *1.1.2.3.4.5.6.7/2'4'
*1.1.2.3.4.5.6.7.8 (Subgoal *1.1.2.3.4.5.6.7/2'4') is pushed for proof
by induction.
Subgoal *1.1.2.3.4.5.6.7/1
Subgoal *1.1.2.3.4.5.6.7/1'
Subgoal *1.1.2.3.4.5.6.7/1''
*1.1.2.3.4.5.6.7.9 (Subgoal *1.1.2.3.4.5.6.7/1'') is pushed for proof
by induction.
So we now return to *1.1.2.3.4.5.6.7.9, which is
(IMPLIES
(AND (NOT (CONSP S14))
(SUBSETP-EQUAL X (CONS S1 S14))
(NOT (SUBSETP-EQUAL X (LIST* S1 S13 S14)))
(SUBSETP-EQUAL X (LIST* S1 S11 S13 S14))
(NOT (SUBSETP-EQUAL X (LIST* S1 S9 S11 S13 S14)))
(SUBSETP-EQUAL X (LIST* S1 S7 S9 S11 S13 S14))
(NOT (SUBSETP-EQUAL X (LIST* S1 S5 S7 S9 S11 S13 S14)))
(SUBSETP-EQUAL X (LIST* S1 S3 S5 S7 S9 S11 S13 S14)))
(EQUAL
(+
(LIST-COUNT S1 X)
(LIST-COUNT S3 (REMOVE-EQUAL S1 X))
(LIST-COUNT S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X)))
(LIST-COUNT S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X))))
(LIST-COUNT
S9
(REMOVE-EQUAL S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X)))))
(LIST-COUNT
S11
(REMOVE-EQUAL
S9
(REMOVE-EQUAL S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X))))))
(LIST-COUNT
S13
(REMOVE-EQUAL
S11
(REMOVE-EQUAL
S9
(REMOVE-EQUAL S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X))))))))
(LEN X))).
Subgoal *1.1.2.3.4.5.6.7.9/9
Subgoal *1.1.2.3.4.5.6.7.9/8
Subgoal *1.1.2.3.4.5.6.7.9/7
Subgoal *1.1.2.3.4.5.6.7.9/6
Subgoal *1.1.2.3.4.5.6.7.9/5
Subgoal *1.1.2.3.4.5.6.7.9/4
Subgoal *1.1.2.3.4.5.6.7.9/3
Subgoal *1.1.2.3.4.5.6.7.9/2
Subgoal *1.1.2.3.4.5.6.7.9/1
*1.1.2.3.4.5.6.7.9 is COMPLETED!
We therefore turn our attention to *1.1.2.3.4.5.6.7.8, which is
(IMPLIES
(AND (NOT (SUBSETP-EQUAL X (CONS S1 S16)))
(SUBSETP-EQUAL X (LIST* S1 S15 S16))
(NOT (SUBSETP-EQUAL X (LIST* S1 S13 S15 S16)))
(SUBSETP-EQUAL X (LIST* S1 S11 S13 S15 S16))
(NOT (SUBSETP-EQUAL X (LIST* S1 S9 S11 S13 S15 S16)))
(SUBSETP-EQUAL X (LIST* S1 S7 S9 S11 S13 S15 S16))
(NOT (SUBSETP-EQUAL X (LIST* S1 S5 S7 S9 S11 S13 S15 S16)))
(SUBSETP-EQUAL X
(LIST* S1 S3 S5 S7 S9 S11 S13 S15 S16)))
(EQUAL
(+
(LIST-COUNT S1 X)
(LIST-COUNT S3 (REMOVE-EQUAL S1 X))
(LIST-COUNT S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X)))
(LIST-COUNT S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X))))
(LIST-COUNT
S9
(REMOVE-EQUAL S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X)))))
(LIST-COUNT
S11
(REMOVE-EQUAL
S9
(REMOVE-EQUAL S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X))))))
(LIST-COUNT
S13
(REMOVE-EQUAL
S11
(REMOVE-EQUAL
S9
(REMOVE-EQUAL S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X)))))))
(LIST-COUNT
S15
(REMOVE-EQUAL
S13
(REMOVE-EQUAL
S11
(REMOVE-EQUAL
S9
(REMOVE-EQUAL
S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X))))))))
(SUM
(MAP-LIST-COUNT
(REMOVE-EQUAL
S15
(REMOVE-EQUAL
S13
(REMOVE-EQUAL
S11
(REMOVE-EQUAL
S9
(REMOVE-EQUAL
S7
(REMOVE-EQUAL S5
(REMOVE-EQUAL S3 (REMOVE-EQUAL S1 X))))))))
S16)))
(LEN X))).
Subgoal *1.1.2.3.4.5.6.7.8/10
Subgoal *1.1.2.3.4.5.6.7.8/10'
Subgoal *1.1.2.3.4.5.6.7.8/10''
Subgoal *1.1.2.3.4.5.6.7.8/10'''
Subgoal *1.1.2.3.4.5.6.7.8/10'4'
Subgoal *1.1.2.3.4.5.6.7.8/10'5'
Subgoal *1.1.2.3.4.5.6.7.8/10'6'
Subgoal *1.1.2.3.4.5.6.7.8/10'7'
Subgoal *1.1.2.3.4.5.6.7.8/10'8'
Subgoal *1.1.2.3.4.5.6.7.8/10'9'
Subgoal *1.1.2.3.4.5.6.7.8/10'10'
Subgoal *1.1.2.3.4.5.6.7.8/10'11'
Subgoal *1.1.2.3.4.5.6.7.8/10'12'
Subgoal *1.1.2.3.4.5.6.7.8/10'13'
Subgoal *1.1.2.3.4.5.6.7.8/10'14'
Subgoal *1.1.2.3.4.5.6.7.8/10'15'
Subgoal *1.1.2.3.4.5.6.7.8/10'16'
Subgoal *1.1.2.3.4.5.6.7.8/10'17'
Subgoal *1.1.2.3.4.5.6.7.8/10'18'
Subgoal *1.1.2.3.4.5.6.7.8/10'19'
Subgoal *1.1.2.3.4.5.6.7.8/10'20'
Subgoal *1.1.2.3.4.5.6.7.8/10'21'
Subgoal *1.1.2.3.4.5.6.7.8/10'22'
Subgoal *1.1.2.3.4.5.6.7.8/10'23'
Subgoal *1.1.2.3.4.5.6.7.8/10'24'
Normally we would attempt to prove Subgoal *1.1.2.3.4.5.6.7.8/10'24'
by induction. However, that would cause the induction-depth-limit
of 9 to be exceeded. See :DOC induction-depth-limit.
Summary
Form: ( DEFTHM SUM-MAP-COUNT-LIST ...)
Rules: ((:DEFINITION ENDP)
(:DEFINITION FIX)
(:DEFINITION LEN)
(:DEFINITION LIST-COUNT)
(:DEFINITION MAP-LIST-COUNT)
(:DEFINITION MEMBER-EQUAL)
(:DEFINITION NOT)
(:DEFINITION REMOVE-EQUAL)
(:DEFINITION SUBSETP-EQUAL)
(:DEFINITION SUM)
(:DEFINITION SYNP)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART BINARY-+)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART SUM)
(:EXECUTABLE-COUNTERPART TAU-SYSTEM)
(:FAKE-RUNE-FOR-LINEAR NIL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION LEN)
(:INDUCTION LIST-COUNT)
(:INDUCTION MAP-LIST-COUNT)
(:INDUCTION REMOVE-EQUAL)
(:INDUCTION SUBSETP-EQUAL)
(:REWRITE ASSOCIATIVITY-OF-+)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE COMMUTATIVITY-2-OF-+)
(:REWRITE COMMUTATIVITY-OF-+)
(:REWRITE CONS-CAR-CDR)
(:REWRITE FOLD-CONSTS-IN-+)
(:REWRITE SUBSETP-REMOVE-CONS)
(:REWRITE UNICITY-OF-0)
(:TYPE-PRESCRIPTION LEN)
(:TYPE-PRESCRIPTION LIST-COUNT)
(:TYPE-PRESCRIPTION MAP-LIST-COUNT)
(:TYPE-PRESCRIPTION REMOVE-EQUAL)
(:TYPE-PRESCRIPTION SUBSETP-EQUAL))
Splitter rules (see :DOC splitter):
if-intro: ((:DEFINITION LIST-COUNT)
(:DEFINITION MEMBER-EQUAL)
(:DEFINITION REMOVE-EQUAL)
(:DEFINITION SUBSETP-EQUAL))
Time: 0.94 seconds (prove: 0.91, print: 0.03, other: 0.00)
Prover steps counted: 667560
---
The key checkpoint goals, below, may help you to debug this failure.
See :DOC failure and see :DOC set-checkpoint-summary-limit.
---
*** Key checkpoint at the top level: ***
Goal
(IMPLIES (LET ((Y S))
(MBE :LOGIC (PROG2$ (SUBSETP-EQL-EXEC$GUARD-CHECK X Y)
(SUBSETP-EQUAL X Y))
:EXEC (SUBSETP-EQL-EXEC X Y)))
(EQUAL (SUM (MAP-LIST-COUNT X S))
(LEN X)))
*** Key checkpoint under a top-level induction
before the induction-depth-limit stopped the proof attempt: ***
Subgoal *1/2''
(IMPLIES (AND (CONSP S)
(EQUAL (SUM (MAP-LIST-COUNT (REMOVE-EQUAL (CAR S) X)
(CDR S)))
(LEN (REMOVE-EQUAL (CAR S) X)))
(SUBSETP-EQUAL X S))
(EQUAL (+ (LIST-COUNT (CAR S) X)
(LEN (REMOVE-EQUAL (CAR S) X)))
(LEN X)))
ACL2 Error in ( DEFTHM SUM-MAP-COUNT-LIST ...): See :DOC failure.
******** FAILED ********
Subgoal *1/2'' の (LEN (REMOVE-EQUAL (CAR S) X)) に注目しましょう。
どうにかして remove を除去できれば式を簡約できそうな感じがします(直感)。
(len (remove e x)) の長さは (len x) から x に含まれている e の数を引いた数です。
すなわち、 (- (len x) (list-count e x)) です。
お、これはちょうど (LEN (REMOVE-EQUAL (CAR S) X)) のところにはまると
(LEN X) と一致しますね。これはラッキーです。
ということで下記を証明します。
(defthm len-remove
(equal (len (remove e x))
(- (len x) (list-count e x))))
証明成功: 出力を確認する
Goal'
([ A key checkpoint:
Goal'
(EQUAL (LEN (REMOVE-EQUAL E X))
(+ (LEN X) (- (LIST-COUNT E X))))
*1 (Goal') is pushed for proof by induction.
])
Perhaps we can prove *1 by induction. Three induction schemes are
suggested by this conjecture. Subsumption reduces that number to two.
These merge into one derived induction scheme.
We will induct according to a scheme suggested by (LEN X), but modified
to accommodate (LIST-COUNT E X). These suggestions were produced using
the :induction rules LEN, LIST-COUNT and REMOVE-EQUAL. If we let (:P E X)
denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP X)) (:P E X))
(IMPLIES (AND (CONSP X) (:P E (CDR X)))
(:P E X))).
This induction is justified by the same argument used to admit LEN.
When applied to the goal at hand the above induction scheme produces
two nontautological subgoals.
Subgoal *1/2
Subgoal *1/1
Splitter note (see :DOC splitter) for Subgoal *1/1 (2 subgoals).
if-intro: ((:DEFINITION LIST-COUNT)
(:DEFINITION REMOVE-EQUAL))
Subgoal *1/1.2
Subgoal *1/1.1
*1 is COMPLETED!
Thus key checkpoint Goal' is COMPLETED!
Q.E.D.
Summary
Form: ( DEFTHM LEN-REMOVE ...)
Rules: ((:DEFINITION LEN)
(:DEFINITION LIST-COUNT)
(:DEFINITION NOT)
(:DEFINITION REMOVE-EQL-EXEC$GUARD-CHECK)
(:DEFINITION REMOVE-EQUAL)
(:DEFINITION RETURN-LAST)
(:EXECUTABLE-COUNTERPART BINARY-+)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART LEN)
(:EXECUTABLE-COUNTERPART TAU-SYSTEM)
(:EXECUTABLE-COUNTERPART UNARY--)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION LEN)
(:INDUCTION LIST-COUNT)
(:INDUCTION REMOVE-EQUAL)
(:REWRITE ASSOCIATIVITY-OF-+)
(:REWRITE CDR-CONS)
(:REWRITE DISTRIBUTIVITY-OF-MINUS-OVER-+)
(:TYPE-PRESCRIPTION REMOVE-EQUAL))
Splitter rules (see :DOC splitter):
if-intro: ((:DEFINITION LIST-COUNT)
(:DEFINITION REMOVE-EQUAL))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 710
LEN-REMOVE
では再度 sum-map-count-list の証明を試みます。
(defthm sum-map-count-list
(implies (subsetp x s)
(equal (sum (map-list-count x s))
(len x)))
:hints (("Goal" :induct (map-list-count x s))))
証明成功: 出力を確認する
*1 (the initial Goal, a key checkpoint) is pushed for proof by induction.
We have been told to use induction. One induction scheme is suggested
by the induction hint.
We will induct according to a scheme suggested by (MAP-LIST-COUNT X S).
This suggestion was produced using the :induction rule MAP-LIST-COUNT.
If we let (:P S X) denote *1 above then the induction scheme we'll
use is
(AND (IMPLIES (AND (NOT (ENDP S))
(:P (CDR S) (REMOVE-EQUAL (CAR S) X)))
(:P S X))
(IMPLIES (ENDP S) (:P S X))).
This induction is justified by the same argument used to admit
MAP-LIST-COUNT. Note, however, that the unmeasured variable X is being
instantiated. When applied to the goal at hand the above induction
scheme produces two nontautological subgoals.
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/1
Subgoal *1/1'
*1 is COMPLETED!
Thus key checkpoint Goal is COMPLETED!
Q.E.D.
Summary
Form: ( DEFTHM SUM-MAP-COUNT-LIST ...)
Rules: ((:DEFINITION ENDP)
(:DEFINITION FIX)
(:DEFINITION LEN)
(:DEFINITION MAP-LIST-COUNT)
(:DEFINITION MEMBER-EQUAL)
(:DEFINITION NOT)
(:DEFINITION SUBSETP-EQUAL)
(:DEFINITION SUM)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART SUM)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION MAP-LIST-COUNT)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE COMMUTATIVITY-2-OF-+)
(:REWRITE COMMUTATIVITY-OF-+)
(:REWRITE CONS-CAR-CDR)
(:REWRITE INVERSE-OF-+)
(:REWRITE LEN-REMOVE)
(:REWRITE SUBSETP-REMOVE-CONS)
(:REWRITE UNICITY-OF-0)
(:TYPE-PRESCRIPTION LEN)
(:TYPE-PRESCRIPTION MAP-LIST-COUNT)
(:TYPE-PRESCRIPTION SUBSETP-EQUAL))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 463
SUM-MAP-COUNT-LIST
やりました。これでピースは揃いました。
8. pigeonhole 定理の証明
pigeonhole の定理を証明します。
(defthm pigeonhole
(implies (and (subsetp x s)
(< (len s) (len x))
(no-duplicatesp s))
(not (no-duplicatesp x)))
:rule-classes ((:rewrite :match-free :all)))
証明成功: 出力を確認する
Goal'
Q.E.D.
Summary
Form: ( DEFTHM PIGEONHOLE ...)
Rules: ((:DEFINITION NO-DUPLICATESP-EQL-EXEC$GUARD-CHECK)
(:DEFINITION NOT)
(:DEFINITION RETURN-LAST)
(:DEFINITION SUBSETP-EQL-EXEC$GUARD-CHECK)
(:FAKE-RUNE-FOR-LINEAR NIL)
(:REWRITE LEN-MAP-LIST-COUNT)
(:REWRITE MEMBER-IF-OVER-1-MAP-LIST-COUNT-IS-DUPLICATED)
(:REWRITE NUMERIC-PIGEONHOLE)
(:REWRITE SUM-MAP-COUNT-LIST)
(:TYPE-PRESCRIPTION LEN)
(:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL)
(:TYPE-PRESCRIPTION SUBSETP-EQUAL))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 345
PIGEONHOLE
証明できました！やりましたね！ こうやって一見無理そうな定理も頑張れば証明できるものなのです(場合による)！
9. pigeonhole で遊ぶ
ある学校で校長先生の話を聞いている生徒が 367 人以上いるとします。 この生徒の誕生日に必ず重複があることを証明します。 誕生日は閏年を考慮し366日あるとします。
まず誕生日IDを 366 個用意します。
(defun nats-below (n) (if (zp n) 0 (cons (- n 1) (nats-below (- n 1)))))
出力を確認する
The admission of NATS-BELOW is trivial, using the relation O< (which
is known to be well-founded on the domain recognized by O-P) and the
measure (ACL2-COUNT N). We observe that the type of NATS-BELOW is
described by the theorem
(OR (EQUAL (NATS-BELOW N) 0)
(AND (CONSP (NATS-BELOW N))
(NOT (TRUE-LISTP (NATS-BELOW N))))).
We used primitive type reasoning.
Summary
Form: ( DEFUN NATS-BELOW ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
NATS-BELOW
(defconst *birthday-ids* (nats-below 366))
出力を確認する
Summary Form: ( DEFCONST *BIRTHDAY-IDS* ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) *BIRTHDAY-IDS*
*birthday-ids* の数が 366 でかつ重複もないことを確認します。
(thm (and (equal (len *birthday-ids*) 366)
(no-duplicatesp *birthday-ids*)))
証明成功: 出力を確認する
Q.E.D.
Summary
Form: ( THM ...)
Rules: ((:DEFINITION RETURN-LAST)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART IF)
(:EXECUTABLE-COUNTERPART LEN)
(:EXECUTABLE-COUNTERPART NO-DUPLICATESP-EQL-EXEC$GUARD-CHECK)
(:EXECUTABLE-COUNTERPART NO-DUPLICATESP-EQUAL)
(:EXECUTABLE-COUNTERPART RETURN-LAST))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 15
Proof succeeded.
では定理を証明します。
(defthm duplicates-birthdays
(implies (and (subsetp birthdays-of-student *birthday-ids*)
(< 366 (len birthdays-of-student)))
(not (no-duplicatesp birthdays-of-student))))
出力を確認する
Goal'
HARD ACL2 ERROR in REWRITE: The call depth limit of 1000 has been
exceeded in the ACL2 rewriter. To see why the limit was exceeded,
first execute
:brr t
and then try the proof again, and then execute the form (cw-gstack)
or, for less verbose output, instead try (cw-gstack :frames 30). You
may then notice a loop caused by some set of enabled rules, some of
which you can then disable; see :DOC disable. For a possible solution
when there is not a loop, see :DOC rewrite-stack-limit.
ACL2 Error in TOP-LEVEL: Evaluation aborted. To debug see :DOC print-
gv, see :DOC trace, and see :DOC wet.
Rules: ((:DEFINITION NO-DUPLICATESP-EQL-EXEC$GUARD-CHECK)
(:DEFINITION NOT)
(:DEFINITION RETURN-LAST)
(:DEFINITION SUBSETP-EQL-EXEC$GUARD-CHECK))
Here is the current pstack [see :DOC pstack]:
(REWRITE-ATM SIMPLIFY-CLAUSE WATERFALL)
*** Note: No checkpoints to print. ***
証明に失敗したので pigeonhole を使うようにヒントを与えます。
(defthm duplicates-birthdays
(implies (and (subsetp birthdays-of-student *birthday-ids*)
(< 366 (len birthdays-of-student)))
(not (no-duplicatesp birthdays-of-student)))
:hints (("Goal" :in-theory (disable pigeonhole)
:use ((:instance pigeonhole
(x birthdays-of-student)
(s *birthday-ids*))))))
証明成功: 出力を確認する
Goal'
Goal''
Q.E.D.
Summary
Form: ( DEFTHM DUPLICATES-BIRTHDAYS ...)
Rules: ((:DEFINITION NO-DUPLICATESP-EQL-EXEC$GUARD-CHECK)
(:DEFINITION NOT)
(:DEFINITION RETURN-LAST)
(:DEFINITION SUBSETP-EQL-EXEC$GUARD-CHECK)
(:EXECUTABLE-COUNTERPART LEN)
(:EXECUTABLE-COUNTERPART NO-DUPLICATESP-EQL-EXEC$GUARD-CHECK)
(:EXECUTABLE-COUNTERPART NO-DUPLICATESP-EQUAL)
(:EXECUTABLE-COUNTERPART RETURN-LAST))
Hint-events: ((:USE PIGEONHOLE))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 119
DUPLICATES-BIRTHDAYS
証明できました！
10. おわりに
鳩の巣の原理をこだわりの方法で表現することができました。 この記事では再帰関数の停止性や関数のガードの話はでてきませんでしたが、 帰納法で使用する induction scheme の選択、 補助定理の作成、定理証明のための補助関数など ACL2 を使うための色々なテクニックについて紹介することができました。 説明は色々不足しているところがあると思うのですが、 この記事を読めばだいたい雰囲気は掴めるかなーという感じがします。
ACL2 のコード自体は私の記事でなくても読むことはできますが、 ACL2 は自動証明に失敗したときに得られる情報を使って定理を書くので失敗を追体験できる形になっているこの文書にはある程度の価値があると思っています。
私の記事だけ読んで ACL2 を実際に使い始めるのは正直現実的ではないと思うので、 面白そうだなと思った人は是非 ACL2 - ACL2-tutorial で勉強を始めてみてください。
この記事を読んだ方は既に感じていると思うのですが、ACL2 は自動証明をするし証明の過程が具体的にどうなっているのかは出力を見てもよく分からないので ACL2 を始める前に 『定理証明手習い』 – 技術書出版と販売のラムダノート を先に読み、手動で定理を証明しながら定理証明について学ぶのがおすすめです。 手動で証明を一度やっていれば ACL2 によって自動証明されてもそれに違和感を覚えることはなくなると思います。
日本語圏の ACL2 ユーザーを増やすきっかけになれば幸いです。