Recorded 6/19/96:
1. Use Free Paramodulation
2. Backward-depth-limit {5}
3. Assume preceding local conjecture are theorems ---- Yes
4. Ignore following local theorems ---- Yes
5. Used induction on B1! {BIT-0, BIT-1}
=====================================================
.> Parsing buffer bits.re ...
;;; ----------------------------------------------------------------------
;;; Linking spec BIT
Warning: Replacing spec BIT (#25)
;;; Type-checking spec BIT ...
;;; ----------------------------------------------------------------------
;;; Linking spec BIT-AS-INTEGER
Warning: Replacing spec BIT-AS-INTEGER (#26)
;;; Linking import declaration
;;; Type-checking spec BIT-AS-INTEGER ...
;;; ----------------------------------------------------------------------
;;; Linking ip-scheme BIT-TO-INTEGER
Warning: Replacing ip-scheme BIT-TO-INTEGER (#27)
;;; Linking rules
;;; Verifying signature translation
;;; Verifying sort axiom translations
;;; ----------------------------------------------------------------------
;;; Linking spec BIT-AS-BOOLEAN
Warning: Replacing spec BIT-AS-BOOLEAN (#28)
;;; Type-checking spec BIT-AS-BOOLEAN ...
;;; ----------------------------------------------------------------------
;;; Linking ip-scheme BIT-TO-BOOLEAN
Warning: Replacing ip-scheme BIT-TO-BOOLEAN (#29)
;;; Linking rules
;;; Verifying signature translation
;;; Verifying sort axiom translations
;;; Linking rules
;;; Verifying signature translation
;;; Verifying sort axiom translations
... done.
.>
SPECWARE Prover Options... Setup User-defined Settings...
done.
.>
SPECWARE Focus...done.
.> ;;; Verify conjecture
;;; (FA (B2: BIT B1: BIT) (EQUAL (BIT-AND B1 B2) (BIT-CARRY B1 B2)))
;;; by induction on B1 over {BIT-1,BIT-0}
gc: done
conjecture BIT-AND-CARRY-BIT-1-1
predicate
(FA (B2: BIT) (EQUAL (BIT-AND BIT-1 B2) (BIT-CARRY BIT-1 B2)))
end-conjecture
Starting Kitp ... #30
b1: ((NOT (EQUAL (BIT-AND BIT-1 B2!) (BIT-CARRY BIT-1 B2!))))
b1? rules
a433: (EQUAL <((PROJECT 1) Z) ((PROJECT 2) Z)> Z)
a435: (EQUAL ((PROJECT 2) X1 X2) X2)
a437: (EQUAL ((PROJECT 1) X1 X2) X1)
a438: (EQUAL (BIT-AND BIT-1 BIT-1) BIT-1)
a439: (EQUAL (BIT-AND BIT-1 BIT-0) BIT-0)
a440: (EQUAL (BIT-AND BIT-0 BIT-1) BIT-0)
a441: (EQUAL (BIT-AND BIT-0 BIT-0) BIT-0)
a442: (EQUAL (BIT-NOT BIT-1) BIT-0)
a443: (EQUAL (BIT-NOT BIT-0) BIT-1)
a444: (EQUAL (BIT-CARRY BIT-1 BIT-1) BIT-1)
a445: (EQUAL (BIT-CARRY BIT-1 BIT-0) BIT-0)
a446: (EQUAL (BIT-CARRY BIT-0 BIT-1) BIT-0)
a447: (EQUAL (BIT-CARRY BIT-0 BIT-0) BIT-0)
a448: (EQUAL (BIT-PLUS BIT-1 BIT-1) BIT-0)
a449: (EQUAL (BIT-PLUS BIT-1 BIT-0) BIT-1)
a450: (EQUAL (BIT-PLUS BIT-0 BIT-1) BIT-1)
a451: (EQUAL (BIT-PLUS BIT-0 BIT-0) BIT-0)
a454: (NOT (EQUAL BIT-0 BIT-1))
a453: ((EQUAL X BIT-0)) ((EQUAL X BIT-1))
a459:
((NOT (EQUAL (BIT-AND BIT-1 B2!) (BIT-CARRY BIT-1 B2!))))
b1? a
Enter automatic mode. To interrupt, press `return' key.
b2 ...................................................................
b70 ...........
%%% KITP says: ** Proved BIT-AND-CARRY-BIT-1-1 by Kitp ** at 06/19/96 13:52:10 with 1.85 Seconds.
CPU seconds used 1.85
Resolvents accepted 80
Useful goal clauses 8
Useful resolvents 13
Nesting limited 2
Depth limited (6) 0
Complexity limited (18) 0
--- THE PROOF TREE ---
[ Input ] a438: (EQUAL (BIT-AND BIT-1 BIT-1) BIT-1)
[ Input ] a439: (EQUAL (BIT-AND BIT-1 BIT-0) BIT-0)
[ Input ] a444: (EQUAL (BIT-CARRY BIT-1 BIT-1) BIT-1)
[ Input ] a445: (EQUAL (BIT-CARRY BIT-1 BIT-0) BIT-0)
[ Input ] a453: ((EQUAL X BIT-0)) ((EQUAL X BIT-1))
[ Input ] a459:
((NOT (EQUAL (BIT-AND BIT-1 B2!) (BIT-CARRY BIT-1 B2!))))
[a459 ()] b1:
((NOT (EQUAL (BIT-AND BIT-1 B2!) (BIT-CARRY BIT-1 B2!))))
[b1 a453] b2:
((NOT (EQUAL (BIT-AND Y1? B2!) (BIT-CARRY Y1? B2!))))
((EQUAL BIT-0 Y1?))
[b1 a453] b3: ((EQUAL (BIT-AND BIT-1 B2!) BIT-0))
((NOT (EQUAL (BIT-CARRY BIT-1 B2!) BIT-1)))
[b1 a453] b6: ((EQUAL (BIT-CARRY BIT-1 B2!) BIT-1))
((NOT (EQUAL (BIT-AND BIT-1 B2!) BIT-0)))
[b1 a453] b8:
((NOT (EQUAL (BIT-AND BIT-1 BIT-0) (BIT-CARRY BIT-1 BIT-0))))
((EQUAL B2! BIT-1))
[b8 a445] b18:
((NOT (EQUAL (BIT-AND BIT-1 BIT-0) BIT-0)))
((EQUAL B2! BIT-1))
[b18 a439] b21: ((EQUAL B2! BIT-1))
[b21 b6] b23: ((EQUAL (BIT-CARRY BIT-1 BIT-1) BIT-1))
((NOT (EQUAL (BIT-AND BIT-1 B2!) BIT-0)))
[b21 b3] b30:
((NOT (EQUAL (BIT-CARRY BIT-1 BIT-1) BIT-1)))
((EQUAL (BIT-AND BIT-1 B2!) BIT-0))
[b21 b2] b31:
((NOT (EQUAL (BIT-AND Y1? BIT-1) (BIT-CARRY Y1? BIT-1))))
((EQUAL BIT-0 Y1?))
[b30 a444] b33: ((EQUAL (BIT-AND BIT-1 B2!) BIT-0))
[b33 b23] b34: ((EQUAL (BIT-CARRY BIT-1 BIT-1) BIT-1))
[b34 b31] b76:
((NOT (EQUAL (BIT-AND BIT-1 BIT-1) BIT-1)))
((EQUAL BIT-0 BIT-1))
[b76 a438] b81:
conjecture BIT-AND-CARRY-BIT-0-1
predicate
(FA (B2: BIT) (EQUAL (BIT-AND BIT-0 B2) (BIT-CARRY BIT-0 B2)))
end-conjecture
Starting Kitp ... #31
b1: ((NOT (EQUAL (BIT-AND BIT-0 B2!) (BIT-CARRY BIT-0 B2!))))
b1? a
Enter automatic mode. To interrupt, press `return' key.
b2 ...................................................................
b70 ....
%%% KITP says: ** Proved BIT-AND-CARRY-BIT-0-1 by Kitp ** at 06/19/96 13:53:15 with 1.58 Seconds.
CPU seconds used 1.58
Resolvents accepted 73
Useful goal clauses 8
Useful resolvents 12
Nesting limited 0
Depth limited (6) 20
Complexity limited (18) 0
--- THE PROOF TREE ---
[ Input ] a440: (EQUAL (BIT-AND BIT-0 BIT-1) BIT-0)
[ Input ] a441: (EQUAL (BIT-AND BIT-0 BIT-0) BIT-0)
[ Input ] a446: (EQUAL (BIT-CARRY BIT-0 BIT-1) BIT-0)
[ Input ] a447: (EQUAL (BIT-CARRY BIT-0 BIT-0) BIT-0)
[ Input ] a453: ((EQUAL X BIT-0)) ((EQUAL X BIT-1))
[ Input ] a459:
((NOT (EQUAL (BIT-AND BIT-0 B2!) (BIT-CARRY BIT-0 B2!))))
[a459 ()] b1:
((NOT (EQUAL (BIT-AND BIT-0 B2!) (BIT-CARRY BIT-0 B2!))))
[b1 a453] b4: ((EQUAL (BIT-AND BIT-0 B2!) BIT-1))
((NOT (EQUAL (BIT-CARRY BIT-0 B2!) BIT-0)))
[b1 a453] b5: ((EQUAL (BIT-CARRY BIT-0 B2!) BIT-0))
((NOT (EQUAL (BIT-AND BIT-0 B2!) BIT-1)))
[b1 a453] b6: ((EQUAL (BIT-CARRY BIT-0 B2!) BIT-1))
((NOT (EQUAL (BIT-AND BIT-0 B2!) BIT-0)))
[b1 a453] b8:
((NOT (EQUAL (BIT-AND BIT-0 BIT-0) (BIT-CARRY BIT-0 BIT-0))))
((EQUAL B2! BIT-1))
[b8 a447] b17:
((NOT (EQUAL (BIT-AND BIT-0 BIT-0) BIT-0)))
((EQUAL B2! BIT-1))
[b17 a441] b20: ((EQUAL B2! BIT-1))
[b20 b6] b23:
((NOT (EQUAL (BIT-AND BIT-0 BIT-1) BIT-0)))
((EQUAL (BIT-CARRY BIT-0 B2!) BIT-1))
[b20 b4] b27:
((NOT (EQUAL (BIT-CARRY BIT-0 BIT-1) BIT-0)))
((EQUAL (BIT-AND BIT-0 B2!) BIT-1))
[b27 a446] b32: ((EQUAL (BIT-AND BIT-0 B2!) BIT-1))
[b32 b5] b34: ((EQUAL (BIT-CARRY BIT-0 B2!) BIT-0))
[b34 b23] b72:
((NOT (EQUAL (BIT-AND BIT-0 BIT-1) BIT-0)))
((EQUAL BIT-0 BIT-1))
[b72 a440] b74:
;;; Verified conjecture Bit-And-Carry.
;;; Verified 1 out of 6 conjectures
;;; Verify conjecture
;;; (FA (B2: BIT B1: BIT)
;;; (IFF (EQUAL (BIT-AND B1 B2) BIT-1) (EQUAL (BIT-CARRY B1 B2) BIT-1)))
;;; by induction on B1 over {BIT-1,BIT-0}
conjecture BIT-AND-CARRY-IFF-BIT-1-0
predicate
(FA (B2: BIT)
(IFF (EQUAL (BIT-AND BIT-1 B2) BIT-1) (EQUAL (BIT-CARRY BIT-1 B2) BIT-1)))
end-conjecture
Starting Kitp ... #32
b2: ((NOT (EQUAL (BIT-CARRY BIT-1 B2!) BIT-1)))
b2? a
Enter automatic mode. To interrupt, press `return' key.
b3
%%% KITP says: ** Proved BIT-AND-CARRY-IFF-BIT-1-0 by Kitp ** at 06/19/96 13:53:38 with 0.1 Seconds.
CPU seconds used 0.1
Resolvents accepted 1
Useful goal clauses 1
Useful resolvents 1
Nesting limited 0
Depth limited (6) 0
Complexity limited (18) 0
--- THE PROOF TREE ---
[ Input ] a463: (EQUAL (BIT-CARRY BIT-1 B2!) BIT-1)
[ Input ] a462: ((NOT (EQUAL (BIT-CARRY BIT-1 B2!) BIT-1)))
[a462 ()] b2:
((NOT (EQUAL (BIT-CARRY BIT-1 B2!) BIT-1)))
[b2 a463] b3:
b2: ((NOT (EQUAL (BIT-AND BIT-1 B2!) BIT-1)))
b2? a
Enter automatic mode. To interrupt, press `return' key.
b3 .....
%%% KITP says: ** Proved BIT-AND-CARRY-IFF-BIT-1-0 by Kitp ** at 06/19/96 13:53:41 with 0.17 Seconds.
CPU seconds used 0.17
Resolvents accepted 6
Useful goal clauses 2
Useful resolvents 2
Nesting limited 0
Depth limited (6) 0
Complexity limited (18) 0
--- THE PROOF TREE ---
[ Input ] a439: (EQUAL (BIT-AND B1 B2) (BIT-CARRY B1 B2))
[ Input ] a463: (EQUAL (BIT-CARRY BIT-1 B2!) BIT-1)
[ Input ] a465: ((NOT (EQUAL (BIT-AND BIT-1 B2!) BIT-1)))
[a465 ()] b2:
((NOT (EQUAL (BIT-AND BIT-1 B2!) BIT-1)))
[b2 a439] b4:
((NOT (EQUAL (BIT-CARRY BIT-1 B2!) BIT-1)))
[b4 a463] b8:
conjecture BIT-AND-CARRY-IFF-BIT-0-0
predicate
(FA (B2: BIT)
(IFF (EQUAL (BIT-AND BIT-0 B2) BIT-1) (EQUAL (BIT-CARRY BIT-0 B2) BIT-1)))
end-conjecture
Starting Kitp ... #33
b2: ((NOT (EQUAL (BIT-CARRY BIT-0 B2!) BIT-1)))
b2? a
Enter automatic mode. To interrupt, press `return' key.
b3
%%% KITP says: ** Proved BIT-AND-CARRY-IFF-BIT-0-0 by Kitp ** at 06/19/96 13:53:48 with 0.2 Seconds.
CPU seconds used 0.2
Resolvents accepted 1
Useful goal clauses 1
Useful resolvents 1
Nesting limited 0
Depth limited (6) 0
Complexity limited (18) 0
--- THE PROOF TREE ---
[ Input ] a465: (EQUAL (BIT-CARRY BIT-0 B2!) BIT-1)
[ Input ] a463: ((NOT (EQUAL (BIT-CARRY BIT-0 B2!) BIT-1)))
[a463 ()] b2:
((NOT (EQUAL (BIT-CARRY BIT-0 B2!) BIT-1)))
[b2 a465] b3: gc: done
b2: ((NOT (EQUAL (BIT-AND BIT-0 B2!) BIT-1)))
b2? a
Enter automatic mode. To interrupt, press `return' key.
b3 .......
%%% KITP says: ** Proved BIT-AND-CARRY-IFF-BIT-0-0 by Kitp ** at 06/19/96 13:53:51 with 0.72 Seconds.
CPU seconds used 0.72
Resolvents accepted 8
Useful goal clauses 2
Useful resolvents 2
Nesting limited 0
Depth limited (6) 0
Complexity limited (18) 0
--- THE PROOF TREE ---
[ Input ] a439: (EQUAL (BIT-AND B1 B2) (BIT-CARRY B1 B2))
[ Input ] a464: (EQUAL BIT-1 (BIT-CARRY BIT-0 B2!))
[ Input ] a469: ((NOT (EQUAL (BIT-AND BIT-0 B2!) BIT-1)))
[a469 ()] b2:
((NOT (EQUAL (BIT-AND BIT-0 B2!) BIT-1)))
[b2 a464] b6:
((NOT (EQUAL (BIT-AND BIT-0 B2!) (BIT-CARRY BIT-0 B2!))))
[b6 a439] b10:
;;; Verified conjecture Bit-And-Carry-Iff.
;;; Verified 1 out of 6 conjectures
;;; Verify conjecture
;;; (FA (B2: BIT B1: BIT)
;;; (IFF (EQUAL (BIT-AND B1 B2) BIT-1)
;;; (AND (EQUAL B1 BIT-1) (EQUAL B2 BIT-1))))
;;; by induction on B1 over {BIT-1,BIT-0}
conjecture BIT-AND-BIT-1-0
predicate
(FA (B2: BIT)
(IFF (EQUAL (BIT-AND BIT-1 B2) BIT-1)
(AND (EQUAL BIT-1 BIT-1) (EQUAL B2 BIT-1))))
end-conjecture
Starting Kitp ... #34
b2: ((NOT (EQUAL B2! BIT-1)))
b2? a
Enter automatic mode. To interrupt, press `return' key.
b3 ...................................................................
b71 ..................
%%% KITP says: ** Proved BIT-AND-BIT-1-0 by Kitp ** at 06/19/96 13:54:19 with 2.47 Seconds.
CPU seconds used 2.47
Resolvents accepted 87
Useful goal clauses 3
Useful resolvents 3
Nesting limited 11
Depth limited (6) 0
Complexity limited (18) 0
--- THE PROOF TREE ---
[ Input ] a452: (EQUAL (BIT-CARRY BIT-1 BIT-0) BIT-0)
[ Input ] a460: ((EQUAL X BIT-0)) ((EQUAL X BIT-1))
[ Input ] a470: ((NOT (EQUAL B2! BIT-1)))
[ Input ] a471: (EQUAL (BIT-CARRY BIT-1 B2!) BIT-1)
[a470 ()] b2: ((NOT (EQUAL B2! BIT-1)))
[b2 a460] b3: ((EQUAL B2! BIT-0))
[b3 a471] b8: ((EQUAL (BIT-CARRY BIT-1 BIT-0) BIT-1))
[b8 a452] b89:
b2: ((NOT (EQUAL (BIT-AND BIT-1 B2!) BIT-1)))
b2? a
Enter automatic mode. To interrupt, press `return' key.
b3 ......
%%% KITP says: ** Proved BIT-AND-BIT-1-0 by Kitp ** at 06/19/96 13:54:23 with 0.29 Seconds.
CPU seconds used 0.29
Resolvents accepted 7
Useful goal clauses 2
Useful resolvents 2
Nesting limited 1
Depth limited (6) 0
Complexity limited (18) 0
--- THE PROOF TREE ---
[ Input ] a445: (EQUAL (BIT-AND BIT-1 BIT-1) BIT-1)
[ Input ] a474: (EQUAL B2! BIT-1)
[ Input ] a476: ((NOT (EQUAL (BIT-AND BIT-1 B2!) BIT-1)))
[a476 ()] b2:
((NOT (EQUAL (BIT-AND BIT-1 B2!) BIT-1)))
[b2 a474] b8:
((NOT (EQUAL (BIT-AND BIT-1 BIT-1) BIT-1)))
[b8 a445] b9:
conjecture BIT-AND-BIT-0-0
predicate
(FA (B2: BIT)
(IFF (EQUAL (BIT-AND BIT-0 B2) BIT-1)
(AND (EQUAL BIT-0 BIT-1) (EQUAL B2 BIT-1))))
end-conjecture
Starting Kitp ... #35
b1: ((EQUAL (BIT-AND BIT-0 B2!) BIT-1))
b1? a
Enter automatic mode. To interrupt, press `return' key.
b2 ...................................................................
b70 ......................
%%% KITP says: ** Proved BIT-AND-BIT-0-0 by Kitp ** at 06/19/96 13:54:36 with 1.43 Seconds.
CPU seconds used 1.43
Resolvents accepted 91
Useful goal clauses 4
Useful resolvents 4
Nesting limited 3
Depth limited (6) 0
Complexity limited (18) 0
--- THE PROOF TREE ---
[ Input ] a447: (EQUAL (BIT-AND BIT-0 BIT-1) BIT-0)
[ Input ] a448: (EQUAL (BIT-AND BIT-0 BIT-0) BIT-0)
[ Input ] a460: ((EQUAL X BIT-0)) ((EQUAL X BIT-1))
[ Input ] a469: ((EQUAL (BIT-AND BIT-0 B2!) BIT-1))
[a469 ()] b1: ((EQUAL (BIT-AND BIT-0 B2!) BIT-1))
[b1 a460] b9: ((EQUAL (BIT-AND BIT-0 BIT-0) BIT-1))
((EQUAL B2! BIT-1))
[b9 a448] b64: ((EQUAL B2! BIT-1))
[b64 a469] b65: ((EQUAL (BIT-AND BIT-0 BIT-1) BIT-1))
[b65 a447] b92:
%%% KITP says: ** Proved BIT-AND-BIT-0-0 by simplification ** at 06/19/96 13:54:37.
;;; Verified conjecture Bit-And.
;;; Verified 1 out of 6 conjectures
;;; Verify conjecture
;;; (FA (B2: BIT B1: BIT)
;;; (IFF (EQUAL (BIT-IOR B1 B2) BIT-1)
;;; (OR (EQUAL B1 BIT-1) (EQUAL B2 BIT-1))))
;;; by induction on B1 over {BIT-1,BIT-0}
conjecture BIT-IOR-BIT-1-0
predicate
(FA (B2: BIT)
(IFF (EQUAL (BIT-IOR BIT-1 B2) BIT-1)
(OR (EQUAL BIT-1 BIT-1) (EQUAL B2 BIT-1))))
end-conjecture
Starting Kitp ... #36gc: done
%%% KITP says: ** Proved BIT-IOR-BIT-1-0 by simplification ** at 06/19/96 13:54:54.
b1: ((NOT (EQUAL (BIT-IOR BIT-1 B2!) BIT-1)))
b1? a
Enter automatic mode. To interrupt, press `return' key.
b2 ...................................................................
b70 .....
%%% KITP says: ** Proved BIT-IOR-BIT-1-0 by Kitp ** at 06/19/96 13:55:00 with 1.64 Seconds.
CPU seconds used 1.64
Resolvents accepted 74
Useful goal clauses 4
Useful resolvents 4
Nesting limited 10
Depth limited (6) 0
Complexity limited (18) 0
--- THE PROOF TREE ---
[ Input ] a438: (EQUAL (BIT-IOR BIT-1 BIT-1) BIT-1)
[ Input ] a439: (EQUAL (BIT-IOR BIT-1 BIT-0) BIT-1)
[ Input ] a471: ((EQUAL X BIT-0)) ((EQUAL X BIT-1))
[ Input ] a484: ((NOT (EQUAL (BIT-IOR BIT-1 B2!) BIT-1)))
[a484 ()] b1:
((NOT (EQUAL (BIT-IOR BIT-1 B2!) BIT-1)))
[b1 a471] b11:
((NOT (EQUAL (BIT-IOR BIT-1 BIT-1) BIT-1)))
((EQUAL B2! BIT-0))
[b11 a438] b64: ((EQUAL B2! BIT-0))
[b64 a484] b65:
((NOT (EQUAL (BIT-IOR BIT-1 BIT-0) BIT-1)))
[b65 a439] b75:
conjecture BIT-IOR-BIT-0-0
predicate
(FA (B2: BIT)
(IFF (EQUAL (BIT-IOR BIT-0 B2) BIT-1)
(OR (EQUAL BIT-0 BIT-1) (EQUAL B2 BIT-1))))
end-conjecture
Starting Kitp ... #37
b2: ((NOT (EQUAL B2! BIT-1)))
b2? a
Enter automatic mode. To interrupt, press `return' key.
b3 ...................................................................
b71 ...................................................................
b139 ...................................................................
b207 ..........gc: done
.........................................................
b275 ...................................................................
b343 ...................................................................
b411 ...................................................................
b479 .............gc: done
......................................................
b547 ...................................................................
b615 ...................................................................
b683 ...................................................................
b751 ..gc: done
.................................................................
b819 ...................................................................
b887 ...................................................................
b955 ...................................................................
b1023 ..............................gc: done
.....................................
b1091 ...................................................................
b1159 ...................................................................
b1227 ...................................................................
b1295 ................................gc: done
...................................
b1363 ...................................................................
b1431 ...................................................................
b1499 ...............
%%% KITP says: ** Proved BIT-IOR-BIT-0-0 by Kitp ** at 06/19/96 13:57:04 with 38.05 Seconds.
CPU seconds used 38.05
Resolvents accepted 1512
Useful goal clauses 4
Useful resolvents 6
Nesting limited 296
Depth limited (6) 717
Complexity limited (18) 0
--- THE PROOF TREE ---
[ Input ] a441: (EQUAL (BIT-IOR BIT-0 BIT-0) BIT-0)
[ Input ] a471: ((EQUAL X BIT-0)) ((EQUAL X BIT-1))
[ Input ] a478: ((EQUAL B1 BIT-1))
((NOT (EQUAL (BIT-AND B1 B2) BIT-1)))
[ Input ] a485: ((NOT (EQUAL B2! BIT-1)))
[ Input ] a494: (EQUAL (BIT-AND (BIT-IOR BIT-0 B2!) (BIT-NOT BIT-0)) BIT-1)
[a485 ()] b2: ((NOT (EQUAL B2! BIT-1)))
[b2 a471] b3: ((EQUAL B2! BIT-0))
[b2 a478] b13: ((NOT (EQUAL (BIT-AND Y1? Y2?) BIT-1)))
((NOT (EQUAL B2! Y1?)))
[b3 a494] b19:
((EQUAL (BIT-AND (BIT-IOR BIT-0 BIT-0) (BIT-NOT BIT-0)) BIT-1))
[b3 b13] b34: ((NOT (EQUAL (BIT-AND Y2? Y1?) BIT-1)))
((NOT (EQUAL BIT-0 Y2?)))
[b19 b34] b1496:
((NOT (EQUAL (BIT-IOR BIT-0 BIT-0) BIT-0)))
[b1496 a441] b1514:
b2: ((NOT (EQUAL (BIT-IOR BIT-0 B2!) BIT-1)))
b2? a
Enter automatic mode. To interrupt, press `return' key.
b3 ................
%%% KITP says: ** Proved BIT-IOR-BIT-0-0 by Kitp ** at 06/19/96 13:57:14 with 0.4 Seconds.
CPU seconds used 0.4
Resolvents accepted 17
Useful goal clauses 2
Useful resolvents 2
Nesting limited 0
Depth limited (6) 0
Complexity limited (18) 0
--- THE PROOF TREE ---
[ Input ] a440: (EQUAL (BIT-IOR BIT-0 BIT-1) BIT-1)
[ Input ] a501: (EQUAL B2! BIT-1)
[ Input ] a503: ((NOT (EQUAL (BIT-IOR BIT-0 B2!) BIT-1)))
[a503 ()] b2:
((NOT (EQUAL (BIT-IOR BIT-0 B2!) BIT-1)))
[b2 a501] b7:
((NOT (EQUAL (BIT-IOR BIT-0 BIT-1) BIT-1)))
[b7 a440] b19:
;;; Verified conjecture Bit-Ior.
;;; Verified 1 out of 6 conjectures
;;; Verify conjecture
;;; (FA (B2: BIT B1: BIT)
;;; (IFF (EQUAL (BIT-XOR B1 B2) BIT-1) (EQUAL (BIT-PLUS B1 B2) BIT-1)))
;;; by induction on B1 over {BIT-1,BIT-0}
conjecture BIT-XOR-PLUS-BIT-1-0
predicate
(FA (B2: BIT)
(IFF (EQUAL (BIT-XOR BIT-1 B2) BIT-1) (EQUAL (BIT-PLUS BIT-1 B2) BIT-1)))
end-conjecture
Starting Kitp ... #38gc: done
b2: ((NOT (EQUAL (BIT-PLUS BIT-1 B2!) BIT-1)))
b2? a
Enter automatic mode. To interrupt, press `return' key.
b3 ...................................................................
b71 ...................................................................
b139 ................
%%% KITP says: ** Proved BIT-XOR-PLUS-BIT-1-0 by Kitp ** at 06/19/96 13:57:45 with 3.36 Seconds.
CPU seconds used 3.36
Resolvents accepted 153
Useful goal clauses 4
Useful resolvents 4
Nesting limited 17
Depth limited (6) 0
Complexity limited (18) 0
--- THE PROOF TREE ---
[ Input ] a438: (EQUAL (BIT-XOR BIT-1 BIT-1) BIT-0)
[ Input ] a478: (EQUAL (BIT-PLUS BIT-1 BIT-0) BIT-1)
[ Input ] a482: ((EQUAL X BIT-0)) ((EQUAL X BIT-1))
[ Input ] a496: (EQUAL (BIT-XOR BIT-1 B2!) BIT-1)
[ Input ] a497: ((NOT (EQUAL (BIT-PLUS BIT-1 B2!) BIT-1)))
[a497 ()] b2:
((NOT (EQUAL (BIT-PLUS BIT-1 B2!) BIT-1)))
[b2 a482] b19:
((NOT (EQUAL (BIT-PLUS BIT-1 BIT-0) BIT-1)))
((EQUAL B2! BIT-1))
[b19 a478] b113: ((EQUAL B2! BIT-1))
[b113 a496] b128: ((EQUAL (BIT-XOR BIT-1 BIT-1) BIT-1))
[b128 a438] b155:
b2: ((NOT (EQUAL (BIT-XOR BIT-1 B2!) BIT-1)))
b2? a
Enter automatic mode. To interrupt, press `return' key.
b3 ...................................................................
b71 ...................................................................
b139 ................
%%% KITP says: ** Proved BIT-XOR-PLUS-BIT-1-0 by Kitp ** at 06/19/96 13:57:58 with 3.15 Seconds.
CPU seconds used 3.15
Resolvents accepted 153
Useful goal clauses 4
Useful resolvents 4
Nesting limited 17
Depth limited (6) 0
Complexity limited (18) 0
--- THE PROOF TREE ---
[ Input ] a439: (EQUAL (BIT-XOR BIT-1 BIT-0) BIT-1)
[ Input ] a477: (EQUAL (BIT-PLUS BIT-1 BIT-1) BIT-0)
[ Input ] a482: ((EQUAL X BIT-0)) ((EQUAL X BIT-1))
[ Input ] a517: (EQUAL (BIT-PLUS BIT-1 B2!) BIT-1)
[ Input ] a518: ((NOT (EQUAL (BIT-XOR BIT-1 B2!) BIT-1)))
[a518 ()] b2:
((NOT (EQUAL (BIT-XOR BIT-1 B2!) BIT-1)))
[b2 a482] b19:
((NOT (EQUAL (BIT-XOR BIT-1 BIT-0) BIT-1)))
((EQUAL B2! BIT-1))
[b19 a439] b113: ((EQUAL B2! BIT-1))
[b113 a517] b128: ((EQUAL (BIT-PLUS BIT-1 BIT-1) BIT-1))
[b128 a477] b155:
conjecture BIT-XOR-PLUS-BIT-0-0
predicate
(FA (B2: BIT)
(IFF (EQUAL (BIT-XOR BIT-0 B2) BIT-1) (EQUAL (BIT-PLUS BIT-0 B2) BIT-1)))
end-conjecture
Starting Kitp ... #39gc: done
b2: ((NOT (EQUAL (BIT-PLUS BIT-0 B2!) BIT-1)))
b2? a
Enter automatic mode. To interrupt, press `return' key.
b3 ...................................................................
b71 ...................................................................
b139 ...................................................................
b207 ...................................................................
b275 ...................................................................
b343 ................gc: done
...................................................
b411 ...................................................................
b479 ...................................................................
b547 ...................................................................
b615 ...............................................................gc: done
....
b683 ............................................................
%%% KITP says: ** Proved BIT-XOR-PLUS-BIT-0-0 by Kitp ** at 06/19/96 13:58:56 with 13.56 Seconds.
CPU seconds used 13.56
Resolvents accepted 741
Useful goal clauses 4
Useful resolvents 4
Nesting limited 107
Depth limited (6) 0
Complexity limited (18) 0
--- THE PROOF TREE ---
[ Input ] a441: (EQUAL (BIT-XOR BIT-0 BIT-0) BIT-0)
[ Input ] a479: (EQUAL (BIT-PLUS BIT-0 BIT-1) BIT-1)
[ Input ] a482: ((EQUAL X BIT-0)) ((EQUAL X BIT-1))
[ Input ] a496: (EQUAL (BIT-XOR BIT-0 B2!) BIT-1)
[ Input ] a498: ((NOT (EQUAL (BIT-PLUS BIT-0 B2!) BIT-1)))
[a498 ()] b2:
((NOT (EQUAL (BIT-PLUS BIT-0 B2!) BIT-1)))
[b2 a482] b28:
((NOT (EQUAL (BIT-PLUS BIT-0 BIT-1) BIT-1)))
((EQUAL B2! BIT-0))
[b28 a479] b258: ((EQUAL B2! BIT-0))
[b258 a496] b281: ((EQUAL (BIT-XOR BIT-0 BIT-0) BIT-1))
[b281 a441] b743:
b2: ((NOT (EQUAL (BIT-XOR BIT-0 B2!) BIT-1)))
b2? a
Enter automatic mode. To interrupt, press `return' key.
b3 ...................................................................
b71 ...................................................................
b139 ...................................................................
b207 ...........................................gc: done
........................
b275 ...................................................................
b343 ...................................................................
b411 ...................................................................
b479 ...................................................................
b547 ...................................................gc: done
................
b615 ...................................................................
b683 ............................................................
%%% KITP says: ** Proved BIT-XOR-PLUS-BIT-0-0 by Kitp ** at 06/19/96 13:59:42 with 13.25 Seconds.
CPU seconds used 13.25
Resolvents accepted 741
Useful goal clauses 4
Useful resolvents 4
Nesting limited 107
Depth limited (6) 0
Complexity limited (18) 0
--- THE PROOF TREE ---
[ Input ] a440: (EQUAL (BIT-XOR BIT-0 BIT-1) BIT-1)
[ Input ] a480: (EQUAL (BIT-PLUS BIT-0 BIT-0) BIT-0)
[ Input ] a482: ((EQUAL X BIT-0)) ((EQUAL X BIT-1))
[ Input ] a534: (EQUAL (BIT-PLUS BIT-0 B2!) BIT-1)
[ Input ] a536: ((NOT (EQUAL (BIT-XOR BIT-0 B2!) BIT-1)))
[a536 ()] b2:
((NOT (EQUAL (BIT-XOR BIT-0 B2!) BIT-1)))
[b2 a482] b28:
((NOT (EQUAL (BIT-XOR BIT-0 BIT-1) BIT-1)))
((EQUAL B2! BIT-0))
[b28 a440] b258: ((EQUAL B2! BIT-0))
[b258 a534] b281: ((EQUAL (BIT-PLUS BIT-0 BIT-0) BIT-1))
[b281 a480] b743:
;;; Verified conjecture Bit-Xor-Plus.
;;; Verified 1 out of 6 conjectures
;;; Verify conjecture
;;; (FA (B2: BIT B1: BIT)
;;; (IFF (EQUAL (BIT-XOR B1 B2) BIT-1) (NOT (EQUAL B1 B2))))
;;; by induction on B1 over {BIT-1,BIT-0}
conjecture BIT-XOR-BIT-1-0
predicate
(FA (B2: BIT)
(IFF (EQUAL (BIT-XOR BIT-1 B2) BIT-1) (NOT (EQUAL BIT-1 B2))))
end-conjecture
Starting Kitp ... #40
b2: ((EQUAL BIT-1 B2!))
b2? a
Enter automatic mode. To interrupt, press `return' key.
b3 ...................................................................
b71 ................................................................gc: done
...
b139 ...................................................................
b207 ...................................................................
b275 ...................................................................
b343 ...................................................................
b411 ...................................................................
b479 .gc: done
..................................................................
b547 ...................................................................
b615 ...................................................................
b683 ...........................
%%% KITP says: ** Proved BIT-XOR-BIT-1-0 by Kitp ** at 06/19/96 14:00:48 with 14.16 Seconds.
CPU seconds used 14.16
Resolvents accepted 708
Useful goal clauses 2
Useful resolvents 2
Nesting limited 48
Depth limited (6) 0
Complexity limited (18) 0
--- THE PROOF TREE ---
[ Input ] a443: (EQUAL (BIT-XOR BIT-1 BIT-1) BIT-0)
[ Input ] a503: (EQUAL (BIT-XOR BIT-1 B2!) BIT-1)
[ Input ] a504: ((EQUAL BIT-1 B2!))
[a503 ()] b1: ((EQUAL (BIT-XOR BIT-1 B2!) BIT-1))
[b1 a504] b534: ((EQUAL (BIT-XOR BIT-1 BIT-1) BIT-1))
[b534 a443] b710:
b1: ((NOT (EQUAL BIT-1 B2!)))
b1? a
Enter automatic mode. To interrupt, press `return' key.
b3 ...................................................................
b71 ......................................gc: done
.............................
b139 ...................................................................
b207 ...................................................................
b275 ...............................................gc: done
....................
b343 ...................................................................
b411 ..............................................
%%% KITP says: ** Proved BIT-XOR-BIT-1-0 by Kitp ** at 06/19/96 14:01:29 with 12.66 Seconds.
CPU seconds used 12.66
Resolvents accepted 455
Useful goal clauses 3
Useful resolvents 3
Nesting limited 49
Depth limited (6) 0
Complexity limited (18) 0
--- THE PROOF TREE ---
[ Input ] a444: (EQUAL (BIT-XOR BIT-1 BIT-0) BIT-1)
[ Input ] a487: ((EQUAL X BIT-0)) ((EQUAL X BIT-1))
[ Input ] a529: (NOT (EQUAL BIT-1 B2!))
[ Input ] a530: ((NOT (EQUAL (BIT-XOR BIT-1 B2!) BIT-1)))
[a529 ()] b1: ((NOT (EQUAL BIT-1 B2!)))
[b1 a487] b15: ((EQUAL B2! BIT-0))
[b15 a530] b444:
((NOT (EQUAL (BIT-XOR BIT-1 BIT-0) BIT-1)))
[b444 a444] b457:
conjecture BIT-XOR-BIT-0-0
predicate
(FA (B2: BIT)
(IFF (EQUAL (BIT-XOR BIT-0 B2) BIT-1) (NOT (EQUAL BIT-0 B2))))
end-conjecture
Starting Kitp ... #41
b2: ((EQUAL BIT-0 B2!))
b2? a
Enter automatic mode. To interrupt, press `return' key.
b3 ...................................................................
b71 ...................................................................
b139 ...................................................................
b207 ..gc: done
.................................................................
b275 ...................................................................
b343 ...................................................................
b411 ...................................................................
b479 ...................................................................
b547 .....................gc: done
..............................................
b615 ...................................................................
b683 ...................................................................
b751 ...................................................................
b819 ...................................................................
b887 .gc: done
..................................................................
b955 ...................................................................
b1023 ...................................................................
b1091 ...................................................................
b1159 ...................................................................
b1227 ................................gc: done
...................................
b1295 ...................................................................
b1363 ...................................................................
b1431 ...................................................................
b1499 ...........................gc: done
........................................
b1567 .........................................
%%% KITP says: ** Proved BIT-XOR-BIT-0-0 by Kitp ** at 06/19/96 14:03:03 with 29.89 Seconds.
CPU seconds used 29.89
Resolvents accepted 1606
Useful goal clauses 2
Useful resolvents 2
Nesting limited 254
Depth limited (6) 0
Complexity limited (18) 0
--- THE PROOF TREE ---
[ Input ] a446: (EQUAL (BIT-XOR BIT-0 BIT-0) BIT-0)
[ Input ] a503: (EQUAL (BIT-XOR BIT-0 B2!) BIT-1)
[ Input ] a505: ((EQUAL BIT-0 B2!))
[a503 ()] b1: ((EQUAL (BIT-XOR BIT-0 B2!) BIT-1))
[b1 a505] b1148: ((EQUAL (BIT-XOR BIT-0 BIT-0) BIT-1))
[b1148 a446] b1608:
b1: ((NOT (EQUAL BIT-0 B2!)))
b1? a
Enter automatic mode. To interrupt, press `return' key.
b3 ...................................................................
b71 ...................................................................
b139 ...................................................................
b207 .....................gc: done
..............................................
b275 ....................................
%%% KITP says: ** Proved BIT-XOR-BIT-0-0 by Kitp ** at 06/19/96 14:03:31 with 8.48 Seconds.
CPU seconds used 8.48
Resolvents accepted 309
Useful goal clauses 3
Useful resolvents 3
Nesting limited 16
Depth limited (6) 0
Complexity limited (18) 0
--- THE PROOF TREE ---
[ Input ] a445: (EQUAL (BIT-XOR BIT-0 BIT-1) BIT-1)
[ Input ] a487: ((EQUAL X BIT-0)) ((EQUAL X BIT-1))
[ Input ] a556: (NOT (EQUAL BIT-0 B2!))
[ Input ] a557: ((NOT (EQUAL (BIT-XOR BIT-0 B2!) BIT-1)))
[a557 ()] b2:
((NOT (EQUAL (BIT-XOR BIT-0 B2!) BIT-1)))
[b2 a487] b32:
((NOT (EQUAL (BIT-XOR BIT-0 BIT-1) BIT-1)))
((EQUAL B2! BIT-0))
[b32 a445] b310: ((EQUAL B2! BIT-0))
[b310 a556] b311:
;;; Verified conjecture Bit-Xor.
;;; Verified 1(6?) out of 6 conjectures
NIL
.>
======================================================================