Proof step 21 from proof diff-01 (previous step)

Heuristic structural induction applied rule structural induction

And obtained the following new goals

• Proof step 1:

  ⊦

• Proof step 2:

  ⊦ ¬ is_throw_mode(noval)

• Proof step 3:

  ⊦ ¬ is_throw_mode(intval(i))

• Proof step 4:

  ⊦ ¬ is_throw_mode(byteval(by))

• Proof step 5:

  ⊦ ¬ is_throw_mode(shortval(sho))

• Proof step 6:

  ⊦ ¬ is_throw_mode(refval(r))

• Proof step 7:

  ⊦ ¬ is_throw_mode(boolval(boolvar))

• Proof step 8:

  ⊦ ¬ is_throw_mode(charval(jchar))

• Proof step 9:

  ⊦ ¬ is_throw_mode(longval(lo))

• Proof step 10:

  ⊦ ¬ is_throw_mode(floatval(floatvar))

• Proof step 11:

  ⊦ ¬ is_throw_mode(doubleval(doublevar))

• Proof step 12:

  ⊦ ¬ is_throw_mode(stringval(stringvar))

• Proof step 13:

  ⊦ ¬ is_throw_mode(val ++ val0)

• Proof step 14:

  ⊦ ¬ is_throw_mode(typeval(ty))

• Proof step 15:

  ⊦ ¬ is_throw_mode(initval(istate))

• Proof step 16:

  ⊦ ¬ is_throw_mode(break(lbl))

• Proof step 17:

  ⊦ ¬ is_throw_mode(continue(lbl))

• Proof step 18:

  ⊦ ¬ is_throw_mode(return(val, ty))

• Proof step 19:

  ⊦ is_throw_mode(throw(r, ty))

• Proof step 20:

  ⊦ ¬ is_break_mode(throw(r, ty))

Rule argument

Additional information

[[CONCRETESIMPRULES : ()]]