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

Heuristic structural induction applied rule structural induction

And obtained the following new goals

• Proof step 1:

  ⊦

• Proof step 2:

  ⊦ ¬ is_referencevalue(noval)

• Proof step 3:

  ⊦ ¬ is_referencevalue(intval(i))

• Proof step 4:

  ⊦ ¬ is_referencevalue(byteval(by))

• Proof step 5:

  ⊦ ¬ is_referencevalue(shortval(sho))

• Proof step 6:

  ⊦ is_referencevalue(refval(r))

• Proof step 7:

  ⊦ ¬ is_bytevalue(refval(r))

• Proof step 8:

  ⊦ ¬ is_referencevalue(boolval(boolvar))

• Proof step 9:

  ⊦ ¬ is_referencevalue(charval(jchar))

• Proof step 10:

  ⊦ ¬ is_referencevalue(longval(lo))

• Proof step 11:

  ⊦ ¬ is_referencevalue(floatval(floatvar))

• Proof step 12:

  ⊦ ¬ is_referencevalue(doubleval(doublevar))

• Proof step 13:

  ⊦ ¬ is_referencevalue(stringval(stringvar))

• Proof step 14:

  ⊦ ¬ is_referencevalue(val ++ val0)

• Proof step 15:

  ⊦ ¬ is_referencevalue(typeval(ty))

• Proof step 16:

  ⊦ ¬ is_referencevalue(initval(istate))

• Proof step 17:

  ⊦ ¬ is_referencevalue(break(lbl))

• Proof step 18:

  ⊦ ¬ is_referencevalue(continue(lbl))

• Proof step 19:

  ⊦ ¬ is_referencevalue(return(val, ty))

• Proof step 20:

  ⊦ ¬ is_referencevalue(throw(r, ty))

Rule argument

Additional information

[[CONCRETESIMPRULES : ()]]