<div dir="ltr">Dear Joe,<div><br></div><div>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)</div><div> <br></div><div><br></div><div>2) I wonder what this is stating if I run the following command instead:</div><div><div> opentheory info --theory --show-assumptions --show-derivations pair</div></div><div><br></div><div>Looks like it is also trying to find out what the dependency is like but this time much more complicated?</div><div><br></div><div><div>2 external type operators: -> bool</div><div>10 external constants: = select ! /\ ==> ? \/ ~ F T</div></div><div><div>20 theorems:</div><div> {(1) (2) (3) (8) (10) (11) (12) (13) (14) (15) (16) (17) (20) (21) (22)</div><div> (25) (26) (27) (28) (31) (32) (33) (34) (35) (36) (37) (38) (39) (41)</div><div> (42) (43) (44) (45) (46) (47)}</div><div> |- !x. (fst x, snd x) = x</div><div> {(1) (2) (3) (8) (10) (11) (12) (13) (15) (16) (17) (20) (21) (22) (25)</div><div> (26) (27) (28) (31) (32) (33) (34) (35) (36) (37) (38) (39) (41) (42)</div><div> (43) (44) (45) (46) (47)}</div><div> |- !a b. fst (a, b) = a</div><div> {(1) (2) (3) (8) (10) (11) (12) (13) (15) (16) (17) (20) (21) (22) (25)</div><div> (26) (27) (28) (31) (32) (33) (34) (35) (36) (37) (38) (39) (41) (42)</div><div> (43) (44) (45) (46) (47)}</div><div> |- !a b. snd (a, b) = b</div><div> {(1) (8) (10) (11) (12) (14) (26) (27) (33) (35) (36)}</div><div> |- !x. ?a b. x = (a, b)</div><div> {(1) (2) (3) (4) (8) (10) (11) (12) (13) (14) (15) (16) (17) (18) (19)</div><div> (20) (21) (22) (23) (24) (25) (26) (27) (28) (31) (32) (33) (34) (35)</div><div> (36) (37) (38) (39) (40) (41) (42) (43) (44) (45) (46) (47) (48) (49)}</div><div> |- !p. (!x. p x) <=> !a b. p (a, b)</div><div> {(1) (2) (3) (4) (5) (6) (7) (8) (10) (11) (12) (13) (14) (15) (16) (17)</div><div> (18) (19) (20) (21) (22) (23) (24) (25) (26) (27) (28) (31) (32) (33)</div><div> (34) (35) (36) (37) (38) (39) (40) (41) (42) (43) (44) (45) (46) (47)</div><div> (48) (49)}</div><div> |- !p. (?x. p x) <=> ?a b. p (a, b)</div><div> {(1) (2) (3) (8) (10) (11) (12) (13) (14) (15) (16) (17) (20) (21) (22)</div><div> (25) (26) (27) (28) (31) (32) (33) (34) (35) (36) (37) (38) (39) (41)</div><div> (42) (43) (44) (45) (46) (47)}</div><div> |- !p. (!a b. p (a, b)) ==> !x. p x</div><div> {(1) (2) (3) (8) (9) (10) (11) (12) (13) (15) (16) (17) (20) (21) (22)</div><div> (25) (26) (27) (28) (29) (30) (31) (32) (33) (34) (35) (36) (37) (38)</div><div> (39) (41) (42) (43) (44) (45) (46) (47)}</div><div> |- !p. (!f. p f) <=> !f. p (\a b. f (a, b))</div><div> {(1) (2) (3) (4) (8) (9) (10) (11) (12) (13) (15) (16) (17) (20) (21)</div><div> (22) (25) (26) (27) (28) (29) (30) (31) (32) (33) (34) (35) (36) (37)</div><div> (38) (39) (41) (42) (43) (44) (45) (46) (47)}</div><div> |- !p. (?f. p f) <=> ?f. p (\a b. f (a, b))</div><div> {(1) (2) (3) (8) (9) (10) (11) (12) (13) (15) (16) (17) (20) (21) (22)</div><div> (25) (26) (27) (28) (31) (32) (33) (34) (35) (36) (37) (38) (39) (41)</div><div> (42) (43) (44) (45) (46) (47)}</div><div> |- !f. ?fn. !a b. fn (a, b) = f a b</div><div> {(1) (2) (3) (4) (8) (9) (10) (11) (12) (13) (14) (15) (16) (17) (18)</div><div> (19) (20) (21) (22) (23) (24) (25) (26) (27) (28) (31) (32) (33) (34)</div><div> (35) (36) (37) (38) (39) (40) (41) (42) (43) (44) (45) (46) (47) (48)</div><div> (49)}</div><div> |- !p. (!x y. p x y) <=> !z. p (fst z) (snd z)</div><div> {(1) (2) (3) (4) (5) (6) (7) (8) (9) (10) (11) (12) (13) (14) (15) (16)</div><div> (17) (18) (19) (20) (21) (22) (23) (24) (25) (26) (27) (28) (31) (32)</div><div> (33) (34) (35) (36) (37) (38) (39) (40) (41) (42) (43) (44) (45) (46)</div><div> (47) (48) (49)}</div><div> |- !p. (?x y. p x y) <=> ?z. p (fst z) (snd z)</div><div> {(1) (2) (3) (4) (8) (9) (10) (11) (12) (13) (14) (15) (16) (17) (18)</div><div> (19) (20) (21) (22) (23) (24) (25) (26) (27) (28) (29) (30) (31) (32)</div><div> (33) (34) (35) (36) (37) (38) (39) (40) (41) (42) (43) (44) (45) (46)</div><div> (47) (48) (49)}</div><div> |- !f. (\x. f x) = \(a, b). f (a, b)</div><div> {(1) (2) (3) (8) (10) (11) (12) (13) (15) (16) (17) (20) (21) (22) (25)</div><div> (26) (27) (28) (31) (32) (33) (34) (35) (36) (37) (38) (39) (41) (42)</div><div> (43) (44) (46) (47)}</div><div> |- !a b a' b'. (a, b) = (a', b') <=> a = a' /\ b = b'</div><div> {(1) (2) (3) (4) (8) (9) (10) (11) (12) (13) (14) (15) (16) (17) (18)</div><div> (19) (20) (21) (22) (23) (24) (25) (26) (27) (28) (29) (30) (31) (32)</div><div> (33) (34) (35) (36) (37) (38) (39) (40) (41) (42) (43) (44) (45) (46)</div><div> (47) (48) (49)}</div><div> |- !p. (!f. p f) <=> !f. p (\(a, b). f a b)</div><div> {(1) (2) (3) (4) (8) (9) (10) (11) (12) (13) (14) (15) (16) (17) (18)</div><div> (19) (20) (21) (22) (23) (24) (25) (26) (27) (28) (29) (30) (31) (32)</div><div> (33) (34) (35) (36) (37) (38) (39) (40) (41) (42) (43) (44) (45) (46)</div><div> (47) (48) (49)}</div><div> |- !p. (?f. p f) <=> ?f. p (\(a, b). f a b)</div><div> {(1) (2) (3) (4) (8) (9) (10) (11) (12) (13) (14) (15) (16) (17) (18)</div><div> (19) (20) (21) (22) (23) (24) (25) (26) (27) (28) (29) (30) (31) (32)</div><div> (33) (34) (35) (36) (37) (38) (39) (40) (41) (42) (43) (44) (45) (46)</div><div> (47) (48) (49)}</div><div> |- !p. (!(a, b). p a b) <=> !a b. p a b</div><div> {(1) (2) (3) (4) (8) (9) (10) (11) (12) (13) (14) (15) (16) (17) (18)</div><div> (19) (20) (21) (22) (23) (24) (25) (26) (27) (28) (29) (30) (31) (32)</div><div> (33) (34) (35) (36) (37) (38) (39) (40) (41) (42) (43) (44) (45) (46)</div><div> (47) (48) (49)}</div><div> |- !p. (?(a, b). p a b) <=> ?a b. p a b</div><div> {(1) (2) (3) (4) (8) (9) (10) (11) (12) (13) (14) (15) (16) (17) (18)</div><div> (19) (20) (21) (22) (23) (24) (25) (26) (27) (28) (29) (30) (31) (32)</div><div> (33) (34) (35) (36) (37) (38) (39) (40) (41) (42) (43) (44) (45) (46)</div><div> (47) (48) (49)}</div><div> |- !p. (!(a, b, c). p a b c) <=> !a b c. p a b c</div><div> {(1) (2) (3) (4) (8) (9) (10) (11) (12) (13) (14) (15) (16) (17) (18)</div><div> (19) (20) (21) (22) (23) (24) (25) (26) (27) (28) (29) (30) (31) (32)</div><div> (33) (34) (35) (36) (37) (38) (39) (40) (41) (42) (43) (44) (45) (46)</div><div> (47) (48) (49)}</div><div> |- !p. (?(a, b, c). p a b c) <=> ?a b c. p a b c</div><div><br></div><div>Looks confusing without any comments explaining what I got here.</div><div><br></div><div>Thanks very much!</div>-- <br><div class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><br></div><div>Regards,</div><div><a href="http://www.dptinfo.ens-cachan.fr/~swang/" target="_blank">Robert White </a>(Shuai Wang)</div><div><a href="https://www.rocq.inria.fr/deducteam/" target="_blank">INRIA Deducteam</a></div><div>[Moving to ILLC of UvA from this Sep. ]</div><div>[New email address will be <a href="mailto:shuai.wang@student.uva.nl" target="_blank">shuai.wang@student.uva.nl</a>]</div><div><br></div></div></div></div></div></div></div></div></div></div></div> </div></div>