Search for blocks/addresses/...
Proofgold Asset
asset id
70a823a7d0675604befe7727e0be188f78b4b14131e9fa740476d7730abc757e
asset hash
07403673985c18ab01ebfaf693ab25fee3159516773c3c47bc80b49f7955788d
bday / block
25648
tx
bdeeb..
preasset
doc published by
PrGxv..
Param
int
int
:
ι
Param
add_SNo
add_SNo
:
ι
→
ι
→
ι
Param
If_i
If_i
:
ο
→
ι
→
ι
→
ι
Param
SNoLe
SNoLe
:
ι
→
ι
→
ο
Param
minus_SNo
minus_SNo
:
ι
→
ι
Param
ordsucc
ordsucc
:
ι
→
ι
Param
mul_SNo
mul_SNo
:
ι
→
ι
→
ι
Conjecture
651ef..
A277355
:
∀ x0 :
ι → ι
.
(
∀ x1 .
x1
∈
int
⟶
x0
x1
∈
int
)
⟶
∀ x1 :
ι →
ι → ι
.
(
∀ x2 .
x2
∈
int
⟶
∀ x3 .
x3
∈
int
⟶
x1
x2
x3
∈
int
)
⟶
∀ x2 :
ι → ι
.
(
∀ x3 .
x3
∈
int
⟶
x2
x3
∈
int
)
⟶
∀ x3 :
ι →
ι → ι
.
(
∀ x4 .
x4
∈
int
⟶
∀ x5 .
x5
∈
int
⟶
x3
x4
x5
∈
int
)
⟶
∀ x4 :
ι →
ι → ι
.
(
∀ x5 .
x5
∈
int
⟶
∀ x6 .
x6
∈
int
⟶
x4
x5
x6
∈
int
)
⟶
∀ x5 :
ι →
ι → ι
.
(
∀ x6 .
x6
∈
int
⟶
∀ x7 .
x7
∈
int
⟶
x5
x6
x7
∈
int
)
⟶
∀ x6 :
ι → ι
.
(
∀ x7 .
x7
∈
int
⟶
x6
x7
∈
int
)
⟶
∀ x7 .
x7
∈
int
⟶
∀ x8 :
ι →
ι → ι
.
(
∀ x9 .
x9
∈
int
⟶
∀ x10 .
x10
∈
int
⟶
x8
x9
x10
∈
int
)
⟶
∀ x9 :
ι → ι
.
(
∀ x10 .
x10
∈
int
⟶
x9
x10
∈
int
)
⟶
∀ x10 :
ι → ι
.
(
∀ x11 .
x11
∈
int
⟶
x10
x11
∈
int
)
⟶
∀ x11 :
ι → ι
.
(
∀ x12 .
x12
∈
int
⟶
x11
x12
∈
int
)
⟶
∀ x12 :
ι →
ι → ι
.
(
∀ x13 .
x13
∈
int
⟶
∀ x14 .
x14
∈
int
⟶
x12
x13
x14
∈
int
)
⟶
∀ x13 .
x13
∈
int
⟶
∀ x14 :
ι →
ι → ι
.
(
∀ x15 .
x15
∈
int
⟶
∀ x16 .
x16
∈
int
⟶
x14
x15
x16
∈
int
)
⟶
∀ x15 :
ι →
ι → ι
.
(
∀ x16 .
x16
∈
int
⟶
∀ x17 .
x17
∈
int
⟶
x15
x16
x17
∈
int
)
⟶
∀ x16 :
ι →
ι → ι
.
(
∀ x17 .
x17
∈
int
⟶
∀ x18 .
x18
∈
int
⟶
x16
x17
x18
∈
int
)
⟶
∀ x17 :
ι → ι
.
(
∀ x18 .
x18
∈
int
⟶
x17
x18
∈
int
)
⟶
∀ x18 .
x18
∈
int
⟶
∀ x19 :
ι →
ι → ι
.
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
x19
x20
x21
∈
int
)
⟶
∀ x20 :
ι → ι
.
(
∀ x21 .
x21
∈
int
⟶
x20
x21
∈
int
)
⟶
∀ x21 :
ι → ι
.
(
∀ x22 .
x22
∈
int
⟶
x21
x22
∈
int
)
⟶
(
∀ x22 .
x22
∈
int
⟶
x0
x22
=
add_SNo
x22
x22
)
⟶
(
∀ x22 .
x22
∈
int
⟶
∀ x23 .
x23
∈
int
⟶
x1
x22
x23
=
x23
)
⟶
(
∀ x22 .
x22
∈
int
⟶
x2
x22
=
x22
)
⟶
(
∀ x22 .
x22
∈
int
⟶
∀ x23 .
x23
∈
int
⟶
x3
x22
x23
=
If_i
(
SNoLe
x22
0
)
x23
(
x0
(
x3
(
add_SNo
x22
(
minus_SNo
1
)
)
x23
)
)
)
⟶
(
∀ x22 .
x22
∈
int
⟶
∀ x23 .
x23
∈
int
⟶
x4
x22
x23
=
x3
(
x1
x22
x23
)
(
x2
x22
)
)
⟶
(
∀ x22 .
x22
∈
int
⟶
∀ x23 .
x23
∈
int
⟶
x5
x22
x23
=
add_SNo
(
mul_SNo
x22
x23
)
(
x4
x22
x23
)
)
⟶
(
∀ x22 .
x22
∈
int
⟶
x6
x22
=
x22
)
⟶
x7
=
1
⟶
(
∀ x22 .
x22
∈
int
⟶
∀ x23 .
x23
∈
int
⟶
x8
x22
x23
=
If_i
(
SNoLe
x22
0
)
x23
(
x5
(
x8
(
add_SNo
x22
(
minus_SNo
1
)
)
x23
)
x22
)
)
⟶
(
∀ x22 .
x22
∈
int
⟶
x9
x22
=
x8
(
x6
x22
)
x7
)
⟶
(
∀ x22 .
x22
∈
int
⟶
x10
x22
=
x9
x22
)
⟶
(
∀ x22 .
x22
∈
int
⟶
x11
x22
=
add_SNo
x22
x22
)
⟶
(
∀ x22 .
x22
∈
int
⟶
∀ x23 .
x23
∈
int
⟶
x12
x22
x23
=
add_SNo
x23
(
minus_SNo
1
)
)
⟶
x13
=
2
⟶
(
∀ x22 .
x22
∈
int
⟶
∀ x23 .
x23
∈
int
⟶
x14
x22
x23
=
If_i
(
SNoLe
x22
0
)
x23
(
x11
(
x14
(
add_SNo
x22
(
minus_SNo
1
)
)
x23
)
)
)
⟶
(
∀ x22 .
x22
∈
int
⟶
∀ x23 .
x23
∈
int
⟶
x15
x22
x23
=
x14
(
x12
x22
x23
)
x13
)
⟶
(
∀ x22 .
x22
∈
int
⟶
∀ x23 .
x23
∈
int
⟶
x16
x22
x23
=
mul_SNo
(
add_SNo
(
x15
x22
x23
)
x23
)
x22
)
⟶
(
∀ x22 .
x22
∈
int
⟶
x17
x22
=
x22
)
⟶
x18
=
1
⟶
(
∀ x22 .
x22
∈
int
⟶
∀ x23 .
x23
∈
int
⟶
x19
x22
x23
=
If_i
(
SNoLe
x22
0
)
x23
(
x16
(
x19
(
add_SNo
x22
(
minus_SNo
1
)
)
x23
)
x22
)
)
⟶
(
∀ x22 .
x22
∈
int
⟶
x20
x22
=
x19
(
x17
x22
)
x18
)
⟶
(
∀ x22 .
x22
∈
int
⟶
x21
x22
=
x20
x22
)
⟶
∀ x22 .
x22
∈
int
⟶
SNoLe
0
x22
⟶
x10
x22
=
x21
x22
Conjecture
660b8..
A277168
:
∀ x0 :
ι →
ι → ι
.
(
∀ x1 .
x1
∈
int
⟶
∀ x2 .
x2
∈
int
⟶
x0
x1
x2
∈
int
)
⟶
∀ x1 :
ι → ι
.
(
∀ x2 .
x2
∈
int
⟶
x1
x2
∈
int
)
⟶
∀ x2 .
x2
∈
int
⟶
∀ x3 :
ι →
ι → ι
.
(
∀ x4 .
x4
∈
int
⟶
∀ x5 .
x5
∈
int
⟶
x3
x4
x5
∈
int
)
⟶
∀ x4 :
ι → ι
.
(
∀ x5 .
x5
∈
int
⟶
x4
x5
∈
int
)
⟶
∀ x5 :
ι →
ι → ι
.
(
∀ x6 .
x6
∈
int
⟶
∀ x7 .
x7
∈
int
⟶
x5
x6
x7
∈
int
)
⟶
∀ x6 :
ι →
ι → ι
.
(
∀ x7 .
x7
∈
int
⟶
∀ x8 .
x8
∈
int
⟶
x6
x7
x8
∈
int
)
⟶
∀ x7 :
ι → ι
.
(
∀ x8 .
x8
∈
int
⟶
x7
x8
∈
int
)
⟶
∀ x8 .
x8
∈
int
⟶
∀ x9 :
ι → ι
.
(
∀ x10 .
x10
∈
int
⟶
x9
x10
∈
int
)
⟶
∀ x10 :
ι →
ι →
ι → ι
.
(
∀ x11 .
x11
∈
int
⟶
∀ x12 .
x12
∈
int
⟶
∀ x13 .
x13
∈
int
⟶
x10
x11
x12
x13
∈
int
)
⟶
∀ x11 :
ι →
ι →
ι → ι
.
(
∀ x12 .
x12
∈
int
⟶
∀ x13 .
x13
∈
int
⟶
∀ x14 .
x14
∈
int
⟶
x11
x12
x13
x14
∈
int
)
⟶
∀ x12 :
ι → ι
.
(
∀ x13 .
x13
∈
int
⟶
x12
x13
∈
int
)
⟶
∀ x13 :
ι → ι
.
(
∀ x14 .
x14
∈
int
⟶
x13
x14
∈
int
)
⟶
∀ x14 :
ι →
ι → ι
.
(
∀ x15 .
x15
∈
int
⟶
∀ x16 .
x16
∈
int
⟶
x14
x15
x16
∈
int
)
⟶
∀ x15 :
ι →
ι → ι
.
(
∀ x16 .
x16
∈
int
⟶
∀ x17 .
x17
∈
int
⟶
x15
x16
x17
∈
int
)
⟶
∀ x16 :
ι → ι
.
(
∀ x17 .
x17
∈
int
⟶
x16
x17
∈
int
)
⟶
∀ x17 .
x17
∈
int
⟶
∀ x18 :
ι → ι
.
(
∀ x19 .
x19
∈
int
⟶
x18
x19
∈
int
)
⟶
∀ x19 :
ι →
ι →
ι → ι
.
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
∀ x22 .
x22
∈
int
⟶
x19
x20
x21
x22
∈
int
)
⟶
∀ x20 :
ι →
ι →
ι → ι
.
(
∀ x21 .
x21
∈
int
⟶
∀ x22 .
x22
∈
int
⟶
∀ x23 .
x23
∈
int
⟶
x20
x21
x22
x23
∈
int
)
⟶
∀ x21 :
ι → ι
.
(
∀ x22 .
x22
∈
int
⟶
x21
x22
∈
int
)
⟶
∀ x22 :
ι →
ι → ι
.
(
∀ x23 .
x23
∈
int
⟶
∀ x24 .
x24
∈
int
⟶
x22
x23
x24
∈
int
)
⟶
∀ x23 :
ι →
ι → ι
.
(
∀ x24 .
x24
∈
int
⟶
∀ x25 .
x25
∈
int
⟶
x23
x24
x25
∈
int
)
⟶
∀ x24 :
ι → ι
.
(
∀ x25 .
x25
∈
int
⟶
x24
x25
∈
int
)
⟶
∀ x25 .
x25
∈
int
⟶
∀ x26 :
ι → ι
.
(
∀ x27 .
x27
∈
int
⟶
x26
x27
∈
int
)
⟶
∀ x27 :
ι →
ι →
ι → ι
.
(
∀ x28 .
x28
∈
int
⟶
∀ x29 .
x29
∈
int
⟶
∀ x30 .
x30
∈
int
⟶
x27
x28
x29
x30
∈
int
)
⟶
∀ x28 :
ι →
ι →
ι → ι
.
(
∀ x29 .
x29
∈
int
⟶
∀ x30 .
x30
∈
int
⟶
∀ x31 .
x31
∈
int
⟶
x28
x29
x30
x31
∈
int
)
⟶
∀ x29 :
ι → ι
.
(
∀ x30 .
x30
∈
int
⟶
x29
x30
∈
int
)
⟶
∀ x30 :
ι → ι
.
(
∀ x31 .
x31
∈
int
⟶
x30
x31
∈
int
)
⟶
(
∀ x31 .
x31
∈
int
⟶
∀ x32 .
x32
∈
int
⟶
x0
x31
x32
=
add_SNo
(
mul_SNo
2
(
mul_SNo
x31
x32
)
)
(
minus_SNo
x31
)
)
⟶
(
∀ x31 .
x31
∈
int
⟶
x1
x31
=
x31
)
⟶
x2
=
1
⟶
(
∀ x31 .
x31
∈
int
⟶
∀ x32 .
x32
∈
int
⟶
x3
x31
x32
=
If_i
(
SNoLe
x31
0
)
x32
(
x0
(
x3
(
add_SNo
x31
(
minus_SNo
1
)
)
x32
)
x31
)
)
⟶
(
∀ x31 .
x31
∈
int
⟶
x4
x31
=
x3
(
x1
x31
)
x2
)
⟶
(
∀ x31 .
x31
∈
int
⟶
∀ x32 .
x32
∈
int
⟶
x5
x31
x32
=
mul_SNo
x31
x32
)
⟶
(
∀ x31 .
x31
∈
int
⟶
∀ x32 .
x32
∈
int
⟶
x6
x31
x32
=
x32
)
⟶
(
∀ x31 .
x31
∈
int
⟶
x7
x31
=
x31
)
⟶
x8
=
1
⟶
(
∀ x31 .
x31
∈
int
⟶
x9
x31
=
add_SNo
2
(
mul_SNo
2
(
add_SNo
x31
x31
)
)
)
⟶
(
∀ x31 .
x31
∈
int
⟶
∀ x32 .
x32
∈
int
⟶
∀ x33 .
x33
∈
int
⟶
x10
x31
x32
x33
=
If_i
(
SNoLe
x31
0
)
x32
(
x5
(
x10
(
add_SNo
x31
(
minus_SNo
1
)
)
x32
x33
)
(
x11
(
add_SNo
x31
(
minus_SNo
1
)
)
x32
x33
)
)
)
⟶
(
∀ x31 .
x31
∈
int
⟶
∀ x32 .
x32
∈
int
⟶
∀ x33 .
x33
∈
int
⟶
x11
x31
x32
x33
=
If_i
(
SNoLe
x31
0
)
x33
(
x6
(
x10
(
add_SNo
x31
(
minus_SNo
1
)
)
x32
x33
)
(
x11
(
add_SNo
x31
(
minus_SNo
1
)
)
x32
x33
)
)
)
⟶
(
∀ x31 .
x31
∈
int
⟶
x12
x31
=
x10
(
x7
x31
)
x8
(
x9
x31
)
)
⟶
(
∀ x31 .
x31
∈
int
⟶
x13
x31
=
mul_SNo
(
x4
x31
)
(
x12
x31
)
)
⟶
(
∀ x31 .
x31
∈
int
⟶
∀ x32 .
x32
∈
int
⟶
x14
x31
x32
=
mul_SNo
x31
x32
)
⟶
(
∀ x31 .
x31
∈
int
⟶
∀ x32 .
x32
∈
int
⟶
x15
x31
x32
=
x32
)
⟶
(
∀ x31 .
x31
∈
int
⟶
x16
x31
=
add_SNo
x31
(
minus_SNo
1
)
)
⟶
x17
=
1
⟶
(
∀ x31 .
x31
∈
int
⟶
x18
x31
=
add_SNo
1
(
add_SNo
x31
x31
)
)
⟶
(
∀ x31 .
x31
∈
int
⟶
∀ x32 .
x32
∈
int
⟶
∀ x33 .
x33
∈
int
⟶
x19
x31
x32
x33
=
If_i
(
SNoLe
x31
0
)
x32
(
x14
(
x19
(
add_SNo
x31
(
minus_SNo
1
)
)
x32
x33
)
(
x20
(
add_SNo
x31
(
minus_SNo
1
)
)
x32
x33
)
)
)
⟶
(
∀ x31 .
x31
∈
int
⟶
∀ x32 .
x32
∈
int
⟶
∀ x33 .
x33
∈
int
⟶
x20
x31
x32
x33
=
If_i
(
SNoLe
x31
0
)
x33
(
x15
(
x19
(
add_SNo
x31
(
minus_SNo
1
)
)
x32
x33
)
(
x20
(
add_SNo
x31
(
minus_SNo
1
)
)
x32
x33
)
)
)
⟶
(
∀ x31 .
x31
∈
int
⟶
x21
x31
=
x19
(
x16
x31
)
x17
(
x18
x31
)
)
⟶
(
∀ x31 .
x31
∈
int
⟶
∀ x32 .
x32
∈
int
⟶
x22
x31
x32
=
mul_SNo
x31
x32
)
⟶
(
∀ x31 .
x31
∈
int
⟶
∀ x32 .
x32
∈
int
⟶
x23
x31
x32
=
add_SNo
1
x32
)
⟶
(
∀ x31 .
x31
∈
int
⟶
x24
x31
=
x31
)
⟶
x25
=
1
⟶
(
∀ x31 .
x31
∈
int
⟶
x26
x31
=
add_SNo
1
x31
)
⟶
(
∀ x31 .
x31
∈
int
⟶
∀ x32 .
x32
∈
int
⟶
∀ x33 .
x33
∈
int
⟶
x27
x31
x32
x33
=
If_i
(
SNoLe
x31
0
)
x32
(
x22
(
x27
(
add_SNo
x31
(
minus_SNo
1
)
)
x32
x33
)
(
x28
(
add_SNo
x31
(
minus_SNo
1
)
)
x32
x33
)
)
)
⟶
(
∀ x31 .
x31
∈
int
⟶
∀ x32 .
x32
∈
int
⟶
∀ x33 .
x33
∈
int
⟶
x28
x31
x32
x33
=
If_i
(
SNoLe
x31
0
)
x33
(
x23
(
x27
(
add_SNo
x31
(
minus_SNo
1
)
)
x32
x33
)
(
x28
(
add_SNo
x31
(
minus_SNo
1
)
)
x32
x33
)
)
)
⟶
(
∀ x31 .
x31
∈
int
⟶
x29
x31
=
x27
(
x24
x31
)
x25
(
x26
x31
)
)
⟶
(
∀ x31 .
x31
∈
int
⟶
x30
x31
=
mul_SNo
(
mul_SNo
(
add_SNo
1
(
add_SNo
x31
x31
)
)
(
x21
x31
)
)
(
x29
x31
)
)
⟶
∀ x31 .
x31
∈
int
⟶
SNoLe
0
x31
⟶
x13
x31
=
x30
x31
Conjecture
84ad8..
A276
:
∀ x0 :
ι →
ι → ι
.
(
∀ x1 .
x1
∈
int
⟶
∀ x2 .
x2
∈
int
⟶
x0
x1
x2
∈
int
)
⟶
∀ x1 :
ι →
ι → ι
.
(
∀ x2 .
x2
∈
int
⟶
∀ x3 .
x3
∈
int
⟶
x1
x2
x3
∈
int
)
⟶
∀ x2 .
x2
∈
int
⟶
∀ x3 :
ι →
ι → ι
.
(
∀ x4 .
x4
∈
int
⟶
∀ x5 .
x5
∈
int
⟶
x3
x4
x5
∈
int
)
⟶
∀ x4 :
ι →
ι → ι
.
(
∀ x5 .
x5
∈
int
⟶
∀ x6 .
x6
∈
int
⟶
x4
x5
x6
∈
int
)
⟶
∀ x5 :
ι →
ι → ι
.
(
∀ x6 .
x6
∈
int
⟶
∀ x7 .
x7
∈
int
⟶
x5
x6
x7
∈
int
)
⟶
∀ x6 :
ι → ι
.
(
∀ x7 .
x7
∈
int
⟶
x6
x7
∈
int
)
⟶
∀ x7 .
x7
∈
int
⟶
∀ x8 :
ι →
ι → ι
.
(
∀ x9 .
x9
∈
int
⟶
∀ x10 .
x10
∈
int
⟶
x8
x9
x10
∈
int
)
⟶
∀ x9 :
ι → ι
.
(
∀ x10 .
x10
∈
int
⟶
x9
x10
∈
int
)
⟶
∀ x10 :
ι → ι
.
(
∀ x11 .
x11
∈
int
⟶
x10
x11
∈
int
)
⟶
∀ x11 :
ι →
ι → ι
.
(
∀ x12 .
x12
∈
int
⟶
∀ x13 .
x13
∈
int
⟶
x11
x12
x13
∈
int
)
⟶
∀ x12 :
ι →
ι → ι
.
(
∀ x13 .
x13
∈
int
⟶
∀ x14 .
x14
∈
int
⟶
x12
x13
x14
∈
int
)
⟶
∀ x13 .
x13
∈
int
⟶
∀ x14 :
ι →
ι → ι
.
(
∀ x15 .
x15
∈
int
⟶
∀ x16 .
x16
∈
int
⟶
x14
x15
x16
∈
int
)
⟶
∀ x15 :
ι →
ι → ι
.
(
∀ x16 .
x16
∈
int
⟶
∀ x17 .
x17
∈
int
⟶
x15
x16
x17
∈
int
)
⟶
∀ x16 :
ι →
ι → ι
.
(
∀ x17 .
x17
∈
int
⟶
∀ x18 .
x18
∈
int
⟶
x16
x17
x18
∈
int
)
⟶
∀ x17 :
ι → ι
.
(
∀ x18 .
x18
∈
int
⟶
x17
x18
∈
int
)
⟶
∀ x18 .
x18
∈
int
⟶
∀ x19 :
ι →
ι → ι
.
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
x19
x20
x21
∈
int
)
⟶
∀ x20 :
ι → ι
.
(
∀ x21 .
x21
∈
int
⟶
x20
x21
∈
int
)
⟶
∀ x21 :
ι → ι
.
(
∀ x22 .
x22
∈
int
⟶
x21
x22
∈
int
)
⟶
(
∀ x22 .
x22
∈
int
⟶
∀ x23 .
x23
∈
int
⟶
x0
x22
x23
=
mul_SNo
x22
x23
)
⟶
(
∀ x22 .
x22
∈
int
⟶
∀ x23 .
x23
∈
int
⟶
x1
x22
x23
=
x23
)
⟶
x2
=
1
⟶
(
∀ x22 .
x22
∈
int
⟶
∀ x23 .
x23
∈
int
⟶
x3
x22
x23
=
If_i
(
SNoLe
x22
0
)
x23
(
x0
(
x3
(
add_SNo
x22
(
minus_SNo
1
)
)
x23
)
x22
)
)
⟶
(
∀ x22 .
x22
∈
int
⟶
∀ x23 .
x23
∈
int
⟶
x4
x22
x23
=
x3
(
x1
x22
x23
)
x2
)
⟶
(
∀ x22 .
x22
∈
int
⟶
∀ x23 .
x23
∈
int
⟶
x5
x22
x23
=
mul_SNo
(
add_SNo
(
x4
x22
x23
)
x22
)
(
add_SNo
2
x23
)
)
⟶
(
∀ x22 .
x22
∈
int
⟶
x6
x22
=
add_SNo
1
x22
)
⟶
x7
=
0
⟶
(
∀ x22 .
x22
∈
int
⟶
∀ x23 .
x23
∈
int
⟶
x8
x22
x23
=
If_i
(
SNoLe
x22
0
)
x23
(
x5
(
x8
(
add_SNo
x22
(
minus_SNo
1
)
)
x23
)
x22
)
)
⟶
(
∀ x22 .
x22
∈
int
⟶
x9
x22
=
x8
(
x6
x22
)
x7
)
⟶
(
∀ x22 .
x22
∈
int
⟶
x10
x22
=
x9
x22
)
⟶
(
∀ x22 .
x22
∈
int
⟶
∀ x23 .
x23
∈
int
⟶
x11
x22
x23
=
mul_SNo
x22
x23
)
⟶
(
∀ x22 .
x22
∈
int
⟶
∀ x23 .
x23
∈
int
⟶
x12
x22
x23
=
x23
)
⟶
x13
=
1
⟶
(
∀ x22 .
x22
∈
int
⟶
∀ x23 .
x23
∈
int
⟶
x14
x22
x23
=
If_i
(
SNoLe
x22
0
)
x23
(
x11
(
x14
(
add_SNo
x22
(
minus_SNo
1
)
)
x23
)
x22
)
)
⟶
(
∀ x22 .
x22
∈
int
⟶
∀ x23 .
x23
∈
int
⟶
x15
x22
x23
=
x14
(
x12
x22
x23
)
x13
)
⟶
(
∀ x22 .
x22
∈
int
⟶
∀ x23 .
x23
∈
int
⟶
x16
x22
x23
=
add_SNo
(
mul_SNo
(
add_SNo
(
x15
x22
x23
)
x22
)
(
add_SNo
1
x23
)
)
x22
)
⟶
(
∀ x22 .
x22
∈
int
⟶
x17
x22
=
x22
)
⟶
x18
=
1
⟶
(
∀ x22 .
x22
∈
int
⟶
∀ x23 .
x23
∈
int
⟶
x19
x22
x23
=
If_i
(
SNoLe
x22
0
)
x23
(
x16
(
x19
(
add_SNo
x22
(
minus_SNo
1
)
)
x23
)
x22
)
)
⟶
(
∀ x22 .
x22
∈
int
⟶
x20
x22
=
x19
(
x17
x22
)
x18
)
⟶
(
∀ x22 .
x22
∈
int
⟶
x21
x22
=
mul_SNo
(
x20
x22
)
(
add_SNo
1
(
add_SNo
2
x22
)
)
)
⟶
∀ x22 .
x22
∈
int
⟶
SNoLe
0
x22
⟶
x10
x22
=
x21
x22
Conjecture
0d162..
A276509
:
∀ x0 :
ι →
ι → ι
.
(
∀ x1 .
x1
∈
int
⟶
∀ x2 .
x2
∈
int
⟶
x0
x1
x2
∈
int
)
⟶
∀ x1 :
ι →
ι → ι
.
(
∀ x2 .
x2
∈
int
⟶
∀ x3 .
x3
∈
int
⟶
x1
x2
x3
∈
int
)
⟶
∀ x2 :
ι → ι
.
(
∀ x3 .
x3
∈
int
⟶
x2
x3
∈
int
)
⟶
∀ x3 .
x3
∈
int
⟶
∀ x4 .
x4
∈
int
⟶
∀ x5 :
ι →
ι →
ι → ι
.
(
∀ x6 .
x6
∈
int
⟶
∀ x7 .
x7
∈
int
⟶
∀ x8 .
x8
∈
int
⟶
x5
x6
x7
x8
∈
int
)
⟶
∀ x6 :
ι →
ι →
ι → ι
.
(
∀ x7 .
x7
∈
int
⟶
∀ x8 .
x8
∈
int
⟶
∀ x9 .
x9
∈
int
⟶
x6
x7
x8
x9
∈
int
)
⟶
∀ x7 :
ι → ι
.
(
∀ x8 .
x8
∈
int
⟶
x7
x8
∈
int
)
⟶
∀ x8 :
ι → ι
.
(
∀ x9 .
x9
∈
int
⟶
x8
x9
∈
int
)
⟶
∀ x9 :
ι →
ι → ι
.
(
∀ x10 .
x10
∈
int
⟶
∀ x11 .
x11
∈
int
⟶
x9
x10
x11
∈
int
)
⟶
∀ x10 :
ι →
ι → ι
.
(
∀ x11 .
x11
∈
int
⟶
∀ x12 .
x12
∈
int
⟶
x10
x11
x12
∈
int
)
⟶
∀ x11 :
ι → ι
.
(
∀ x12 .
x12
∈
int
⟶
x11
x12
∈
int
)
⟶
∀ x12 .
x12
∈
int
⟶
∀ x13 .
x13
∈
int
⟶
∀ x14 :
ι →
ι →
ι → ι
.
(
∀ x15 .
x15
∈
int
⟶
∀ x16 .
x16
∈
int
⟶
∀ x17 .
x17
∈
int
⟶
x14
x15
x16
x17
∈
int
)
⟶
∀ x15 :
ι →
ι →
ι → ι
.
(
∀ x16 .
x16
∈
int
⟶
∀ x17 .
x17
∈
int
⟶
∀ x18 .
x18
∈
int
⟶
x15
x16
x17
x18
∈
int
)
⟶
∀ x16 :
ι → ι
.
(
∀ x17 .
x17
∈
int
⟶
x16
x17
∈
int
)
⟶
∀ x17 :
ι → ι
.
(
∀ x18 .
x18
∈
int
⟶
x17
x18
∈
int
)
⟶
(
∀ x18 .
x18
∈
int
⟶
∀ x19 .
x19
∈
int
⟶
x0
x18
x19
=
add_SNo
(
mul_SNo
(
add_SNo
x18
x19
)
(
mul_SNo
x19
x19
)
)
x18
)
⟶
(
∀ x18 .
x18
∈
int
⟶
∀ x19 .
x19
∈
int
⟶
x1
x18
x19
=
x19
)
⟶
(
∀ x18 .
x18
∈
int
⟶
x2
x18
=
x18
)
⟶
x3
=
2
⟶
x4
=
add_SNo
1
2
⟶
(
∀ x18 .
x18
∈
int
⟶
∀ x19 .
x19
∈
int
⟶
∀ x20 .
x20
∈
int
⟶
x5
x18
x19
x20
=
If_i
(
SNoLe
x18
0
)
x19
(
x0
(
x5
(
add_SNo
x18
(
minus_SNo
1
)
)
x19
x20
)
(
x6
(
add_SNo
x18
(
minus_SNo
1
)
)
x19
x20
)
)
)
⟶
(
∀ x18 .
x18
∈
int
⟶
∀ x19 .
x19
∈
int
⟶
∀ x20 .
x20
∈
int
⟶
x6
x18
x19
x20
=
If_i
(
SNoLe
x18
0
)
x20
(
x1
(
x5
(
add_SNo
x18
(
minus_SNo
1
)
)
x19
x20
)
(
x6
(
add_SNo
x18
(
minus_SNo
1
)
)
x19
x20
)
)
)
⟶
(
∀ x18 .
x18
∈
int
⟶
x7
x18
=
x5
(
x2
x18
)
x3
x4
)
⟶
(
∀ x18 .
x18
∈
int
⟶
x8
x18
=
x7
x18
)
⟶
(
∀ x18 .
x18
∈
int
⟶
∀ x19 .
x19
∈
int
⟶
x9
x18
x19
=
mul_SNo
x18
x19
)
⟶
(
∀ x18 .
x18
∈
int
⟶
∀ x19 .
x19
∈
int
⟶
x10
x18
x19
=
x19
)
⟶
(
∀ x18 .
x18
∈
int
⟶
x11
x18
=
add_SNo
x18
(
minus_SNo
1
)
)
⟶
x12
=
1
⟶
x13
=
add_SNo
2
(
mul_SNo
2
(
add_SNo
2
2
)
)
⟶
(
∀ x18 .
x18
∈
int
⟶
∀ x19 .
x19
∈
int
⟶
∀ x20 .
x20
∈
int
⟶
x14
x18
x19
x20
=
If_i
(
SNoLe
x18
0
)
x19
(
x9
(
x14
(
add_SNo
x18
(
minus_SNo
1
)
)
x19
x20
)
(
x15
(
add_SNo
x18
(
minus_SNo
1
)
)
x19
x20
)
)
)
⟶
(
∀ x18 .
x18
∈
int
⟶
∀ x19 .
x19
∈
int
⟶
∀ x20 .
x20
∈
int
⟶
x15
x18
x19
x20
=
If_i
(
SNoLe
x18
0
)
x20
(
x10
(
x14
(
add_SNo
x18
(
minus_SNo
1
)
)
x19
x20
)
(
x15
(
add_SNo
x18
(
minus_SNo
1
)
)
x19
x20
)
)
)
⟶
(
∀ x18 .
x18
∈
int
⟶
x16
x18
=
x14
(
x11
x18
)
x12
x13
)
⟶
(
∀ x18 .
x18
∈
int
⟶
x17
x18
=
add_SNo
(
mul_SNo
(
x16
x18
)
(
mul_SNo
(
If_i
(
SNoLe
x18
0
)
1
(
add_SNo
2
(
mul_SNo
2
(
add_SNo
2
2
)
)
)
)
(
add_SNo
1
(
add_SNo
2
2
)
)
)
)
(
minus_SNo
(
add_SNo
1
2
)
)
)
⟶
∀ x18 .
x18
∈
int
⟶
SNoLe
0
x18
⟶
x8
x18
=
x17
x18
Conjecture
ed2aa..
A274755
:
∀ x0 :
ι →
ι → ι
.
(
∀ x1 .
x1
∈
int
⟶
∀ x2 .
x2
∈
int
⟶
x0
x1
x2
∈
int
)
⟶
∀ x1 :
ι →
ι → ι
.
(
∀ x2 .
x2
∈
int
⟶
∀ x3 .
x3
∈
int
⟶
x1
x2
x3
∈
int
)
⟶
∀ x2 :
ι → ι
.
(
∀ x3 .
x3
∈
int
⟶
x2
x3
∈
int
)
⟶
∀ x3 .
x3
∈
int
⟶
∀ x4 .
x4
∈
int
⟶
∀ x5 :
ι →
ι →
ι → ι
.
(
∀ x6 .
x6
∈
int
⟶
∀ x7 .
x7
∈
int
⟶
∀ x8 .
x8
∈
int
⟶
x5
x6
x7
x8
∈
int
)
⟶
∀ x6 :
ι →
ι →
ι → ι
.
(
∀ x7 .
x7
∈
int
⟶
∀ x8 .
x8
∈
int
⟶
∀ x9 .
x9
∈
int
⟶
x6
x7
x8
x9
∈
int
)
⟶
∀ x7 :
ι → ι
.
(
∀ x8 .
x8
∈
int
⟶
x7
x8
∈
int
)
⟶
∀ x8 :
ι → ι
.
(
∀ x9 .
x9
∈
int
⟶
x8
x9
∈
int
)
⟶
∀ x9 :
ι → ι
.
(
∀ x10 .
x10
∈
int
⟶
x9
x10
∈
int
)
⟶
∀ x10 .
x10
∈
int
⟶
∀ x11 :
ι →
ι → ι
.
(
∀ x12 .
x12
∈
int
⟶
∀ x13 .
x13
∈
int
⟶
x11
x12
x13
∈
int
)
⟶
∀ x12 :
ι →
ι → ι
.
(
∀ x13 .
x13
∈
int
⟶
∀ x14 .
x14
∈
int
⟶
x12
x13
x14
∈
int
)
⟶
∀ x13 :
ι → ι
.
(
∀ x14 .
x14
∈
int
⟶
x13
x14
∈
int
)
⟶
∀ x14 .
x14
∈
int
⟶
∀ x15 .
x15
∈
int
⟶
∀ x16 :
ι →
ι →
ι → ι
.
(
∀ x17 .
x17
∈
int
⟶
∀ x18 .
x18
∈
int
⟶
∀ x19 .
x19
∈
int
⟶
x16
x17
x18
x19
∈
int
)
⟶
∀ x17 :
ι →
ι →
ι → ι
.
(
∀ x18 .
x18
∈
int
⟶
∀ x19 .
x19
∈
int
⟶
∀ x20 .
x20
∈
int
⟶
x17
x18
x19
x20
∈
int
)
⟶
∀ x18 :
ι → ι
.
(
∀ x19 .
x19
∈
int
⟶
x18
x19
∈
int
)
⟶
∀ x19 :
ι → ι
.
(
∀ x20 .
x20
∈
int
⟶
x19
x20
∈
int
)
⟶
∀ x20 :
ι →
ι → ι
.
(
∀ x21 .
x21
∈
int
⟶
∀ x22 .
x22
∈
int
⟶
x20
x21
x22
∈
int
)
⟶
∀ x21 :
ι → ι
.
(
∀ x22 .
x22
∈
int
⟶
x21
x22
∈
int
)
⟶
∀ x22 :
ι → ι
.
(
∀ x23 .
x23
∈
int
⟶
x22
x23
∈
int
)
⟶
(
∀ x23 .
x23
∈
int
⟶
∀ x24 .
x24
∈
int
⟶
x0
x23
x24
=
add_SNo
(
mul_SNo
(
add_SNo
x23
x24
)
x24
)
x23
)
⟶
(
∀ x23 .
x23
∈
int
⟶
∀ x24 .
x24
∈
int
⟶
x1
x23
x24
=
x24
)
⟶
(
∀ x23 .
x23
∈
int
⟶
x2
x23
=
add_SNo
(
mul_SNo
x23
2
)
2
)
⟶
x3
=
2
⟶
x4
=
add_SNo
(
mul_SNo
(
mul_SNo
2
2
)
2
)
1
⟶
(
∀ x23 .
x23
∈
int
⟶
∀ x24 .
x24
∈
int
⟶
∀ x25 .
x25
∈
int
⟶
x5
x23
x24
x25
=
If_i
(
SNoLe
x23
0
)
x24
(
x0
(
x5
(
add_SNo
x23
(
minus_SNo
1
)
)
x24
x25
)
(
x6
(
add_SNo
x23
(
minus_SNo
1
)
)
x24
x25
)
)
)
⟶
(
∀ x23 .
x23
∈
int
⟶
∀ x24 .
x24
∈
int
⟶
∀ x25 .
x25
∈
int
⟶
x6
x23
x24
x25
=
If_i
(
SNoLe
x23
0
)
x25
(
x1
(
x5
(
add_SNo
x23
(
minus_SNo
1
)
)
x24
x25
)
(
x6
(
add_SNo
x23
(
minus_SNo
1
)
)
x24
x25
)
)
)
⟶
(
∀ x23 .
x23
∈
int
⟶
x7
x23
=
x5
(
x2
x23
)
x3
x4
)
⟶
(
∀ x23 .
x23
∈
int
⟶
x8
x23
=
add_SNo
(
x7
x23
)
(
minus_SNo
2
)
)
⟶
(
∀ x23 .
x23
∈
int
⟶
x9
x23
=
mul_SNo
x23
x23
)
⟶
x10
=
1
⟶
(
∀ x23 .
x23
∈
int
⟶
∀ x24 .
x24
∈
int
⟶
x11
x23
x24
=
mul_SNo
x23
x24
)
⟶
(
∀ x23 .
x23
∈
int
⟶
∀ x24 .
x24
∈
int
⟶
x12
x23
x24
=
x24
)
⟶
(
∀ x23 .
x23
∈
int
⟶
x13
x23
=
add_SNo
1
x23
)
⟶
x14
=
1
⟶
x15
=
add_SNo
2
(
mul_SNo
2
(
add_SNo
2
2
)
)
⟶
(
∀ x23 .
x23
∈
int
⟶
∀ x24 .
x24
∈
int
⟶
∀ x25 .
x25
∈
int
⟶
x16
x23
x24
x25
=
If_i
(
SNoLe
x23
0
)
x24
(
x11
(
x16
(
add_SNo
x23
(
minus_SNo
1
)
)
x24
x25
)
(
x17
(
add_SNo
x23
(
minus_SNo
1
)
)
x24
x25
)
)
)
⟶
(
∀ x23 .
x23
∈
int
⟶
∀ x24 .
x24
∈
int
⟶
∀ x25 .
x25
∈
int
⟶
x17
x23
x24
x25
=
If_i
(
SNoLe
x23
0
)
x25
(
x12
(
x16
(
add_SNo
x23
(
minus_SNo
1
)
)
x24
x25
)
(
x17
(
add_SNo
x23
(
minus_SNo
1
)
)
x24
x25
)
)
)
⟶
(
∀ x23 .
x23
∈
int
⟶
x18
x23
=
x16
(
x13
x23
)
x14
x15
)
⟶
(
∀ x23 .
x23
∈
int
⟶
x19
x23
=
x18
x23
)
⟶
(
∀ x23 .
x23
∈
int
⟶
∀ x24 .
x24
∈
int
⟶
x20
x23
x24
=
If_i
(
SNoLe
x23
0
)
x24
(
x9
(
x20
(
add_SNo
x23
(
minus_SNo
1
)
)
x24
)
)
)
⟶
(
∀ x23 .
x23
∈
int
⟶
x21
x23
=
x20
x10
(
x19
x23
)
)
⟶
(
∀ x23 .
x23
∈
int
⟶
x22
x23
=
mul_SNo
(
add_SNo
1
(
add_SNo
2
(
mul_SNo
2
(
add_SNo
2
2
)
)
)
)
(
add_SNo
(
x21
x23
)
(
minus_SNo
1
)
)
)
⟶
∀ x23 .
x23
∈
int
⟶
SNoLe
0
x23
⟶
x8
x23
=
x22
x23
Conjecture
36013..
A272263
:
∀ x0 :
ι →
ι → ι
.
(
∀ x1 .
x1
∈
int
⟶
∀ x2 .
x2
∈
int
⟶
x0
x1
x2
∈
int
)
⟶
∀ x1 :
ι →
ι → ι
.
(
∀ x2 .
x2
∈
int
⟶
∀ x3 .
x3
∈
int
⟶
x1
x2
x3
∈
int
)
⟶
∀ x2 :
ι → ι
.
(
∀ x3 .
x3
∈
int
⟶
x2
x3
∈
int
)
⟶
∀ x3 .
x3
∈
int
⟶
∀ x4 .
x4
∈
int
⟶
∀ x5 :
ι →
ι →
ι → ι
.
(
∀ x6 .
x6
∈
int
⟶
∀ x7 .
x7
∈
int
⟶
∀ x8 .
x8
∈
int
⟶
x5
x6
x7
x8
∈
int
)
⟶
∀ x6 :
ι →
ι →
ι → ι
.
(
∀ x7 .
x7
∈
int
⟶
∀ x8 .
x8
∈
int
⟶
∀ x9 .
x9
∈
int
⟶
x6
x7
x8
x9
∈
int
)
⟶
∀ x7 :
ι → ι
.
(
∀ x8 .
x8
∈
int
⟶
x7
x8
∈
int
)
⟶
∀ x8 :
ι → ι
.
(
∀ x9 .
x9
∈
int
⟶
x8
x9
∈
int
)
⟶
∀ x9 :
ι → ι
.
(
∀ x10 .
x10
∈
int
⟶
x9
x10
∈
int
)
⟶
∀ x10 :
ι → ι
.
(
∀ x11 .
x11
∈
int
⟶
x10
x11
∈
int
)
⟶
∀ x11 :
ι →
ι → ι
.
(
∀ x12 .
x12
∈
int
⟶
∀ x13 .
x13
∈
int
⟶
x11
x12
x13
∈
int
)
⟶
∀ x12 :
ι → ι
.
(
∀ x13 .
x13
∈
int
⟶
x12
x13
∈
int
)
⟶
∀ x13 :
ι → ι
.
(
∀ x14 .
x14
∈
int
⟶
x13
x14
∈
int
)
⟶
∀ x14 .
x14
∈
int
⟶
∀ x15 .
x15
∈
int
⟶
∀ x16 :
ι →
ι →
ι → ι
.
(
∀ x17 .
x17
∈
int
⟶
∀ x18 .
x18
∈
int
⟶
∀ x19 .
x19
∈
int
⟶
x16
x17
x18
x19
∈
int
)
⟶
∀ x17 :
ι →
ι →
ι → ι
.
(
∀ x18 .
x18
∈
int
⟶
∀ x19 .
x19
∈
int
⟶
∀ x20 .
x20
∈
int
⟶
x17
x18
x19
x20
∈
int
)
⟶
∀ x18 :
ι → ι
.
(
∀ x19 .
x19
∈
int
⟶
x18
x19
∈
int
)
⟶
∀ x19 :
ι → ι
.
(
∀ x20 .
x20
∈
int
⟶
x19
x20
∈
int
)
⟶
∀ x20 :
ι →
ι → ι
.
(
∀ x21 .
x21
∈
int
⟶
∀ x22 .
x22
∈
int
⟶
x20
x21
x22
∈
int
)
⟶
∀ x21 :
ι → ι
.
(
∀ x22 .
x22
∈
int
⟶
x21
x22
∈
int
)
⟶
∀ x22 :
ι → ι
.
(
∀ x23 .
x23
∈
int
⟶
x22
x23
∈
int
)
⟶
(
∀ x23 .
x23
∈
int
⟶
∀ x24 .
x24
∈
int
⟶
x0
x23
x24
=
add_SNo
x24
x24
)
⟶
(
∀ x23 .
x23
∈
int
⟶
∀ x24 .
x24
∈
int
⟶
x1
x23
x24
=
mul_SNo
2
(
add_SNo
x23
x24
)
)
⟶
(
∀ x23 .
x23
∈
int
⟶
x2
x23
=
x23
)
⟶
x3
=
2
⟶
x4
=
1
⟶
(
∀ x23 .
x23
∈
int
⟶
∀ x24 .
x24
∈
int
⟶
∀ x25 .
x25
∈
int
⟶
x5
x23
x24
x25
=
If_i
(
SNoLe
x23
0
)
x24
(
x0
(
x5
(
add_SNo
x23
(
minus_SNo
1
)
)
x24
x25
)
(
x6
(
add_SNo
x23
(
minus_SNo
1
)
)
x24
x25
)
)
)
⟶
(
∀ x23 .
x23
∈
int
⟶
∀ x24 .
x24
∈
int
⟶
∀ x25 .
x25
∈
int
⟶
x6
x23
x24
x25
=
If_i
(
SNoLe
x23
0
)
x25
(
x1
(
x5
(
add_SNo
x23
(
minus_SNo
1
)
)
x24
x25
)
(
x6
(
add_SNo
x23
(
minus_SNo
1
)
)
x24
x25
)
)
)
⟶
(
∀ x23 .
x23
∈
int
⟶
x7
x23
=
x5
(
x2
x23
)
x3
x4
)
⟶
(
∀ x23 .
x23
∈
int
⟶
x8
x23
=
add_SNo
(
x7
x23
)
(
minus_SNo
1
)
)
⟶
(
∀ x23 .
x23
∈
int
⟶
x9
x23
=
add_SNo
x23
x23
)
⟶
(
∀ x23 .
x23
∈
int
⟶
x10
x23
=
add_SNo
x23
(
minus_SNo
1
)
)
⟶
(
∀ x23 .
x23
∈
int
⟶
∀ x24 .
x24
∈
int
⟶
x11
x23
x24
=
add_SNo
x23
x24
)
⟶
(
∀ x23 .
x23
∈
int
⟶
x12
x23
=
x23
)
⟶
(
∀ x23 .
x23
∈
int
⟶
x13
x23
=
add_SNo
x23
(
minus_SNo
1
)
)
⟶
x14
=
1
⟶
x15
=
2
⟶
(
∀ x23 .
x23
∈
int
⟶
∀ x24 .
x24
∈
int
⟶
∀ x25 .
x25
∈
int
⟶
x16
x23
x24
x25
=
If_i
(
SNoLe
x23
0
)
x24
(
x11
(
x16
(
add_SNo
x23
(
minus_SNo
1
)
)
x24
x25
)
(
x17
(
add_SNo
x23
(
minus_SNo
1
)
)
x24
x25
)
)
)
⟶
(
∀ x23 .
x23
∈
int
⟶
∀ x24 .
x24
∈
int
⟶
∀ x25 .
x25
∈
int
⟶
x17
x23
x24
x25
=
If_i
(
SNoLe
x23
0
)
x25
(
x12
(
x16
(
add_SNo
x23
(
minus_SNo
1
)
)
x24
x25
)
)
)
⟶
(
∀ x23 .
x23
∈
int
⟶
x18
x23
=
x16
(
x13
x23
)
x14
x15
)
⟶
(
∀ x23 .
x23
∈
int
⟶
x19
x23
=
x18
x23
)
⟶
(
∀ x23 .
x23
∈
int
⟶
∀ x24 .
x24
∈
int
⟶
x20
x23
x24
=
If_i
(
SNoLe
x23
0
)
x24
(
x9
(
x20
(
add_SNo
x23
(
minus_SNo
1
)
)
x24
)
)
)
⟶
(
∀ x23 .
x23
∈
int
⟶
x21
x23
=
x20
(
x10
x23
)
(
x19
x23
)
)
⟶
(
∀ x23 .
x23
∈
int
⟶
x22
x23
=
add_SNo
(
mul_SNo
2
(
x21
x23
)
)
(
minus_SNo
1
)
)
⟶
∀ x23 .
x23
∈
int
⟶
SNoLe
0
x23
⟶
x8
x23
=
x22
x23
Conjecture
7a067..
A271939
:
∀ x0 :
ι →
ι → ι
.
(
∀ x1 .
x1
∈
int
⟶
∀ x2 .
x2
∈
int
⟶
x0
x1
x2
∈
int
)
⟶
∀ x1 :
ι →
ι → ι
.
(
∀ x2 .
x2
∈
int
⟶
∀ x3 .
x3
∈
int
⟶
x1
x2
x3
∈
int
)
⟶
∀ x2 :
ι → ι
.
(
∀ x3 .
x3
∈
int
⟶
x2
x3
∈
int
)
⟶
∀ x3 .
x3
∈
int
⟶
∀ x4 .
x4
∈
int
⟶
∀ x5 :
ι →
ι →
ι → ι
.
(
∀ x6 .
x6
∈
int
⟶
∀ x7 .
x7
∈
int
⟶
∀ x8 .
x8
∈
int
⟶
x5
x6
x7
x8
∈
int
)
⟶
∀ x6 :
ι →
ι →
ι → ι
.
(
∀ x7 .
x7
∈
int
⟶
∀ x8 .
x8
∈
int
⟶
∀ x9 .
x9
∈
int
⟶
x6
x7
x8
x9
∈
int
)
⟶
∀ x7 :
ι → ι
.
(
∀ x8 .
x8
∈
int
⟶
x7
x8
∈
int
)
⟶
∀ x8 :
ι → ι
.
(
∀ x9 .
x9
∈
int
⟶
x8
x9
∈
int
)
⟶
∀ x9 :
ι →
ι → ι
.
(
∀ x10 .
x10
∈
int
⟶
∀ x11 .
x11
∈
int
⟶
x9
x10
x11
∈
int
)
⟶
∀ x10 :
ι →
ι → ι
.
(
∀ x11 .
x11
∈
int
⟶
∀ x12 .
x12
∈
int
⟶
x10
x11
x12
∈
int
)
⟶
∀ x11 :
ι → ι
.
(
∀ x12 .
x12
∈
int
⟶
x11
x12
∈
int
)
⟶
∀ x12 .
x12
∈
int
⟶
∀ x13 .
x13
∈
int
⟶
∀ x14 :
ι →
ι →
ι → ι
.
(
∀ x15 .
x15
∈
int
⟶
∀ x16 .
x16
∈
int
⟶
∀ x17 .
x17
∈
int
⟶
x14
x15
x16
x17
∈
int
)
⟶
∀ x15 :
ι →
ι →
ι → ι
.
(
∀ x16 .
x16
∈
int
⟶
∀ x17 .
x17
∈
int
⟶
∀ x18 .
x18
∈
int
⟶
x15
x16
x17
x18
∈
int
)
⟶
∀ x16 :
ι → ι
.
(
∀ x17 .
x17
∈
int
⟶
x16
x17
∈
int
)
⟶
∀ x17 :
ι → ι
.
(
∀ x18 .
x18
∈
int
⟶
x17
x18
∈
int
)
⟶
(
∀ x18 .
x18
∈
int
⟶
∀ x19 .
x19
∈
int
⟶
x0
x18
x19
=
add_SNo
(
add_SNo
(
add_SNo
(
mul_SNo
(
mul_SNo
x19
x19
)
x19
)
x18
)
x18
)
x18
)
⟶
(
∀ x18 .
x18
∈
int
⟶
∀ x19 .
x19
∈
int
⟶
x1
x18
x19
=
add_SNo
x19
x19
)
⟶
(
∀ x18 .
x18
∈
int
⟶
x2
x18
=
add_SNo
1
x18
)
⟶
x3
=
0
⟶
x4
=
2
⟶
(
∀ x18 .
x18
∈
int
⟶
∀ x19 .
x19
∈
int
⟶
∀ x20 .
x20
∈
int
⟶
x5
x18
x19
x20
=
If_i
(
SNoLe
x18
0
)
x19
(
x0
(
x5
(
add_SNo
x18
(
minus_SNo
1
)
)
x19
x20
)
(
x6
(
add_SNo
x18
(
minus_SNo
1
)
)
x19
x20
)
)
)
⟶
(
∀ x18 .
x18
∈
int
⟶
∀ x19 .
x19
∈
int
⟶
∀ x20 .
x20
∈
int
⟶
x6
x18
x19
x20
=
If_i
(
SNoLe
x18
0
)
x20
(
x1
(
x5
(
add_SNo
x18
(
minus_SNo
1
)
)
x19
x20
)
(
x6
(
add_SNo
x18
(
minus_SNo
1
)
)
x19
x20
)
)
)
⟶
(
∀ x18 .
x18
∈
int
⟶
x7
x18
=
x5
(
x2
x18
)
x3
x4
)
⟶
(
∀ x18 .
x18
∈
int
⟶
x8
x18
=
x7
x18
)
⟶
(
∀ x18 .
x18
∈
int
⟶
∀ x19 .
x19
∈
int
⟶
x9
x18
x19
=
add_SNo
(
mul_SNo
2
(
add_SNo
(
mul_SNo
(
mul_SNo
x19
x19
)
x19
)
x18
)
)
x18
)
⟶
(
∀ x18 .
x18
∈
int
⟶
∀ x19 .
x19
∈
int
⟶
x10
x18
x19
=
add_SNo
x19
x19
)
⟶
(
∀ x18 .
x18
∈
int
⟶
x11
x18
=
x18
)
⟶
x12
=
2
⟶
x13
=
2
⟶
(
∀ x18 .
x18
∈
int
⟶
∀ x19 .
x19
∈
int
⟶
∀ x20 .
x20
∈
int
⟶
x14
x18
x19
x20
=
If_i
(
SNoLe
x18
0
)
x19
(
x9
(
x14
(
add_SNo
x18
(
minus_SNo
1
)
)
x19
x20
)
(
x15
(
add_SNo
x18
(
minus_SNo
1
)
)
x19
x20
)
)
)
⟶
(
∀ x18 .
x18
∈
int
⟶
∀ x19 .
x19
∈
int
⟶
∀ x20 .
x20
∈
int
⟶
x15
x18
x19
x20
=
If_i
(
SNoLe
x18
0
)
x20
(
x10
(
x14
(
add_SNo
x18
(
minus_SNo
1
)
)
x19
x20
)
(
x15
(
add_SNo
x18
(
minus_SNo
1
)
)
x19
x20
)
)
)
⟶
(
∀ x18 .
x18
∈
int
⟶
x16
x18
=
x14
(
x11
x18
)
x12
x13
)
⟶
(
∀ x18 .
x18
∈
int
⟶
x17
x18
=
mul_SNo
(
mul_SNo
(
x16
x18
)
2
)
2
)
⟶
∀ x18 .
x18
∈
int
⟶
SNoLe
0
x18
⟶
x8
x18
=
x17
x18
Conjecture
eb24f..
A2700
:
∀ x0 :
ι → ι
.
(
∀ x1 .
x1
∈
int
⟶
x0
x1
∈
int
)
⟶
∀ x1 :
ι → ι
.
(
∀ x2 .
x2
∈
int
⟶
x1
x2
∈
int
)
⟶
∀ x2 :
ι → ι
.
(
∀ x3 .
x3
∈
int
⟶
x2
x3
∈
int
)
⟶
∀ x3 :
ι →
ι → ι
.
(
∀ x4 .
x4
∈
int
⟶
∀ x5 .
x5
∈
int
⟶
x3
x4
x5
∈
int
)
⟶
∀ x4 :
ι → ι
.
(
∀ x5 .
x5
∈
int
⟶
x4
x5
∈
int
)
⟶
∀ x5 :
ι → ι
.
(
∀ x6 .
x6
∈
int
⟶
x5
x6
∈
int
)
⟶
∀ x6 :
ι → ι
.
(
∀ x7 .
x7
∈
int
⟶
x6
x7
∈
int
)
⟶
∀ x7 .
x7
∈
int
⟶
∀ x8 :
ι → ι
.
(
∀ x9 .
x9
∈
int
⟶
x8
x9
∈
int
)
⟶
∀ x9 :
ι → ι
.
(
∀ x10 .
x10
∈
int
⟶
x9
x10
∈
int
)
⟶
∀ x10 .
x10
∈
int
⟶
∀ x11 :
ι →
ι → ι
.
(
∀ x12 .
x12
∈
int
⟶
∀ x13 .
x13
∈
int
⟶
x11
x12
x13
∈
int
)
⟶
∀ x12 :
ι → ι
.
(
∀ x13 .
x13
∈
int
⟶
x12
x13
∈
int
)
⟶
∀ x13 :
ι → ι
.
(
∀ x14 .
x14
∈
int
⟶
x13
x14
∈
int
)
⟶
∀ x14 :
ι →
ι → ι
.
(
∀ x15 .
x15
∈
int
⟶
∀ x16 .
x16
∈
int
⟶
x14
x15
x16
∈
int
)
⟶
∀ x15 :
ι → ι
.
(
∀ x16 .
x16
∈
int
⟶
x15
x16
∈
int
)
⟶
∀ x16 :
ι → ι
.
(
∀ x17 .
x17
∈
int
⟶
x16
x17
∈
int
)
⟶
(
∀ x17 .
x17
∈
int
⟶
x0
x17
=
add_SNo
x17
x17
)
⟶
(
∀ x17 .
x17
∈
int
⟶
x1
x17
=
add_SNo
x17
x17
)
⟶
(
∀ x17 .
x17
∈
int
⟶
x2
x17
=
add_SNo
1
x17
)
⟶
(
∀ x17 .
x17
∈
int
⟶
∀ x18 .
x18
∈
int
⟶
x3
x17
x18
=
If_i
(
SNoLe
x17
0
)
x18
(
x0
(
x3
(
add_SNo
x17
(
minus_SNo
1
)
)
x18
)
)
)
⟶
(
∀ x17 .
x17
∈
int
⟶
x4
x17
=
x3
(
x1
x17
)
(
x2
x17
)
)
⟶
(
∀ x17 .
x17
∈
int
⟶
x5
x17
=
mul_SNo
(
add_SNo
1
(
add_SNo
2
(
add_SNo
x17
x17
)
)
)
(
x4
x17
)
)
⟶
(
∀ x17 .
x17
∈
int
⟶
x6
x17
=
mul_SNo
x17
x17
)
⟶
x7
=
1
⟶
(
∀ x17 .
x17
∈
int
⟶
x8
x17
=
add_SNo
x17
x17
)
⟶
(
∀ x17 .
x17
∈
int
⟶
x9
x17
=
x17
)
⟶
x10
=
1
⟶
(
∀ x17 .
x17
∈
int
⟶
∀ x18 .
x18
∈
int
⟶
x11
x17
x18
=
If_i
(
SNoLe
x17
0
)
x18
(
x8
(
x11
(
add_SNo
x17
(
minus_SNo
1
)
)
x18
)
)
)
⟶
(
∀ x17 .
x17
∈
int
⟶
x12
x17
=
x11
(
x9
x17
)
x10
)
⟶
(
∀ x17 .
x17
∈
int
⟶
x13
x17
=
x12
x17
)
⟶
(
∀ x17 .
x17
∈
int
⟶
∀ x18 .
x18
∈
int
⟶
x14
x17
x18
=
If_i
(
SNoLe
x17
0
)
x18
(
x6
(
x14
(
add_SNo
x17
(
minus_SNo
1
)
)
x18
)
)
)
⟶
(
∀ x17 .
x17
∈
int
⟶
x15
x17
=
x14
x7
(
x13
x17
)
)
⟶
(
∀ x17 .
x17
∈
int
⟶
x16
x17
=
mul_SNo
(
add_SNo
1
(
add_SNo
2
(
add_SNo
x17
x17
)
)
)
(
mul_SNo
(
add_SNo
1
x17
)
(
x15
x17
)
)
)
⟶
∀ x17 .
x17
∈
int
⟶
SNoLe
0
x17
⟶
x5
x17
=
x16
x17
Conjecture
fe67d..
A2697
:
∀ x0 :
ι → ι
.
(
∀ x1 .
x1
∈
int
⟶
x0
x1
∈
int
)
⟶
∀ x1 :
ι → ι
.
(
∀ x2 .
x2
∈
int
⟶
x1
x2
∈
int
)
⟶
∀ x2 :
ι → ι
.
(
∀ x3 .
x3
∈
int
⟶
x2
x3
∈
int
)
⟶
∀ x3 :
ι →
ι → ι
.
(
∀ x4 .
x4
∈
int
⟶
∀ x5 .
x5
∈
int
⟶
x3
x4
x5
∈
int
)
⟶
∀ x4 :
ι → ι
.
(
∀ x5 .
x5
∈
int
⟶
x4
x5
∈
int
)
⟶
∀ x5 :
ι → ι
.
(
∀ x6 .
x6
∈
int
⟶
x5
x6
∈
int
)
⟶
∀ x6 :
ι → ι
.
(
∀ x7 .
x7
∈
int
⟶
x6
x7
∈
int
)
⟶
∀ x7 .
x7
∈
int
⟶
∀ x8 :
ι → ι
.
(
∀ x9 .
x9
∈
int
⟶
x8
x9
∈
int
)
⟶
∀ x9 :
ι → ι
.
(
∀ x10 .
x10
∈
int
⟶
x9
x10
∈
int
)
⟶
∀ x10 .
x10
∈
int
⟶
∀ x11 :
ι →
ι → ι
.
(
∀ x12 .
x12
∈
int
⟶
∀ x13 .
x13
∈
int
⟶
x11
x12
x13
∈
int
)
⟶
∀ x12 :
ι → ι
.
(
∀ x13 .
x13
∈
int
⟶
x12
x13
∈
int
)
⟶
∀ x13 :
ι → ι
.
(
∀ x14 .
x14
∈
int
⟶
x13
x14
∈
int
)
⟶
∀ x14 :
ι →
ι → ι
.
(
∀ x15 .
x15
∈
int
⟶
∀ x16 .
x16
∈
int
⟶
x14
x15
x16
∈
int
)
⟶
∀ x15 :
ι → ι
.
(
∀ x16 .
x16
∈
int
⟶
x15
x16
∈
int
)
⟶
∀ x16 :
ι → ι
.
(
∀ x17 .
x17
∈
int
⟶
x16
x17
∈
int
)
⟶
(
∀ x17 .
x17
∈
int
⟶
x0
x17
=
add_SNo
x17
x17
)
⟶
(
∀ x17 .
x17
∈
int
⟶
x1
x17
=
add_SNo
(
add_SNo
x17
(
minus_SNo
2
)
)
x17
)
⟶
(
∀ x17 .
x17
∈
int
⟶
x2
x17
=
x17
)
⟶
(
∀ x17 .
x17
∈
int
⟶
∀ x18 .
x18
∈
int
⟶
x3
x17
x18
=
If_i
(
SNoLe
x17
0
)
x18
(
x0
(
x3
(
add_SNo
x17
(
minus_SNo
1
)
)
x18
)
)
)
⟶
(
∀ x17 .
x17
∈
int
⟶
x4
x17
=
x3
(
x1
x17
)
(
x2
x17
)
)
⟶
(
∀ x17 .
x17
∈
int
⟶
x5
x17
=
x4
x17
)
⟶
(
∀ x17 .
x17
∈
int
⟶
x6
x17
=
mul_SNo
x17
x17
)
⟶
x7
=
1
⟶
(
∀ x17 .
x17
∈
int
⟶
x8
x17
=
add_SNo
x17
x17
)
⟶
(
∀ x17 .
x17
∈
int
⟶
x9
x17
=
add_SNo
x17
(
minus_SNo
1
)
)
⟶
x10
=
1
⟶
(
∀ x17 .
x17
∈
int
⟶
∀ x18 .
x18
∈
int
⟶
x11
x17
x18
=
If_i
(
SNoLe
x17
0
)
x18
(
x8
(
x11
(
add_SNo
x17
(
minus_SNo
1
)
)
x18
)
)
)
⟶
(
∀ x17 .
x17
∈
int
⟶
x12
x17
=
x11
(
x9
x17
)
x10
)
⟶
(
∀ x17 .
x17
∈
int
⟶
x13
x17
=
x12
x17
)
⟶
(
∀ x17 .
x17
∈
int
⟶
∀ x18 .
x18
∈
int
⟶
x14
x17
x18
=
If_i
(
SNoLe
x17
0
)
x18
(
x6
(
x14
(
add_SNo
x17
(
minus_SNo
1
)
)
x18
)
)
)
⟶
(
∀ x17 .
x17
∈
int
⟶
x15
x17
=
x14
x7
(
x13
x17
)
)
⟶
(
∀ x17 .
x17
∈
int
⟶
x16
x17
=
mul_SNo
(
x15
x17
)
x17
)
⟶
∀ x17 .
x17
∈
int
⟶
SNoLe
0
x17
⟶
x5
x17
=
x16
x17
Conjecture
4188a..
A2690
:
∀ x0 :
ι →
ι → ι
.
(
∀ x1 .
x1
∈
int
⟶
∀ x2 .
x2
∈
int
⟶
x0
x1
x2
∈
int
)
⟶
∀ x1 :
ι → ι
.
(
∀ x2 .
x2
∈
int
⟶
x1
x2
∈
int
)
⟶
∀ x2 :
ι → ι
.
(
∀ x3 .
x3
∈
int
⟶
x2
x3
∈
int
)
⟶
∀ x3 :
ι →
ι → ι
.
(
∀ x4 .
x4
∈
int
⟶
∀ x5 .
x5
∈
int
⟶
x3
x4
x5
∈
int
)
⟶
∀ x4 :
ι → ι
.
(
∀ x5 .
x5
∈
int
⟶
x4
x5
∈
int
)
⟶
∀ x5 :
ι → ι
.
(
∀ x6 .
x6
∈
int
⟶
x5
x6
∈
int
)
⟶
∀ x6 :
ι → ι
.
(
∀ x7 .
x7
∈
int
⟶
x6
x7
∈
int
)
⟶
∀ x7 :
ι → ι
.
(
∀ x8 .
x8
∈
int
⟶
x7
x8
∈
int
)
⟶
∀ x8 :
ι → ι
.
(
∀ x9 .
x9
∈
int
⟶
x8
x9
∈
int
)
⟶
∀ x9 :
ι →
ι → ι
.
(
∀ x10 .
x10
∈
int
⟶
∀ x11 .
x11
∈
int
⟶
x9
x10
x11
∈
int
)
⟶
∀ x10 :
ι → ι
.
(
∀ x11 .
x11
∈
int
⟶
x10
x11
∈
int
)
⟶
∀ x11 :
ι →
ι → ι
.
(
∀ x12 .
x12
∈
int
⟶
∀ x13 .
x13
∈
int
⟶
x11
x12
x13
∈
int
)
⟶
∀ x12 :
ι →
ι → ι
.
(
∀ x13 .
x13
∈
int
⟶
∀ x14 .
x14
∈
int
⟶
x12
x13
x14
∈
int
)
⟶
∀ x13 :
ι → ι
.
(
∀ x14 .
x14
∈
int
⟶
x13
x14
∈
int
)
⟶
∀ x14 .
x14
∈
int
⟶
∀ x15 .
x15
∈
int
⟶
∀ x16 :
ι →
ι →
ι → ι
.
(
∀ x17 .
x17
∈
int
⟶
∀ x18 .
x18
∈
int
⟶
∀ x19 .
x19
∈
int
⟶
x16
x17
x18
x19
∈
int
)
⟶
∀ x17 :
ι →
ι →
ι → ι
.
(
∀ x18 .
x18
∈
int
⟶
∀ x19 .
x19
∈
int
⟶
∀ x20 .
x20
∈
int
⟶
x17
x18
x19
x20
∈
int
)
⟶
∀ x18 :
ι → ι
.
(
∀ x19 .
x19
∈
int
⟶
x18
x19
∈
int
)
⟶
∀ x19 :
ι → ι
.
(
∀ x20 .
x20
∈
int
⟶
x19
x20
∈
int
)
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
x0
x20
x21
=
mul_SNo
2
(
add_SNo
(
mul_SNo
2
(
mul_SNo
x20
x21
)
)
(
minus_SNo
x20
)
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x1
x20
=
x20
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x2
x20
=
add_SNo
1
x20
)
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
x3
x20
x21
=
If_i
(
SNoLe
x20
0
)
x21
(
x0
(
x3
(
add_SNo
x20
(
minus_SNo
1
)
)
x21
)
x20
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x4
x20
=
x3
(
x1
x20
)
(
x2
x20
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x5
x20
=
x4
x20
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x6
x20
=
add_SNo
x20
x20
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x7
x20
=
x20
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x8
x20
=
add_SNo
1
x20
)
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
x9
x20
x21
=
If_i
(
SNoLe
x20
0
)
x21
(
x6
(
x9
(
add_SNo
x20
(
minus_SNo
1
)
)
x21
)
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x10
x20
=
x9
(
x7
x20
)
(
x8
x20
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
x11
x20
x21
=
mul_SNo
x20
x21
)
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
x12
x20
x21
=
add_SNo
2
x21
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x13
x20
=
add_SNo
x20
(
minus_SNo
1
)
)
⟶
x14
=
1
⟶
x15
=
add_SNo
1
2
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
∀ x22 .
x22
∈
int
⟶
x16
x20
x21
x22
=
If_i
(
SNoLe
x20
0
)
x21
(
x11
(
x16
(
add_SNo
x20
(
minus_SNo
1
)
)
x21
x22
)
(
x17
(
add_SNo
x20
(
minus_SNo
1
)
)
x21
x22
)
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
∀ x22 .
x22
∈
int
⟶
x17
x20
x21
x22
=
If_i
(
SNoLe
x20
0
)
x22
(
x12
(
x16
(
add_SNo
x20
(
minus_SNo
1
)
)
x21
x22
)
(
x17
(
add_SNo
x20
(
minus_SNo
1
)
)
x21
x22
)
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x18
x20
=
x16
(
x13
x20
)
x14
x15
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x19
x20
=
mul_SNo
(
x10
x20
)
(
x18
x20
)
)
⟶
∀ x20 .
x20
∈
int
⟶
SNoLe
0
x20
⟶
x5
x20
=
x19
x20
Conjecture
b91c5..
A269025
:
∀ x0 :
ι →
ι → ι
.
(
∀ x1 .
x1
∈
int
⟶
∀ x2 .
x2
∈
int
⟶
x0
x1
x2
∈
int
)
⟶
∀ x1 .
x1
∈
int
⟶
∀ x2 :
ι → ι
.
(
∀ x3 .
x3
∈
int
⟶
x2
x3
∈
int
)
⟶
∀ x3 :
ι →
ι → ι
.
(
∀ x4 .
x4
∈
int
⟶
∀ x5 .
x5
∈
int
⟶
x3
x4
x5
∈
int
)
⟶
∀ x4 :
ι → ι
.
(
∀ x5 .
x5
∈
int
⟶
x4
x5
∈
int
)
⟶
∀ x5 :
ι → ι
.
(
∀ x6 .
x6
∈
int
⟶
x5
x6
∈
int
)
⟶
∀ x6 :
ι → ι
.
(
∀ x7 .
x7
∈
int
⟶
x6
x7
∈
int
)
⟶
∀ x7 .
x7
∈
int
⟶
∀ x8 :
ι →
ι → ι
.
(
∀ x9 .
x9
∈
int
⟶
∀ x10 .
x10
∈
int
⟶
x8
x9
x10
∈
int
)
⟶
∀ x9 :
ι → ι
.
(
∀ x10 .
x10
∈
int
⟶
x9
x10
∈
int
)
⟶
∀ x10 :
ι → ι
.
(
∀ x11 .
x11
∈
int
⟶
x10
x11
∈
int
)
⟶
∀ x11 :
ι →
ι → ι
.
(
∀ x12 .
x12
∈
int
⟶
∀ x13 .
x13
∈
int
⟶
x11
x12
x13
∈
int
)
⟶
∀ x12 :
ι →
ι → ι
.
(
∀ x13 .
x13
∈
int
⟶
∀ x14 .
x14
∈
int
⟶
x12
x13
x14
∈
int
)
⟶
∀ x13 :
ι → ι
.
(
∀ x14 .
x14
∈
int
⟶
x13
x14
∈
int
)
⟶
∀ x14 .
x14
∈
int
⟶
∀ x15 :
ι → ι
.
(
∀ x16 .
x16
∈
int
⟶
x15
x16
∈
int
)
⟶
∀ x16 .
x16
∈
int
⟶
∀ x17 .
x17
∈
int
⟶
∀ x18 :
ι →
ι → ι
.
(
∀ x19 .
x19
∈
int
⟶
∀ x20 .
x20
∈
int
⟶
x18
x19
x20
∈
int
)
⟶
∀ x19 .
x19
∈
int
⟶
∀ x20 .
x20
∈
int
⟶
∀ x21 :
ι →
ι →
ι → ι
.
(
∀ x22 .
x22
∈
int
⟶
∀ x23 .
x23
∈
int
⟶
∀ x24 .
x24
∈
int
⟶
x21
x22
x23
x24
∈
int
)
⟶
∀ x22 :
ι →
ι →
ι → ι
.
(
∀ x23 .
x23
∈
int
⟶
∀ x24 .
x24
∈
int
⟶
∀ x25 .
x25
∈
int
⟶
x22
x23
x24
x25
∈
int
)
⟶
∀ x23 :
ι → ι
.
(
∀ x24 .
x24
∈
int
⟶
x23
x24
∈
int
)
⟶
∀ x24 :
ι → ι
.
(
∀ x25 .
x25
∈
int
⟶
x24
x25
∈
int
)
⟶
(
∀ x25 .
x25
∈
int
⟶
∀ x26 .
x26
∈
int
⟶
x0
x25
x26
=
mul_SNo
(
add_SNo
2
x26
)
x25
)
⟶
x1
=
add_SNo
1
2
⟶
(
∀ x25 .
x25
∈
int
⟶
x2
x25
=
x25
)
⟶
(
∀ x25 .
x25
∈
int
⟶
∀ x26 .
x26
∈
int
⟶
x3
x25
x26
=
If_i
(
SNoLe
x25
0
)
x26
(
x0
(
x3
(
add_SNo
x25
(
minus_SNo
1
)
)
x26
)
x25
)
)
⟶
(
∀ x25 .
x25
∈
int
⟶
x4
x25
=
x3
x1
(
x2
x25
)
)
⟶
(
∀ x25 .
x25
∈
int
⟶
x5
x25
=
add_SNo
1
(
x4
x25
)
)
⟶
(
∀ x25 .
x25
∈
int
⟶
x6
x25
=
x25
)
⟶
x7
=
1
⟶
(
∀ x25 .
x25
∈
int
⟶
∀ x26 .
x26
∈
int
⟶
x8
x25
x26
=
If_i
(
SNoLe
x25
0
)
x26
(
x5
(
x8
(
add_SNo
x25
(
minus_SNo
1
)
)
x26
)
)
)
⟶
(
∀ x25 .
x25
∈
int
⟶
x9
x25
=
x8
(
x6
x25
)
x7
)
⟶
(
∀ x25 .
x25
∈
int
⟶
x10
x25
=
x9
x25
)
⟶
(
∀ x25 .
x25
∈
int
⟶
∀ x26 .
x26
∈
int
⟶
x11
x25
x26
=
add_SNo
1
(
mul_SNo
x25
x26
)
)
⟶
(
∀ x25 .
x25
∈
int
⟶
∀ x26 .
x26
∈
int
⟶
x12
x25
x26
=
x26
)
⟶
(
∀ x25 .
x25
∈
int
⟶
x13
x25
=
x25
)
⟶
x14
=
1
⟶
(
∀ x25 .
x25
∈
int
⟶
x15
x25
=
add_SNo
(
mul_SNo
(
mul_SNo
x25
x25
)
x25
)
(
minus_SNo
x25
)
)
⟶
x16
=
1
⟶
x17
=
add_SNo
2
2
⟶
(
∀ x25 .
x25
∈
int
⟶
∀ x26 .
x26
∈
int
⟶
x18
x25
x26
=
If_i
(
SNoLe
x25
0
)
x26
(
x15
(
x18
(
add_SNo
x25
(
minus_SNo
1
)
)
x26
)
)
)
⟶
x19
=
x18
x16
x17
⟶
x20
=
x19
⟶
(
∀ x25 .
x25
∈
int
⟶
∀ x26 .
x26
∈
int
⟶
∀ x27 .
x27
∈
int
⟶
x21
x25
x26
x27
=
If_i
(
SNoLe
x25
0
)
x26
(
x11
(
x21
(
add_SNo
x25
(
minus_SNo
1
)
)
x26
x27
)
(
x22
(
add_SNo
x25
(
minus_SNo
1
)
)
x26
x27
)
)
)
⟶
(
∀ x25 .
x25
∈
int
⟶
∀ x26 .
x26
∈
int
⟶
∀ x27 .
x27
∈
int
⟶
x22
x25
x26
x27
=
If_i
(
SNoLe
x25
0
)
x27
(
x12
(
x21
(
add_SNo
x25
(
minus_SNo
1
)
)
x26
x27
)
(
x22
(
add_SNo
x25
(
minus_SNo
1
)
)
x26
x27
)
)
)
⟶
(
∀ x25 .
x25
∈
int
⟶
x23
x25
=
x21
(
x13
x25
)
x14
x20
)
⟶
(
∀ x25 .
x25
∈
int
⟶
x24
x25
=
x23
x25
)
⟶
∀ x25 .
x25
∈
int
⟶
SNoLe
0
x25
⟶
x10
x25
=
x24
x25
Conjecture
86183..
A268839
:
∀ x0 :
ι →
ι → ι
.
(
∀ x1 .
x1
∈
int
⟶
∀ x2 .
x2
∈
int
⟶
x0
x1
x2
∈
int
)
⟶
∀ x1 .
x1
∈
int
⟶
∀ x2 :
ι → ι
.
(
∀ x3 .
x3
∈
int
⟶
x2
x3
∈
int
)
⟶
∀ x3 :
ι →
ι → ι
.
(
∀ x4 .
x4
∈
int
⟶
∀ x5 .
x5
∈
int
⟶
x3
x4
x5
∈
int
)
⟶
∀ x4 :
ι → ι
.
(
∀ x5 .
x5
∈
int
⟶
x4
x5
∈
int
)
⟶
∀ x5 :
ι → ι
.
(
∀ x6 .
x6
∈
int
⟶
x5
x6
∈
int
)
⟶
∀ x6 :
ι → ι
.
(
∀ x7 .
x7
∈
int
⟶
x6
x7
∈
int
)
⟶
∀ x7 .
x7
∈
int
⟶
∀ x8 :
ι →
ι → ι
.
(
∀ x9 .
x9
∈
int
⟶
∀ x10 .
x10
∈
int
⟶
x8
x9
x10
∈
int
)
⟶
∀ x9 :
ι → ι
.
(
∀ x10 .
x10
∈
int
⟶
x9
x10
∈
int
)
⟶
∀ x10 :
ι → ι
.
(
∀ x11 .
x11
∈
int
⟶
x10
x11
∈
int
)
⟶
∀ x11 :
ι →
ι → ι
.
(
∀ x12 .
x12
∈
int
⟶
∀ x13 .
x13
∈
int
⟶
x11
x12
x13
∈
int
)
⟶
∀ x12 :
ι →
ι → ι
.
(
∀ x13 .
x13
∈
int
⟶
∀ x14 .
x14
∈
int
⟶
x12
x13
x14
∈
int
)
⟶
∀ x13 :
ι → ι
.
(
∀ x14 .
x14
∈
int
⟶
x13
x14
∈
int
)
⟶
∀ x14 .
x14
∈
int
⟶
∀ x15 .
x15
∈
int
⟶
∀ x16 :
ι →
ι →
ι → ι
.
(
∀ x17 .
x17
∈
int
⟶
∀ x18 .
x18
∈
int
⟶
∀ x19 .
x19
∈
int
⟶
x16
x17
x18
x19
∈
int
)
⟶
∀ x17 :
ι →
ι →
ι → ι
.
(
∀ x18 .
x18
∈
int
⟶
∀ x19 .
x19
∈
int
⟶
∀ x20 .
x20
∈
int
⟶
x17
x18
x19
x20
∈
int
)
⟶
∀ x18 :
ι → ι
.
(
∀ x19 .
x19
∈
int
⟶
x18
x19
∈
int
)
⟶
∀ x19 :
ι → ι
.
(
∀ x20 .
x20
∈
int
⟶
x19
x20
∈
int
)
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
x0
x20
x21
=
mul_SNo
(
add_SNo
2
x21
)
x20
)
⟶
x1
=
2
⟶
(
∀ x20 .
x20
∈
int
⟶
x2
x20
=
x20
)
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
x3
x20
x21
=
If_i
(
SNoLe
x20
0
)
x21
(
x0
(
x3
(
add_SNo
x20
(
minus_SNo
1
)
)
x21
)
x20
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x4
x20
=
x3
x1
(
x2
x20
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x5
x20
=
add_SNo
(
add_SNo
(
x4
x20
)
(
minus_SNo
1
)
)
(
minus_SNo
x20
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x6
x20
=
add_SNo
1
x20
)
⟶
x7
=
1
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
x8
x20
x21
=
If_i
(
SNoLe
x20
0
)
x21
(
x5
(
x8
(
add_SNo
x20
(
minus_SNo
1
)
)
x21
)
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x9
x20
=
x8
(
x6
x20
)
x7
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x10
x20
=
add_SNo
(
x9
x20
)
(
minus_SNo
1
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
x11
x20
x21
=
add_SNo
1
(
mul_SNo
x20
x21
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
x12
x20
x21
=
x21
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x13
x20
=
x20
)
⟶
x14
=
1
⟶
x15
=
add_SNo
1
(
add_SNo
2
(
mul_SNo
2
(
add_SNo
2
2
)
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
∀ x22 .
x22
∈
int
⟶
x16
x20
x21
x22
=
If_i
(
SNoLe
x20
0
)
x21
(
x11
(
x16
(
add_SNo
x20
(
minus_SNo
1
)
)
x21
x22
)
(
x17
(
add_SNo
x20
(
minus_SNo
1
)
)
x21
x22
)
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
∀ x22 .
x22
∈
int
⟶
x17
x20
x21
x22
=
If_i
(
SNoLe
x20
0
)
x22
(
x12
(
x16
(
add_SNo
x20
(
minus_SNo
1
)
)
x21
x22
)
(
x17
(
add_SNo
x20
(
minus_SNo
1
)
)
x21
x22
)
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x18
x20
=
x16
(
x13
x20
)
x14
x15
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x19
x20
=
mul_SNo
(
add_SNo
1
(
mul_SNo
2
(
add_SNo
2
2
)
)
)
(
x18
x20
)
)
⟶
∀ x20 .
x20
∈
int
⟶
SNoLe
0
x20
⟶
x10
x20
=
x19
x20
Conjecture
45f2a..
A268730
:
∀ x0 :
ι → ι
.
(
∀ x1 .
x1
∈
int
⟶
x0
x1
∈
int
)
⟶
∀ x1 .
x1
∈
int
⟶
∀ x2 :
ι →
ι → ι
.
(
∀ x3 .
x3
∈
int
⟶
∀ x4 .
x4
∈
int
⟶
x2
x3
x4
∈
int
)
⟶
∀ x3 :
ι →
ι → ι
.
(
∀ x4 .
x4
∈
int
⟶
∀ x5 .
x5
∈
int
⟶
x3
x4
x5
∈
int
)
⟶
∀ x4 :
ι →
ι → ι
.
(
∀ x5 .
x5
∈
int
⟶
∀ x6 .
x6
∈
int
⟶
x4
x5
x6
∈
int
)
⟶
∀ x5 :
ι →
ι → ι
.
(
∀ x6 .
x6
∈
int
⟶
∀ x7 .
x7
∈
int
⟶
x5
x6
x7
∈
int
)
⟶
∀ x6 :
ι → ι
.
(
∀ x7 .
x7
∈
int
⟶
x6
x7
∈
int
)
⟶
∀ x7 .
x7
∈
int
⟶
∀ x8 :
ι →
ι → ι
.
(
∀ x9 .
x9
∈
int
⟶
∀ x10 .
x10
∈
int
⟶
x8
x9
x10
∈
int
)
⟶
∀ x9 :
ι → ι
.
(
∀ x10 .
x10
∈
int
⟶
x9
x10
∈
int
)
⟶
∀ x10 :
ι → ι
.
(
∀ x11 .
x11
∈
int
⟶
x10
x11
∈
int
)
⟶
∀ x11 :
ι →
ι → ι
.
(
∀ x12 .
x12
∈
int
⟶
∀ x13 .
x13
∈
int
⟶
x11
x12
x13
∈
int
)
⟶
∀ x12 :
ι →
ι → ι
.
(
∀ x13 .
x13
∈
int
⟶
∀ x14 .
x14
∈
int
⟶
x12
x13
x14
∈
int
)
⟶
∀ x13 :
ι → ι
.
(
∀ x14 .
x14
∈
int
⟶
x13
x14
∈
int
)
⟶
∀ x14 .
x14
∈
int
⟶
∀ x15 .
x15
∈
int
⟶
∀ x16 :
ι →
ι →
ι → ι
.
(
∀ x17 .
x17
∈
int
⟶
∀ x18 .
x18
∈
int
⟶
∀ x19 .
x19
∈
int
⟶
x16
x17
x18
x19
∈
int
)
⟶
∀ x17 :
ι →
ι →
ι → ι
.
(
∀ x18 .
x18
∈
int
⟶
∀ x19 .
x19
∈
int
⟶
∀ x20 .
x20
∈
int
⟶
x17
x18
x19
x20
∈
int
)
⟶
∀ x18 :
ι → ι
.
(
∀ x19 .
x19
∈
int
⟶
x18
x19
∈
int
)
⟶
∀ x19 :
ι → ι
.
(
∀ x20 .
x20
∈
int
⟶
x19
x20
∈
int
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x0
x20
=
add_SNo
2
(
minus_SNo
(
mul_SNo
2
(
add_SNo
x20
x20
)
)
)
)
⟶
x1
=
2
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
x2
x20
x21
=
x21
)
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
x3
x20
x21
=
If_i
(
SNoLe
x20
0
)
x21
(
x0
(
x3
(
add_SNo
x20
(
minus_SNo
1
)
)
x21
)
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
x4
x20
x21
=
x3
x1
(
x2
x20
x21
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
x5
x20
x21
=
mul_SNo
(
x4
x20
x21
)
x20
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x6
x20
=
add_SNo
1
x20
)
⟶
x7
=
1
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
x8
x20
x21
=
If_i
(
SNoLe
x20
0
)
x21
(
x5
(
x8
(
add_SNo
x20
(
minus_SNo
1
)
)
x21
)
x20
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x9
x20
=
x8
(
x6
x20
)
x7
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x10
x20
=
x9
x20
)
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
x11
x20
x21
=
mul_SNo
x20
x21
)
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
x12
x20
x21
=
add_SNo
(
mul_SNo
2
(
mul_SNo
2
(
add_SNo
2
2
)
)
)
x21
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x13
x20
=
add_SNo
1
x20
)
⟶
x14
=
1
⟶
x15
=
add_SNo
2
(
mul_SNo
2
(
add_SNo
2
2
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
∀ x22 .
x22
∈
int
⟶
x16
x20
x21
x22
=
If_i
(
SNoLe
x20
0
)
x21
(
x11
(
x16
(
add_SNo
x20
(
minus_SNo
1
)
)
x21
x22
)
(
x17
(
add_SNo
x20
(
minus_SNo
1
)
)
x21
x22
)
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
∀ x22 .
x22
∈
int
⟶
x17
x20
x21
x22
=
If_i
(
SNoLe
x20
0
)
x22
(
x12
(
x16
(
add_SNo
x20
(
minus_SNo
1
)
)
x21
x22
)
(
x17
(
add_SNo
x20
(
minus_SNo
1
)
)
x21
x22
)
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x18
x20
=
x16
(
x13
x20
)
x14
x15
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x19
x20
=
x18
x20
)
⟶
∀ x20 .
x20
∈
int
⟶
SNoLe
0
x20
⟶
x10
x20
=
x19
x20
Conjecture
60b6e..
A267797
:
∀ x0 :
ι →
ι → ι
.
(
∀ x1 .
x1
∈
int
⟶
∀ x2 .
x2
∈
int
⟶
x0
x1
x2
∈
int
)
⟶
∀ x1 :
ι → ι
.
(
∀ x2 .
x2
∈
int
⟶
x1
x2
∈
int
)
⟶
∀ x2 :
ι → ι
.
(
∀ x3 .
x3
∈
int
⟶
x2
x3
∈
int
)
⟶
∀ x3 .
x3
∈
int
⟶
∀ x4 .
x4
∈
int
⟶
∀ x5 :
ι →
ι →
ι → ι
.
(
∀ x6 .
x6
∈
int
⟶
∀ x7 .
x7
∈
int
⟶
∀ x8 .
x8
∈
int
⟶
x5
x6
x7
x8
∈
int
)
⟶
∀ x6 :
ι →
ι →
ι → ι
.
(
∀ x7 .
x7
∈
int
⟶
∀ x8 .
x8
∈
int
⟶
∀ x9 .
x9
∈
int
⟶
x6
x7
x8
x9
∈
int
)
⟶
∀ x7 :
ι → ι
.
(
∀ x8 .
x8
∈
int
⟶
x7
x8
∈
int
)
⟶
∀ x8 :
ι → ι
.
(
∀ x9 .
x9
∈
int
⟶
x8
x9
∈
int
)
⟶
∀ x9 :
ι → ι
.
(
∀ x10 .
x10
∈
int
⟶
x9
x10
∈
int
)
⟶
∀ x10 .
x10
∈
int
⟶
∀ x11 :
ι →
ι → ι
.
(
∀ x12 .
x12
∈
int
⟶
∀ x13 .
x13
∈
int
⟶
x11
x12
x13
∈
int
)
⟶
∀ x12 :
ι → ι
.
(
∀ x13 .
x13
∈
int
⟶
x12
x13
∈
int
)
⟶
∀ x13 :
ι → ι
.
(
∀ x14 .
x14
∈
int
⟶
x13
x14
∈
int
)
⟶
∀ x14 .
x14
∈
int
⟶
∀ x15 .
x15
∈
int
⟶
∀ x16 :
ι →
ι →
ι → ι
.
(
∀ x17 .
x17
∈
int
⟶
∀ x18 .
x18
∈
int
⟶
∀ x19 .
x19
∈
int
⟶
x16
x17
x18
x19
∈
int
)
⟶
∀ x17 :
ι →
ι →
ι → ι
.
(
∀ x18 .
x18
∈
int
⟶
∀ x19 .
x19
∈
int
⟶
∀ x20 .
x20
∈
int
⟶
x17
x18
x19
x20
∈
int
)
⟶
∀ x18 :
ι → ι
.
(
∀ x19 .
x19
∈
int
⟶
x18
x19
∈
int
)
⟶
∀ x19 :
ι → ι
.
(
∀ x20 .
x20
∈
int
⟶
x19
x20
∈
int
)
⟶
∀ x20 :
ι →
ι → ι
.
(
∀ x21 .
x21
∈
int
⟶
∀ x22 .
x22
∈
int
⟶
x20
x21
x22
∈
int
)
⟶
∀ x21 :
ι → ι
.
(
∀ x22 .
x22
∈
int
⟶
x21
x22
∈
int
)
⟶
∀ x22 :
ι → ι
.
(
∀ x23 .
x23
∈
int
⟶
x22
x23
∈
int
)
⟶
(
∀ x23 .
x23
∈
int
⟶
∀ x24 .
x24
∈
int
⟶
x0
x23
x24
=
add_SNo
x23
x24
)
⟶
(
∀ x23 .
x23
∈
int
⟶
x1
x23
=
x23
)
⟶
(
∀ x23 .
x23
∈
int
⟶
x2
x23
=
mul_SNo
2
(
add_SNo
(
mul_SNo
2
(
add_SNo
2
x23
)
)
x23
)
)
⟶
x3
=
1
⟶
x4
=
2
⟶
(
∀ x23 .
x23
∈
int
⟶
∀ x24 .
x24
∈
int
⟶
∀ x25 .
x25
∈
int
⟶
x5
x23
x24
x25
=
If_i
(
SNoLe
x23
0
)
x24
(
x0
(
x5
(
add_SNo
x23
(
minus_SNo
1
)
)
x24
x25
)
(
x6
(
add_SNo
x23
(
minus_SNo
1
)
)
x24
x25
)
)
)
⟶
(
∀ x23 .
x23
∈
int
⟶
∀ x24 .
x24
∈
int
⟶
∀ x25 .
x25
∈
int
⟶
x6
x23
x24
x25
=
If_i
(
SNoLe
x23
0
)
x25
(
x1
(
x5
(
add_SNo
x23
(
minus_SNo
1
)
)
x24
x25
)
)
)
⟶
(
∀ x23 .
x23
∈
int
⟶
x7
x23
=
x5
(
x2
x23
)
x3
x4
)
⟶
(
∀ x23 .
x23
∈
int
⟶
x8
x23
=
x7
x23
)
⟶
(
∀ x23 .
x23
∈
int
⟶
x9
x23
=
mul_SNo
(
add_SNo
(
add_SNo
1
2
)
(
mul_SNo
x23
x23
)
)
x23
)
⟶
x10
=
1
⟶
(
∀ x23 .
x23
∈
int
⟶
∀ x24 .
x24
∈
int
⟶
x11
x23
x24
=
add_SNo
(
add_SNo
(
add_SNo
x23
(
minus_SNo
x24
)
)
x23
)
x23
)
⟶
(
∀ x23 .
x23
∈
int
⟶
x12
x23
=
x23
)
⟶
(
∀ x23 .
x23
∈
int
⟶
x13
x23
=
x23
)
⟶
x14
=
add_SNo
2
2
⟶
x15
=
1
⟶
(
∀ x23 .
x23
∈
int
⟶
∀ x24 .
x24
∈
int
⟶
∀ x25 .
x25
∈
int
⟶
x16
x23
x24
x25
=
If_i
(
SNoLe
x23
0
)
x24
(
x11
(
x16
(
add_SNo
x23
(
minus_SNo
1
)
)
x24
x25
)
(
x17
(
add_SNo
x23
(
minus_SNo
1
)
)
x24
x25
)
)
)
⟶
(
∀ x23 .
x23
∈
int
⟶
∀ x24 .
x24
∈
int
⟶
∀ x25 .
x25
∈
int
⟶
x17
x23
x24
x25
=
If_i
(
SNoLe
x23
0
)
x25
(
x12
(
x16
(
add_SNo
x23
(
minus_SNo
1
)
)
x24
x25
)
)
)
⟶
(
∀ x23 .
x23
∈
int
⟶
x18
x23
=
x16
(
x13
x23
)
x14
x15
)
⟶
(
∀ x23 .
x23
∈
int
⟶
x19
x23
=
x18
x23
)
⟶
(
∀ x23 .
x23
∈
int
⟶
∀ x24 .
x24
∈
int
⟶
x20
x23
x24
=
If_i
(
SNoLe
x23
0
)
x24
(
x9
(
x20
(
add_SNo
x23
(
minus_SNo
1
)
)
x24
)
)
)
⟶
(
∀ x23 .
x23
∈
int
⟶
x21
x23
=
x20
x10
(
x19
x23
)
)
⟶
(
∀ x23 .
x23
∈
int
⟶
x22
x23
=
x21
x23
)
⟶
∀ x23 .
x23
∈
int
⟶
SNoLe
0
x23
⟶
x8
x23
=
x22
x23
Conjecture
4e4a3..
A2674
:
∀ x0 :
ι →
ι → ι
.
(
∀ x1 .
x1
∈
int
⟶
∀ x2 .
x2
∈
int
⟶
x0
x1
x2
∈
int
)
⟶
∀ x1 :
ι → ι
.
(
∀ x2 .
x2
∈
int
⟶
x1
x2
∈
int
)
⟶
∀ x2 .
x2
∈
int
⟶
∀ x3 :
ι →
ι → ι
.
(
∀ x4 .
x4
∈
int
⟶
∀ x5 .
x5
∈
int
⟶
x3
x4
x5
∈
int
)
⟶
∀ x4 :
ι → ι
.
(
∀ x5 .
x5
∈
int
⟶
x4
x5
∈
int
)
⟶
∀ x5 :
ι → ι
.
(
∀ x6 .
x6
∈
int
⟶
x5
x6
∈
int
)
⟶
∀ x6 :
ι →
ι → ι
.
(
∀ x7 .
x7
∈
int
⟶
∀ x8 .
x8
∈
int
⟶
x6
x7
x8
∈
int
)
⟶
∀ x7 :
ι → ι
.
(
∀ x8 .
x8
∈
int
⟶
x7
x8
∈
int
)
⟶
∀ x8 :
ι → ι
.
(
∀ x9 .
x9
∈
int
⟶
x8
x9
∈
int
)
⟶
∀ x9 :
ι →
ι → ι
.
(
∀ x10 .
x10
∈
int
⟶
∀ x11 .
x11
∈
int
⟶
x9
x10
x11
∈
int
)
⟶
∀ x10 :
ι → ι
.
(
∀ x11 .
x11
∈
int
⟶
x10
x11
∈
int
)
⟶
∀ x11 :
ι →
ι → ι
.
(
∀ x12 .
x12
∈
int
⟶
∀ x13 .
x13
∈
int
⟶
x11
x12
x13
∈
int
)
⟶
∀ x12 :
ι →
ι → ι
.
(
∀ x13 .
x13
∈
int
⟶
∀ x14 .
x14
∈
int
⟶
x12
x13
x14
∈
int
)
⟶
∀ x13 :
ι → ι
.
(
∀ x14 .
x14
∈
int
⟶
x13
x14
∈
int
)
⟶
∀ x14 .
x14
∈
int
⟶
∀ x15 :
ι → ι
.
(
∀ x16 .
x16
∈
int
⟶
x15
x16
∈
int
)
⟶
∀ x16 :
ι →
ι →
ι → ι
.
(
∀ x17 .
x17
∈
int
⟶
∀ x18 .
x18
∈
int
⟶
∀ x19 .
x19
∈
int
⟶
x16
x17
x18
x19
∈
int
)
⟶
∀ x17 :
ι →
ι →
ι → ι
.
(
∀ x18 .
x18
∈
int
⟶
∀ x19 .
x19
∈
int
⟶
∀ x20 .
x20
∈
int
⟶
x17
x18
x19
x20
∈
int
)
⟶
∀ x18 :
ι → ι
.
(
∀ x19 .
x19
∈
int
⟶
x18
x19
∈
int
)
⟶
∀ x19 :
ι → ι
.
(
∀ x20 .
x20
∈
int
⟶
x19
x20
∈
int
)
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
x0
x20
x21
=
mul_SNo
(
add_SNo
2
x21
)
x20
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x1
x20
=
add_SNo
x20
x20
)
⟶
x2
=
1
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
x3
x20
x21
=
If_i
(
SNoLe
x20
0
)
x21
(
x0
(
x3
(
add_SNo
x20
(
minus_SNo
1
)
)
x21
)
x20
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x4
x20
=
x3
(
x1
x20
)
x2
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x5
x20
=
x4
x20
)
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
x6
x20
x21
=
mul_SNo
x20
x21
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x7
x20
=
x20
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x8
x20
=
add_SNo
1
x20
)
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
x9
x20
x21
=
If_i
(
SNoLe
x20
0
)
x21
(
x6
(
x9
(
add_SNo
x20
(
minus_SNo
1
)
)
x21
)
x20
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x10
x20
=
x9
(
x7
x20
)
(
x8
x20
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
x11
x20
x21
=
mul_SNo
x20
x21
)
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
x12
x20
x21
=
add_SNo
1
x21
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x13
x20
=
x20
)
⟶
x14
=
1
⟶
(
∀ x20 .
x20
∈
int
⟶
x15
x20
=
add_SNo
1
x20
)
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
∀ x22 .
x22
∈
int
⟶
x16
x20
x21
x22
=
If_i
(
SNoLe
x20
0
)
x21
(
x11
(
x16
(
add_SNo
x20
(
minus_SNo
1
)
)
x21
x22
)
(
x17
(
add_SNo
x20
(
minus_SNo
1
)
)
x21
x22
)
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
∀ x22 .
x22
∈
int
⟶
x17
x20
x21
x22
=
If_i
(
SNoLe
x20
0
)
x22
(
x12
(
x16
(
add_SNo
x20
(
minus_SNo
1
)
)
x21
x22
)
(
x17
(
add_SNo
x20
(
minus_SNo
1
)
)
x21
x22
)
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x18
x20
=
x16
(
x13
x20
)
x14
(
x15
x20
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x19
x20
=
mul_SNo
(
mul_SNo
(
add_SNo
1
(
add_SNo
x20
x20
)
)
(
x10
x20
)
)
(
x18
x20
)
)
⟶
∀ x20 .
x20
∈
int
⟶
SNoLe
0
x20
⟶
x5
x20
=
x19
x20
Conjecture
db13e..
A26727
:
∀ x0 :
ι →
ι → ι
.
(
∀ x1 .
x1
∈
int
⟶
∀ x2 .
x2
∈
int
⟶
x0
x1
x2
∈
int
)
⟶
∀ x1 :
ι →
ι → ι
.
(
∀ x2 .
x2
∈
int
⟶
∀ x3 .
x3
∈
int
⟶
x1
x2
x3
∈
int
)
⟶
∀ x2 :
ι →
ι → ι
.
(
∀ x3 .
x3
∈
int
⟶
∀ x4 .
x4
∈
int
⟶
x2
x3
x4
∈
int
)
⟶
∀ x3 .
x3
∈
int
⟶
∀ x4 .
x4
∈
int
⟶
∀ x5 :
ι →
ι →
ι → ι
.
(
∀ x6 .
x6
∈
int
⟶
∀ x7 .
x7
∈
int
⟶
∀ x8 .
x8
∈
int
⟶
x5
x6
x7
x8
∈
int
)
⟶
∀ x6 :
ι →
ι →
ι → ι
.
(
∀ x7 .
x7
∈
int
⟶
∀ x8 .
x8
∈
int
⟶
∀ x9 .
x9
∈
int
⟶
x6
x7
x8
x9
∈
int
)
⟶
∀ x7 :
ι →
ι → ι
.
(
∀ x8 .
x8
∈
int
⟶
∀ x9 .
x9
∈
int
⟶
x7
x8
x9
∈
int
)
⟶
∀ x8 :
ι →
ι → ι
.
(
∀ x9 .
x9
∈
int
⟶
∀ x10 .
x10
∈
int
⟶
x8
x9
x10
∈
int
)
⟶
∀ x9 .
x9
∈
int
⟶
∀ x10 :
ι → ι
.
(
∀ x11 .
x11
∈
int
⟶
x10
x11
∈
int
)
⟶
∀ x11 :
ι →
ι → ι
.
(
∀ x12 .
x12
∈
int
⟶
∀ x13 .
x13
∈
int
⟶
x11
x12
x13
∈
int
)
⟶
∀ x12 :
ι → ι
.
(
∀ x13 .
x13
∈
int
⟶
x12
x13
∈
int
)
⟶
∀ x13 :
ι →
ι → ι
.
(
∀ x14 .
x14
∈
int
⟶
∀ x15 .
x15
∈
int
⟶
x13
x14
x15
∈
int
)
⟶
∀ x14 :
ι →
ι → ι
.
(
∀ x15 .
x15
∈
int
⟶
∀ x16 .
x16
∈
int
⟶
x14
x15
x16
∈
int
)
⟶
∀ x15 .
x15
∈
int
⟶
∀ x16 :
ι →
ι → ι
.
(
∀ x17 .
x17
∈
int
⟶
∀ x18 .
x18
∈
int
⟶
x16
x17
x18
∈
int
)
⟶
∀ x17 :
ι →
ι → ι
.
(
∀ x18 .
x18
∈
int
⟶
∀ x19 .
x19
∈
int
⟶
x17
x18
x19
∈
int
)
⟶
∀ x18 :
ι →
ι → ι
.
(
∀ x19 .
x19
∈
int
⟶
∀ x20 .
x20
∈
int
⟶
x18
x19
x20
∈
int
)
⟶
∀ x19 :
ι → ι
.
(
∀ x20 .
x20
∈
int
⟶
x19
x20
∈
int
)
⟶
∀ x20 .
x20
∈
int
⟶
∀ x21 :
ι →
ι → ι
.
(
∀ x22 .
x22
∈
int
⟶
∀ x23 .
x23
∈
int
⟶
x21
x22
x23
∈
int
)
⟶
∀ x22 :
ι → ι
.
(
∀ x23 .
x23
∈
int
⟶
x22
x23
∈
int
)
⟶
∀ x23 :
ι → ι
.
(
∀ x24 .
x24
∈
int
⟶
x23
x24
∈
int
)
⟶
∀ x24 :
ι →
ι → ι
.
(
∀ x25 .
x25
∈
int
⟶
∀ x26 .
x26
∈
int
⟶
x24
x25
x26
∈
int
)
⟶
∀ x25 :
ι →
ι → ι
.
(
∀ x26 .
x26
∈
int
⟶
∀ x27 .
x27
∈
int
⟶
x25
x26
x27
∈
int
)
⟶
∀ x26 :
ι → ι
.
(
∀ x27 .
x27
∈
int
⟶
x26
x27
∈
int
)
⟶
∀ x27 .
x27
∈
int
⟶
∀ x28 .
x28
∈
int
⟶
∀ x29 :
ι →
ι →
ι → ι
.
(
∀ x30 .
x30
∈
int
⟶
∀ x31 .
x31
∈
int
⟶
∀ x32 .
x32
∈
int
⟶
x29
x30
x31
x32
∈
int
)
⟶
∀ x30 :
ι →
ι →
ι → ι
.
(
∀ x31 .
x31
∈
int
⟶
∀ x32 .
x32
∈
int
⟶
∀ x33 .
x33
∈
int
⟶
x30
x31
x32
x33
∈
int
)
⟶
∀ x31 :
ι → ι
.
(
∀ x32 .
x32
∈
int
⟶
x31
x32
∈
int
)
⟶
∀ x32 :
ι → ι
.
(
∀ x33 .
x33
∈
int
⟶
x32
x33
∈
int
)
⟶
∀ x33 :
ι → ι
.
(
∀ x34 .
x34
∈
int
⟶
x33
x34
∈
int
)
⟶
∀ x34 .
x34
∈
int
⟶
∀ x35 :
ι →
ι → ι
.
(
∀ x36 .
x36
∈
int
⟶
∀ x37 .
x37
∈
int
⟶
x35
x36
x37
∈
int
)
⟶
∀ x36 :
ι → ι
.
(
∀ x37 .
x37
∈
int
⟶
x36
x37
∈
int
)
⟶
∀ x37 :
ι → ι
.
(
∀ x38 .
x38
∈
int
⟶
x37
x38
∈
int
)
⟶
∀ x38 .
x38
∈
int
⟶
∀ x39 :
ι →
ι → ι
.
(
∀ x40 .
x40
∈
int
⟶
∀ x41 .
x41
∈
int
⟶
x39
x40
x41
∈
int
)
⟶
∀ x40 :
ι →
ι → ι
.
(
∀ x41 .
x41
∈
int
⟶
∀ x42 .
x42
∈
int
⟶
x40
x41
x42
∈
int
)
⟶
∀ x41 :
ι →
ι → ι
.
(
∀ x42 .
x42
∈
int
⟶
∀ x43 .
x43
∈
int
⟶
x41
x42
x43
∈
int
)
⟶
∀ x42 :
ι →
ι → ι
.
(
∀ x43 .
x43
∈
int
⟶
∀ x44 .
x44
∈
int
⟶
x42
x43
x44
∈
int
)
⟶
∀ x43 :
ι → ι
.
(
∀ x44 .
x44
∈
int
⟶
x43
x44
∈
int
)
⟶
∀ x44 .
x44
∈
int
⟶
∀ x45 :
ι →
ι → ι
.
(
∀ x46 .
x46
∈
int
⟶
∀ x47 .
x47
∈
int
⟶
x45
x46
x47
∈
int
)
⟶
∀ x46 :
ι → ι
.
(
∀ x47 .
x47
∈
int
⟶
x46
x47
∈
int
)
⟶
∀ x47 :
ι → ι
.
(
∀ x48 .
x48
∈
int
⟶
x47
x48
∈
int
)
⟶
(
∀ x48 .
x48
∈
int
⟶
∀ x49 .
x49
∈
int
⟶
x0
x48
x49
=
add_SNo
(
mul_SNo
2
(
add_SNo
(
add_SNo
x48
x48
)
x48
)
)
(
mul_SNo
(
mul_SNo
x49
x49
)
x49
)
)
⟶
(
∀ x48 .
x48
∈
int
⟶
∀ x49 .
x49
∈
int
⟶
x1
x48
x49
=
add_SNo
x49
x49
)
⟶
(
∀ x48 .
x48
∈
int
⟶
∀ x49 .
x49
∈
int
⟶
x2
x48
x49
=
x49
)
⟶
x3
=
1
⟶
x4
=
2
⟶
(
∀ x48 .
x48
∈
int
⟶
∀ x49 .
x49
∈
int
⟶
∀ x50 .
x50
∈
int
⟶
x5
x48
x49
x50
=
If_i
(
SNoLe
x48
0
)
x49
(
x0
(
x5
(
add_SNo
x48
(
minus_SNo
1
)
)
x49
x50
)
(
x6
(
add_SNo
x48
(
minus_SNo
1
)
)
x49
x50
)
)
)
⟶
(
∀ x48 .
x48
∈
int
⟶
∀ x49 .
x49
∈
int
⟶
∀ x50 .
x50
∈
int
⟶
x6
x48
x49
x50
=
If_i
(
SNoLe
x48
0
)
x50
(
x1
(
x5
(
add_SNo
x48
(
minus_SNo
1
)
)
x49
x50
)
(
x6
(
add_SNo
x48
(
minus_SNo
1
)
)
x49
x50
)
)
)
⟶
(
∀ x48 .
x48
∈
int
⟶
∀ x49 .
x49
∈
int
⟶
x7
x48
x49
=
x5
(
x2
x48
x49
)
x3
x4
)
⟶
(
∀ x48 .
x48
∈
int
⟶
∀ x49 .
x49
∈
int
⟶
x8
x48
x49
=
mul_SNo
(
add_SNo
2
x49
)
x48
)
⟶
x9
=
2
⟶
(
∀ x48 .
x48
∈
int
⟶
x10
x48
=
x48
)
⟶
(
∀ x48 .
x48
∈
int
⟶
∀ x49 .
x49
∈
int
⟶
x11
x48
x49
=
If_i
(
SNoLe
x48
0
)
x49
(
x8
(
x11
(
add_SNo
x48
(
minus_SNo
1
)
)
x49
)
x48
)
)
⟶
(
∀ x48 .
x48
∈
int
⟶
x12
x48
=
x11
x9
(
x10
x48
)
)
⟶
(
∀ x48 .
x48
∈
int
⟶
∀ x49 .
x49
∈
int
⟶
x13
x48
x49
=
add_SNo
(
add_SNo
(
x7
x48
x49
)
(
minus_SNo
x48
)
)
(
x12
x48
)
)
⟶
(
∀ x48 .
x48
∈
int
⟶
∀ x49 .
x49
∈
int
⟶
x14
x48
x49
=
x49
)
⟶
x15
=
1
⟶
(
∀ x48 .
x48
∈
int
⟶
∀ x49 .
x49
∈
int
⟶
x16
x48
x49
=
If_i
(
SNoLe
x48
0
)
x49
(
x13
(
x16
(
add_SNo
x48
(
minus_SNo
1
)
)
x49
)
x48
)
)
⟶
(
∀ x48 .
x48
∈
int
⟶
∀ x49 .
x49
∈
int
⟶
x17
x48
x49
=
x16
(
x14
x48
x49
)
x15
)
⟶
(
∀ x48 .
x48
∈
int
⟶
∀ x49 .
x49
∈
int
⟶
x18
x48
x49
=
add_SNo
(
add_SNo
(
x17
x48
x49
)
x48
)
x48
)
⟶
(
∀ x48 .
x48
∈
int
⟶
x19
x48
=
x48
)
⟶
x20
=
1
⟶
(
∀ x48 .
x48
∈
int
⟶
∀ x49 .
x49
∈
int
⟶
x21
x48
x49
=
If_i
(
SNoLe
x48
0
)
x49
(
x18
(
x21
(
add_SNo
x48
(
minus_SNo
1
)
)
x49
)
x48
)
)
⟶
(
∀ x48 .
x48
∈
int
⟶
x22
x48
=
x21
(
x19
x48
)
x20
)
⟶
(
∀ x48 .
x48
∈
int
⟶
x23
x48
=
x22
x48
)
⟶
(
∀ x48 .
x48
∈
int
⟶
∀ x49 .
x49
∈
int
⟶
x24
x48
x49
=
add_SNo
(
mul_SNo
2
(
add_SNo
x48
x48
)
)
x49
)
⟶
(
∀ x48 .
x48
∈
int
⟶
∀ x49 .
x49
∈
int
⟶
x25
x48
x49
=
add_SNo
1
(
add_SNo
(
add_SNo
x49
x49
)
x49
)
)
⟶
(
∀ x48 .
x48
∈
int
⟶
x26
x48
=
x48
)
⟶
x27
=
1
⟶
x28
=
add_SNo
2
2
⟶
(
∀ x48 .
x48
∈
int
⟶
∀ x49 .
x49
∈
int
⟶
∀ x50 .
x50
∈
int
⟶
x29
x48
x49
x50
=
If_i
(
SNoLe
x48
0
)
x49
(
x24
(
x29
(
add_SNo
x48
(
minus_SNo
1
)
)
x49
x50
)
(
x30
(
add_SNo
x48
(
minus_SNo
1
)
)
x49
x50
)
)
)
⟶
(
∀ x48 .
x48
∈
int
⟶
∀ x49 .
x49
∈
int
⟶
∀ x50 .
x50
∈
int
⟶
x30
x48
x49
x50
=
If_i
(
SNoLe
x48
0
)
x50
(
x25
(
x29
(
add_SNo
x48
(
minus_SNo
1
)
)
x49
x50
)
(
x30
(
add_SNo
x48
(
minus_SNo
1
)
)
x49
x50
)
)
)
⟶
(
∀ x48 .
x48
∈
int
⟶
x31
x48
=
x29
(
x26
x48
)
x27
x28
)
⟶
(
∀ x48 .
x48
∈
int
⟶
x32
x48
=
add_SNo
x48
x48
)
⟶
(
∀ x48 .
x48
∈
int
⟶
x33
x48
=
x48
)
⟶
x34
=
1
⟶
(
∀ x48 .
x48
∈
int
⟶
∀ x49 .
x49
∈
int
⟶
x35
x48
x49
=
If_i
(
SNoLe
x48
0
)
x49
(
x32
(
x35
(
add_SNo
x48
(
minus_SNo
1
)
)
x49
)
)
)
⟶
(
∀ x48 .
x48
∈
int
⟶
x36
x48
=
x35
(
x33
x48
)
x34
)
⟶
(
∀ x48 .
x48
∈
int
⟶
x37
x48
=
mul_SNo
(
x31
x48
)
(
x36
x48
)
)
⟶
x38
=
1
⟶
(
∀ x48 .
x48
∈
int
⟶
∀ x49 .
x49
∈
int
⟶
x39
x48
x49
=
x49
)
⟶
(
∀ x48 .
x48
∈
int
⟶
∀ x49 .
x49
∈
int
⟶
x40
x48
x49
=
If_i
(
SNoLe
x48
0
)
x49
(
x37
(
x40
(
add_SNo
x48
(
minus_SNo
1
)
)
x49
)
)
)
⟶
(
∀ x48 .
x48
∈
int
⟶
∀ x49 .
x49
∈
int
⟶
x41
x48
x49
=
x40
x38
(
x39
x48
x49
)
)
⟶
(
∀ x48 .
x48
∈
int
⟶
∀ x49 .
x49
∈
int
⟶
x42
x48
x49
=
add_SNo
(
add_SNo
(
x41
x48
x49
)
(
mul_SNo
2
(
add_SNo
(
mul_SNo
2
(
add_SNo
x48
x48
)
)
x48
)
)
)
x48
)
⟶
(
∀ x48 .
x48
∈
int
⟶
x43
x48
=
x48
)
⟶
x44
=
1
⟶
(
∀ x48 .
x48
∈
int
⟶
∀ x49 .
x49
∈
int
⟶
x45
x48
x49
=
If_i
(
SNoLe
x48
0
)
x49
(
x42
(
x45
(
add_SNo
x48
(
minus_SNo
1
)
)
x49
)
x48
)
)
⟶
(
∀ x48 .
x48
∈
int
⟶
x46
x48
=
x45
(
x43
x48
)
x44
)
⟶
(
∀ x48 .
x48
∈
int
⟶
x47
x48
=
x46
x48
)
⟶
∀ x48 .
x48
∈
int
⟶
SNoLe
0
x48
⟶
x23
x48
=
x47
x48
Conjecture
5efc9..
A2671
:
∀ x0 :
ι →
ι → ι
.
(
∀ x1 .
x1
∈
int
⟶
∀ x2 .
x2
∈
int
⟶
x0
x1
x2
∈
int
)
⟶
∀ x1 :
ι → ι
.
(
∀ x2 .
x2
∈
int
⟶
x1
x2
∈
int
)
⟶
∀ x2 .
x2
∈
int
⟶
∀ x3 :
ι →
ι → ι
.
(
∀ x4 .
x4
∈
int
⟶
∀ x5 .
x5
∈
int
⟶
x3
x4
x5
∈
int
)
⟶
∀ x4 :
ι → ι
.
(
∀ x5 .
x5
∈
int
⟶
x4
x5
∈
int
)
⟶
∀ x5 :
ι → ι
.
(
∀ x6 .
x6
∈
int
⟶
x5
x6
∈
int
)
⟶
∀ x6 :
ι →
ι → ι
.
(
∀ x7 .
x7
∈
int
⟶
∀ x8 .
x8
∈
int
⟶
x6
x7
x8
∈
int
)
⟶
∀ x7 :
ι → ι
.
(
∀ x8 .
x8
∈
int
⟶
x7
x8
∈
int
)
⟶
∀ x8 :
ι → ι
.
(
∀ x9 .
x9
∈
int
⟶
x8
x9
∈
int
)
⟶
∀ x9 :
ι →
ι → ι
.
(
∀ x10 .
x10
∈
int
⟶
∀ x11 .
x11
∈
int
⟶
x9
x10
x11
∈
int
)
⟶
∀ x10 :
ι → ι
.
(
∀ x11 .
x11
∈
int
⟶
x10
x11
∈
int
)
⟶
∀ x11 :
ι →
ι → ι
.
(
∀ x12 .
x12
∈
int
⟶
∀ x13 .
x13
∈
int
⟶
x11
x12
x13
∈
int
)
⟶
∀ x12 :
ι →
ι → ι
.
(
∀ x13 .
x13
∈
int
⟶
∀ x14 .
x14
∈
int
⟶
x12
x13
x14
∈
int
)
⟶
∀ x13 :
ι → ι
.
(
∀ x14 .
x14
∈
int
⟶
x13
x14
∈
int
)
⟶
∀ x14 .
x14
∈
int
⟶
∀ x15 :
ι → ι
.
(
∀ x16 .
x16
∈
int
⟶
x15
x16
∈
int
)
⟶
∀ x16 :
ι →
ι →
ι → ι
.
(
∀ x17 .
x17
∈
int
⟶
∀ x18 .
x18
∈
int
⟶
∀ x19 .
x19
∈
int
⟶
x16
x17
x18
x19
∈
int
)
⟶
∀ x17 :
ι →
ι →
ι → ι
.
(
∀ x18 .
x18
∈
int
⟶
∀ x19 .
x19
∈
int
⟶
∀ x20 .
x20
∈
int
⟶
x17
x18
x19
x20
∈
int
)
⟶
∀ x18 :
ι → ι
.
(
∀ x19 .
x19
∈
int
⟶
x18
x19
∈
int
)
⟶
∀ x19 :
ι → ι
.
(
∀ x20 .
x20
∈
int
⟶
x19
x20
∈
int
)
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
x0
x20
x21
=
mul_SNo
2
(
add_SNo
(
mul_SNo
x20
x21
)
x20
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x1
x20
=
add_SNo
x20
x20
)
⟶
x2
=
1
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
x3
x20
x21
=
If_i
(
SNoLe
x20
0
)
x21
(
x0
(
x3
(
add_SNo
x20
(
minus_SNo
1
)
)
x21
)
x20
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x4
x20
=
x3
(
x1
x20
)
x2
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x5
x20
=
x4
x20
)
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
x6
x20
x21
=
mul_SNo
2
(
mul_SNo
2
(
mul_SNo
x20
x21
)
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x7
x20
=
x20
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x8
x20
=
add_SNo
1
x20
)
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
x9
x20
x21
=
If_i
(
SNoLe
x20
0
)
x21
(
x6
(
x9
(
add_SNo
x20
(
minus_SNo
1
)
)
x21
)
x20
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x10
x20
=
x9
(
x7
x20
)
(
x8
x20
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
x11
x20
x21
=
mul_SNo
x20
x21
)
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
x12
x20
x21
=
add_SNo
1
x21
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x13
x20
=
x20
)
⟶
x14
=
1
⟶
(
∀ x20 .
x20
∈
int
⟶
x15
x20
=
add_SNo
2
x20
)
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
∀ x22 .
x22
∈
int
⟶
x16
x20
x21
x22
=
If_i
(
SNoLe
x20
0
)
x21
(
x11
(
x16
(
add_SNo
x20
(
minus_SNo
1
)
)
x21
x22
)
(
x17
(
add_SNo
x20
(
minus_SNo
1
)
)
x21
x22
)
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
∀ x22 .
x22
∈
int
⟶
x17
x20
x21
x22
=
If_i
(
SNoLe
x20
0
)
x22
(
x12
(
x16
(
add_SNo
x20
(
minus_SNo
1
)
)
x21
x22
)
(
x17
(
add_SNo
x20
(
minus_SNo
1
)
)
x21
x22
)
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x18
x20
=
x16
(
x13
x20
)
x14
(
x15
x20
)
)
⟶
(
∀ x20 .
x20
∈
int
⟶
x19
x20
=
mul_SNo
(
x10
x20
)
(
x18
x20
)
)
⟶
∀ x20 .
x20
∈
int
⟶
SNoLe
0
x20
⟶
x5
x20
=
x19
x20
Conjecture
055f7..
A26543
:
∀ x0 :
ι → ι
.
(
∀ x1 .
x1
∈
int
⟶
x0
x1
∈
int
)
⟶
∀ x1 :
ι → ι
.
(
∀ x2 .
x2
∈
int
⟶
x1
x2
∈
int
)
⟶
∀ x2 :
ι → ι
.
(
∀ x3 .
x3
∈
int
⟶
x2
x3
∈
int
)
⟶
∀ x3 :
ι → ι
.
(
∀ x4 .
x4
∈
int
⟶
x3
x4
∈
int
)
⟶
∀ x4 .
x4
∈
int
⟶
∀ x5 :
ι →
ι → ι
.
(
∀ x6 .
x6
∈
int
⟶
∀ x7 .
x7
∈
int
⟶
x5
x6
x7
∈
int
)
⟶
∀ x6 :
ι → ι
.
(
∀ x7 .
x7
∈
int
⟶
x6
x7
∈
int
)
⟶
∀ x7 :
ι → ι
.
(
∀ x8 .
x8
∈
int
⟶
x7
x8
∈
int
)
⟶
∀ x8 :
ι →
ι → ι
.
(
∀ x9 .
x9
∈
int
⟶
∀ x10 .
x10
∈
int
⟶
x8
x9
x10
∈
int
)
⟶
∀ x9 :
ι → ι
.
(
∀ x10 .
x10
∈
int
⟶
x9
x10
∈
int
)
⟶
∀ x10 :
ι → ι
.
(
∀ x11 .
x11
∈
int
⟶
x10
x11
∈
int
)
⟶
∀ x11 .
x11
∈
int
⟶
∀ x12 :
ι →
ι → ι
.
(
∀ x13 .
x13
∈
int
⟶
∀ x14 .
x14
∈
int
⟶
x12
x13
x14
∈
int
)
⟶
∀ x13 :
ι →
ι → ι
.
(
∀ x14 .
x14
∈
int
⟶
∀ x15 .
x15
∈
int
⟶
x13
x14
x15
∈
int
)
⟶
∀ x14 :
ι →
ι → ι
.
(
∀ x15 .
x15
∈
int
⟶
∀ x16 .
x16
∈
int
⟶
x14
x15
x16
∈
int
)
⟶
∀ x15 :
ι →
ι → ι
.
(
∀ x16 .
x16
∈
int
⟶
∀ x17 .
x17
∈
int
⟶
x15
x16
x17
∈
int
)
⟶
∀ x16 :
ι →
ι → ι
.
(
∀ x17 .
x17
∈
int
⟶
∀ x18 .
x18
∈
int
⟶
x16
x17
x18
∈
int
)
⟶
∀ x17 .
x17
∈
int
⟶
∀ x18 :
ι →
ι → ι
.
(
∀ x19 .
x19
∈
int
⟶
∀ x20 .
x20
∈
int
⟶
x18
x19
x20
∈
int
)
⟶
∀ x19 :
ι →
ι → ι
.
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
x19
x20
x21
∈
int
)
⟶
∀ x20 :
ι →
ι → ι
.
(
∀ x21 .
x21
∈
int
⟶
∀ x22 .
x22
∈
int
⟶
x20
x21
x22
∈
int
)
⟶
∀ x21 :
ι → ι
.
(
∀ x22 .
x22
∈
int
⟶
x21
x22
∈
int
)
⟶
∀ x22 .
x22
∈
int
⟶
∀ x23 :
ι →
ι → ι
.
(
∀ x24 .
x24
∈
int
⟶
∀ x25 .
x25
∈
int
⟶
x23
x24
x25
∈
int
)
⟶
∀ x24 :
ι → ι
.
(
∀ x25 .
x25
∈
int
⟶
x24
x25
∈
int
)
⟶
∀ x25 :
ι → ι
.
(
∀ x26 .
x26
∈
int
⟶
x25
x26
∈
int
)
⟶
∀ x26 :
ι →
ι → ι
.
(
∀ x27 .
x27
∈
int
⟶
∀ x28 .
x28
∈
int
⟶
x26
x27
x28
∈
int
)
⟶
∀ x27 :
ι →
ι → ι
.
(
∀ x28 .
x28
∈
int
⟶
∀ x29 .
x29
∈
int
⟶
x27
x28
x29
∈
int
)
⟶
∀ x28 :
ι → ι
.
(
∀ x29 .
x29
∈
int
⟶
x28
x29
∈
int
)
⟶
∀ x29 .
x29
∈
int
⟶
∀ x30 .
x30
∈
int
⟶
∀ x31 :
ι →
ι →
ι → ι
.
(
∀ x32 .
x32
∈
int
⟶
∀ x33 .
x33
∈
int
⟶
∀ x34 .
x34
∈
int
⟶
x31
x32
x33
x34
∈
int
)
⟶
∀ x32 :
ι →
ι →
ι → ι
.
(
∀ x33 .
x33
∈
int
⟶
∀ x34 .
x34
∈
int
⟶
∀ x35 .
x35
∈
int
⟶
x32
x33
x34
x35
∈
int
)
⟶
∀ x33 :
ι → ι
.
(
∀ x34 .
x34
∈
int
⟶
x33
x34
∈
int
)
⟶
∀ x34 :
ι → ι
.
(
∀ x35 .
x35
∈
int
⟶
x34
x35
∈
int
)
⟶
∀ x35 :
ι → ι
.
(
∀ x36 .
x36
∈
int
⟶
x35
x36
∈
int
)
⟶
∀ x36 .
x36
∈
int
⟶
∀ x37 :
ι →
ι → ι
.
(
∀ x38 .
x38
∈
int
⟶
∀ x39 .
x39
∈
int
⟶
x37
x38
x39
∈
int
)
⟶
∀ x38 :
ι → ι
.
(
∀ x39 .
x39
∈
int
⟶
x38
x39
∈
int
)
⟶
∀ x39 :
ι → ι
.
(
∀ x40 .
x40
∈
int
⟶
x39
x40
∈
int
)
⟶
∀ x40 .
x40
∈
int
⟶
∀ x41 :
ι →
ι → ι
.
(
∀ x42 .
x42
∈
int
⟶
∀ x43 .
x43
∈
int
⟶
x41
x42
x43
∈
int
)
⟶
∀ x42 :
ι →
ι → ι
.
(
∀ x43 .
x43
∈
int
⟶
∀ x44 .
x44
∈
int
⟶
x42
x43
x44
∈
int
)
⟶
∀ x43 :
ι →
ι → ι
.
(
∀ x44 .
x44
∈
int
⟶
∀ x45 .
x45
∈
int
⟶
x43
x44
x45
∈
int
)
⟶
∀ x44 :
ι →
ι → ι
.
(
∀ x45 .
x45
∈
int
⟶
∀ x46 .
x46
∈
int
⟶
x44
x45
x46
∈
int
)
⟶
∀ x45 :
ι → ι
.
(
∀ x46 .
x46
∈
int
⟶
x45
x46
∈
int
)
⟶
∀ x46 .
x46
∈
int
⟶
∀ x47 :
ι →
ι → ι
.
(
∀ x48 .
x48
∈
int
⟶
∀ x49 .
x49
∈
int
⟶
x47
x48
x49
∈
int
)
⟶
∀ x48 :
ι → ι
.
(
∀ x49 .
x49
∈
int
⟶
x48
x49
∈
int
)
⟶
∀ x49 :
ι → ι
.
(
∀ x50 .
x50
∈
int
⟶
x49
x50
∈
int
)
⟶
(
∀ x50 .
x50
∈
int
⟶
x0
x50
=
mul_SNo
2
(
add_SNo
(
add_SNo
x50
x50
)
x50
)
)
⟶
(
∀ x50 .
x50
∈
int
⟶
x1
x50
=
x50
)
⟶
(
∀ x50 .
x50
∈
int
⟶
x2
x50
=
add_SNo
x50
x50
)
⟶
(
∀ x50 .
x50
∈
int
⟶
x3
x50
=
x50
)
⟶
x4
=
2
⟶
(
∀ x50 .
x50
∈
int
⟶
∀ x51 .
x51
∈
int
⟶
x5
x50
x51
=
If_i
(
SNoLe
x50
0
)
x51
(
x2
(
x5
(
add_SNo
x50
(
minus_SNo
1
)
)
x51
)
)
)
⟶
(
∀ x50 .
x50
∈
int
⟶
x6
x50
=
x5
(
x3
x50
)
x4
)
⟶
(
∀ x50 .
x50
∈
int
⟶
x7
x50
=
add_SNo
(
x6
x50
)
(
minus_SNo
1
)
)
⟶
(
∀ x50 .
x50
∈
int
⟶
∀ x51 .
x51
∈
int
⟶
x8
x50
x51
=
If_i
(
SNoLe
x50
0
)
x51
(
x0
(
x8
(
add_SNo
x50
(
minus_SNo
1
)
)
x51
)
)
)
⟶
(
∀ x50 .
x50
∈
int
⟶
x9
x50
=
x8
(
x1
x50
)
(
x7
x50
)
)
⟶
(
∀ x50 .
x50
∈
int
⟶
x10
x50
=
x9
x50
)
⟶
x11
=
1
⟶
(
∀ x50 .
x50
∈
int
⟶
∀ x51 .
x51
∈
int
⟶
x12
x50
x51
=
x51
)
⟶
(
∀ x50 .
x50
∈
int
⟶
∀ x51 .
x51
∈
int
⟶
x13
x50
x51
=
If_i
(
SNoLe
x50
0
)
x51
(
x10
(
x13
(
add_SNo
x50
(
minus_SNo
1
)
)
x51
)
)
)
⟶
(
∀ x50 .
x50
∈
int
⟶
∀ x51 .
x51
∈
int
⟶
x14
x50
x51
=
x13
x11
(
x12
x50
x51
)
)
⟶
(
∀ x50 .
x50
∈
int
⟶
∀ x51 .
x51
∈
int
⟶
x15
x50
x51
=
add_SNo
(
add_SNo
(
x14
x50
x51
)
(
mul_SNo
2
(
add_SNo
(
add_SNo
x50
x50
)
x50
)
)
)
x50
)
⟶
(
∀ x50 .
x50
∈
int
⟶
∀ x51 .
x51
∈
int
⟶
x16
x50
x51
=
x51
)
⟶
x17
=
1
⟶
(
∀ x50 .
x50
∈
int
⟶
∀ x51 .
x51
∈
int
⟶
x18
x50
x51
=
If_i
(
SNoLe
x50
0
)
x51
(
x15
(
x18
(
add_SNo
x50
(
minus_SNo
1
)
)
x51
)
x50
)
)
⟶
(
∀ x50 .
x50
∈
int
⟶
∀ x51 .
x51
∈
int
⟶
x19
x50
x51
=
x18
(
x16
x50
x51
)
x17
)
⟶
(
∀ x50 .
x50
∈
int
⟶
∀ x51 .
x51
∈
int
⟶
x20
x50
x51
=
add_SNo
(
add_SNo
(
x19
x50
x51
)
x50
)
x50
)
⟶
(
∀ x50 .
x50
∈
int
⟶
x21
x50
=
x50
)
⟶
x22
=
1
⟶
(
∀ x50 .
x50
∈
int
⟶
∀ x51 .
x51
∈
int
⟶
x23
x50
x51
=
If_i
(
SNoLe
x50
0
)
x51
(
x20
(
x23
(
add_SNo
x50
(
minus_SNo
1
)
)
x51
)
x50
)
)
⟶
(
∀ x50 .
x50
∈
int
⟶
x24
x50
=
x23
(
x21
x50
)
x22
)
⟶
(
∀ x50 .
x50
∈
int
⟶
x25
x50
=
x24
x50
)
⟶
(
∀ x50 .
x50
∈
int
⟶
∀ x51 .
x51
∈
int
⟶
x26
x50
x51
=
add_SNo
(
mul_SNo
2
(
add_SNo
(
add_SNo
x50
x50
)
x50
)
)
x51
)
⟶
(
∀ x50 .
x50
∈
int
⟶
∀ x51 .
x51
∈
int
⟶
x27
x50
x51
=
add_SNo
1
(
add_SNo
(
add_SNo
x51
x51
)
x51
)
)
⟶
(
∀ x50 .
x50
∈
int
⟶
x28
x50
=
x50
)
⟶
x29
=
1
⟶
x30
=
add_SNo
2
2
⟶
(
∀ x50 .
x50
∈
int
⟶
∀ x51 .
x51
∈
int
⟶
∀ x52 .
x52
∈
int
⟶
x31
x50
x51
x52
=
If_i
(
SNoLe
x50
0
)
x51
(
x26
(
x31
(
add_SNo
x50
(
minus_SNo
1
)
)
x51
x52
)
(
x32
(
add_SNo
x50
(
minus_SNo
1
)
)
x51
x52
)
)
)
⟶
(
∀ x50 .
x50
∈
int
⟶
∀ x51 .
x51
∈
int
⟶
∀ x52 .
x52
∈
int
⟶
x32
x50
x51
x52
=
If_i
(
SNoLe
x50
0
)
x52
(
x27
(
x31
(
add_SNo
x50
(
minus_SNo
1
)
)
x51
x52
)
(
x32
(
add_SNo
x50
(
minus_SNo
1
)
)
x51
x52
)
)
)
⟶
(
∀ x50 .
x50
∈
int
⟶
x33
x50
=
x31
(
x28
x50
)
x29
x30
)
⟶
(
∀ x50 .
x50
∈
int
⟶
x34
x50
=
add_SNo
x50
x50
)
⟶
(
∀ x50 .
x50
∈
int
⟶
x35
x50
=
x50
)
⟶
x36
=
1
⟶
(
∀ x50 .
x50
∈
int
⟶
∀ x51 .
x51
∈
int
⟶
x37
x50
x51
=
If_i
(
SNoLe
x50
0
)
x51
(
x34
(
x37
(
add_SNo
x50
(
minus_SNo
1
)
)
x51
)
)
)
⟶
(
∀ x50 .
x50
∈
int
⟶
x38
x50
=
x37
(
x35
x50
)
x36
)
⟶
(
∀ x50 .
x50
∈
int
⟶
x39
x50
=
mul_SNo
(
x33
x50
)
(
x38
x50
)
)
⟶
x40
=
1
⟶
(
∀ x50 .
x50
∈
int
⟶
∀ x51 .
x51
∈
int
⟶
x41
x50
x51
=
x51
)
⟶
(
∀ x50 .
x50
∈
int
⟶
∀ x51 .
x51
∈
int
⟶
x42
x50
x51
=
If_i
(
SNoLe
x50
0
)
x51
(
x39
(
x42
(
add_SNo
x50
(
minus_SNo
1
)
)
x51
)
)
)
⟶
(
∀ x50 .
x50
∈
int
⟶
∀ x51 .
x51
∈
int
⟶
x43
x50
x51
=
x42
x40
(
x41
x50
x51
)
)
⟶
(
∀ x50 .
x50
∈
int
⟶
∀ x51 .
x51
∈
int
⟶
x44
x50
x51
=
add_SNo
(
add_SNo
(
x43
x50
x51
)
(
mul_SNo
2
(
add_SNo
(
add_SNo
x50
x50
)
x50
)
)
)
x50
)
⟶
(
∀ x50 .
x50
∈
int
⟶
x45
x50
=
x50
)
⟶
x46
=
1
⟶
(
∀ x50 .
x50
∈
int
⟶
∀ x51 .
x51
∈
int
⟶
x47
x50
x51
=
If_i
(
SNoLe
x50
0
)
x51
(
x44
(
x47
(
add_SNo
x50
(
minus_SNo
1
)
)
x51
)
x50
)
)
⟶
(
∀ x50 .
x50
∈
int
⟶
x48
x50
=
x47
(
x45
x50
)
x46
)
⟶
(
∀ x50 .
x50
∈
int
⟶
x49
x50
=
x48
x50
)
⟶
∀ x50 .
x50
∈
int
⟶
SNoLe
0
x50
⟶
x25
x50
=
x49
x50
Conjecture
c344a..
A26324
:
∀ x0 :
ι →
ι → ι
.
(
∀ x1 .
x1
∈
int
⟶
∀ x2 .
x2
∈
int
⟶
x0
x1
x2
∈
int
)
⟶
∀ x1 :
ι →
ι → ι
.
(
∀ x2 .
x2
∈
int
⟶
∀ x3 .
x3
∈
int
⟶
x1
x2
x3
∈
int
)
⟶
∀ x2 :
ι →
ι → ι
.
(
∀ x3 .
x3
∈
int
⟶
∀ x4 .
x4
∈
int
⟶
x2
x3
x4
∈
int
)
⟶
∀ x3 .
x3
∈
int
⟶
∀ x4 .
x4
∈
int
⟶
∀ x5 :
ι →
ι →
ι → ι
.
(
∀ x6 .
x6
∈
int
⟶
∀ x7 .
x7
∈
int
⟶
∀ x8 .
x8
∈
int
⟶
x5
x6
x7
x8
∈
int
)
⟶
∀ x6 :
ι →
ι →
ι → ι
.
(
∀ x7 .
x7
∈
int
⟶
∀ x8 .
x8
∈
int
⟶
∀ x9 .
x9
∈
int
⟶
x6
x7
x8
x9
∈
int
)
⟶
∀ x7 :
ι →
ι → ι
.
(
∀ x8 .
x8
∈
int
⟶
∀ x9 .
x9
∈
int
⟶
x7
x8
x9
∈
int
)
⟶
∀ x8 :
ι →
ι → ι
.
(
∀ x9 .
x9
∈
int
⟶
∀ x10 .
x10
∈
int
⟶
x8
x9
x10
∈
int
)
⟶
∀ x9 :
ι →
ι → ι
.
(
∀ x10 .
x10
∈
int
⟶
∀ x11 .
x11
∈
int
⟶
x9
x10
x11
∈
int
)
⟶
∀ x10 .
x10
∈
int
⟶
∀ x11 :
ι →
ι → ι
.
(
∀ x12 .
x12
∈
int
⟶
∀ x13 .
x13
∈
int
⟶
x11
x12
x13
∈
int
)
⟶
∀ x12 :
ι →
ι → ι
.
(
∀ x13 .
x13
∈
int
⟶
∀ x14 .
x14
∈
int
⟶
x12
x13
x14
∈
int
)
⟶
∀ x13 :
ι →
ι → ι
.
(
∀ x14 .
x14
∈
int
⟶
∀ x15 .
x15
∈
int
⟶
x13
x14
x15
∈
int
)
⟶
∀ x14 :
ι → ι
.
(
∀ x15 .
x15
∈
int
⟶
x14
x15
∈
int
)
⟶
∀ x15 .
x15
∈
int
⟶
∀ x16 :
ι →
ι → ι
.
(
∀ x17 .
x17
∈
int
⟶
∀ x18 .
x18
∈
int
⟶
x16
x17
x18
∈
int
)
⟶
∀ x17 :
ι → ι
.
(
∀ x18 .
x18
∈
int
⟶
x17
x18
∈
int
)
⟶
∀ x18 :
ι → ι
.
(
∀ x19 .
x19
∈
int
⟶
x18
x19
∈
int
)
⟶
∀ x19 :
ι →
ι → ι
.
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
x19
x20
x21
∈
int
)
⟶
∀ x20 :
ι →
ι → ι
.
(
∀ x21 .
x21
∈
int
⟶
∀ x22 .
x22
∈
int
⟶
x20
x21
x22
∈
int
)
⟶
∀ x21 :
ι → ι
.
(
∀ x22 .
x22
∈
int
⟶
x21
x22
∈
int
)
⟶
∀ x22 .
x22
∈
int
⟶
∀ x23 .
x23
∈
int
⟶
∀ x24 :
ι →
ι →
ι → ι
.
(
∀ x25 .
x25
∈
int
⟶
∀ x26 .
x26
∈
int
⟶
∀ x27 .
x27
∈
int
⟶
x24
x25
x26
x27
∈
int
)
⟶
∀ x25 :
ι →
ι →
ι → ι
.
(
∀ x26 .
x26
∈
int
⟶
∀ x27 .
x27
∈
int
⟶
∀ x28 .
x28
∈
int
⟶
x25
x26
x27
x28
∈
int
)
⟶
∀ x26 :
ι → ι
.
(
∀ x27 .
x27
∈
int
⟶
x26
x27
∈
int
)
⟶
∀ x27 :
ι → ι
.
(
∀ x28 .
x28
∈
int
⟶
x27
x28
∈
int
)
⟶
∀ x28 :
ι → ι
.
(
∀ x29 .
x29
∈
int
⟶
x28
x29
∈
int
)
⟶
∀ x29 .
x29
∈
int
⟶
∀ x30 :
ι →
ι → ι
.
(
∀ x31 .
x31
∈
int
⟶
∀ x32 .
x32
∈
int
⟶
x30
x31
x32
∈
int
)
⟶
∀ x31 :
ι → ι
.
(
∀ x32 .
x32
∈
int
⟶
x31
x32
∈
int
)
⟶
∀ x32 :
ι → ι
.
(
∀ x33 .
x33
∈
int
⟶
x32
x33
∈
int
)
⟶
∀ x33 .
x33
∈
int
⟶
∀ x34 :
ι →
ι → ι
.
(
∀ x35 .
x35
∈
int
⟶
∀ x36 .
x36
∈
int
⟶
x34
x35
x36
∈
int
)
⟶
∀ x35 :
ι →
ι → ι
.
(
∀ x36 .
x36
∈
int
⟶
∀ x37 .
x37
∈
int
⟶
x35
x36
x37
∈
int
)
⟶
∀ x36 :
ι →
ι → ι
.
(
∀ x37 .
x37
∈
int
⟶
∀ x38 .
x38
∈
int
⟶
x36
x37
x38
∈
int
)
⟶
∀ x37 :
ι →
ι → ι
.
(
∀ x38 .
x38
∈
int
⟶
∀ x39 .
x39
∈
int
⟶
x37
x38
x39
∈
int
)
⟶
∀ x38 :
ι → ι
.
(
∀ x39 .
x39
∈
int
⟶
x38
x39
∈
int
)
⟶
∀ x39 .
x39
∈
int
⟶
∀ x40 :
ι →
ι → ι
.
(
∀ x41 .
x41
∈
int
⟶
∀ x42 .
x42
∈
int
⟶
x40
x41
x42
∈
int
)
⟶
∀ x41 :
ι → ι
.
(
∀ x42 .
x42
∈
int
⟶
x41
x42
∈
int
)
⟶
∀ x42 :
ι → ι
.
(
∀ x43 .
x43
∈
int
⟶
x42
x43
∈
int
)
⟶
(
∀ x43 .
x43
∈
int
⟶
∀ x44 .
x44
∈
int
⟶
x0
x43
x44
=
add_SNo
(
mul_SNo
2
(
add_SNo
(
add_SNo
x43
x43
)
x43
)
)
(
mul_SNo
(
mul_SNo
x44
x44
)
x44
)
)
⟶
(
∀ x43 .
x43
∈
int
⟶
∀ x44 .
x44
∈
int
⟶
x1
x43
x44
=
add_SNo
x44
x44
)
⟶
(
∀ x43 .
x43
∈
int
⟶
∀ x44 .
x44
∈
int
⟶
x2
x43
x44
=
x44
)
⟶
x3
=
1
⟶
x4
=
2
⟶
(
∀ x43 .
x43
∈
int
⟶
∀ x44 .
x44
∈
int
⟶
∀ x45 .
x45
∈
int
⟶
x5
x43
x44
x45
=
If_i
(
SNoLe
x43
0
)
x44
(
x0
(
x5
(
add_SNo
x43
(
minus_SNo
1
)
)
x44
x45
)
(
x6
(
add_SNo
x43
(
minus_SNo
1
)
)
x44
x45
)
)
)
⟶
(
∀ x43 .
x43
∈
int
⟶
∀ x44 .
x44
∈
int
⟶
∀ x45 .
x45
∈
int
⟶
x6
x43
x44
x45
=
If_i
(
SNoLe
x43
0
)
x45
(
x1
(
x5
(
add_SNo
x43
(
minus_SNo
1
)
)
x44
x45
)
(
x6
(
add_SNo
x43
(
minus_SNo
1
)
)
x44
x45
)
)
)
⟶
(
∀ x43 .
x43
∈
int
⟶
∀ x44 .
x44
∈
int
⟶
x7
x43
x44
=
x5
(
x2
x43
x44
)
x3
x4
)
⟶
(
∀ x43 .
x43
∈
int
⟶
∀ x44 .
x44
∈
int
⟶
x8
x43
x44
=
add_SNo
(
add_SNo
(
x7
x43
x44
)
(
mul_SNo
2
(
add_SNo
(
add_SNo
x43
x43
)
x43
)
)
)
x43
)
⟶
(
∀ x43 .
x43
∈
int
⟶
∀ x44 .
x44
∈
int
⟶
x9
x43
x44
=
x44
)
⟶
x10
=
1
⟶
(
∀ x43 .
x43
∈
int
⟶
∀ x44 .
x44
∈
int
⟶
x11
x43
x44
=
If_i
(
SNoLe
x43
0
)
x44
(
x8
(
x11
(
add_SNo
x43
(
minus_SNo
1
)
)
x44
)
x43
)
)
⟶
(
∀ x43 .
x43
∈
int
⟶
∀ x44 .
x44
∈
int
⟶
x12
x43
x44
=
x11
(
x9
x43
x44
)
x10
)
⟶
(
∀ x43 .
x43
∈
int
⟶
∀ x44 .
x44
∈
int
⟶
x13
x43
x44
=
add_SNo
(
add_SNo
(
x12
x43
x44
)
x43
)
x43
)
⟶
(
∀ x43 .
x43
∈
int
⟶
x14
x43
=
x43
)
⟶
x15
=
1
⟶
(
∀ x43 .
x43
∈
int
⟶
∀ x44 .
x44
∈
int
⟶
x16
x43
x44
=
If_i
(
SNoLe
x43
0
)
x44
(
x13
(
x16
(
add_SNo
x43
(
minus_SNo
1
)
)
x44
)
x43
)
)
⟶
(
∀ x43 .
x43
∈
int
⟶
x17
x43
=
x16
(
x14
x43
)
x15
)
⟶
(
∀ x43 .
x43
∈
int
⟶
x18
x43
=
x17
x43
)
⟶
(
∀ x43 .
x43
∈
int
⟶
∀ x44 .
x44
∈
int
⟶
x19
x43
x44
=
add_SNo
(
mul_SNo
2
(
add_SNo
x43
x43
)
)
x44
)
⟶
(
∀ x43 .
x43
∈
int
⟶
∀ x44 .
x44
∈
int
⟶
x20
x43
x44
=
add_SNo
1
(
add_SNo
(
add_SNo
x44
x44
)
x44
)
)
⟶
(
∀ x43 .
x43
∈
int
⟶
x21
x43
=
x43
)
⟶
x22
=
1
⟶
x23
=
add_SNo
2
2
⟶
(
∀ x43 .
x43
∈
int
⟶
∀ x44 .
x44
∈
int
⟶
∀ x45 .
x45
∈
int
⟶
x24
x43
x44
x45
=
If_i
(
SNoLe
x43
0
)
x44
(
x19
(
x24
(
add_SNo
x43
(
minus_SNo
1
)
)
x44
x45
)
(
x25
(
add_SNo
x43
(
minus_SNo
1
)
)
x44
x45
)
)
)
⟶
(
∀ x43 .
x43
∈
int
⟶
∀ x44 .
x44
∈
int
⟶
∀ x45 .
x45
∈
int
⟶
x25
x43
x44
x45
=
If_i
(
SNoLe
x43
0
)
x45
(
x20
(
x24
(
add_SNo
x43
(
minus_SNo
1
)
)
x44
x45
)
(
x25
(
add_SNo
x43
(
minus_SNo
1
)
)
x44
x45
)
)
)
⟶
(
∀ x43 .
x43
∈
int
⟶
x26
x43
=
x24
(
x21
x43
)
x22
x23
)
⟶
(
∀ x43 .
x43
∈
int
⟶
x27
x43
=
add_SNo
x43
x43
)
⟶
(
∀ x43 .
x43
∈
int
⟶
x28
x43
=
x43
)
⟶
x29
=
1
⟶
(
∀ x43 .
x43
∈
int
⟶
∀ x44 .
x44
∈
int
⟶
x30
x43
x44
=
If_i
(
SNoLe
x43
0
)
x44
(
x27
(
x30
(
add_SNo
x43
(
minus_SNo
1
)
)
x44
)
)
)
⟶
(
∀ x43 .
x43
∈
int
⟶
x31
x43
=
x30
(
x28
x43
)
x29
)
⟶
(
∀ x43 .
x43
∈
int
⟶
x32
x43
=
mul_SNo
(
x26
x43
)
(
x31
x43
)
)
⟶
x33
=
1
⟶
(
∀ x43 .
x43
∈
int
⟶
∀ x44 .
x44
∈
int
⟶
x34
x43
x44
=
x44
)
⟶
(
∀ x43 .
x43
∈
int
⟶
∀ x44 .
x44
∈
int
⟶
x35
x43
x44
=
If_i
(
SNoLe
x43
0
)
x44
(
x32
(
x35
(
add_SNo
x43
(
minus_SNo
1
)
)
x44
)
)
)
⟶
(
∀ x43 .
x43
∈
int
⟶
∀ x44 .
x44
∈
int
⟶
x36
x43
x44
=
x35
x33
(
x34
x43
x44
)
)
⟶
(
∀ x43 .
x43
∈
int
⟶
∀ x44 .
x44
∈
int
⟶
x37
x43
x44
=
add_SNo
(
add_SNo
(
x36
x43
x44
)
(
mul_SNo
2
(
add_SNo
(
add_SNo
x43
x43
)
x43
)
)
)
x43
)
⟶
(
∀ x43 .
x43
∈
int
⟶
x38
x43
=
x43
)
⟶
x39
=
1
⟶
(
∀ x43 .
x43
∈
int
⟶
∀ x44 .
x44
∈
int
⟶
x40
x43
x44
=
If_i
(
SNoLe
x43
0
)
x44
(
x37
(
x40
(
add_SNo
x43
(
minus_SNo
1
)
)
x44
)
x43
)
)
⟶
(
∀ x43 .
x43
∈
int
⟶
x41
x43
=
x40
(
x38
x43
)
x39
)
⟶
(
∀ x43 .
x43
∈
int
⟶
x42
x43
=
x41
x43
)
⟶
∀ x43 .
x43
∈
int
⟶
SNoLe
0
x43
⟶
x18
x43
=
x42
x43
Conjecture
7915f..
A262787
:
∀ x0 :
ι → ι
.
(
∀ x1 .
x1
∈
int
⟶
x0
x1
∈
int
)
⟶
∀ x1 .
x1
∈
int
⟶
∀ x2 .
x2
∈
int
⟶
∀ x3 :
ι →
ι → ι
.
(
∀ x4 .
x4
∈
int
⟶
∀ x5 .
x5
∈
int
⟶
x3
x4
x5
∈
int
)
⟶
∀ x4 .
x4
∈
int
⟶
∀ x5 :
ι → ι
.
(
∀ x6 .
x6
∈
int
⟶
x5
x6
∈
int
)
⟶
∀ x6 :
ι → ι
.
(
∀ x7 .
x7
∈
int
⟶
x6
x7
∈
int
)
⟶
∀ x7 .
x7
∈
int
⟶
∀ x8 :
ι →
ι → ι
.
(
∀ x9 .
x9
∈
int
⟶
∀ x10 .
x10
∈
int
⟶
x8
x9
x10
∈
int
)
⟶
∀ x9 :
ι → ι
.
(
∀ x10 .
x10
∈
int
⟶
x9
x10
∈
int
)
⟶
∀ x10 :
ι → ι
.
(
∀ x11 .
x11
∈
int
⟶
x10
x11
∈
int
)
⟶
∀ x11 :
ι →
ι → ι
.
(
∀ x12 .
x12
∈
int
⟶
∀ x13 .
x13
∈
int
⟶
x11
x12
x13
∈
int
)
⟶
∀ x12 :
ι →
ι → ι
.
(
∀ x13 .
x13
∈
int
⟶
∀ x14 .
x14
∈
int
⟶
x12
x13
x14
∈
int
)
⟶
∀ x13 :
ι → ι
.
(
∀ x14 .
x14
∈
int
⟶
x13
x14
∈
int
)
⟶
∀ x14 .
x14
∈
int
⟶
∀ x15 .
x15
∈
int
⟶
∀ x16 :
ι →
ι →
ι → ι
.
(
∀ x17 .
x17
∈
int
⟶
∀ x18 .
x18
∈
int
⟶
∀ x19 .
x19
∈
int
⟶
x16
x17
x18
x19
∈
int
)
⟶
∀ x17 :
ι →
ι →
ι → ι
.
(
∀ x18 .
x18
∈
int
⟶
∀ x19 .
x19
∈
int
⟶
∀ x20 .
x20
∈
int
⟶
x17
x18
x19
x20
∈
int
)
⟶
∀ x18 :
ι → ι
.
(
∀ x19 .
x19
∈
int
⟶
x18
x19
∈
int
)
⟶
∀ x19 :
ι →
ι → ι
.
(
∀ x20 .
x20
∈
int
⟶
∀ x21 .
x21
∈
int
⟶
x19
x20
x21
∈
int
)
⟶
∀ x20 :
ι →
ι → ι
.
(
∀ x21 .
x21
∈
int
⟶
∀ x22 .
x22
∈
int
⟶
x20
x21
x22
∈
int
)
⟶
∀ x21 :
ι → ι
.
(
∀ x22 .
x22
∈
int
⟶
x21
x22
∈
int
)
⟶
∀ x22 .
x22
∈
int
⟶
∀ x23 .
x23
∈
int
⟶
∀ x24 :
ι →
ι →
ι → ι
.
(
∀ x25 .
x25
∈
int
⟶
∀ x26 .
x26
∈
int
⟶
∀ x27 .
x27
∈
int
⟶
x24
x25
x26
x27
∈
int
)
⟶
∀ x25 :
ι →
ι →
ι → ι
.
(
∀ x26 .
x26
∈
int
⟶
∀ x27 .
x27
∈
int
⟶
∀ x28 .
x28
∈
int
⟶
x25
x26
x27
x28
∈
int
)
⟶
∀ x26 :
ι → ι
.
(
∀ x27 .
x27
∈
int
⟶
x26
x27
∈
int
)
⟶
∀ x27 :
ι → ι
.
(
∀ x28 .
x28
∈
int
⟶
x27
x28
∈
int
)
⟶
(
∀ x28 .
x28
∈
int
⟶
x0
x28
=
add_SNo
(
mul_SNo
x28
x28
)
x28
)
⟶
x1
=
2
⟶
x2
=
2
⟶
(
∀ x28 .
x28
∈
int
⟶
∀ x29 .
x29
∈
int
⟶
x3
x28
x29
=
If_i
(
SNoLe
x28
0
)
x29
(
x0
(
x3
(
add_SNo
x28
(
minus_SNo
1
)
)
x29
)
)
)
⟶
x4
=
x3
x1
x2
⟶
(
∀ x28 .
x28
∈
int
⟶
x5
x28
=
add_SNo
(
mul_SNo
x4
x28
)
(
minus_SNo
x28
)
)
⟶
(
∀ x28 .
x28
∈
int
⟶
x6
x28
=
add_SNo
1
(
add_SNo
x28
x28
)
)
⟶
x7
=
1
⟶
(
∀ x28 .
x28
∈
int
⟶
∀ x29 .
x29
∈
int
⟶
x8
x28
x29
=
If_i
(
SNoLe
x28
0
)
x29
(
x5
(
x8
(
add_SNo
x28
(
minus_SNo
1
)
)
x29
)
)
)
⟶
(
∀ x28 .
x28
∈
int
⟶
x9
x28
=
x8
(
x6
x28
)
x7
)
⟶
(
∀ x28 .
x28
∈
int
⟶
x10
x28
=
x9
x28
)
⟶
(
∀ x28 .
x28
∈
int
⟶
∀ x29 .
x29
∈
int
⟶
x11
x28
x29
=
mul_SNo
x28
x29
)
⟶
(
∀ x28 .
x28
∈
int
⟶
∀ x29 .
x29
∈
int
⟶
x12
x28
x29
=
x29
)
⟶
(
∀ x28 .
x28
∈
int
⟶
x13
x28
=
add_SNo
1
x28
)
⟶
x14
=
1
⟶
x15
=
add_SNo
1
(
mul_SNo
2
(
mul_SNo
2
(
add_SNo
2
(
mul_SNo
2
(
add_SNo
2
2
)
)
)
)
)
⟶
(
∀ x28 .
x28
∈
int
⟶
∀ x29 .
x29
∈
int
⟶
∀ x30 .
x30
∈
int
⟶
x16
x28
x29
x30
=
If_i
(
SNoLe
x28
0
)
x29
(
x11
(
x16
(
add_SNo
x28
(
minus_SNo
1
)
)
x29
x30
)
(
x17
(
add_SNo
x28
(
minus_SNo
1
)
)
x29
x30
)
)
)
⟶
(
∀ x28 .
x28
∈
int
⟶
∀ x29 .
x29
∈
int
⟶
∀ x30 .
x30
∈
int
⟶
x17
x28
x29
x30
=
If_i
(
SNoLe
x28
0
)
x30
(
x12
(
x16
(
add_SNo
x28
(
minus_SNo
1
)
)
x29
x30
)
(
x17
(
add_SNo
x28
(
minus_SNo
1
)
)
x29
x30
)
)
)
⟶
(
∀ x28 .
x28
∈
int
⟶
x18
x28
=
x16
(
x13
x28
)
x14
x15
)
⟶
(
∀ x28 .
x28
∈
int
⟶
∀ x29 .
x29
∈
int
⟶
x19
x28
x29
=
mul_SNo
x28
x29
)
⟶
(
∀ x28 .
x28
∈
int
⟶
∀ x29 .
x29
∈
int
⟶
x20
x28
x29
=
x29
)
⟶
(
∀ x28 .
x28
∈
int
⟶
x21
x28
=
x28
)
⟶
x22
=
1
⟶
x23
=
add_SNo
1
(
mul_SNo
2
(
mul_SNo
2
(
add_SNo
2
(
mul_SNo
2
(
add_SNo
2
2
)
)
)
)
)
⟶
(
∀ x28 .
x28
∈
int
⟶
∀ x29 .
x29
∈
int
⟶
∀ x30 .
x30
∈
int
⟶
x24
x28
x29
x30
=
If_i
(
SNoLe
x28
0
)
x29
(
x19
(
x24
(
add_SNo
x28
(
minus_SNo
1
)
)
x29
x30
)
(
x25
(
add_SNo
x28
(
minus_SNo
1
)
)
x29
x30
)
)
)
⟶
(
∀ x28 .
x28
∈
int
⟶
∀ x29 .
x29
∈
int
⟶
∀ x30 .
x30
∈
int
⟶
x25
x28
x29
x30
=
If_i
(
SNoLe
x28
0
)
x30
(
x20
(
x24
(
add_SNo
x28
(
minus_SNo
1
)
)
x29
x30
)
(
x25
(
add_SNo
x28
(
minus_SNo
1
)
)
x29
x30
)
)
)
⟶
(
∀ x28 .
x28
∈
int
⟶
x26
x28
=
x24
(
x21
x28
)
x22
x23
)
⟶
(
∀ x28 .
x28
∈
int
⟶
x27
x28
=
mul_SNo
(
x18
x28
)
(
x26
x28
)
)
⟶
∀ x28 .
x28
∈
int
⟶
SNoLe
0
x28
⟶
x10
x28
=
x27
x28