Lehekülje Prax4: induktiivne tõestus 2015 lähteteksti vaatamine


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>