Forum studentów informatyki UWB
Master of Disaster
Mój przykład z drugiego koła:
theorem
for f being Real_Sequence st
for i being Nat holds f.i=2*i+5
for n being Nat holds Partial_Sums(f).n=(n+1)*(n+5)
proof
let f being Real_Sequence such that p0: for i being Nat holds f.i=2*i+5;
thus for n being Nat holds Partial_Sums(f).n=(n+1)*(n+5)
proof
defpred Q[Nat] means Partial_Sums(f).$1=($1+1)*($1+5);
p1: Q[0]
proof
Partial_Sums(f).0=f.0 by SERIES_1:def 1
.=2*0+5 by p0;
hence thesis;
end;
p2: for n holds Q[n] implies Q[n+1]
proof
let n;
assume a1: Q[n];
reconsider n1=n as Element of NAT by ORDINAL1:def 13;
Partial_Sums(f).(n1+1)=Partial_Sums(f).n1+f.(n+1) by SERIES_1:def 1
.=(n+1)*(n+5)+(2*(n+1)+5) by a1, p0;
hence Q[n+1];
end;
for n being Nat holds Q[n] from NAT_1: sch 2(p1,p2);
hence thesis;
end;
end;
Specjalnie dla Szpadyzora To był przykład nr 5 z listy, którą nam dziś pokazała.
EDIT:
Z pierwszego koła:
zad.1
dla każdego n P[n]
(1) P[0]
(2) P[1]
(3) P[2]
(4) dla każdego n>=2 P[n] implies P[n+1]
zad.2
dla każdego n (n^2)+1>=2*n
zad.3
dla każdego n 9|((10^n)-1)
Offline