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

Heuristic structural induction applied rule structural induction

And obtained the following new goals

• Proof step 1:

  ⊦

• Proof step 2:

  ⊦ ¬ is_boolvalue(noval)

• Proof step 3:

  ⊦ ¬ is_boolvalue(intval(i))

• Proof step 4:

  ⊦ ¬ is_boolvalue(byteval(by))

• Proof step 5:

  ⊦ ¬ is_boolvalue(shortval(sho))

• Proof step 6:

  ⊦ ¬ is_boolvalue(refval(r))

• Proof step 7:

  ⊦ is_boolvalue(boolval(boolvar))

• Proof step 8:

  ⊦ ¬ is_referencevalue(boolval(boolvar))

• Proof step 9:

  ⊦ ¬ is_boolvalue(charval(jchar))

• Proof step 10:

  ⊦ ¬ is_boolvalue(longval(lo))

• Proof step 11:

  ⊦ ¬ is_boolvalue(floatval(floatvar))

• Proof step 12:

  ⊦ ¬ is_boolvalue(doubleval(doublevar))

• Proof step 13:

  ⊦ ¬ is_boolvalue(stringval(stringvar))

• Proof step 14:

  ⊦ ¬ is_boolvalue(val ++ val0)

• Proof step 15:

  ⊦ ¬ is_boolvalue(typeval(ty))

• Proof step 16:

  ⊦ ¬ is_boolvalue(initval(istate))

• Proof step 17:

  ⊦ ¬ is_boolvalue(break(lbl))

• Proof step 18:

  ⊦ ¬ is_boolvalue(continue(lbl))

• Proof step 19:

  ⊦ ¬ is_boolvalue(return(val, ty))

• Proof step 20:

  ⊦ ¬ is_boolvalue(throw(r, ty))

Rule argument

Additional information

[[CONCRETESIMPRULES : ()]]