title: Proof by induction on Context Free Grammars
body: <p>So I have this problem I am working on regarding inductive proofs on Context Free Grammars. </p>
  
  <p>Given this grammar</p>
  
  <p>S-> aSb | SS | ab</p>
  
  <p>Prove using induction that no string generated by the grammar starts with <em>abb</em>.</p>
  
  <p>It's easy to see that this is in fact true, but I have some problem with how make a formal proof of it. </p>
  
  <p>I'm thinking either using course by value induction on the length of the word, or course by value induction on the length of the derivation(don't really know which one is better in this case). </p>
  
  <p>Let's use induction on the length of the derivation. </p>
  
  <p>Base case: The length of the derivation is one step, then the only possibilility is S-> ab, which clearly holds. </p>
  
  <p>Inductive hypothesis: if S=>w' with n derivations(n>0), then w' does not start with abb</p>
  
  <p>Inductive step:??</p>
  
  <p>The inductive step is where I'm having my problems, and I don't really understand what to do. </p>
  
  <p>I'm wondering if some one can explain what I'm supposed to do there?</p>
  
  <p>Thanks!</p>