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

Heuristic structural induction applied rule structural induction

And obtained the following new goals

• Proof step 1:

  ⊦

• Proof step 2:

  ⊦ ¬ is_shortvalue(noval)

• Proof step 3:

  ⊦ ¬ is_shortvalue(intval(i))

• Proof step 4:

  ⊦ ¬ is_shortvalue(byteval(by))

• Proof step 5:

  ⊦ is_shortvalue(shortval(sho))

• Proof step 6:

  ⊦ ¬ is_bytevalue(shortval(sho))

• Proof step 7:

  ⊦ ¬ is_shortvalue(refval(r))

• Proof step 8:

  ⊦ ¬ is_shortvalue(boolval(boolvar))

• Proof step 9:

  ⊦ ¬ is_shortvalue(charval(jchar))

• Proof step 10:

  ⊦ ¬ is_shortvalue(longval(lo))

• Proof step 11:

  ⊦ ¬ is_shortvalue(floatval(floatvar))

• Proof step 12:

  ⊦ ¬ is_shortvalue(doubleval(doublevar))

• Proof step 13:

  ⊦ ¬ is_shortvalue(stringval(stringvar))

• Proof step 14:

  ⊦ ¬ is_shortvalue(val ++ val0)

• Proof step 15:

  ⊦ ¬ is_shortvalue(typeval(ty))

• Proof step 16:

  ⊦ ¬ is_shortvalue(initval(istate))

• Proof step 17:

  ⊦ ¬ is_shortvalue(break(lbl))

• Proof step 18:

  ⊦ ¬ is_shortvalue(continue(lbl))

• Proof step 19:

  ⊦ ¬ is_shortvalue(return(val, ty))

• Proof step 20:

  ⊦ ¬ is_shortvalue(throw(r, ty))

Rule argument

Additional information

[[CONCRETESIMPRULES : ()]]