This is a listing of all goals defined over the current specification. Axioms are yellow, proof obligations purple and theorems green. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| disj-01 | ⊦ intval(i) ≠ refval(r) | An Axiom |
| disj-02 | ⊦ intval(i) ≠ boolval(boolvar) | An Axiom |
| disj-03 | ⊦ intval(i) ≠ val ++ val0 | An Axiom |
| disj-05 | ⊦ refval(r) ≠ boolval(boolvar) | An Axiom |
| disj-06 | ⊦ val ++ val0 ≠ throw(r, ty) | An Axiom |
| disj-08 | ⊦ refval(r) ≠ val ++ val0 | An Axiom |
| sel-01 | ⊦ (val ++ val0) .restval = val0 | An Axiom |
| sel-02 | ⊦ (val ++ val0) .firstval = val | An Axiom |
| sel-03 | ⊦ stringval(stringvar) .stringval = stringvar | An Axiom |
| sel-04 | ⊦ intval(i) .intval = i | An Axiom |
| sel-05 | ⊦ boolval(boolvar) .boolval ↔ boolvar | An Axiom |
| test-07 | ⊦ ¬ is_integervalue(val ++ val0) | An Axiom |
| test-08 | ⊦ ¬ is_valuelist(boolval(boolvar)) | An Axiom |
| test-09 | ⊦ ¬ is_valuelist(refval(r)) | An Axiom |
| test-10 | ⊦ ¬ is_valuelist(intval(i)) | An Axiom |
| test-12 | ⊦ ¬ is_throw_mode(val ++ val0) | An Axiom |
| test-13 | ⊦ is_boolvalue(boolval(boolvar)) | An Axiom |
| test-14 | ⊦ ¬ is_boolvalue(refval(r)) | An Axiom |
| test-15 | ⊦ ¬ is_boolvalue(intval(i)) | An Axiom |
| test-17 | ⊦ ¬ is_return_mode(val ++ val0) | An Axiom |
| test-18 | ⊦ ¬ is_referencevalue(boolval(boolvar)) | An Axiom |
| test-19 | ⊦ is_referencevalue(refval(r)) | An Axiom |
| test-20 | ⊦ ¬ is_referencevalue(intval(i)) | An Axiom |
| test-22 | ⊦ ¬ is_boolvalue(val ++ val0) | An Axiom |
| test-23 | ⊦ ¬ is_integervalue(boolval(boolvar)) | An Axiom |
| test-24 | ⊦ ¬ is_integervalue(refval(r)) | An Axiom |
| test-25 | ⊦ is_integervalue(intval(i)) | An Axiom |
| inj-01 | ⊦ val ++ val0 = val1 ++ val2 ↔ val = val1 ∧ val0 = val2 | An Axiom |
| inj-02 | ⊦ boolval(boolvar) = boolval(boolvar0) ↔ (boolvar ↔ boolvar0) | An Axiom |
| inj-03 | ⊦ refval(r) = refval(r0) ↔ r = r0 | An Axiom |
| inj-04 | ⊦ intval(i) = intval(i0) ↔ i = i0 | An Axiom |
| case | ⊦ val = intval(val .intval) ∨ val = byteval(val .byteval) ∨ val = shortval(val .shortval) ∨ val = refval(val .refval) ∨ val = boolval(val .boolval) ∨ val = charval(val .charval) ∨ val = longval(val .longval) ∨ val = floatval(val .floatval) ∨ val = doubleval(val .doubleval) ∨ val = stringval(val .stringval) ∨ val = val .firstval ++ val .restval ∨ val = noval ∨ val = typeval(val .type) ∨ val = initval(val .istate) ∨ val = break(val .label) ∨ val = continue(val .label) ∨ val = return(val .val, val .type) ∨ val = throw(val .refval, val .type) | An Axiom |
| ex-02 | ⊦ is_valuelist(val) ↔ (∃ val0, val1. val = val0 ++ val1) | An Axiom |
| ex-03 | ⊦ is_boolvalue(val) ↔ (∃ boolvar. val = boolval(boolvar)) | An Axiom |
| ex-04 | ⊦ is_referencevalue(val) ↔ (∃ r. val = refval(r)) | An Axiom |
| ex-05 | ⊦ is_integervalue(val) ↔ (∃ i. val = intval(i)) | An Axiom |
| elim-01 | ⊦ is_valuelist(val) → (val0 = val .firstval ∧ val1 = val .restval ↔ val = val0 ++ val1) | An Axiom |
| elim-02 | ⊦ is_integervalue(val) → (i = val .intval ↔ val = intval(i)) | An Axiom |
| elim-03 | ⊦ is_bytevalue(val) → (by = val .byteval ↔ val = byteval(by)) | An Axiom |
| elim-04 | ⊦ is_stringvalue(val) → (stringvar = val .stringval ↔ val = stringval(stringvar)) | An Axiom |
| elim-05 | ⊦ is_break_mode(val) → (lbl = val .label ↔ val = break(lbl)) | An Axiom |
| elim-06 | ⊦ is_continue_mode(val) → (lbl = val .label ↔ val = continue(lbl)) | An Axiom |
| ex-06 | ⊦ is_break_mode(val) ↔ (∃ lbl. val = break(lbl)) | An Axiom |
| ex-07 | ⊦ is_continue_mode(val) ↔ (∃ lbl. val = continue(lbl)) | An Axiom |
| inj-05 | ⊦ continue(lbl) = continue(lbl0) ↔ lbl = lbl0 | An Axiom |
| inj-06 | ⊦ break(lbl) = break(lbl0) ↔ lbl = lbl0 | An Axiom |
| test-26 | ⊦ ¬ is_integervalue(break(lbl)) | An Axiom |
| test-27 | ⊦ ¬ is_throw_mode(continue(lbl)) | An Axiom |
| test-30 | ⊦ ¬ is_integervalue(continue(lbl)) | An Axiom |
| test-31 | ⊦ ¬ is_throw_mode(break(lbl)) | An Axiom |
| test-34 | ⊦ ¬ is_referencevalue(break(lbl)) | An Axiom |
| test-35 | ⊦ ¬ is_return_mode(continue(lbl)) | An Axiom |
| test-38 | ⊦ ¬ is_referencevalue(continue(lbl)) | An Axiom |
| test-39 | ⊦ ¬ is_return_mode(break(lbl)) | An Axiom |
| test-46 | ⊦ ¬ is_break_mode(intval(i)) | An Axiom |
| test-47 | ⊦ ¬ is_break_mode(refval(r)) | An Axiom |
| test-48 | ⊦ ¬ is_break_mode(boolval(boolvar)) | An Axiom |
| test-49 | ⊦ ¬ is_continue_mode(val ++ val0) | An Axiom |
| test-51 | ⊦ ¬ is_boolvalue(continue(lbl)) | An Axiom |
| test-52 | ⊦ ¬ is_continue_mode(break(lbl)) | An Axiom |
| test-55 | ⊦ ¬ is_continue_mode(intval(i)) | An Axiom |
| test-56 | ⊦ ¬ is_continue_mode(refval(r)) | An Axiom |
| test-57 | ⊦ ¬ is_continue_mode(boolval(boolvar)) | An Axiom |
| test-58 | ⊦ is_valuelist(val ++ val0) | An Axiom |
| test-60 | ⊦ ¬ is_valuelist(break(lbl)) | An Axiom |
| test-61 | ⊦ ¬ is_break_mode(continue(lbl)) | An Axiom |
| test-64 | ⊦ ¬ is_return_mode(intval(i)) | An Axiom |
| test-65 | ⊦ ¬ is_return_mode(refval(r)) | An Axiom |
| test-66 | ⊦ ¬ is_return_mode(boolval(boolvar)) | An Axiom |
| test-67 | ⊦ ¬ is_break_mode(val ++ val0) | An Axiom |
| test-69 | ⊦ ¬ is_valuelist(continue(lbl)) | An Axiom |
| test-70 | ⊦ is_break_mode(break(lbl)) | An Axiom |
| test-73 | ⊦ ¬ is_throw_mode(intval(i)) | An Axiom |
| test-74 | ⊦ ¬ is_throw_mode(refval(r)) | An Axiom |
| test-75 | ⊦ ¬ is_throw_mode(boolval(boolvar)) | An Axiom |
| test-76 | ⊦ ¬ is_novalue(val ++ val0) | An Axiom |
| test-78 | ⊦ ¬ is_novalue(break(lbl)) | An Axiom |
| test-79 | ⊦ ¬ is_typevalue(continue(lbl)) | An Axiom |
| sel-06 | ⊦ continue(lbl) .label = lbl | An Axiom |
| sel-07 | ⊦ break(lbl) .label = lbl | An Axiom |
| disj-16 | ⊦ intval(i) ≠ continue(lbl) | An Axiom |
| disj-23 | ⊦ boolval(boolvar) ≠ val ++ val0 | An Axiom |
| disj-24 | ⊦ continue(lbl) ≠ return(val, ty) | An Axiom |
| disj-27 | ⊦ refval(r) ≠ break(lbl) | An Axiom |
| disj-28 | ⊦ break(lbl) ≠ throw(r, ty) | An Axiom |
| disj-31 | ⊦ refval(r) ≠ continue(lbl) | An Axiom |
| disj-32 | ⊦ break(lbl) ≠ return(val, ty) | An Axiom |
| disj-35 | ⊦ boolval(boolvar) ≠ break(lbl) | An Axiom |
| disj-36 | ⊦ break(lbl) ≠ continue(lbl0) | An Axiom |
| ex-01 | ⊦ is_novalue(val) ↔ val = noval | An Axiom |
| test-01 | ⊦ ¬ is_integervalue(noval) | An Axiom |
| test-02 | ⊦ ¬ is_referencevalue(noval) | An Axiom |
| test-03 | ⊦ ¬ is_boolvalue(noval) | An Axiom |
| test-04 | ⊦ ¬ is_valuelist(noval) | An Axiom |
| test-05 | ⊦ ¬ is_novalue(intval(i)) | An Axiom |
| test-06 | ⊦ ¬ is_novalue(refval(r)) | An Axiom |
| test-11 | ⊦ ¬ is_novalue(boolval(boolvar)) | An Axiom |
| test-16 | ⊦ ¬ is_referencevalue(val ++ val0) | An Axiom |
| test-21 | ⊦ is_novalue(noval) | An Axiom |
| test-42 | ⊦ ¬ is_boolvalue(break(lbl)) | An Axiom |
| test-43 | ⊦ is_continue_mode(continue(lbl)) | An Axiom |
| test-50 | ⊦ ¬ is_break_mode(noval) | An Axiom |
| test-59 | ⊦ ¬ is_continue_mode(noval) | An Axiom |
| test-68 | ⊦ ¬ is_return_mode(noval) | An Axiom |
| test-77 | ⊦ ¬ is_throw_mode(noval) | An Axiom |
| disj-09 | ⊦ intval(i) ≠ break(lbl) | An Axiom |
| disj-10 | ⊦ continue(lbl) ≠ throw(r, ty) | An Axiom |
| disj-17 | ⊦ val ++ val0 ≠ return(val1, ty) | An Axiom |
| disj-18 | ⊦ boolval(boolvar) ≠ noval | An Axiom |
| disj-19 | ⊦ refval(r) ≠ noval | An Axiom |
| disj-20 | ⊦ intval(i) ≠ noval | An Axiom |
| ex-10 | ⊦ is_typevalue(val) ↔ (∃ ty. val = typeval(ty)) | An Axiom |
| inj-09 | ⊦ typeval(ty) = typeval(ty0) ↔ ty = ty0 | An Axiom |
| test-82 | ⊦ ¬ is_integervalue(typeval(ty)) | An Axiom |
| test-83 | ⊦ ¬ is_referencevalue(typeval(ty)) | An Axiom |
| test-84 | ⊦ ¬ is_boolvalue(typeval(ty)) | An Axiom |
| test-85 | ⊦ ¬ is_valuelist(typeval(ty)) | An Axiom |
| test-86 | ⊦ ¬ is_novalue(typeval(ty)) | An Axiom |
| test-87 | ⊦ ¬ is_typevalue(intval(i)) | An Axiom |
| test-88 | ⊦ ¬ is_typevalue(refval(r)) | An Axiom |
| test-89 | ⊦ ¬ is_typevalue(boolval(boolvar)) | An Axiom |
| test-90 | ⊦ ¬ is_typevalue(val ++ val0) | An Axiom |
| test-91 | ⊦ ¬ is_typevalue(noval) | An Axiom |
| test-92 | ⊦ is_typevalue(typeval(ty)) | An Axiom |
| test-93 | ⊦ ¬ is_novalue(continue(lbl)) | An Axiom |
| test-94 | ⊦ ¬ is_typevalue(break(lbl)) | An Axiom |
| test-97 | ⊦ ¬ is_break_mode(typeval(ty)) | An Axiom |
| test-98 | ⊦ ¬ is_continue_mode(typeval(ty)) | An Axiom |
| test-99 | ⊦ ¬ is_return_mode(typeval(ty)) | An Axiom |
| test-100 | ⊦ ¬ is_throw_mode(typeval(ty)) | An Axiom |
| disj-39 | ⊦ boolval(boolvar) ≠ continue(lbl) | An Axiom |
| disj-40 | ⊦ typeval(ty) ≠ continue(lbl) | An Axiom |
| disj-41 | ⊦ noval ≠ typeval(ty) | An Axiom |
| disj-42 | ⊦ val ++ val0 ≠ noval | An Axiom |
| disj-43 | ⊦ boolval(boolvar) ≠ typeval(ty) | An Axiom |
| disj-44 | ⊦ refval(r) ≠ typeval(ty) | An Axiom |
| disj-45 | ⊦ intval(i) ≠ typeval(ty) | An Axiom |
| gen | An Axiom | |
| elim-10 | ⊦ is_typevalue(val) → (ty = val .type ↔ val = typeval(ty)) | An Axiom |
| elim-11 | ⊦ is_return_mode(val) → (val0 = val .val ∧ ty = val .type ↔ val = return(val0, ty)) | An Axiom |
| elim-12 | ⊦ is_throw_mode(val) → (r = val .refval ∧ ty = val .type ↔ val = throw(r, ty)) | An Axiom |
| ex-11 | ⊦ is_return_mode(val) ↔ (∃ val0, ty. val = return(val0, ty)) | An Axiom |
| ex-12 | ⊦ is_throw_mode(val) ↔ (∃ r, ty. val = throw(r, ty)) | An Axiom |
| inj-10 | ⊦ return(val, ty) = return(val0, ty0) ↔ val = val0 ∧ ty = ty0 | An Axiom |
| inj-11 | ⊦ throw(r, ty) = throw(r0, ty0) ↔ r = r0 ∧ ty = ty0 | An Axiom |
| test-101 | ⊦ ¬ is_integervalue(return(val, ty)) | An Axiom |
| test-102 | ⊦ ¬ is_integervalue(throw(r, ty)) | An Axiom |
| test-103 | ⊦ ¬ is_referencevalue(return(val, ty)) | An Axiom |
| test-104 | ⊦ ¬ is_referencevalue(throw(r, ty)) | An Axiom |
| test-105 | ⊦ ¬ is_boolvalue(return(val, ty)) | An Axiom |
| test-106 | ⊦ ¬ is_boolvalue(throw(r, ty)) | An Axiom |
| test-107 | ⊦ ¬ is_valuelist(return(val, ty)) | An Axiom |
| test-108 | ⊦ ¬ is_valuelist(throw(r, ty)) | An Axiom |
| test-109 | ⊦ ¬ is_novalue(return(val, ty)) | An Axiom |
| test-110 | ⊦ ¬ is_novalue(throw(r, ty)) | An Axiom |
| test-111 | ⊦ ¬ is_typevalue(return(val, ty)) | An Axiom |
| test-112 | ⊦ ¬ is_typevalue(throw(r, ty)) | An Axiom |
| test-113 | ⊦ ¬ is_break_mode(return(val, ty)) | An Axiom |
| test-114 | ⊦ ¬ is_break_mode(throw(r, ty)) | An Axiom |
| test-115 | ⊦ ¬ is_continue_mode(return(val, ty)) | An Axiom |
| test-116 | ⊦ ¬ is_continue_mode(throw(r, ty)) | An Axiom |
| test-117 | ⊦ is_return_mode(return(val, ty)) | An Axiom |
| test-118 | ⊦ ¬ is_return_mode(throw(r, ty)) | An Axiom |
| test-119 | ⊦ ¬ is_throw_mode(return(val, ty)) | An Axiom |
| test-120 | ⊦ is_throw_mode(throw(r, ty)) | An Axiom |
| sel-11 | ⊦ typeval(ty) .type = ty | An Axiom |
| sel-12 | ⊦ return(val, ty) .val = val | An Axiom |
| sel-13 | ⊦ return(val, ty) .type = ty | An Axiom |
| sel-14 | ⊦ throw(r, ty) .refval = r | An Axiom |
| sel-15 | ⊦ throw(r, ty) .type = ty | An Axiom |
| disj-46 | ⊦ return(val, ty) ≠ throw(r, ty0) | An Axiom |
| disj-47 | ⊦ val ++ val0 ≠ break(lbl) | An Axiom |
| disj-48 | ⊦ typeval(ty) ≠ break(lbl) | An Axiom |
| disj-49 | ⊦ val ++ val0 ≠ continue(lbl) | An Axiom |
| disj-50 | ⊦ noval ≠ continue(lbl) | An Axiom |
| disj-51 | ⊦ typeval(ty) ≠ throw(r, ty0) | An Axiom |
| disj-52 | ⊦ typeval(ty) ≠ return(val, ty0) | An Axiom |
| disj-53 | ⊦ noval ≠ throw(r, ty) | An Axiom |
| disj-54 | ⊦ noval ≠ return(val, ty) | An Axiom |
| disj-55 | ⊦ noval ≠ break(lbl) | An Axiom |
| disj-56 | ⊦ val ++ val0 ≠ typeval(ty) | An Axiom |
| disj-57 | ⊦ boolval(boolvar) ≠ throw(r, ty) | An Axiom |
| disj-58 | ⊦ boolval(boolvar) ≠ return(val, ty) | An Axiom |
| disj-59 | ⊦ refval(r) ≠ throw(r0, ty) | An Axiom |
| disj-60 | ⊦ refval(r) ≠ return(val, ty) | An Axiom |
| disj-61 | ⊦ intval(i) ≠ throw(r, ty) | An Axiom |
| disj-62 | ⊦ intval(i) ≠ return(val, ty) | An Axiom |
| elim-07 | ⊦ is_shortvalue(val) → (sho = val .shortval ↔ val = shortval(sho)) | An Axiom |
| elim-08 | ⊦ is_boolvalue(val) → ((boolvar ↔ val .boolval) ↔ val = boolval(boolvar)) | An Axiom |
| elim-09 | ⊦ is_initvalue(val) → (istate = val .istate ↔ val = initval(istate)) | An Axiom |
| ex-08 | ⊦ is_bytevalue(val) ↔ (∃ by. val = byteval(by)) | An Axiom |
| ex-09 | ⊦ is_shortvalue(val) ↔ (∃ sho. val = shortval(sho)) | An Axiom |
| ex-13 | ⊦ is_initvalue(val) ↔ (∃ istate. val = initval(istate)) | An Axiom |
| inj-07 | ⊦ byteval(by) = byteval(by0) ↔ by = by0 | An Axiom |
| inj-08 | ⊦ shortval(sho) = shortval(sho0) ↔ sho = sho0 | An Axiom |
| inj-12 | ⊦ initval(istate) = initval(istate0) ↔ istate = istate0 | An Axiom |
| test-28 | ⊦ ¬ is_integervalue(byteval(by)) | An Axiom |
| test-29 | ⊦ ¬ is_integervalue(shortval(sho)) | An Axiom |
| test-32 | ⊦ ¬ is_integervalue(initval(istate)) | An Axiom |
| test-33 | ⊦ ¬ is_bytevalue(intval(i)) | An Axiom |
| test-36 | ⊦ is_bytevalue(byteval(by)) | An Axiom |
| test-37 | ⊦ ¬ is_bytevalue(shortval(sho)) | An Axiom |
| test-40 | ⊦ ¬ is_bytevalue(refval(r)) | An Axiom |
| test-41 | ⊦ ¬ is_bytevalue(boolval(boolvar)) | An Axiom |
| test-44 | ⊦ ¬ is_bytevalue(val ++ val0) | An Axiom |
| test-45 | ⊦ ¬ is_bytevalue(noval) | An Axiom |
| test-53 | ⊦ ¬ is_bytevalue(typeval(ty)) | An Axiom |
| test-54 | ⊦ ¬ is_bytevalue(initval(istate)) | An Axiom |
| test-62 | ⊦ ¬ is_bytevalue(break(lbl)) | An Axiom |
| test-63 | ⊦ ¬ is_bytevalue(continue(lbl)) | An Axiom |
| test-71 | ⊦ ¬ is_bytevalue(return(val, ty)) | An Axiom |
| test-72 | ⊦ ¬ is_bytevalue(throw(r, ty)) | An Axiom |
| test-80 | ⊦ ¬ is_shortvalue(intval(i)) | An Axiom |
| test-81 | ⊦ ¬ is_shortvalue(byteval(by)) | An Axiom |
| test-95 | ⊦ is_shortvalue(shortval(sho)) | An Axiom |
| test-96 | ⊦ ¬ is_shortvalue(refval(r)) | An Axiom |
| test-121 | ⊦ ¬ is_shortvalue(boolval(boolvar)) | An Axiom |
| test-122 | ⊦ ¬ is_shortvalue(val ++ val0) | An Axiom |
| test-123 | ⊦ ¬ is_shortvalue(noval) | An Axiom |
| test-124 | ⊦ ¬ is_shortvalue(typeval(ty)) | An Axiom |
| test-125 | ⊦ ¬ is_shortvalue(initval(istate)) | An Axiom |
| test-126 | ⊦ ¬ is_shortvalue(break(lbl)) | An Axiom |
| test-127 | ⊦ ¬ is_shortvalue(continue(lbl)) | An Axiom |
| test-128 | ⊦ ¬ is_shortvalue(return(val, ty)) | An Axiom |
| test-129 | ⊦ ¬ is_shortvalue(throw(r, ty)) | An Axiom |
| test-130 | ⊦ ¬ is_referencevalue(byteval(by)) | An Axiom |
| test-131 | ⊦ ¬ is_referencevalue(shortval(sho)) | An Axiom |
| test-132 | ⊦ ¬ is_referencevalue(initval(istate)) | An Axiom |
| test-133 | ⊦ ¬ is_boolvalue(byteval(by)) | An Axiom |
| test-134 | ⊦ ¬ is_boolvalue(shortval(sho)) | An Axiom |
| test-135 | ⊦ ¬ is_boolvalue(initval(istate)) | An Axiom |
| test-136 | ⊦ ¬ is_valuelist(byteval(by)) | An Axiom |
| test-137 | ⊦ ¬ is_valuelist(shortval(sho)) | An Axiom |
| test-138 | ⊦ ¬ is_valuelist(initval(istate)) | An Axiom |
| test-139 | ⊦ ¬ is_novalue(byteval(by)) | An Axiom |
| test-140 | ⊦ ¬ is_novalue(shortval(sho)) | An Axiom |
| test-141 | ⊦ ¬ is_novalue(initval(istate)) | An Axiom |
| test-142 | ⊦ ¬ is_typevalue(byteval(by)) | An Axiom |
| test-143 | ⊦ ¬ is_typevalue(shortval(sho)) | An Axiom |
| test-144 | ⊦ ¬ is_typevalue(initval(istate)) | An Axiom |
| test-145 | ⊦ ¬ is_initvalue(intval(i)) | An Axiom |
| test-146 | ⊦ ¬ is_initvalue(byteval(by)) | An Axiom |
| test-147 | ⊦ ¬ is_initvalue(shortval(sho)) | An Axiom |
| test-148 | ⊦ ¬ is_initvalue(refval(r)) | An Axiom |
| test-149 | ⊦ ¬ is_initvalue(boolval(boolvar)) | An Axiom |
| test-150 | ⊦ ¬ is_initvalue(val ++ val0) | An Axiom |
| test-151 | ⊦ ¬ is_initvalue(noval) | An Axiom |
| test-152 | ⊦ ¬ is_initvalue(typeval(ty)) | An Axiom |
| test-153 | ⊦ is_initvalue(initval(istate)) | An Axiom |
| test-154 | ⊦ ¬ is_initvalue(break(lbl)) | An Axiom |
| test-155 | ⊦ ¬ is_initvalue(continue(lbl)) | An Axiom |
| test-156 | ⊦ ¬ is_initvalue(return(val, ty)) | An Axiom |
| test-157 | ⊦ ¬ is_initvalue(throw(r, ty)) | An Axiom |
| test-158 | ⊦ ¬ is_break_mode(byteval(by)) | An Axiom |
| test-159 | ⊦ ¬ is_break_mode(shortval(sho)) | An Axiom |
| test-160 | ⊦ ¬ is_break_mode(initval(istate)) | An Axiom |
| test-161 | ⊦ ¬ is_continue_mode(byteval(by)) | An Axiom |
| test-162 | ⊦ ¬ is_continue_mode(shortval(sho)) | An Axiom |
| test-163 | ⊦ ¬ is_continue_mode(initval(istate)) | An Axiom |
| test-164 | ⊦ ¬ is_return_mode(byteval(by)) | An Axiom |
| test-165 | ⊦ ¬ is_return_mode(shortval(sho)) | An Axiom |
| test-166 | ⊦ ¬ is_return_mode(initval(istate)) | An Axiom |
| test-167 | ⊦ ¬ is_throw_mode(byteval(by)) | An Axiom |
| test-168 | ⊦ ¬ is_throw_mode(shortval(sho)) | An Axiom |
| test-169 | ⊦ ¬ is_throw_mode(initval(istate)) | An Axiom |
| sel-08 | ⊦ byteval(by) .byteval = by | An Axiom |
| sel-09 | ⊦ refval(r) .refval = r | An Axiom |
| sel-10 | ⊦ initval(istate) .istate = istate | An Axiom |
| disj-04 | ⊦ initval(istate) ≠ throw(r, ty) | An Axiom |
| disj-07 | ⊦ initval(istate) ≠ return(val, ty) | An Axiom |
| disj-11 | ⊦ initval(istate) ≠ continue(lbl) | An Axiom |
| disj-12 | ⊦ initval(istate) ≠ break(lbl) | An Axiom |
| disj-13 | ⊦ typeval(ty) ≠ initval(istate) | An Axiom |
| disj-14 | ⊦ noval ≠ initval(istate) | An Axiom |
| disj-15 | ⊦ val ++ val0 ≠ initval(istate) | An Axiom |
| disj-21 | ⊦ boolval(boolvar) ≠ initval(istate) | An Axiom |
| disj-22 | ⊦ refval(r) ≠ initval(istate) | An Axiom |
| disj-25 | ⊦ shortval(sho) ≠ throw(r, ty) | An Axiom |
| disj-26 | ⊦ shortval(sho) ≠ return(val, ty) | An Axiom |
| disj-29 | ⊦ shortval(sho) ≠ continue(lbl) | An Axiom |
| disj-30 | ⊦ shortval(sho) ≠ break(lbl) | An Axiom |
| disj-33 | ⊦ shortval(sho) ≠ initval(istate) | An Axiom |
| disj-34 | ⊦ shortval(sho) ≠ typeval(ty) | An Axiom |
| disj-37 | ⊦ shortval(sho) ≠ noval | An Axiom |
| disj-38 | ⊦ shortval(sho) ≠ val ++ val0 | An Axiom |
| disj-63 | ⊦ shortval(sho) ≠ boolval(boolvar) | An Axiom |
| disj-64 | ⊦ shortval(sho) ≠ refval(r) | An Axiom |
| disj-65 | ⊦ byteval(by) ≠ throw(r, ty) | An Axiom |
| disj-66 | ⊦ byteval(by) ≠ return(val, ty) | An Axiom |
| disj-67 | ⊦ byteval(by) ≠ continue(lbl) | An Axiom |
| disj-68 | ⊦ byteval(by) ≠ break(lbl) | An Axiom |
| disj-69 | ⊦ byteval(by) ≠ initval(istate) | An Axiom |
| disj-70 | ⊦ byteval(by) ≠ typeval(ty) | An Axiom |
| disj-71 | ⊦ byteval(by) ≠ noval | An Axiom |
| disj-72 | ⊦ byteval(by) ≠ val ++ val0 | An Axiom |
| disj-73 | ⊦ byteval(by) ≠ boolval(boolvar) | An Axiom |
| disj-74 | ⊦ byteval(by) ≠ refval(r) | An Axiom |
| disj-75 | ⊦ byteval(by) ≠ shortval(sho) | An Axiom |
| disj-76 | ⊦ intval(i) ≠ initval(istate) | An Axiom |
| disj-77 | ⊦ intval(i) ≠ shortval(sho) | An Axiom |
| disj-78 | ⊦ intval(i) ≠ byteval(by) | An Axiom |
| elim-13 | ⊦ is_referencevalue(val) → (r = val .refval ↔ val = refval(r)) | An Axiom |
| ex-14 | ⊦ is_stringvalue(val) ↔ (∃ stringvar. val = stringval(stringvar)) | An Axiom |
| inj-13 | ⊦ stringval(stringvar) = stringval(stringvar0) ↔ stringvar = stringvar0 | An Axiom |
| test-170 | ⊦ ¬ is_integervalue(stringval(stringvar)) | An Axiom |
| test-171 | ⊦ ¬ is_bytevalue(stringval(stringvar)) | An Axiom |
| test-172 | ⊦ ¬ is_shortvalue(stringval(stringvar)) | An Axiom |
| test-173 | ⊦ ¬ is_referencevalue(stringval(stringvar)) | An Axiom |
| test-174 | ⊦ ¬ is_boolvalue(stringval(stringvar)) | An Axiom |
| test-175 | ⊦ ¬ is_stringvalue(intval(i)) | An Axiom |
| test-176 | ⊦ ¬ is_stringvalue(byteval(by)) | An Axiom |
| test-177 | ⊦ ¬ is_stringvalue(shortval(sho)) | An Axiom |
| test-178 | ⊦ ¬ is_stringvalue(refval(r)) | An Axiom |
| test-179 | ⊦ ¬ is_stringvalue(boolval(boolvar)) | An Axiom |
| test-180 | ⊦ is_stringvalue(stringval(stringvar)) | An Axiom |
| test-181 | ⊦ ¬ is_stringvalue(val ++ val0) | An Axiom |
| test-182 | ⊦ ¬ is_stringvalue(noval) | An Axiom |
| test-183 | ⊦ ¬ is_stringvalue(typeval(ty)) | An Axiom |
| test-184 | ⊦ ¬ is_stringvalue(initval(istate)) | An Axiom |
| test-185 | ⊦ ¬ is_stringvalue(break(lbl)) | An Axiom |
| test-186 | ⊦ ¬ is_stringvalue(continue(lbl)) | An Axiom |
| test-187 | ⊦ ¬ is_stringvalue(return(val, ty)) | An Axiom |
| test-188 | ⊦ ¬ is_stringvalue(throw(r, ty)) | An Axiom |
| test-189 | ⊦ ¬ is_valuelist(stringval(stringvar)) | An Axiom |
| test-190 | ⊦ ¬ is_novalue(stringval(stringvar)) | An Axiom |
| test-191 | ⊦ ¬ is_typevalue(stringval(stringvar)) | An Axiom |
| test-192 | ⊦ ¬ is_initvalue(stringval(stringvar)) | An Axiom |
| test-193 | ⊦ ¬ is_break_mode(stringval(stringvar)) | An Axiom |
| test-194 | ⊦ ¬ is_continue_mode(stringval(stringvar)) | An Axiom |
| test-195 | ⊦ ¬ is_return_mode(stringval(stringvar)) | An Axiom |
| test-196 | ⊦ ¬ is_throw_mode(stringval(stringvar)) | An Axiom |
| sel-16 | ⊦ shortval(sho) .shortval = sho | An Axiom |
| disj-79 | ⊦ stringval(stringvar) ≠ throw(r, ty) | An Axiom |
| disj-80 | ⊦ stringval(stringvar) ≠ return(val, ty) | An Axiom |
| disj-81 | ⊦ stringval(stringvar) ≠ continue(lbl) | An Axiom |
| disj-82 | ⊦ stringval(stringvar) ≠ break(lbl) | An Axiom |
| disj-83 | ⊦ stringval(stringvar) ≠ initval(istate) | An Axiom |
| disj-84 | ⊦ stringval(stringvar) ≠ typeval(ty) | An Axiom |
| disj-85 | ⊦ stringval(stringvar) ≠ noval | An Axiom |
| disj-86 | ⊦ stringval(stringvar) ≠ val ++ val0 | An Axiom |
| disj-87 | ⊦ boolval(boolvar) ≠ stringval(stringvar) | An Axiom |
| disj-88 | ⊦ refval(r) ≠ stringval(stringvar) | An Axiom |
| disj-89 | ⊦ shortval(sho) ≠ stringval(stringvar) | An Axiom |
| disj-90 | ⊦ byteval(by) ≠ stringval(stringvar) | An Axiom |
| disj-91 | ⊦ intval(i) ≠ stringval(stringvar) | An Axiom |
| elim-14 | ⊦ is_longvalue(val) → (lo = val .longval ↔ val = longval(lo)) | An Axiom |
| elim-15 | ⊦ is_floatvalue(val) → (floatvar = val .floatval ↔ val = floatval(floatvar)) | An Axiom |
| elim-16 | ⊦ is_doublevalue(val) → (doublevar = val .doubleval ↔ val = doubleval(doublevar)) | An Axiom |
| ex-15 | ⊦ is_longvalue(val) ↔ (∃ lo. val = longval(lo)) | An Axiom |
| ex-16 | ⊦ is_floatvalue(val) ↔ (∃ floatvar. val = floatval(floatvar)) | An Axiom |
| ex-17 | ⊦ is_doublevalue(val) ↔ (∃ doublevar. val = doubleval(doublevar)) | An Axiom |
| inj-14 | ⊦ longval(lo) = longval(lo0) ↔ lo = lo0 | An Axiom |
| inj-15 | ⊦ floatval(floatvar) = floatval(floatvar0) ↔ floatvar = floatvar0 | An Axiom |
| inj-16 | ⊦ doubleval(doublevar) = doubleval(doublevar0) ↔ doublevar = doublevar0 | An Axiom |
| test-197 | ⊦ ¬ is_integervalue(longval(lo)) | An Axiom |
| test-198 | ⊦ ¬ is_integervalue(floatval(floatvar)) | An Axiom |
| test-199 | ⊦ ¬ is_integervalue(doubleval(doublevar)) | An Axiom |
| test-200 | ⊦ ¬ is_bytevalue(longval(lo)) | An Axiom |
| test-201 | ⊦ ¬ is_bytevalue(floatval(floatvar)) | An Axiom |
| test-202 | ⊦ ¬ is_bytevalue(doubleval(doublevar)) | An Axiom |
| test-203 | ⊦ ¬ is_shortvalue(longval(lo)) | An Axiom |
| test-204 | ⊦ ¬ is_shortvalue(floatval(floatvar)) | An Axiom |
| test-205 | ⊦ ¬ is_shortvalue(doubleval(doublevar)) | An Axiom |
| test-206 | ⊦ ¬ is_referencevalue(longval(lo)) | An Axiom |
| test-207 | ⊦ ¬ is_referencevalue(floatval(floatvar)) | An Axiom |
| test-208 | ⊦ ¬ is_referencevalue(doubleval(doublevar)) | An Axiom |
| test-209 | ⊦ ¬ is_boolvalue(longval(lo)) | An Axiom |
| test-210 | ⊦ ¬ is_boolvalue(floatval(floatvar)) | An Axiom |
| test-211 | ⊦ ¬ is_boolvalue(doubleval(doublevar)) | An Axiom |
| test-212 | ⊦ ¬ is_longvalue(intval(i)) | An Axiom |
| test-213 | ⊦ ¬ is_longvalue(byteval(by)) | An Axiom |
| test-214 | ⊦ ¬ is_longvalue(shortval(sho)) | An Axiom |
| test-215 | ⊦ ¬ is_longvalue(refval(r)) | An Axiom |
| test-216 | ⊦ ¬ is_longvalue(boolval(boolvar)) | An Axiom |
| test-217 | ⊦ is_longvalue(longval(lo)) | An Axiom |
| test-218 | ⊦ ¬ is_longvalue(floatval(floatvar)) | An Axiom |
| test-219 | ⊦ ¬ is_longvalue(doubleval(doublevar)) | An Axiom |
| test-220 | ⊦ ¬ is_longvalue(stringval(stringvar)) | An Axiom |
| test-221 | ⊦ ¬ is_longvalue(val ++ val0) | An Axiom |
| test-222 | ⊦ ¬ is_longvalue(noval) | An Axiom |
| test-223 | ⊦ ¬ is_longvalue(typeval(ty)) | An Axiom |
| test-224 | ⊦ ¬ is_longvalue(initval(istate)) | An Axiom |
| test-225 | ⊦ ¬ is_longvalue(break(lbl)) | An Axiom |
| test-226 | ⊦ ¬ is_longvalue(continue(lbl)) | An Axiom |
| test-227 | ⊦ ¬ is_longvalue(return(val, ty)) | An Axiom |
| test-228 | ⊦ ¬ is_longvalue(throw(r, ty)) | An Axiom |
| test-229 | ⊦ ¬ is_floatvalue(intval(i)) | An Axiom |
| test-230 | ⊦ ¬ is_floatvalue(byteval(by)) | An Axiom |
| test-231 | ⊦ ¬ is_floatvalue(shortval(sho)) | An Axiom |
| test-232 | ⊦ ¬ is_floatvalue(refval(r)) | An Axiom |
| test-233 | ⊦ ¬ is_floatvalue(boolval(boolvar)) | An Axiom |
| test-234 | ⊦ ¬ is_floatvalue(longval(lo)) | An Axiom |
| test-235 | ⊦ is_floatvalue(floatval(floatvar)) | An Axiom |
| test-236 | ⊦ ¬ is_floatvalue(doubleval(doublevar)) | An Axiom |
| test-237 | ⊦ ¬ is_floatvalue(stringval(stringvar)) | An Axiom |
| test-238 | ⊦ ¬ is_floatvalue(val ++ val0) | An Axiom |
| test-239 | ⊦ ¬ is_floatvalue(noval) | An Axiom |
| test-240 | ⊦ ¬ is_floatvalue(typeval(ty)) | An Axiom |
| test-241 | ⊦ ¬ is_floatvalue(initval(istate)) | An Axiom |
| test-242 | ⊦ ¬ is_floatvalue(break(lbl)) | An Axiom |
| test-243 | ⊦ ¬ is_floatvalue(continue(lbl)) | An Axiom |
| test-244 | ⊦ ¬ is_floatvalue(return(val, ty)) | An Axiom |
| test-245 | ⊦ ¬ is_floatvalue(throw(r, ty)) | An Axiom |
| test-246 | ⊦ ¬ is_doublevalue(intval(i)) | An Axiom |
| test-247 | ⊦ ¬ is_doublevalue(byteval(by)) | An Axiom |
| test-248 | ⊦ ¬ is_doublevalue(shortval(sho)) | An Axiom |
| test-249 | ⊦ ¬ is_doublevalue(refval(r)) | An Axiom |
| test-250 | ⊦ ¬ is_doublevalue(boolval(boolvar)) | An Axiom |
| test-251 | ⊦ ¬ is_doublevalue(longval(lo)) | An Axiom |
| test-252 | ⊦ ¬ is_doublevalue(floatval(floatvar)) | An Axiom |
| test-253 | ⊦ is_doublevalue(doubleval(doublevar)) | An Axiom |
| test-254 | ⊦ ¬ is_doublevalue(stringval(stringvar)) | An Axiom |
| test-255 | ⊦ ¬ is_doublevalue(val ++ val0) | An Axiom |
| test-256 | ⊦ ¬ is_doublevalue(noval) | An Axiom |
| test-257 | ⊦ ¬ is_doublevalue(typeval(ty)) | An Axiom |
| test-258 | ⊦ ¬ is_doublevalue(initval(istate)) | An Axiom |
| test-259 | ⊦ ¬ is_doublevalue(break(lbl)) | An Axiom |
| test-260 | ⊦ ¬ is_doublevalue(continue(lbl)) | An Axiom |
| test-261 | ⊦ ¬ is_doublevalue(return(val, ty)) | An Axiom |
| test-262 | ⊦ ¬ is_doublevalue(throw(r, ty)) | An Axiom |
| test-263 | ⊦ ¬ is_stringvalue(longval(lo)) | An Axiom |
| test-264 | ⊦ ¬ is_stringvalue(floatval(floatvar)) | An Axiom |
| test-265 | ⊦ ¬ is_stringvalue(doubleval(doublevar)) | An Axiom |
| test-266 | ⊦ ¬ is_valuelist(longval(lo)) | An Axiom |
| test-267 | ⊦ ¬ is_valuelist(floatval(floatvar)) | An Axiom |
| test-268 | ⊦ ¬ is_valuelist(doubleval(doublevar)) | An Axiom |
| test-269 | ⊦ ¬ is_novalue(longval(lo)) | An Axiom |
| test-270 | ⊦ ¬ is_novalue(floatval(floatvar)) | An Axiom |
| test-271 | ⊦ ¬ is_novalue(doubleval(doublevar)) | An Axiom |
| test-272 | ⊦ ¬ is_typevalue(longval(lo)) | An Axiom |
| test-273 | ⊦ ¬ is_typevalue(floatval(floatvar)) | An Axiom |
| test-274 | ⊦ ¬ is_typevalue(doubleval(doublevar)) | An Axiom |
| test-275 | ⊦ ¬ is_initvalue(longval(lo)) | An Axiom |
| test-276 | ⊦ ¬ is_initvalue(floatval(floatvar)) | An Axiom |
| test-277 | ⊦ ¬ is_initvalue(doubleval(doublevar)) | An Axiom |
| test-278 | ⊦ ¬ is_break_mode(longval(lo)) | An Axiom |
| test-279 | ⊦ ¬ is_break_mode(floatval(floatvar)) | An Axiom |
| test-280 | ⊦ ¬ is_break_mode(doubleval(doublevar)) | An Axiom |
| test-281 | ⊦ ¬ is_continue_mode(longval(lo)) | An Axiom |
| test-282 | ⊦ ¬ is_continue_mode(floatval(floatvar)) | An Axiom |
| test-283 | ⊦ ¬ is_continue_mode(doubleval(doublevar)) | An Axiom |
| test-284 | ⊦ ¬ is_return_mode(longval(lo)) | An Axiom |
| test-285 | ⊦ ¬ is_return_mode(floatval(floatvar)) | An Axiom |
| test-286 | ⊦ ¬ is_return_mode(doubleval(doublevar)) | An Axiom |
| test-287 | ⊦ ¬ is_throw_mode(longval(lo)) | An Axiom |
| test-288 | ⊦ ¬ is_throw_mode(floatval(floatvar)) | An Axiom |
| test-289 | ⊦ ¬ is_throw_mode(doubleval(doublevar)) | An Axiom |
| sel-17 | ⊦ longval(lo) .longval = lo | An Axiom |
| sel-18 | ⊦ floatval(floatvar) .floatval = floatvar | An Axiom |
| sel-19 | ⊦ doubleval(doublevar) .doubleval = doublevar | An Axiom |
| disj-92 | ⊦ doubleval(doublevar) ≠ throw(r, ty) | An Axiom |
| disj-93 | ⊦ doubleval(doublevar) ≠ return(val, ty) | An Axiom |
| disj-94 | ⊦ doubleval(doublevar) ≠ continue(lbl) | An Axiom |
| disj-95 | ⊦ doubleval(doublevar) ≠ break(lbl) | An Axiom |
| disj-96 | ⊦ doubleval(doublevar) ≠ initval(istate) | An Axiom |
| disj-97 | ⊦ doubleval(doublevar) ≠ typeval(ty) | An Axiom |
| disj-98 | ⊦ doubleval(doublevar) ≠ noval | An Axiom |
| disj-99 | ⊦ doubleval(doublevar) ≠ val ++ val0 | An Axiom |
| disj-100 | ⊦ doubleval(doublevar) ≠ stringval(stringvar) | An Axiom |
| disj-101 | ⊦ floatval(floatvar) ≠ throw(r, ty) | An Axiom |
| disj-102 | ⊦ floatval(floatvar) ≠ return(val, ty) | An Axiom |
| disj-103 | ⊦ floatval(floatvar) ≠ continue(lbl) | An Axiom |
| disj-104 | ⊦ floatval(floatvar) ≠ break(lbl) | An Axiom |
| disj-105 | ⊦ floatval(floatvar) ≠ initval(istate) | An Axiom |
| disj-106 | ⊦ floatval(floatvar) ≠ typeval(ty) | An Axiom |
| disj-107 | ⊦ floatval(floatvar) ≠ noval | An Axiom |
| disj-108 | ⊦ floatval(floatvar) ≠ val ++ val0 | An Axiom |
| disj-109 | ⊦ floatval(floatvar) ≠ stringval(stringvar) | An Axiom |
| disj-110 | ⊦ floatval(floatvar) ≠ doubleval(doublevar) | An Axiom |
| disj-111 | ⊦ longval(lo) ≠ throw(r, ty) | An Axiom |
| disj-112 | ⊦ longval(lo) ≠ return(val, ty) | An Axiom |
| disj-113 | ⊦ longval(lo) ≠ continue(lbl) | An Axiom |
| disj-114 | ⊦ longval(lo) ≠ break(lbl) | An Axiom |
| disj-115 | ⊦ longval(lo) ≠ initval(istate) | An Axiom |
| disj-116 | ⊦ longval(lo) ≠ typeval(ty) | An Axiom |
| disj-117 | ⊦ longval(lo) ≠ noval | An Axiom |
| disj-118 | ⊦ longval(lo) ≠ val ++ val0 | An Axiom |
| disj-119 | ⊦ longval(lo) ≠ stringval(stringvar) | An Axiom |
| disj-120 | ⊦ longval(lo) ≠ doubleval(doublevar) | An Axiom |
| disj-121 | ⊦ longval(lo) ≠ floatval(floatvar) | An Axiom |
| disj-122 | ⊦ boolval(boolvar) ≠ doubleval(doublevar) | An Axiom |
| disj-123 | ⊦ boolval(boolvar) ≠ floatval(floatvar) | An Axiom |
| disj-124 | ⊦ boolval(boolvar) ≠ longval(lo) | An Axiom |
| disj-125 | ⊦ refval(r) ≠ doubleval(doublevar) | An Axiom |
| disj-126 | ⊦ refval(r) ≠ floatval(floatvar) | An Axiom |
| disj-127 | ⊦ refval(r) ≠ longval(lo) | An Axiom |
| disj-128 | ⊦ shortval(sho) ≠ doubleval(doublevar) | An Axiom |
| disj-129 | ⊦ shortval(sho) ≠ floatval(floatvar) | An Axiom |
| disj-130 | ⊦ shortval(sho) ≠ longval(lo) | An Axiom |
| disj-131 | ⊦ byteval(by) ≠ doubleval(doublevar) | An Axiom |
| disj-132 | ⊦ byteval(by) ≠ floatval(floatvar) | An Axiom |
| disj-133 | ⊦ byteval(by) ≠ longval(lo) | An Axiom |
| disj-134 | ⊦ intval(i) ≠ doubleval(doublevar) | An Axiom |
| disj-135 | ⊦ intval(i) ≠ floatval(floatvar) | An Axiom |
| disj-136 | ⊦ intval(i) ≠ longval(lo) | An Axiom |
| elim-17 | ⊦ is_charvalue(val) → (jchar = val .charval ↔ val = charval(jchar)) | An Axiom |
| ex-18 | ⊦ is_charvalue(val) ↔ (∃ jchar. val = charval(jchar)) | An Axiom |
| inj-17 | ⊦ charval(jchar) = charval(jchar0) ↔ jchar = jchar0 | An Axiom |
| test-290 | ⊦ ¬ is_integervalue(charval(jchar)) | An Axiom |
| test-291 | ⊦ ¬ is_bytevalue(charval(jchar)) | An Axiom |
| test-292 | ⊦ ¬ is_shortvalue(charval(jchar)) | An Axiom |
| test-293 | ⊦ ¬ is_referencevalue(charval(jchar)) | An Axiom |
| test-294 | ⊦ ¬ is_boolvalue(charval(jchar)) | An Axiom |
| test-295 | ⊦ ¬ is_charvalue(intval(i)) | An Axiom |
| test-296 | ⊦ ¬ is_charvalue(byteval(by)) | An Axiom |
| test-297 | ⊦ ¬ is_charvalue(shortval(sho)) | An Axiom |
| test-298 | ⊦ ¬ is_charvalue(refval(r)) | An Axiom |
| test-299 | ⊦ ¬ is_charvalue(boolval(boolvar)) | An Axiom |
| test-300 | ⊦ is_charvalue(charval(jchar)) | An Axiom |
| test-301 | ⊦ ¬ is_charvalue(longval(lo)) | An Axiom |
| test-302 | ⊦ ¬ is_charvalue(floatval(floatvar)) | An Axiom |
| test-303 | ⊦ ¬ is_charvalue(doubleval(doublevar)) | An Axiom |
| test-304 | ⊦ ¬ is_charvalue(stringval(stringvar)) | An Axiom |
| test-305 | ⊦ ¬ is_charvalue(val ++ val0) | An Axiom |
| test-306 | ⊦ ¬ is_charvalue(noval) | An Axiom |
| test-307 | ⊦ ¬ is_charvalue(typeval(ty)) | An Axiom |
| test-308 | ⊦ ¬ is_charvalue(initval(istate)) | An Axiom |
| test-309 | ⊦ ¬ is_charvalue(break(lbl)) | An Axiom |
| test-310 | ⊦ ¬ is_charvalue(continue(lbl)) | An Axiom |
| test-311 | ⊦ ¬ is_charvalue(return(val, ty)) | An Axiom |
| test-312 | ⊦ ¬ is_charvalue(throw(r, ty)) | An Axiom |
| test-313 | ⊦ ¬ is_longvalue(charval(jchar)) | An Axiom |
| test-314 | ⊦ ¬ is_floatvalue(charval(jchar)) | An Axiom |
| test-315 | ⊦ ¬ is_doublevalue(charval(jchar)) | An Axiom |
| test-316 | ⊦ ¬ is_stringvalue(charval(jchar)) | An Axiom |
| test-317 | ⊦ ¬ is_valuelist(charval(jchar)) | An Axiom |
| test-318 | ⊦ ¬ is_novalue(charval(jchar)) | An Axiom |
| test-319 | ⊦ ¬ is_typevalue(charval(jchar)) | An Axiom |
| test-320 | ⊦ ¬ is_initvalue(charval(jchar)) | An Axiom |
| test-321 | ⊦ ¬ is_break_mode(charval(jchar)) | An Axiom |
| test-322 | ⊦ ¬ is_continue_mode(charval(jchar)) | An Axiom |
| test-323 | ⊦ ¬ is_return_mode(charval(jchar)) | An Axiom |
| test-324 | ⊦ ¬ is_throw_mode(charval(jchar)) | An Axiom |
| sel-20 | ⊦ charval(jchar) .charval = jchar | An Axiom |
| disj-137 | ⊦ charval(jchar) ≠ throw(r, ty) | An Axiom |
| disj-138 | ⊦ charval(jchar) ≠ return(val, ty) | An Axiom |
| disj-139 | ⊦ charval(jchar) ≠ continue(lbl) | An Axiom |
| disj-140 | ⊦ charval(jchar) ≠ break(lbl) | An Axiom |
| disj-141 | ⊦ charval(jchar) ≠ initval(istate) | An Axiom |
| disj-142 | ⊦ charval(jchar) ≠ typeval(ty) | An Axiom |
| disj-143 | ⊦ charval(jchar) ≠ noval | An Axiom |
| disj-144 | ⊦ charval(jchar) ≠ val ++ val0 | An Axiom |
| disj-145 | ⊦ charval(jchar) ≠ stringval(stringvar) | An Axiom |
| disj-146 | ⊦ charval(jchar) ≠ doubleval(doublevar) | An Axiom |
| disj-147 | ⊦ charval(jchar) ≠ floatval(floatvar) | An Axiom |
| disj-148 | ⊦ charval(jchar) ≠ longval(lo) | An Axiom |
| disj-149 | ⊦ boolval(boolvar) ≠ charval(jchar) | An Axiom |
| disj-150 | ⊦ refval(r) ≠ charval(jchar) | An Axiom |
| disj-151 | ⊦ shortval(sho) ≠ charval(jchar) | An Axiom |
| disj-152 | ⊦ byteval(by) ≠ charval(jchar) | An Axiom |
| disj-153 | ⊦ intval(i) ≠ charval(jchar) | An Axiom |
| byteval | is_bytevalue(val) ⊦ byteval(val .byteval) = val | A User Theorem |
| concat-red | ⊦ val ++ val1 = val0 ++ val1 ↔ val = val0 | A User Theorem |
| concat-red-01 | ⊦ val ++ val0 = val ++ val1 ↔ val0 = val1 | A User Theorem |
| diff | ⊦ is_throw_mode(val) → ¬ is_return_mode(val) | A User Theorem |
| diff-01 | ⊦ is_throw_mode(val) → ¬ is_break_mode(val) | A User Theorem |
| diff-02 | ⊦ is_bytevalue(val) → ¬ is_integervalue(val) | A User Theorem |
| diff-03 | ⊦ is_bytevalue(val) → ¬ is_shortvalue(val) | A User Theorem |
| diff-04 | ⊦ is_bytevalue(val) → ¬ is_boolvalue(val) | A User Theorem |
| diff-05 | ⊦ is_bytevalue(val) → ¬ is_referencevalue(val) | A User Theorem |
| diff-06 | ⊦ is_referencevalue(val) → ¬ is_integervalue(val) | A User Theorem |
| diff-07 | ⊦ is_referencevalue(val) → ¬ is_shortvalue(val) | A User Theorem |
| diff-08 | ⊦ is_referencevalue(val) → ¬ is_bytevalue(val) | A User Theorem |
| diff-09 | ⊦ is_referencevalue(val) → ¬ is_boolvalue(val) | A User Theorem |
| diff-10 | ⊦ is_boolvalue(val) → ¬ is_integervalue(val) | A User Theorem |
| diff-11 | ⊦ is_boolvalue(val) → ¬ is_shortvalue(val) | A User Theorem |
| diff-12 | ⊦ is_boolvalue(val) → ¬ is_bytevalue(val) | A User Theorem |
| diff-13 | ⊦ is_boolvalue(val) → ¬ is_referencevalue(val) | A User Theorem |
| diff-14 | ⊦ is_shortvalue(val) → ¬ is_integervalue(val) | A User Theorem |
| diff-15 | ⊦ is_shortvalue(val) → ¬ is_boolvalue(val) | A User Theorem |
| diff-16 | ⊦ is_shortvalue(val) → ¬ is_bytevalue(val) | A User Theorem |
| diff-17 | ⊦ is_shortvalue(val) → ¬ is_referencevalue(val) | A User Theorem |
| diff-18 | ⊦ is_integervalue(val) → ¬ is_boolvalue(val) | A User Theorem |
| diff-19 | ⊦ is_integervalue(val) → ¬ is_shortvalue(val) | A User Theorem |
| diff-20 | ⊦ is_integervalue(val) → ¬ is_bytevalue(val) | A User Theorem |
| diff-21 | ⊦ is_integervalue(val) → ¬ is_referencevalue(val) | A User Theorem |
| elim-refval | is_referencevalue(val) ⊦ r = val .refval ↔ val = refval(r) | A User Theorem |
| eqbyteval | ⊦ byteval(by) = val ↔ by = val .byteval ∧ is_bytevalue(val) | A User Theorem |
| eqrefval | ⊦ refval(r) = val ↔ r = val .refval ∧ is_referencevalue(val) | A User Theorem |
| eqrefval-01 | ⊦ val = refval(r) ↔ r = val .refval ∧ is_referencevalue(val) | A User Theorem |
| eqtypeval | ⊦ is_typevalue(val) → (val .type = ty ↔ val = typeval(ty)) | A User Theorem |
| inj-strong | ⊦ val ++ val0 = val1 ++ val2 ↔ ¬ ¬ (val = val1 ∧ val0 = val2) | A User Theorem |
| int2bytes-shortval | ⊦ 0 ≤ s2i(sho) → ¬ 2 < # int2bytes(s2i(sho)) | A User Theorem |
| intval | is_integervalue(val) ⊦ intval(val .intval) = val | A User Theorem |
| refva-sel | ⊦ is_referencevalue(val) → refval(val .refval) = val | A User Theorem |
| refval | ⊦ is_referencevalue(val) ∧ val .refval = r → (val ≠ refval(r) ↔ false) | A User Theorem |
| shortval-sel | ⊦ is_shortvalue(val) → shortval(val .shortval) = val | A User Theorem |
| typeval | ⊦ is_typevalue(val) ∧ val .type = ty → (val ≠ typeval(ty) ↔ false) | A User Theorem |