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

Heuristic structural induction applied rule structural induction

And obtained the following new goals

• Proof step 1:

  ⊦

• Proof step 2:

  ⊦ ¬ is_integervalue(noval)

• Proof step 3:

  ⊦ is_integervalue(intval(i))

• Proof step 4:

  ⊦ ¬ is_referencevalue(intval(i))

• Proof step 5:

  ⊦ ¬ is_integervalue(byteval(by))

• Proof step 6:

  ⊦ ¬ is_integervalue(shortval(sho))

• Proof step 7:

  ⊦ ¬ is_integervalue(refval(r))

• Proof step 8:

  ⊦ ¬ is_integervalue(boolval(boolvar))

• Proof step 9:

  ⊦ ¬ is_integervalue(charval(jchar))

• Proof step 10:

  ⊦ ¬ is_integervalue(longval(lo))

• Proof step 11:

  ⊦ ¬ is_integervalue(floatval(floatvar))

• Proof step 12:

  ⊦ ¬ is_integervalue(doubleval(doublevar))

• Proof step 13:

  ⊦ ¬ is_integervalue(stringval(stringvar))

• Proof step 14:

  ⊦ ¬ is_integervalue(val ++ val0)

• Proof step 15:

  ⊦ ¬ is_integervalue(typeval(ty))

• Proof step 16:

  ⊦ ¬ is_integervalue(initval(istate))

• Proof step 17:

  ⊦ ¬ is_integervalue(break(lbl))

• Proof step 18:

  ⊦ ¬ is_integervalue(continue(lbl))

• Proof step 19:

  ⊦ ¬ is_integervalue(return(val, ty))

• Proof step 20:

  ⊦ ¬ is_integervalue(throw(r, ty))

Rule argument

Additional information

[[CONCRETESIMPRULES : ()]]