Skip to content

Commit f9d5378

Browse files
jkingdonjkingdon
authored
Add big-unifier-bad1.mm test (#65)
This is taken from the metamath-tests repository and would have been in the previous metamath-tests change except that I didn't yet understand the set scroll continuous issue then.
1 parent 296f66c commit f9d5378

File tree

3 files changed

+187
-0
lines changed

3 files changed

+187
-0
lines changed

‎tests/big-unifier-bad1.expected‎

Lines changed: 86 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,86 @@
1+
MM> READ "big-unifier-bad1.mm"
2+
Reading source file "big-unifier-bad1.mm"... 3369 bytes
3+
3369 bytes were read into the source buffer.
4+
The source has 28 statements; 4 are $a and 1 are $p.
5+
No errors were found. However, proofs were not checked. Type VERIFY PROOF *
6+
if you want to check them.
7+
MM> Continuous scrolling is now in effect.
8+
MM> 0 10% 20% 30% 40% 50% 60% 70% 80% 90% 100%
9+
..................................................
10+
?Error on line 68 of file "big-unifier-bad1.mm" at statement 28, label
11+
"theorem1", type "$p":
12+
FFZMPAFFZFPFQPFZFLRFFLNKMJAJNQPLAPGPMKBADCEOARLIH $.
13+
^
14+
The hypotheses of statement "ax-mp" at proof step 82 cannot be unified.
15+
Hypothesis 1: wff x
16+
Step 78: wff e ( e ( e ( x , e ( y , e ( e ( e ( y , z ) , e ( u , z ) ) , u
17+
) ) ) , e ( e ( e ( e ( x , e ( y , e ( e ( e ( y , z ) , e ( u , z ) ) , u ) )
18+
) , e ( e ( e ( e ( x , e ( y , e ( e ( e ( y , z ) , e ( u , z ) ) , u ) ) ) ,
19+
v ) , e ( x , v ) ) , x ) ) , e ( e ( y , e ( e ( e ( y , z ) , e ( u , z ) ) ,
20+
u ) ) , e ( e ( e ( e ( x , e ( y , e ( e ( e ( y , z ) , e ( u , z ) ) , u ) )
21+
) , v ) , e ( x , v ) ) , x ) ) ) , e ( y , e ( e ( e ( y , z ) , e ( u , z ) )
22+
, u ) ) ) ) , e ( e ( e ( x , e ( y , e ( e ( e ( y , z ) , e ( u , z ) ) , u )
23+
) ) , e ( e ( e ( e ( x , e ( y , e ( e ( e ( y , z ) , e ( u , z ) ) , u ) ) )
24+
, v ) , e ( x , v ) ) , x ) ) , e ( e ( y , e ( e ( e ( y , z ) , e ( u , z ) )
25+
, u ) ) , e ( e ( e ( e ( x , e ( y , e ( e ( e ( y , z ) , e ( u , z ) ) , u )
26+
) ) , v ) , e ( x , v ) ) , x ) ) ) )
27+
Hypothesis 2: wff y
28+
Step 79: wff x
29+
Hypothesis 3: |- x
30+
Step 80: wff e ( e ( e ( e ( e ( e ( x , e ( y , e ( e ( e ( y , z ) , e ( u
31+
, z ) ) , u ) ) ) , v ) , e ( x , v ) ) , x ) , e ( e ( e ( e ( e ( e ( x , e (
32+
y , e ( e ( e ( y , z ) , e ( u , z ) ) , u ) ) ) , e ( e ( e ( e ( x , e ( y ,
33+
e ( e ( e ( y , z ) , e ( u , z ) ) , u ) ) ) , v ) , e ( x , v ) ) , x ) ) , e
34+
( e ( y , e ( e ( e ( y , z ) , e ( u , z ) ) , u ) ) , e ( e ( e ( e ( x , e (
35+
y , e ( e ( e ( y , z ) , e ( u , z ) ) , u ) ) ) , v ) , e ( x , v ) ) , x ) )
36+
) , e ( e ( e ( x , e ( y , e ( e ( e ( y , z ) , e ( u , z ) ) , u ) ) ) , e (
37+
e ( e ( e ( x , e ( y , e ( e ( e ( y , z ) , e ( u , z ) ) , u ) ) ) , e ( e (
38+
e ( e ( x , e ( y , e ( e ( e ( y , z ) , e ( u , z ) ) , u ) ) ) , v ) , e ( x
39+
, v ) ) , x ) ) , e ( e ( y , e ( e ( e ( y , z ) , e ( u , z ) ) , u ) ) , e (
40+
e ( e ( e ( x , e ( y , e ( e ( e ( y , z ) , e ( u , z ) ) , u ) ) ) , v ) , e
41+
( x , v ) ) , x ) ) ) , e ( y , e ( e ( e ( y , z ) , e ( u , z ) ) , u ) ) ) )
42+
, e ( e ( e ( x , e ( y , e ( e ( e ( y , z ) , e ( u , z ) ) , u ) ) ) , e ( e
43+
( e ( e ( x , e ( y , e ( e ( e ( y , z ) , e ( u , z ) ) , u ) ) ) , v ) , e (
44+
x , v ) ) , x ) ) , e ( e ( y , e ( e ( e ( y , z ) , e ( u , z ) ) , u ) ) , e
45+
( e ( e ( e ( x , e ( y , e ( e ( e ( y , z ) , e ( u , z ) ) , u ) ) ) , v ) ,
46+
e ( x , v ) ) , x ) ) ) ) ) , e ( x , e ( e ( e ( x , e ( y , e ( e ( e ( y , z
47+
) , e ( u , z ) ) , u ) ) ) , e ( e ( e ( e ( x , e ( y , e ( e ( e ( y , z ) ,
48+
e ( u , z ) ) , u ) ) ) , e ( e ( e ( e ( x , e ( y , e ( e ( e ( y , z ) , e (
49+
u , z ) ) , u ) ) ) , v ) , e ( x , v ) ) , x ) ) , e ( e ( y , e ( e ( e ( y ,
50+
z ) , e ( u , z ) ) , u ) ) , e ( e ( e ( e ( x , e ( y , e ( e ( e ( y , z ) ,
51+
e ( u , z ) ) , u ) ) ) , v ) , e ( x , v ) ) , x ) ) ) , e ( y , e ( e ( e ( y
52+
, z ) , e ( u , z ) ) , u ) ) ) ) , e ( e ( e ( x , e ( y , e ( e ( e ( y , z )
53+
, e ( u , z ) ) , u ) ) ) , e ( e ( e ( e ( x , e ( y , e ( e ( e ( y , z ) , e
54+
( u , z ) ) , u ) ) ) , v ) , e ( x , v ) ) , x ) ) , e ( e ( y , e ( e ( e ( y
55+
, z ) , e ( u , z ) ) , u ) ) , e ( e ( e ( e ( x , e ( y , e ( e ( e ( y , z )
56+
, e ( u , z ) ) , u ) ) ) , v ) , e ( x , v ) ) , x ) ) ) ) ) ) , x ) ) , e ( e
57+
( e ( e ( e ( x , e ( y , e ( e ( e ( y , z ) , e ( u , z ) ) , u ) ) ) , e ( e
58+
( e ( e ( x , e ( y , e ( e ( e ( y , z ) , e ( u , z ) ) , u ) ) ) , v ) , e (
59+
x , v ) ) , x ) ) , e ( e ( y , e ( e ( e ( y , z ) , e ( u , z ) ) , u ) ) , e
60+
( e ( e ( e ( x , e ( y , e ( e ( e ( y , z ) , e ( u , z ) ) , u ) ) ) , v ) ,
61+
e ( x , v ) ) , x ) ) ) , e ( e ( e ( x , e ( y , e ( e ( e ( y , z ) , e ( u ,
62+
z ) ) , u ) ) ) , e ( e ( e ( e ( x , e ( y , e ( e ( e ( y , z ) , e ( u , z )
63+
) , u ) ) ) , e ( e ( e ( e ( x , e ( y , e ( e ( e ( y , z ) , e ( u , z ) ) ,
64+
u ) ) ) , v ) , e ( x , v ) ) , x ) ) , e ( e ( y , e ( e ( e ( y , z ) , e ( u
65+
, z ) ) , u ) ) , e ( e ( e ( e ( x , e ( y , e ( e ( e ( y , z ) , e ( u , z )
66+
) , u ) ) ) , v ) , e ( x , v ) ) , x ) ) ) , e ( y , e ( e ( e ( y , z ) , e (
67+
u , z ) ) , u ) ) ) ) , e ( e ( e ( x , e ( y , e ( e ( e ( y , z ) , e ( u , z
68+
) ) , u ) ) ) , e ( e ( e ( e ( x , e ( y , e ( e ( e ( y , z ) , e ( u , z ) )
69+
, u ) ) ) , v ) , e ( x , v ) ) , x ) ) , e ( e ( y , e ( e ( e ( y , z ) , e (
70+
u , z ) ) , u ) ) , e ( e ( e ( e ( x , e ( y , e ( e ( e ( y , z ) , e ( u , z
71+
) ) , u ) ) ) , v ) , e ( x , v ) ) , x ) ) ) ) ) , e ( x , e ( e ( e ( x , e (
72+
y , e ( e ( e ( y , z ) , e ( u , z ) ) , u ) ) ) , e ( e ( e ( e ( x , e ( y ,
73+
e ( e ( e ( y , z ) , e ( u , z ) ) , u ) ) ) , e ( e ( e ( e ( x , e ( y , e (
74+
e ( e ( y , z ) , e ( u , z ) ) , u ) ) ) , v ) , e ( x , v ) ) , x ) ) , e ( e
75+
( y , e ( e ( e ( y , z ) , e ( u , z ) ) , u ) ) , e ( e ( e ( e ( x , e ( y ,
76+
e ( e ( e ( y , z ) , e ( u , z ) ) , u ) ) ) , v ) , e ( x , v ) ) , x ) ) ) ,
77+
e ( y , e ( e ( e ( y , z ) , e ( u , z ) ) , u ) ) ) ) , e ( e ( e ( x , e ( y
78+
, e ( e ( e ( y , z ) , e ( u , z ) ) , u ) ) ) , e ( e ( e ( e ( x , e ( y , e
79+
( e ( e ( y , z ) , e ( u , z ) ) , u ) ) ) , v ) , e ( x , v ) ) , x ) ) , e (
80+
e ( y , e ( e ( e ( y , z ) , e ( u , z ) ) , u ) ) , e ( e ( e ( e ( x , e ( y
81+
, e ( e ( e ( y , z ) , e ( u , z ) ) , u ) ) ) , v ) , e ( x , v ) ) , x ) ) )
82+
) ) ) )
83+
Hypothesis 4: |- e ( x , y )
84+
Step 81: wff e ( e ( e ( x , e ( y , e ( e ( e ( y , z ) , e ( u , z ) ) , u
85+
) ) ) , v ) , e ( x , v ) )
86+

‎tests/big-unifier-bad1.in‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
verify proof *

‎tests/big-unifier-bad1.mm‎

Lines changed: 100 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,100 @@
1+
$( big-unifier.mm - Version of 30-Aug-2008
2+
3+
PUBLIC DOMAIN
4+
5+
This file (specifically, the version of this file with the above date)
6+
has been placed in the Public Domain per the Creative Commons Public
7+
Domain Dedication. http://creativecommons.org/licenses/publicdomain/
8+
9+
The public domain release applies worldwide. In case this is not
10+
legally possible, the right is granted to use the work for any purpose,
11+
without any conditions, unless such conditions are required by law.
12+
13+
Norman Megill - http://metamath.org $)
14+
15+
$(
16+
17+
This file (big-unifier.mm) is a unification and substitution test for
18+
Metamath verifiers, where small input expressions blow up to thousands
19+
of symbols. It is a translation of William McCune's "big-unifier.in"
20+
for the OTTER theorem prover:
21+
22+
http://www-unix.mcs.anl.gov/AR/award-2003/big-unifier.in
23+
http://www-unix.mcs.anl.gov/AR/award-2003/big-unifier.out
24+
25+
Description: "Examples of complicated substitutions in condensed
26+
detachment. These occur in Larry Wos's proofs that XCB is a single
27+
axiom for EC."
28+
$)
29+
30+
31+
$c wff |- e ( , ) $.
32+
$v x y z w v u v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 $.
33+
34+
wx $f wff x $. wy $f wff y $. wz $f wff z $. ww $f wff w $.
35+
wv $f wff v $. wu $f wff u $. wv1 $f wff v1 $. wv2 $f wff v2 $.
36+
wv3 $f wff v3 $. wv4 $f wff v4 $. wv5 $f wff v5 $. wv6 $f wff v6 $.
37+
wv7 $f wff v7 $. wv8 $f wff v8 $. wv9 $f wff v9 $. wv10 $f wff v10 $.
38+
wv11 $f wff v11 $.
39+
40+
$( The binary connective of the language "EC". $)
41+
wi $a wff e ( x , y ) $.
42+
43+
${
44+
ax-mp.1 $e |- x $.
45+
ax-mp.2 $e |- e ( x , y ) $.
46+
$( The inference rule. $)
47+
ax-mp $a |- y $.
48+
$}
49+
50+
$( The first axiom. $)
51+
ax-maj $a |- e ( e ( e ( e ( e ( x , e ( y , e ( e ( e ( e ( e ( z , e (
52+
e ( e ( z , u ) , e ( v , u ) ) , v ) ) , e ( e ( w , e ( e ( e ( w , v6
53+
) , e ( v7 , v6 ) ) , v7 ) ) , y ) ) , v8 ) , e ( v9 , v8 ) ) , v9 ) ) )
54+
, x ) , v10 ) , e ( v11 , v10 ) ) , v11 ) $.
55+
56+
$( The second axiom. $)
57+
ax-min $a |- e ( e ( e ( e ( e ( e ( x , e ( e ( y , e ( e ( e ( y , z )
58+
, e ( u , z ) ) , u ) ) , x ) ) , e ( v , e ( e ( e ( v , w ) , e ( v6 ,
59+
w ) ) , v6 ) ) ) , v7 ) , v8 ) , e ( v7 , v8 ) ) , e ( v9 , e ( e ( e (
60+
v9 , v10 ) , e ( v11 , v10 ) ) , v11 ) ) ) $.
61+
62+
$( A 3-step proof that applies ~ ax-mp to the two axioms. The proof was
63+
saved in compressed format with "save proof theorem1 /compressed" in
64+
the metamath program. $)
65+
theorem1 $p |- e ( e ( e ( x , e ( y , e ( e ( e ( y , z ) , e ( u , z ) )
66+
, u ) ) ) , v ) , e ( x , v ) ) $=
67+
( wi ax-min ax-maj ax-mp ) ABBCFECFFEFFZFZKDFADFFZAFZFJMFFZKNJFFNFZFAO
68+
FFZMPAFFZFPFQPFZFLRFFLNKMJAJNQPLAPGPMKBADCEOARLIH $.
69+
70+
$(
71+
72+
This comment holds a simple typesetting definition file so that HTML
73+
pages can be created with "show statement theorem1/html" in the
74+
metamath program.
75+
76+
$t
77+
htmldef "(" as " ( ";
78+
htmldef ")" as " ) ";
79+
htmldef "e" as " e ";
80+
htmldef "wff" as " wff ";
81+
htmldef "|-" as " |- ";
82+
htmldef "," as " , ";
83+
htmldef "x" as " x ";
84+
htmldef "y" as " y ";
85+
htmldef "z" as " z ";
86+
htmldef "w" as " w ";
87+
htmldef "v" as " v ";
88+
htmldef "u" as " u ";
89+
htmldef "v1" as " v1 ";
90+
htmldef "v2" as " v2 ";
91+
htmldef "v3" as " v3 ";
92+
htmldef "v4" as " v4 ";
93+
htmldef "v5" as " v5 ";
94+
htmldef "v6" as " v6 ";
95+
htmldef "v7" as " v7 ";
96+
htmldef "v8" as " v8 ";
97+
htmldef "v9" as " v9 ";
98+
htmldef "v10" as " v10 ";
99+
htmldef "v11" as " v11 ";
100+
$)

0 commit comments

Comments
 (0)