[opentheory-users] statistics based on opentheory

[Robert White]

Dear Joe,

1) Is there any function I can call in (OpenTheory's) HOL Light to test
which axioms it is based on and how the dependency looks like? (to avoid
collecting the result and do analysis from the terminal, which is too
painful for a guy with poor eye sight)


2) I wonder what this is stating if I run the following command instead:
 opentheory info --theory --show-assumptions --show-derivations pair

Looks like it is also trying to find out what the dependency is like but
this time much more complicated?

2 external type operators: -> bool
10 external constants: = select ! /\ ==> ? \/ ~ F T
20 theorems:
  {(1) (2) (3) (8) (10) (11) (12) (13) (14) (15) (16) (17) (20) (21) (22)
     (25) (26) (27) (28) (31) (32) (33) (34) (35) (36) (37) (38) (39) (41)
     (42) (43) (44) (45) (46) (47)}
    |- !x. (fst x, snd x) = x
  {(1) (2) (3) (8) (10) (11) (12) (13) (15) (16) (17) (20) (21) (22) (25)
     (26) (27) (28) (31) (32) (33) (34) (35) (36) (37) (38) (39) (41) (42)
     (43) (44) (45) (46) (47)}
    |- !a b. fst (a, b) = a
  {(1) (2) (3) (8) (10) (11) (12) (13) (15) (16) (17) (20) (21) (22) (25)
     (26) (27) (28) (31) (32) (33) (34) (35) (36) (37) (38) (39) (41) (42)
     (43) (44) (45) (46) (47)}
    |- !a b. snd (a, b) = b
  {(1) (8) (10) (11) (12) (14) (26) (27) (33) (35) (36)}
    |- !x. ?a b. x = (a, b)
  {(1) (2) (3) (4) (8) (10) (11) (12) (13) (14) (15) (16) (17) (18) (19)
     (20) (21) (22) (23) (24) (25) (26) (27) (28) (31) (32) (33) (34) (35)
     (36) (37) (38) (39) (40) (41) (42) (43) (44) (45) (46) (47) (48) (49)}
    |- !p. (!x. p x) <=> !a b. p (a, b)
  {(1) (2) (3) (4) (5) (6) (7) (8) (10) (11) (12) (13) (14) (15) (16) (17)
     (18) (19) (20) (21) (22) (23) (24) (25) (26) (27) (28) (31) (32) (33)
     (34) (35) (36) (37) (38) (39) (40) (41) (42) (43) (44) (45) (46) (47)
     (48) (49)}
    |- !p. (?x. p x) <=> ?a b. p (a, b)
  {(1) (2) (3) (8) (10) (11) (12) (13) (14) (15) (16) (17) (20) (21) (22)
     (25) (26) (27) (28) (31) (32) (33) (34) (35) (36) (37) (38) (39) (41)
     (42) (43) (44) (45) (46) (47)}
    |- !p. (!a b. p (a, b)) ==> !x. p x
  {(1) (2) (3) (8) (9) (10) (11) (12) (13) (15) (16) (17) (20) (21) (22)
     (25) (26) (27) (28) (29) (30) (31) (32) (33) (34) (35) (36) (37) (38)
     (39) (41) (42) (43) (44) (45) (46) (47)}
    |- !p. (!f. p f) <=> !f. p (\a b. f (a, b))
  {(1) (2) (3) (4) (8) (9) (10) (11) (12) (13) (15) (16) (17) (20) (21)
     (22) (25) (26) (27) (28) (29) (30) (31) (32) (33) (34) (35) (36) (37)
     (38) (39) (41) (42) (43) (44) (45) (46) (47)}
    |- !p. (?f. p f) <=> ?f. p (\a b. f (a, b))
  {(1) (2) (3) (8) (9) (10) (11) (12) (13) (15) (16) (17) (20) (21) (22)
     (25) (26) (27) (28) (31) (32) (33) (34) (35) (36) (37) (38) (39) (41)
     (42) (43) (44) (45) (46) (47)}
    |- !f. ?fn. !a b. fn (a, b) = f a b
  {(1) (2) (3) (4) (8) (9) (10) (11) (12) (13) (14) (15) (16) (17) (18)
     (19) (20) (21) (22) (23) (24) (25) (26) (27) (28) (31) (32) (33) (34)
     (35) (36) (37) (38) (39) (40) (41) (42) (43) (44) (45) (46) (47) (48)
     (49)}
    |- !p. (!x y. p x y) <=> !z. p (fst z) (snd z)
  {(1) (2) (3) (4) (5) (6) (7) (8) (9) (10) (11) (12) (13) (14) (15) (16)
     (17) (18) (19) (20) (21) (22) (23) (24) (25) (26) (27) (28) (31) (32)
     (33) (34) (35) (36) (37) (38) (39) (40) (41) (42) (43) (44) (45) (46)
     (47) (48) (49)}
    |- !p. (?x y. p x y) <=> ?z. p (fst z) (snd z)
  {(1) (2) (3) (4) (8) (9) (10) (11) (12) (13) (14) (15) (16) (17) (18)
     (19) (20) (21) (22) (23) (24) (25) (26) (27) (28) (29) (30) (31) (32)
     (33) (34) (35) (36) (37) (38) (39) (40) (41) (42) (43) (44) (45) (46)
     (47) (48) (49)}
    |- !f. (\x. f x) = \(a, b). f (a, b)
  {(1) (2) (3) (8) (10) (11) (12) (13) (15) (16) (17) (20) (21) (22) (25)
     (26) (27) (28) (31) (32) (33) (34) (35) (36) (37) (38) (39) (41) (42)
     (43) (44) (46) (47)}
    |- !a b a' b'. (a, b) = (a', b') <=> a = a' /\ b = b'
  {(1) (2) (3) (4) (8) (9) (10) (11) (12) (13) (14) (15) (16) (17) (18)
     (19) (20) (21) (22) (23) (24) (25) (26) (27) (28) (29) (30) (31) (32)
     (33) (34) (35) (36) (37) (38) (39) (40) (41) (42) (43) (44) (45) (46)
     (47) (48) (49)}
    |- !p. (!f. p f) <=> !f. p (\(a, b). f a b)
  {(1) (2) (3) (4) (8) (9) (10) (11) (12) (13) (14) (15) (16) (17) (18)
     (19) (20) (21) (22) (23) (24) (25) (26) (27) (28) (29) (30) (31) (32)
     (33) (34) (35) (36) (37) (38) (39) (40) (41) (42) (43) (44) (45) (46)
     (47) (48) (49)}
    |- !p. (?f. p f) <=> ?f. p (\(a, b). f a b)
  {(1) (2) (3) (4) (8) (9) (10) (11) (12) (13) (14) (15) (16) (17) (18)
     (19) (20) (21) (22) (23) (24) (25) (26) (27) (28) (29) (30) (31) (32)
     (33) (34) (35) (36) (37) (38) (39) (40) (41) (42) (43) (44) (45) (46)
     (47) (48) (49)}
    |- !p. (!(a, b). p a b) <=> !a b. p a b
  {(1) (2) (3) (4) (8) (9) (10) (11) (12) (13) (14) (15) (16) (17) (18)
     (19) (20) (21) (22) (23) (24) (25) (26) (27) (28) (29) (30) (31) (32)
     (33) (34) (35) (36) (37) (38) (39) (40) (41) (42) (43) (44) (45) (46)
     (47) (48) (49)}
    |- !p. (?(a, b). p a b) <=> ?a b. p a b
  {(1) (2) (3) (4) (8) (9) (10) (11) (12) (13) (14) (15) (16) (17) (18)
     (19) (20) (21) (22) (23) (24) (25) (26) (27) (28) (29) (30) (31) (32)
     (33) (34) (35) (36) (37) (38) (39) (40) (41) (42) (43) (44) (45) (46)
     (47) (48) (49)}
    |- !p. (!(a, b, c). p a b c) <=> !a b c. p a b c
  {(1) (2) (3) (4) (8) (9) (10) (11) (12) (13) (14) (15) (16) (17) (18)
     (19) (20) (21) (22) (23) (24) (25) (26) (27) (28) (29) (30) (31) (32)
     (33) (34) (35) (36) (37) (38) (39) (40) (41) (42) (43) (44) (45) (46)
     (47) (48) (49)}
    |- !p. (?(a, b, c). p a b c) <=> ?a b c. p a b c

Looks confusing without any comments explaining what I got here.

Thanks very much!
-- 

Regards,
Robert White <http://www.dptinfo.ens-cachan.fr/~swang/>(Shuai Wang)
INRIA Deducteam <https://www.rocq.inria.fr/deducteam/>
[Moving to ILLC of UvA from this Sep. ]
[New email address will be shuai.wang at student.uva.nl]
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150608/83078c23/attachment.html>