Theorem expr ≪ | index | src | ≫ 

theorem expr (a: nat) {x y: nat}: $ E. x E. y a = x, y $;
StepHypRefExpression
1
 
_1 = a -> _1 = a
2
 
_1 = a -> x, y = x, y
3
1, 2
 
_1 = a -> (_1 = x, y <-> a = x, y)
4
 
_1 = a -> (E. y _1 = x, y <-> E. y a = x, y)
5
 
_1 = a -> (E. x E. y _1 = x, y <-> E. x E. y a = x, y)
6
 
_1 = 0 -> _1 = 0
7
 
_1 = 0 -> x, y = x, y
8
6, 7
 
_1 = 0 -> (_1 = x, y <-> 0 = x, y)
9
 
_1 = 0 -> (E. y _1 = x, y <-> E. y 0 = x, y)
10
 
_1 = 0 -> (E. x E. y _1 = x, y <-> E. x E. y 0 = x, y)
11
 
_1 = a1 -> _1 = a1
12
 
_1 = a1 -> x, y = x, y
13
 
_1 = a1 -> (_1 = x, y <-> a1 = x, y)
14
 
_1 = a1 -> (E. y _1 = x, y <-> E. y a1 = x, y)
15
 
_1 = a1 -> (E. x E. y _1 = x, y <-> E. x E. y a1 = x, y)
16
 
_1 = suc a1 -> _1 = suc a1
17
 
_1 = suc a1 -> x, y = x, y
18
 
_1 = suc a1 -> (_1 = x, y <-> suc a1 = x, y)
19
 
_1 = suc a1 -> (E. y _1 = x, y <-> E. y suc a1 = x, y)
20
 
_1 = suc a1 -> (E. x E. y _1 = x, y <-> E. x E. y suc a1 = x, y)
21
 
0, 0 = 0
22
 
x = 0 -> y = 0 -> x, y = 0, 0
23
 
x = 0 /\ y = 0 -> x, y = 0, 0
24
 
x = 0 /\ y = 0 -> 0, 0 = x, y
25
 
x = 0 /\ y = 0 -> 0 = x, y
26
 
x = 0 -> E. y 0 = x, y
27
 
E. x E. y 0 = x, y
28
 
m = x /\ n = y -> m = x
29
 
m = x /\ n = y -> n = y
30
 
m = x /\ n = y -> m, n = x, y
31
 
m = x /\ n = y -> (suc a1 = m, n <-> suc a1 = x, y)
32
 
m = x -> (E. n suc a1 = m, n <-> E. y suc a1 = x, y)
33
 
E. m E. n suc a1 = m, n <-> E. x E. y suc a1 = x, y
34
 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> a1 = x, y
35
 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> suc a1 = suc (x, y)
36
 
(x + y) * suc (x + y) // 2 + suc y = suc ((x + y) * suc (x + y) // 2 + y)
37
conv pr
 
(x + y) * suc (x + y) // 2 + suc y = suc (x, y)
39
 
2 != 0
40
 
2 * ((x + y) * suc (x + y) // 2 + suc y) = 2 * (suc y * suc (suc y) // 2) <-> (x + y) * suc (x + y) // 2 + suc y = suc y * suc (suc y) // 2
41
 
2 * ((x + y) * suc (x + y) // 2 + suc y) = 2 * ((x + y) * suc (x + y) // 2) + 2 * suc y
44
 
2 || suc y * suc (suc y)
45
 
2 * (suc y * suc (suc y) // 2) = suc y * suc (suc y)
47
 
suc y * suc (suc y) = suc (suc y) * suc y
48
 
2 * (suc y * suc (suc y) // 2) = suc (suc y) * suc y
50
 
2 || (x + y) * suc (x + y)
51
 
2 * ((x + y) * suc (x + y) // 2) = (x + y) * suc (x + y)
52
 
0 + y = y
53
 
a1 = x, y /\ x = 0 -> x = 0
54
 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> x = 0
55
 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> x + y = 0 + y
56
 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> x + y = y
57
 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> suc (x + y) = suc y
58
 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> (x + y) * suc (x + y) = y * suc y
59
 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> 2 * ((x + y) * suc (x + y) // 2) = y * suc y
60
 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> 2 * ((x + y) * suc (x + y) // 2) + 2 * suc y = y * suc y + 2 * suc y
61
 
(y + 2) * suc y = y * suc y + 2 * suc y
64
 
y + suc 1 = suc (y + 1)
65
conv d2
 
y + 2 = suc (y + 1)
68
 
y + 1 = suc y
69
 
suc (y + 1) = suc (suc y)
70
 
y + 2 = suc (suc y)
71
 
(y + 2) * suc y = suc (suc y) * suc y
72
 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> (y + 2) * suc y = suc (suc y) * suc y
73
 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> y * suc y + 2 * suc y = suc (suc y) * suc y
74
 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> 2 * ((x + y) * suc (x + y) // 2) + 2 * suc y = suc (suc y) * suc y
75
 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> 2 * ((x + y) * suc (x + y) // 2) + 2 * suc y = 2 * (suc y * suc (suc y) // 2)
76
 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> 2 * ((x + y) * suc (x + y) // 2 + suc y) = 2 * (suc y * suc (suc y) // 2)
77
 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> (x + y) * suc (x + y) // 2 + suc y = suc y * suc (suc y) // 2
78
 
suc y * suc (suc y) // 2 + 0 = suc y * suc (suc y) // 2
79
 
suc y + 0 = suc y
80
 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> m = suc y
81
 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> n = 0
82
 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> m + n = suc y + 0
83
 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> m + n = suc y
84
 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> suc (m + n) = suc (suc y)
85
 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> (m + n) * suc (m + n) = suc y * suc (suc y)
86
 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> (m + n) * suc (m + n) // 2 = suc y * suc (suc y) // 2
87
 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> (m + n) * suc (m + n) // 2 + n = suc y * suc (suc y) // 2 + 0
88
conv pr
 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> m, n = suc y * suc (suc y) // 2 + 0
89
 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> m, n = suc y * suc (suc y) // 2
90
 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> (x + y) * suc (x + y) // 2 + suc y = m, n
91
 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> suc (x, y) = m, n
92
 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> suc a1 = m, n
93
 
a1 = x, y /\ x = 0 /\ m = suc y -> E. n suc a1 = m, n
94
 
a1 = x, y /\ x = 0 -> E. m E. n suc a1 = m, n
95
 
a1 = x, y -> x = 0 -> E. m E. n suc a1 = m, n
96
 
x != 0 <-> E. z x = suc z
97
conv ne
 
~x = 0 <-> E. z x = suc z
98
 
a1 = x, y -> suc a1 = suc (x, y)
99
 
a1 = x, y /\ x = suc z /\ m = z /\ n = suc y -> suc a1 = suc (x, y)
100
 
suc z + y = z + suc y
101
 
x = suc z -> x + y = suc z + y
102
 
a1 = x, y /\ x = suc z -> x + y = suc z + y
103
 
a1 = x, y /\ x = suc z /\ m = z /\ n = suc y -> x + y = suc z + y
104
 
a1 = x, y /\ x = suc z /\ m = z /\ n = suc y -> x + y = z + suc y
105
 
a1 = x, y /\ x = suc z /\ m = z /\ n = suc y -> m = z
106
 
a1 = x, y /\ x = suc z /\ m = z /\ n = suc y -> n = suc y
107
 
a1 = x, y /\ x = suc z /\ m = z /\ n = suc y -> m + n = z + suc y
108
 
a1 = x, y /\ x = suc z /\ m = z /\ n = suc y -> x + y = m + n
109
 
a1 = x, y /\ x = suc z /\ m = z /\ n = suc y -> suc (x + y) = suc (m + n)
110
 
a1 = x, y /\ x = suc z /\ m = z /\ n = suc y -> (x + y) * suc (x + y) = (m + n) * suc (m + n)
111
 
a1 = x, y /\ x = suc z /\ m = z /\ n = suc y -> (x + y) * suc (x + y) // 2 = (m + n) * suc (m + n) // 2
112
 
a1 = x, y /\ x = suc z /\ m = z /\ n = suc y -> suc y = n
113
 
a1 = x, y /\ x = suc z /\ m = z /\ n = suc y -> (x + y) * suc (x + y) // 2 + suc y = (m + n) * suc (m + n) // 2 + n
114
conv pr
 
a1 = x, y /\ x = suc z /\ m = z /\ n = suc y -> (x + y) * suc (x + y) // 2 + suc y = m, n
115
 
a1 = x, y /\ x = suc z /\ m = z /\ n = suc y -> suc (x, y) = m, n
116
 
a1 = x, y /\ x = suc z /\ m = z /\ n = suc y -> suc a1 = m, n
117
 
a1 = x, y /\ x = suc z /\ m = z -> E. n suc a1 = m, n
118
 
a1 = x, y /\ x = suc z -> E. m E. n suc a1 = m, n
119
 
a1 = x, y -> E. z x = suc z -> E. m E. n suc a1 = m, n
120
 
a1 = x, y -> ~x = 0 -> E. m E. n suc a1 = m, n
121
 
a1 = x, y -> E. m E. n suc a1 = m, n
122
 
E. y a1 = x, y -> E. m E. n suc a1 = m, n
123
 
E. x E. y a1 = x, y -> E. m E. n suc a1 = m, n
124
 
E. x E. y a1 = x, y -> E. x E. y suc a1 = x, y
125
5, 10, 15, 20, 27, 124
 
E. x E. y a = x, y

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)