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

UptoLike

ВУЗ: 

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

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

Рубрика: 

§1
u
v
Trm(u)&WVbl(v)&Trm(ex(1,γ)) &
((∃z)
z<ex(1,γ)
(ex(1,γ)=2
z
&
(ex(1,γ)=v & ex(0,γ)=u) ∨ (ex(1,γ) = v & ex(0,γ)=ex(1,γ))) ∨
(∃α)
α<ex(1,γ)
(∃β)
β<ex(1,γ)
(∃δ)
δ<ex(1,γ)
(WFL(δ)&Trm(α)&Trm(β)&
ex(1,γ)=2
3
∗ α ∗ δ ∗ β ∗ 2
5
&
(∃α
0
)
α
0
<ex(0,γ)
(∃β
0
)
β
0
<ex(0,γ)
(ex(0,γ)=2
3
∗ α
0
∗ δ ∗β
0
∗ 2
5
&
Subst
Trm
(2
α
0
· 3
α
,u,v)&Subst
Trm
(2
β
0
·3
β
,u,v)))).
Subst
Atmfl
(γ,u,v) ex(1,γ)
ex(0,γ)
u v
Trm(u)&WVbl(v)&Atmf l(ex(1,γ)) &
(∃α)
α<ex(1,γ)
(∃β)
β<ex(1,γ)
(Trm(α)&Trm(β)&
ex(1,γ)=2
3
∗ α ∗ 2
29
∗ β ∗2
5
&
(∃α
0
)
α
0
<ex(0,γ)
(∃β
0
)
β
0
<ex(0,γ)
(ex(0,γ)=2
3
∗ α
0
∗ 2
29
∗ β
0
∗ 2
5
&
Subst
Trm
(2
α
0
·3
α
,u,v)&Subst
Trm
(2
β
0
·3
β
,u,v)))
Subst
(1)
Fml
(γ,u,v) ex(1,γ) ex(0,γ)
u
v
Fml(ex(1,γ)) & (Atmfl(ex(1,γ)) & Subst
Atmfl
(γ,u,v)) ∨
((∃α)
α<ex(1,γ)
(∃α
0
)
α
0
<ex(0,γ)
(Fml(α)&
ex(1,γ)=2
3
∗ 2
9
∗ α ∗ 2
5
& ex(0,γ)=2
3
∗ 2
9
∗ α
0
∗ 2
5
&
Subst
Fml
(2
α
0
· 3
α
,u,v)) ∨
((∃α)
α<ex(1,γ)
(∃α
0
)
α
0
<ex(0,γ)
(∃β)
β<ex(1,γ)
(∃β
0
)
β
0
<ex(0,γ)
(∃δ)
δ<ex(1,γ)
((δ =2
11
∨ δ =2
13
∨ δ =2
15
)&(Fml(α)&Fml(β)&
ex(1,γ)=2
3
∗ α ∗ δ ∗β ∗ 2
5
& ex(0,γ)=2
3
∗ α
0
∗ δ ∗β
0
∗ 2
5
&
Subst
Fml
(2
α
0
·3
α
,u,v)&Subst
Fml
(2
β
0
· 3
β
,u,v)) ∨
((∃α)
α<ex(1,γ)
(∃α
0
)
α
0
<ex(0,γ)
(∃β)
β<ex(1,γ)
(∃β
0
)
β
0
<ex(0,γ)
(∃δ)
δ<ex(1,γ)
((δ =2
17
∨ δ =2
19
)&(Fml(α)&WVbl(β)&
ex(1,γ)=2
3
∗ δ ∗β ∗ 2
5
∗ α & ex(0,γ)=2
3
∗ δ ∗β ∗ α
0
∗ 2
5
&
((β = v & α
0
= α) ∨ (β = v & Subst
Fml
(2
α
0
· 3
α
,u,v)).
Subst
Fml
(x, y, u, v) x
y
u
v

Страницы