UWB Informatyka - Nieoficjalne Forum Studentów

::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;