Prax4: induktiivne tõestus 2015

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 x All y Exists z All u ((m(u,x) & m(u,y)) <=> m(u,z))

eeldades, et on defineeritud member funktsioon

-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)).

Ja Otteri jaoks ära unusta ka lisada aksioomi

X=X

Tõestuse jaoks on vaja kasutada induktsiooni, st tõestada nii induktsiooni baas

All y Exists z All u ((m(u,n) & m(u,y)) <=> m(u,z))

kui induktsiooni samm

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)))