Tammet: Uus lehekülg: ' See ülesanne on näide 2013 aastast, mida lähiajal uuendatakse 2015 aastaks. See on vabatahtlik praks, mis annab hulgaliselt ekstrapunkte. Ülesanne on tõestada

 All ...'

2015-02-05T13:56:28Z

Uus lehekülg: ' See ülesanne on näide 2013 aastast, mida lähiajal uuendatakse 2015 aastaks. See on vabatahtlik praks, mis annab hulgaliselt ekstrapunkte. Ülesanne on tõestada <pre> All ...'

Uus lehekülg

See ülesanne on näide 2013 aastast, mida lähiajal uuendatakse 2015 aastaks.

See on vabatahtlik praks, mis annab hulgaliselt ekstrapunkte.

Ülesanne on tõestada
<pre>
All x All y Exists z All u ((m(u,x) & m(u,y)) <=> m(u,z))
</pre>
eeldades, et on defineeritud member funktsioon
<pre>
-m(X,n).
m(X,c(X,Y)).
X=Z | m(X,Y) | -m(X,c(Z,Y)).
-m(X,Y) | m(X,c(Z,Y)).
</pre>
Ja Otteri jaoks ära unusta ka lisada aksioomi
<pre>
X=X
</pre>

Tõestuse jaoks on vaja kasutada induktsiooni, st tõestada nii
induktsiooni baas
<pre>
All y Exists z All u ((m(u,n) & m(u,y)) <=> m(u,z))
</pre>
kui induktsiooni samm
<pre>
All x ((All y Exists z All u ((m(u,x) & m(u,y)) <=> m(u,z)))
=>
(All h All y1 Exists z1 All u1 ((m(u1,c(h,x)) & m(u1,y1))
<=> m(u1,z1)))
</pre>

Prax4: induktiivne tõestus 2015 - Redigeerimiste ajalugu

Tammet: Uus lehekülg: ' See ülesanne on näide 2013 aastast, mida lähiajal uuendatakse 2015 aastaks. See on vabatahtlik praks, mis annab hulgaliselt ekstrapunkte. Ülesanne on tõestada
All ...'