forked from ewenmaclean/Reformation
-
Notifications
You must be signed in to change notification settings - Fork 0
/
lemmas_gn_n4.tptp
73 lines (73 loc) · 2.46 KB
/
lemmas_gn_n4.tptp
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
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
%---------------------------------------------------------------------------
% Problem : hets_exported
% Name : gn_n4
% Author : hets
% Status : unknown
% Desc :
% Date : 2015-06-23 08:36:33.366041 UTC
% Option :
%---------------------------------------------------------------------------
fof(declaration0,axiom,
h(canonical_element)).
fof(declaration1,axiom,
! [X1, X2] : ((g(X1) & g(X2)) => g(plus(X1, X2)))).
fof(declaration2,axiom,
! [X1, X2] : ((g(X1) & g(X2)) => g(qrev(X1, X2)))).
fof(declaration3,axiom,
! [X1] : (g(X1) => g(rev(X1)))).
fof(declaration4,axiom,
! [X1, X2] : ((h(X1) & g(X2)) => g(s(X1, X2)))).
fof(declaration5,axiom,
! [X1, X2] : ((g(X1) & g(X2)) => g(times(X1, X2)))).
fof(declaration6,axiom,
g(zero)).
fof(disjoint_sorts_g_h,axiom,
! [Y1, Y2] : ((g(Y1) & h(Y2)) => ~ Y1 = Y2)).
fof(ga_non_empty_sort_g,axiom,
? [Y] : g(Y)).
fof(ga_non_empty_sort_h,axiom,
? [Y] : h(Y)).
fof(ax1,axiom,
! [X] : (g(X) => ? [A] : (g(A) & s(canonical_element, X) = A))).
fof(ax2,axiom,
! [X] : (g(X) => ~ s(canonical_element, X) = zero)).
fof(ax3,axiom,
rev(zero) = s(canonical_element, zero)).
fof(ax4,axiom,
! [X] : (g(X)
=> rev(s(canonical_element, X))
= times(s(canonical_element, X), rev(X)))).
fof(ax5,axiom,
! [X, Y] : ((g(X) & g(Y))
=> qrev(s(canonical_element, X), Y)
= times(qrev(X, s(canonical_element, X)), Y))).
fof(ax7,axiom,
! [X] : (g(X) => rev(X) = qrev(X, zero))).
fof(ax8,axiom,
! [X, Y] : ((g(X) & g(Y)) => times(rev(X), Y) = qrev(X, Y))).
fof(ax9,axiom,
! [X] : (g(X) => plus(zero, X) = X)).
fof(ax10,axiom,
! [X, Y] : ((g(X) & g(Y))
=> plus(s(canonical_element, X), Y)
= s(canonical_element, plus(X, Y)))).
fof(ax11,axiom,
! [Y] : (g(Y) => times(zero, Y) = zero)).
fof(ax12,axiom,
! [X, Y] : ((g(X) & g(Y))
=> times(s(canonical_element, X), Y) = plus(Y, times(X, Y)))).
fof(ax1_13,axiom,
! [X] : (g(X) => times(zero, X) = X)).
fof(ax2_14,axiom,
! [X, Y, H] : ((g(X) & g(Y) & h(H))
=> times(s(H, X), Y) = s(H, times(X, Y)))).
fof(ax3_15,axiom,
rev(zero) = zero).
fof(ax4_16,axiom,
! [X, H] : ((g(X) & h(H))
=> rev(s(H, X)) = times(rev(X), s(H, zero)))).
fof(ax5_17,axiom,
! [X] : (g(X) => qrev(zero, X) = X)).
fof(ax6_18,axiom,
! [X, Y, H] : ((g(X) & g(Y) & h(H))
=> qrev(s(H, X), Y) = qrev(X, s(H, Y)))).