Forum studentów informatyki UWB
Dr Hardkor
::Zadanie 5 scheme S5 {P[Nat]}: for n st n>=1 holds P[n] provided z1: P[1] and z2: for n st n>=1 holds P[n] implies P[n+1] proof defpred Q[Nat] means $1>=1 implies P[$1]; p1:Q[0]; p2:Q[k] implies Q[k+1] proof assume Q[k]; then a1: k>=1 implies P[k]; thus Q[k+1] :: musimy udowodnic k+1 >= 1 => P [k+1] proof assume (k+1)>=1; k=0 or k>0; ::z k>0 mamy, ze k>=1 then u1: k=0 or k>=0+1 by INT_1:20; per cases by u1; suppose k=0; hence P[k+1] by z1; end; suppose k>=1; hence P[k+1] by a1,z2; end; end; end; for k holds Q[k] from NAT_1:sch 2(p1,p2); hence thesis; end;
Pomimo, że dziś to tłumaczone było, to już nei pamiętam...
Darjus, a pamiętasz, jak na gmailu odpisałeś mi po co rozwiązane zadania z Mizara nam?:d
Ostatnio edytowany przez tomek_aka_marjan-_- (2009-10-29 18:06:00)
Offline
Użytkownik
To mój plik z zadaniami z mizara
http://www.speedyshare.com/files/20384302/test1.miz
Offline