UWB Informatyka - Nieoficjalne Forum Studentów

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)