Элементы теории алгоритмов - 138 стр.

UptoLike

ВУЗ: 

ЯрГУ | Ярославль

Составители: 

Рубрика: 

S(x, z)
WIC(x) ∨ WVbl(x) ∨
(∃u)
u<x
(∃v)
v<x
(∃t)
t<x
(ex(u, z)=1&ex(v,z)=1&WFL(t)&
x =2
3
∗ u ∗ t ∗ v ∗ 2
5
).
Trm(x) S(x, (χ
Trm
)
#
(x))
Atmfl(x) x
(t
1
˜= t
2
) t
1
t
2
Atmfl(x)
(∃u)
u<x
(∃v)
v<x
(Trm(u)&Trm(v)&x =2
3
∗ u ∗ 2
29
∗ v ∗ 2
5
).
Fmfl(x) x
(Atmfl(x) ∨∃u)
u<x
(Fmfl(u)&x =2
3
∗ 2
9
∗ u ∗ 2
5
) ∨
(∃u)
u<x
(∃v)
v<x
(Frml(u)&Frml(v)&
(x =2
3
∗ u ∗ 2
11
∗ v ∗ 2
5
∨ x =2
3
∗ u ∗ 2
13
∗ v ∗ 2
5
∨
x =2
3
∗ u ∗ 2
15
∗ v ∗ 2
5
)) ∨
(∃u)
u<x
(∃v)
v<x
(WVbl(u)&Frml(v)&
(x =2
3
∗ 2
17
∗ u ∗ 2
5
∗ v ∨ (x =2
3
∗ 2
19
∗ u ∗ 2
5
∗ v)).
Subst
(1)
Fml
(γ,u, v) ex(0,γ)
ex(1,γ)
u
v
Subst
Trm
(γ,u, v) ex(1,γ) ex(0,γ)

Страницы