C

• CSub (SORT)

• castAdd (TACLET)

• castAdd2 (TACLET)

• castDel (TACLET)

• castDel2 (TACLET)

• castType (TACLET)

• castType2 (TACLET)

• ineffectiveCast2 (TACLET)

CSub

• castAdd (TACLET)

• castDel2 (TACLET)

• castType (TACLET)

• castType2 (TACLET)

• ineffectiveCast2 (TACLET)

Field

• LocSet (SORT)

• accDefinition (TACLET)

• allFieldsSubsetOf (TACLET)

• alphaObj (SORT)

• assertSafe (TACLET)

• assertSafeWithMessage (TACLET)

• assignableDefinition (TACLET)

• castTrueImpliesOriginalTrue (TACLET)

• createdInHeapToElementOf (TACLET)

• createdInHeapWithSelect (TACLET)

• createdInHeapWithSelectEQ (TACLET)

• createdInHeapWithSingleton (TACLET)

• createdInHeapWithSingletonEQ (TACLET)

• definitionAllElementsOfArray (TACLET)

• definitionAllElementsOfArray2 (TACLET)

• definitionAllElementsOfArrayLocsets (TACLET)

• definitionSeqdefWorkaround2 (TACLET)

• disjointAllFields (TACLET)

• disjointAllFields_2 (TACLET)

• disjointAllObjects (TACLET)

• disjointInfiniteUnion (TACLET)

• disjointInfiniteUnion_2 (TACLET)

• disjointNotInOtherLocset1 (TACLET)

• disjointNotInOtherLocset2 (TACLET)

• disjointToElementOf (TACLET)

• disjointWithSingleton1 (TACLET)

• disjointWithSingleton2 (TACLET)

• dismissNonSelectedField (TACLET)

• dismissNonSelectedFieldEQ (TACLET)

• dropEffectlessStores (TACLET)

• elementOf (PREDICATE)

• elementOfAllFields (TACLET)

• elementOfAllLocs (TACLET)

• elementOfAllObjects (TACLET)

• elementOfArrayRange (TACLET)

• elementOfArrayRangeEQ (TACLET)

• elementOfEmpty (TACLET)

• elementOfFreshLocs (TACLET)

• elementOfGuardedSet (TACLET)

• elementOfInfiniteUnion (TACLET)

• elementOfInfiniteUnion2Vars (TACLET)

• elementOfInfiniteUnion2VarsEQ (TACLET)

• elementOfInfiniteUnionEQ (TACLET)

• elementOfIntersect (TACLET)

• elementOfIntersectEQ (TACLET)

• elementOfSetMinus (TACLET)

• elementOfSetMinusEQ (TACLET)

• elementOfSingleton (TACLET)

• elementOfSubsetImpliesElementOfSuperset (TACLET)

• elementOfSubsetOfUnion1 (TACLET)

• elementOfSubsetOfUnion2 (TACLET)

• elementOfUnion (TACLET)

• elementOfUnionEQ (TACLET)

• emptyEqualsSingleton (TACLET)

• equalityToElementOf (TACLET)

• equalityToElementOfRight (TACLET)

• equalityToSelect (TACLET)

• intersectAllFieldsFreshLocs (TACLET)

• intersectWithSingleton (TACLET)

• narrowSelectType (TACLET)

• noElementOfSupersetImpliesNoElementOfSubset (TACLET)

• onlyCreatedObjectsAreInLocSets (TACLET)

• onlyCreatedObjectsAreInLocSetsEQ (TACLET)

• onlyCreatedObjectsAreObserved (TACLET)

• onlyCreatedObjectsAreObservedInLocSets (TACLET)

• onlyCreatedObjectsAreObservedInLocSetsEQ (TACLET)

• onlyCreatedObjectsAreReferenced (TACLET)

• pullOutSelect (TACLET)

• reachDependenciesAnon (TACLET)

• reachDependenciesAnonCoarse (TACLET)

• reachDependenciesStore (TACLET)

• reachDependenciesStoreEQ (TACLET)

• reachDependenciesStoreSimple (TACLET)

• reachDependenciesStoreSimpleEQ (TACLET)

• reachEndOfUniquePath (TACLET)

• reachEndOfUniquePath2 (TACLET)

• reachUniquePathSameSteps (TACLET)

• referencedObjectIsCreatedRight (TACLET)

• referencedObjectIsCreatedRightEQ (TACLET)

• selectOfAnon (TACLET)

• selectOfAnonEQ (TACLET)

• selectOfCreate (TACLET)

• selectOfCreateEQ (TACLET)

• selectOfMemset (TACLET)

• selectOfMemsetEQ (TACLET)

• selectOfStore (TACLET)

• selectOfStoreEQ (TACLET)

• setMinusSingleton (TACLET)

• simplifySelectOfAnon (TACLET)

• simplifySelectOfAnonEQ (TACLET)

• simplifySelectOfCreate (TACLET)

• simplifySelectOfCreateEQ (TACLET)

• simplifySelectOfMemset (TACLET)

• simplifySelectOfMemsetEQ (TACLET)

• simplifySelectOfStore (TACLET)

• simplifySelectOfStoreEQ (TACLET)

• singletonEqualsEmpty (TACLET)

• subsetSingletonLeft (TACLET)

• subsetSingletonLeftEQ (TACLET)

• subsetSingletonRight (TACLET)

• subsetSingletonRightEQ (TACLET)

• subsetToElementOf (TACLET)

• subsetToElementOfRight (TACLET)

• unionWithSingletonEqualsUnionWithSingleton (TACLET)

• unionWithSingletonEqualsUnionWithSingleton_2 (TACLET)

• wellFormedStoreLocSet (TACLET)

• wellFormedStoreLocSetEQ (TACLET)

• wellFormedStoreObject (TACLET)

• wellFormedStoreObjectEQ (TACLET)

• wellFormedStorePrimitive (TACLET)

• wellFormedStorePrimitiveEQ (TACLET)

Free

• Free (SORT)

G

• GSub (SORT)

• J (SORT)

• array_self_reference (TACLET)

• array_self_reference_eq (TACLET)

• assignment_array2 (TACLET)

• assignment_read_attribute (TACLET)

• assignment_read_attribute_this (TACLET)

• assignment_read_static_attribute (TACLET)

• assignment_read_static_attribute_with_variable_prefix (TACLET)

• castAdd2 (TACLET)

• castDel2 (TACLET)

• closeType (TACLET)

• closeTypeSwitched (TACLET)

• delete_unnecessary_cast (TACLET)

• elim_exists2 (TACLET)

• elim_exists3 (TACLET)

• elim_exists6 (TACLET)

• elim_exists7 (TACLET)

• elim_forall10 (TACLET)

• elim_forall11 (TACLET)

• elim_forall14 (TACLET)

• elim_forall15 (TACLET)

• elim_forall18 (TACLET)

• elim_forall19 (TACLET)

• elim_forall2 (TACLET)

• elim_forall3 (TACLET)

• elim_forall6 (TACLET)

• elim_forall7 (TACLET)

• exact_instance_for_interfaces_or_abstract_classes (TACLET)

• exact_instance_known_dynamic_type (TACLET)

• ineffectiveCast2 (TACLET)

• instanceof_known_dynamic_type (TACLET)

• instanceof_known_dynamic_type_2 (TACLET)

• instanceof_not_compatible (TACLET)

• instanceof_not_compatible_2 (TACLET)

• instanceof_not_compatible_3 (TACLET)

• instanceof_not_compatible_4 (TACLET)

• instanceof_not_compatible_5 (TACLET)

• instanceof_static_type (TACLET)

• instanceof_static_type_2 (TACLET)

• reference_type_cast (TACLET)

• sameTypeFalse (TACLET)

• sameTypeTrue (TACLET)

• sortsDisjoint1 (TACLET)

• sortsDisjoint2 (TACLET)

• sortsDisjointModuloNull (TACLET)

• subG (SORT)

• typeEq (TACLET)

• typeEqDerived2 (TACLET)

• typeStatic (TACLET)

GSub

• closeType (TACLET)

• closeTypeSwitched (TACLET)

H

• applyEqRigid (TACLET)

• castType (TACLET)

• castType2 (TACLET)

• exact_instance_known_dynamic_type (TACLET)

• ineffectiveCast (TACLET)

• ineffectiveCast3 (TACLET)

• instanceof_known_dynamic_type (TACLET)

• instanceof_known_dynamic_type_2 (TACLET)

• instanceof_not_compatible_5 (TACLET)

• sameTypeFalse (TACLET)

• sortsDisjoint1 (TACLET)

• sortsDisjoint2 (TACLET)

• sortsDisjointModuloNull (TACLET)

• typeEq (TACLET)

• typeEqDerived (TACLET)

Heap

• LocSet (SORT)

• acc (PREDICATE)

• accDefinition (TACLET)

• alphaObj (SORT)

• array2seqDef (TACLET)

• array_self_reference (TACLET)

• array_self_reference_eq (TACLET)

• assertSafe (TACLET)

• assertSafeWithMessage (TACLET)

• assignable (PREDICATE)

• assignableDefinition (TACLET)

• castTrueImpliesOriginalTrue (TACLET)

• createdInHeap (PREDICATE)

• createdInHeapToElementOf (TACLET)

• createdInHeapWithAllFields (TACLET)

• createdInHeapWithAllFieldsEQ (TACLET)

• createdInHeapWithArrayRange (TACLET)

• createdInHeapWithArrayRangeEQ (TACLET)

• createdInHeapWithEmpty (TACLET)

• createdInHeapWithObserver (TACLET)

• createdInHeapWithObserverEQ (TACLET)

• createdInHeapWithSelect (TACLET)

• createdInHeapWithSelectEQ (TACLET)

• createdInHeapWithSetMinusFreshLocs (TACLET)

• createdInHeapWithSetMinusFreshLocsEQ (TACLET)

• createdInHeapWithSingleton (TACLET)

• createdInHeapWithSingletonEQ (TACLET)

• createdInHeapWithUnion (TACLET)

• createdInHeapWithUnionEQ (TACLET)

• createdOnHeapImpliesCreatedOnPermissions (TACLET)

• definitionAllElementsOfArray (TACLET)

• definitionAllElementsOfArray2 (TACLET)

• definitionAllElementsOfArrayLocsets (TACLET)

• definitionOfNewObjectsIsomorphic (TACLET)

• definitionOfNewOnHeap (TACLET)

• definitionSeqdefWorkaround (TACLET)

• definitionSeqdefWorkaround2 (TACLET)

• dismissNonSelectedField (TACLET)

• dismissNonSelectedFieldEQ (TACLET)

• dropEffectlessStores (TACLET)

• elementOfFreshLocs (TACLET)

• elementOfSubsetOfUnion1 (TACLET)

• elementOfSubsetOfUnion2 (TACLET)

• equalityToSelect (TACLET)

• getAnyOfArray2seq (TACLET)

• getOfArray2seq (TACLET)

• getOfSwap (TACLET)

• intersectAllFieldsFreshLocs (TACLET)

• lenOfArray2seq (TACLET)

• loopScopeInvBox (TACLET)

• loopScopeInvDia (TACLET)

• memsetEmpty (TACLET)

• narrowSelectArrayType (TACLET)

• narrowSelectType (TACLET)

• newObjectsIsomorphic (PREDICATE)

• newOnHeap (PREDICATE)

• nonNull (PREDICATE)

• nonNull (TACLET)

• nonNullZero (TACLET)

• nullCreated (TACLET)

• nullIsNotNonNull (TACLET)

• onlyCreatedObjectsAreInLocSets (TACLET)

• onlyCreatedObjectsAreInLocSetsEQ (TACLET)

• onlyCreatedObjectsAreObserved (TACLET)

• onlyCreatedObjectsAreObservedInLocSets (TACLET)

• onlyCreatedObjectsAreObservedInLocSetsEQ (TACLET)

• onlyCreatedObjectsAreReferenced (TACLET)

• only_created_objects_are_reachable (TACLET)

• permissionsFor (PREDICATE)

• pullOutSelect (TACLET)

• reach (PREDICATE)

• reachAddOne (TACLET)

• reachAddOne2 (TACLET)

• reachDefinition (TACLET)

• reachDependenciesAnon (TACLET)

• reachDependenciesAnonCoarse (TACLET)

• reachDependenciesStore (TACLET)

• reachDependenciesStoreEQ (TACLET)

• reachDependenciesStoreSimple (TACLET)

• reachDependenciesStoreSimpleEQ (TACLET)

• reachDoesNotDependOnCreatedness (TACLET)

• reachEndOfUniquePath (TACLET)

• reachEndOfUniquePath2 (TACLET)

• reachNull (TACLET)

• reachNull2 (TACLET)

• reachOne (TACLET)

• reachUniquePathSameSteps (TACLET)

• reachZero (TACLET)

• reach_does_not_depend_on_fresh_locs (TACLET)

• reach_does_not_depend_on_fresh_locs_EQ (TACLET)

• referencedObjectIsCreatedRight (TACLET)

• referencedObjectIsCreatedRightEQ (TACLET)

• selectCreatedOfAnon (TACLET)

• selectCreatedOfAnonAsFormula (TACLET)

• selectCreatedOfAnonAsFormulaEQ (TACLET)

• selectCreatedOfAnonEQ (TACLET)

• selectOfAnon (TACLET)

• selectOfAnonEQ (TACLET)

• selectOfCreate (TACLET)

• selectOfCreateEQ (TACLET)

• selectOfMemset (TACLET)

• selectOfMemsetEQ (TACLET)

• selectOfStore (TACLET)

• selectOfStoreEQ (TACLET)

• seqNPerm (PREDICATE)

• simplifySelectOfAnon (TACLET)

• simplifySelectOfAnonEQ (TACLET)

• simplifySelectOfCreate (TACLET)

• simplifySelectOfCreateEQ (TACLET)

• simplifySelectOfMemset (TACLET)

• simplifySelectOfMemsetEQ (TACLET)

• simplifySelectOfStore (TACLET)

• simplifySelectOfStoreEQ (TACLET)

• threeBranchLoopScopeInvRuleBox (TACLET)

• threeBranchLoopScopeInvRuleDia (TACLET)

• wellFormed (PREDICATE)

• wellFormedAnon (TACLET)

• wellFormedAnonEQ (TACLET)

• wellFormedCreate (TACLET)

• wellFormedMemsetArrayObject (TACLET)

• wellFormedMemsetArrayPrimitive (TACLET)

• wellFormedStoreArray (TACLET)

• wellFormedStoreLocSet (TACLET)

• wellFormedStoreLocSetEQ (TACLET)

• wellFormedStoreObject (TACLET)

• wellFormedStoreObjectEQ (TACLET)

• wellFormedStorePrimitive (TACLET)

• wellFormedStorePrimitiveArray (TACLET)

• wellFormedStorePrimitiveEQ (TACLET)

J

• array_store_known_dynamic_array_type (TACLET)

LocSet

• LocSet (SORT)

• acc (PREDICATE)

• accDefinition (TACLET)

• allFieldsSubsetOf (TACLET)

• alphaObj (SORT)

• assignable (PREDICATE)

• assignableDefinition (TACLET)

• associativeLawIntersect (TACLET)

• associativeLawUnion (TACLET)

• commuteDisjoint (TACLET)

• commuteIntersection (TACLET)

• commuteIntersection_2 (TACLET)

• commuteUnion (TACLET)

• commuteUnion_2 (TACLET)

• createdInHeap (PREDICATE)

• createdInHeapToElementOf (TACLET)

• createdInHeapWithAllFieldsEQ (TACLET)

• createdInHeapWithArrayRangeEQ (TACLET)

• createdInHeapWithObserver (TACLET)

• createdInHeapWithObserverEQ (TACLET)

• createdInHeapWithSelect (TACLET)

• createdInHeapWithSelectEQ (TACLET)

• createdInHeapWithSetMinusFreshLocs (TACLET)

• createdInHeapWithSetMinusFreshLocsEQ (TACLET)

• createdInHeapWithSingletonEQ (TACLET)

• createdInHeapWithUnion (TACLET)

• createdInHeapWithUnionEQ (TACLET)

• definitionAllElementsOfArrayLocsets (TACLET)

• disjoint (PREDICATE)

• disjointAllFields (TACLET)

• disjointAllObjects (TACLET)

• disjointAndSubset1 (TACLET)

• disjointAndSubset2 (TACLET)

• disjointAndSubset_3 (TACLET)

• disjointAndSubset_4 (TACLET)

• disjointAndSubset_5 (TACLET)

• disjointAndSubset_6 (TACLET)

• disjointDefinition (TACLET)

• disjointInfiniteUnion (TACLET)

• disjointInfiniteUnion_2 (TACLET)

• disjointNotInOtherLocset1 (TACLET)

• disjointNotInOtherLocset2 (TACLET)

• disjointToElementOf (TACLET)

• disjointWithEmpty (TACLET)

• disjointWithSingleton1 (TACLET)

• disjointWithSingleton2 (TACLET)

• distributeIntersection (TACLET)

• distributeIntersection_2 (TACLET)

• elementOf (PREDICATE)

• elementOfArrayRangeEQ (TACLET)

• elementOfGuardedSet (TACLET)

• elementOfInfiniteUnion (TACLET)

• elementOfInfiniteUnion2Vars (TACLET)

• elementOfInfiniteUnion2VarsEQ (TACLET)

• elementOfInfiniteUnionEQ (TACLET)

• elementOfIntersect (TACLET)

• elementOfIntersectEQ (TACLET)

• elementOfSetMinus (TACLET)

• elementOfSetMinusEQ (TACLET)

• elementOfSubsetImpliesElementOfSuperset (TACLET)

• elementOfSubsetOfUnion1 (TACLET)

• elementOfSubsetOfUnion2 (TACLET)

• elementOfUnion (TACLET)

• elementOfUnionEQ (TACLET)

• elim_exists_sub_1 (TACLET)

• elim_exists_sub_1_and_phi (TACLET)

• elim_exists_sub_1_or_phi (TACLET)

• elim_forall_eqSet_imp_phi (TACLET)

• elim_forall_subOfAll (TACLET)

• elim_forall_subOfAll_and_phi (TACLET)

• elim_forall_superOfAll (TACLET)

• elim_forall_superOfAll_and_phi (TACLET)

• equalityToElementOf (TACLET)

• equalityToElementOfRight (TACLET)

• infiniteUnionUnused (TACLET)

• intersectWithAllLocs (TACLET)

• intersectWithAllLocsRight (TACLET)

• intersectWithEmpty (TACLET)

• intersectWithEmptyRight (TACLET)

• intersectWithItself (TACLET)

• intersectWithSingleton (TACLET)

• intersectionSetMinusItself (TACLET)

• intersectionSetMinusItself_2 (TACLET)

• noElementOfSupersetImpliesNoElementOfSubset (TACLET)

• onlyCreatedObjectsAreInLocSets (TACLET)

• onlyCreatedObjectsAreInLocSetsEQ (TACLET)

• onlyCreatedObjectsAreObservedInLocSets (TACLET)

• onlyCreatedObjectsAreObservedInLocSetsEQ (TACLET)

• only_created_objects_are_reachable (TACLET)

• reach (PREDICATE)

• reachAddOne (TACLET)

• reachAddOne2 (TACLET)

• reachDefinition (TACLET)

• reachDependenciesAnon (TACLET)

• reachDependenciesAnonCoarse (TACLET)

• reachDependenciesStore (TACLET)

• reachDependenciesStoreEQ (TACLET)

• reachDoesNotDependOnCreatedness (TACLET)

• reachEndOfUniquePath (TACLET)

• reachEndOfUniquePath2 (TACLET)

• reachNull (TACLET)

• reachNull2 (TACLET)

• reachOne (TACLET)

• reachUniquePathSameSteps (TACLET)

• reachZero (TACLET)

• reach_does_not_depend_on_fresh_locs (TACLET)

• reach_does_not_depend_on_fresh_locs_EQ (TACLET)

• selectCreatedOfAnon (TACLET)

• selectCreatedOfAnonAsFormula (TACLET)

• selectCreatedOfAnonAsFormulaEQ (TACLET)

• selectCreatedOfAnonEQ (TACLET)

• selectOfAnon (TACLET)

• selectOfAnonEQ (TACLET)

• selectOfMemset (TACLET)

• selectOfMemsetEQ (TACLET)

• seqNPerm (PREDICATE)

• setMinusItself (TACLET)

• setMinusOfUnion (TACLET)

• setMinusOfUnionEQ (TACLET)

• setMinusSingleton (TACLET)

• setMinusWithAllLocs (TACLET)

• setMinusWithEmpty1 (TACLET)

• setMinusWithEmpty2 (TACLET)

• simplifySelectOfAnon (TACLET)

• simplifySelectOfAnonEQ (TACLET)

• simplifySelectOfMemset (TACLET)

• simplifySelectOfMemsetEQ (TACLET)

• subset (PREDICATE)

• subsetOfEmpty (TACLET)

• subsetOfIntersectWithItSelf1 (TACLET)

• subsetOfIntersectWithItSelf2 (TACLET)

• subsetOfIntersectWithItSelfEQ1 (TACLET)

• subsetOfIntersectWithItSelfEQ2 (TACLET)

• subsetOfItself (TACLET)

• subsetOfUnionWithItSelf1 (TACLET)

• subsetOfUnionWithItSelf2 (TACLET)

• subsetOfUnionWithItSelfEQ1 (TACLET)

• subsetOfUnionWithItSelfEQ2 (TACLET)

• subsetSingletonLeft (TACLET)

• subsetSingletonLeftEQ (TACLET)

• subsetSingletonRight (TACLET)

• subsetSingletonRightEQ (TACLET)

• subsetToElementOf (TACLET)

• subsetToElementOfRight (TACLET)

• subsetUnionLeft (TACLET)

• subsetUnionLeftEQ (TACLET)

• subsetWithAllLocs (TACLET)

• subsetWithAllLocs2 (TACLET)

• subsetWithEmpty (TACLET)

• subsetWithSetMinusLeft (TACLET)

• subsetWithSetMinusLeftEQ (TACLET)

• unionEqualsEmpty (TACLET)

• unionEqualsEmptyEQ (TACLET)

• unionIntersectItself (TACLET)

• unionIntersectItself_2 (TACLET)

• unionIntersectItself_3 (TACLET)

• unionIntersectItself_4 (TACLET)

• unionIntersectItself_5 (TACLET)

• unionIntersectItself_6 (TACLET)

• unionWithAllLocs (TACLET)

• unionWithAllLocsRight (TACLET)

• unionWithEmpty (TACLET)

• unionWithEmptyRight (TACLET)

• unionWithItself (TACLET)

• unionWithSingletonEqualsUnionWithSingleton (TACLET)

• unionWithSingletonEqualsUnionWithSingleton_2 (TACLET)

• wellFormedAnon (TACLET)

• wellFormedAnonEQ (TACLET)

• wellFormedStoreLocSet (TACLET)

• wellFormedStoreLocSetEQ (TACLET)

Map

• Map (SORT)

• inDomain (PREDICATE)

• inDomainImpliesCreated (PREDICATE)

• isFinite (PREDICATE)

• mapSize (FILE)

Pair

• Pair (SORT)

Permission

• PermissionOwnerList (SORT)

• assignment_array2 (TACLET)

• assignment_read_attribute (TACLET)

• assignment_read_attribute_this (TACLET)

• assignment_read_static_attribute (TACLET)

• assignment_read_static_attribute_with_variable_prefix (TACLET)

• assignment_to_primitive_array_component (TACLET)

• assignment_to_reference_array_component (TACLET)

• assignment_write_array_this_access_normalassign (TACLET)

• assignment_write_attribute (TACLET)

• assignment_write_attribute_this (TACLET)

• assignment_write_static_attribute (TACLET)

• assignment_write_static_attribute_with_variable_prefix (TACLET)

• nonEmptyPermission (PREDICATE)

• nonEmptyPermission (TACLET)

• permissionDefaultValue (TACLET)

• permissionTransferReturnIdentity (TACLET)

• permissionTransferReturnIdentityEQ (TACLET)

• readPermission (PREDICATE)

• readPermission (TACLET)

• readPermissionAfterTransferRead (TACLET)

• readPermissionAfterTransferReadEQ (TACLET)

• readPermissionAfterTransferWrite (TACLET)

• readPermissionAfterTransferWriteEQ (TACLET)

• readPermissionObject (PREDICATE)

• readPermissionObject (TACLET)

• readPermissionOwe (PREDICATE)

• readPermissionOwe (TACLET)

• readPermissionOwe2 (PREDICATE)

• readPermissionOwe2 (TACLET)

• readPermissionSlice (TACLET)

• returnPermission_slice (TACLET)

• returnPermission_slice_split (TACLET)

• transferPermission_slice (TACLET)

• twoPermissions (PREDICATE)

• twoPermissions (TACLET)

• writePermission (PREDICATE)

• writePermission (TACLET)

• writePermissionAfterFullTransfer (TACLET)

• writePermissionAfterFullTransferEQ (TACLET)

• writePermissionAfterReturn (TACLET)

• writePermissionAfterReturnEQ (TACLET)

• writePermissionImpliesReadPermission (TACLET)

• writePermissionObject (PREDICATE)

• writePermissionObject (TACLET)

• writePermissionOtherNoPermissionCurrentRead (TACLET)

• writePermissionOtherNoPermissionCurrentWrite (TACLET)

• writePermissionSlice (TACLET)

PermissionOwnerList

• PermissionOwnerList (SORT)

• checkPermissionOwner (PREDICATE)

• checkPermissionOwner_nonempty (TACLET)

• insertPermissionOwner (TACLET)

• nonEmptyPermission (TACLET)

• permSlice1 (TACLET)

• permSlice2 (TACLET)

• readPermissionOwe (TACLET)

• readPermissionOwe2 (TACLET)

• readPermissionSlice (TACLET)

• returnPermissionOwner (TACLET)

• returnPermission_slice (TACLET)

• returnPermission_slice_split (TACLET)

• transferPermission_slice (TACLET)

• twoPermissions (TACLET)

• writePermissionSlice (TACLET)

RegEx

• RegEx (SORT)

• altAxiom (TACLET)

• concatRepeatContraction1 (TACLET)

• concatRepeatContraction2 (TACLET)

• concatRepeatContraction2Sym (TACLET)

• concatRepeatContraction3 (TACLET)

• concatRepeatContraction3Sym (TACLET)

• equalRegEx (TACLET)

• match (PREDICATE)

• optAxiom (TACLET)

• optEmpty (TACLET)

• regExConcatAltLeft (TACLET)

• regExConcatAltRight (TACLET)

• regExConcatAxiom (TACLET)

• regExConcatConcreteStringLeft (TACLET)

• regExConcatConcreteStringRight (TACLET)

• regExConcatOptLeft (TACLET)

• regExConcatOptRight (TACLET)

• regExConcatRepeatLeft (TACLET)

• regExConcatRepeatRight (TACLET)

• repeatAxiom (TACLET)

• repeatMatchEmpty (TACLET)

• repeatOnce (TACLET)

• repeatPlusAxiom (TACLET)

• repeatRepeatContraction (TACLET)

• repeatStarAxiom (TACLET)

• repeatZero (TACLET)

SORT

• alphSub (SORT)

• ssubsort (PREDICATE)

• ssubsortTop (TACLET)

• subsortTrans (TACLET)

Seq

• Map (SORT)

• RegEx (SORT)

• altAxiom (TACLET)

• castedGetAny (TACLET)

• charListHeader (FILE)

• clContains (PREDICATE)

• clEndsWith (PREDICATE)

• clStartsWith (PREDICATE)

• contains (TACLET)

• containsAxiomAntec (TACLET)

• containsAxiomSucc (TACLET)

• defIsFinite (TACLET)

• defOfSeqConcat (TACLET)

• defOfSeqNPermInv (TACLET)

• defOfSeqRemove (TACLET)

• defOfSeqReverse (TACLET)

• defOfSeqSub (TACLET)

• defOfSeqSwap (TACLET)

• defOfSeqUpd (TACLET)

• defSeq2Map (TACLET)

• definitionOfNewObjectsIsomorphic (TACLET)

• definitionOfNewOnHeap (TACLET)

• definitionOfObjectIsomorphic (TACLET)

• definitionOfObjectsIsomorphic (TACLET)

• definitionOfSameTypes (TACLET)

• endsWith (TACLET)

• eqSameSeq (TACLET)

• eqSeqConcat (TACLET)

• eqSeqConcat2 (TACLET)

• eqSeqConcat2EQ (TACLET)

• eqSeqConcat3 (TACLET)

• eqSeqConcat3EQ (TACLET)

• eqSeqConcat4 (TACLET)

• eqSeqConcat4EQ (TACLET)

• eqSeqConcat5 (TACLET)

• eqSeqConcat5EQ (TACLET)

• eqSeqConcatEQ (TACLET)

• eqSeqDef (TACLET)

• eqSeqDef2 (TACLET)

• eqSeqEmpty (TACLET)

• eqSeqReverse (TACLET)

• eqSeqReverse2 (TACLET)

• eqSeqSingleton (TACLET)

• eqSeqSingleton2 (TACLET)

• equalRegEx (TACLET)

• equalityToSeqGetAndSeqLen (TACLET)

• equalityToSeqGetAndSeqLenLeft (TACLET)

• equalityToSeqGetAndSeqLenRight (TACLET)

• getAnyOfNPermInv (TACLET)

• getOfNPermInv (TACLET)

• getOfRemoveAny (TACLET)

• getOfRemoveAnyConcrete1 (TACLET)

• getOfRemoveAnyConcrete2 (TACLET)

• getOfRemoveInt (TACLET)

• getOfSeq2Map (TACLET)

• getOfSeqConcat (TACLET)

• getOfSeqConcatEQ (TACLET)

• getOfSeqDefEQ (TACLET)

• getOfSeqReverse (TACLET)

• getOfSeqReverseEQ (TACLET)

• getOfSeqSingletonEQ (TACLET)

• getOfSeqSub (TACLET)

• getOfSeqSubEQ (TACLET)

• getOfSeqUpd (TACLET)

• getOfSwap (TACLET)

• inDomainOfSeq2Map (TACLET)

• indexOf (TACLET)

• indexOfSeqConcatFirst (TACLET)

• indexOfSeqConcatSecond (TACLET)

• indexOfSeqSub (TACLET)

• indexOfStr (TACLET)

• isFiniteOfSeq2Map (TACLET)

• lastIndexOf (TACLET)

• lastIndexOfStr (TACLET)

• lenNonNegative (TACLET)

• lenOfNPermInv (TACLET)

• lenOfRemove (TACLET)

• lenOfRemoveConcrete1 (TACLET)

• lenOfRemoveConcrete2 (TACLET)

• lenOfSeqConcat (TACLET)

• lenOfSeqConcatEQ (TACLET)

• lenOfSeqDefEQ (TACLET)

• lenOfSeqEmptyEQ (TACLET)

• lenOfSeqReverse (TACLET)

• lenOfSeqReverseEQ (TACLET)

• lenOfSeqSingletonEQ (TACLET)

• lenOfSeqSub (TACLET)

• lenOfSeqSubEQ (TACLET)

• lenOfSeqUpd (TACLET)

• lenOfSwap (TACLET)

• lengthReplace (TACLET)

• lengthReplaceEQ (TACLET)

• match (PREDICATE)

• newObjectsIsomorphic (PREDICATE)

• newOnHeap (PREDICATE)

• objectIsomorphic (PREDICATE)

• objectsIsomorphic (PREDICATE)

• optAxiom (TACLET)

• precOfSeq (TACLET)

• regExAxiom (TACLET)

• regExConcatAltLeft (TACLET)

• regExConcatAltRight (TACLET)

• regExConcatAxiom (TACLET)

• regExConcatConcreteStringLeft (TACLET)

• regExConcatConcreteStringRight (TACLET)

• regExConcatOptLeft (TACLET)

• regExConcatOptRight (TACLET)

• regExConcatRepeatLeft (TACLET)

• regExConcatRepeatRight (TACLET)

• removeZeros (TACLET)

• repeatAxiom (TACLET)

• repeatPlusAxiom (TACLET)

• repeatStarAxiom (TACLET)

• repeatZero (TACLET)

• replaceConcat (TACLET)

• replaceCons (TACLET)

• replaceDef (TACLET)

• replaceSingleton (TACLET)

• replaceSubstring (TACLET)

• sameTypes (PREDICATE)

• schiffl_lemma_2 (TACLET)

• schiffl_thm_1 (TACLET)

• seqConcatWithSeqEmpty1 (TACLET)

• seqConcatWithSeqEmpty2 (TACLET)

• seqDefOfSeq (TACLET)

• seqGetAlphaCast (TACLET)

• seqGetSInvS (TACLET)

• seqIndexOf (TACLET)

• seqNPerm (PREDICATE)

• seqNPermComp (TACLET)

• seqNPermDefLeft (TACLET)

• seqNPermDefReplace (TACLET)

• seqNPermInjective (TACLET)

• seqNPermInvNPermLeft (TACLET)

• seqNPermInvNPermReplace (TACLET)

• seqNPermRange (TACLET)

• seqNPermRight (TACLET)

• seqNPermSwapNPerm (TACLET)

• seqOutsideValue (TACLET)

• seqPerm (PREDICATE)

• seqPermConcatBW (TACLET)

• seqPermConcatFW (TACLET)

• seqPermCountsInt (TACLET)

• seqPermDef (TACLET)

• seqPermDefLeft (TACLET)

• seqPermEmpty1 (TACLET)

• seqPermEmpty2 (TACLET)

• seqPermExists (TACLET)

• seqPermForall (TACLET)

• seqPermFromSwap (TACLET)

• seqPermRefl (TACLET)

• seqPermSplit (TACLET)

• seqPermSym (TACLET)

• seqPermTrans (TACLET)

• seqPermTransAlt0 (TACLET)

• seqPermTransAlt1 (TACLET)

• seqPermTransAlt2 (TACLET)

• seqPermTransAlt3 (TACLET)

• seqSelfDefinition (TACLET)

• seqSelfDefinitionEQ2 (TACLET)

• seqSwapPreservesSeqPerm (TACLET)

• seqSwapPreservesSeqPermEQ (TACLET)

• seqnormalizeDef (TACLET)

• sizeOfSeq2Map (TACLET)

• startsWith (TACLET)

• subSeqComplete (TACLET)

• subSeqCompleteSeqDefEQ (TACLET)

• subSeqConcat (TACLET)

• subSeqConcatEQ (TACLET)

• subSeqEmpty (TACLET)

• subSeqHeadSeqDef (TACLET)

• subSeqHeadSeqDefEQ (TACLET)

• subSeqSingleton (TACLET)

• subSeqSingleton2 (TACLET)

• subSeqSingleton2EQ (TACLET)

• subSeqSingletonEQ (TACLET)

• subSeqTailEQL (TACLET)

• subSeqTailEQR (TACLET)

• subSeqTailL (TACLET)

• subSeqTailR (TACLET)

• substringSubstring (TACLET)

• substringSubstring2 (TACLET)

alph

• alphSub (SORT)

• ssubsortDirect (TACLET)

• ssubsortSup (TACLET)

alphSub

• ssubsortDirect (TACLET)

• ssubsortSup (TACLET)

alpha

• alphaObj (SORT)

• betaObj (SORT)

• dismissNonSelectedField (TACLET)

• dismissNonSelectedFieldEQ (TACLET)

• elementOfInfiniteUnion (TACLET)

• elementOfInfiniteUnion2Vars (TACLET)

• elementOfInfiniteUnion2VarsEQ (TACLET)

• elementOfInfiniteUnionEQ (TACLET)

• getOfArray2seq (TACLET)

• getOfMapForeach (TACLET)

• getOfRemoveAny (TACLET)

• getOfRemoveAnyConcrete1 (TACLET)

• getOfRemoveAnyConcrete2 (TACLET)

• getOfSeqConcat (TACLET)

• getOfSeqConcatEQ (TACLET)

• getOfSeqDef (TACLET)

• getOfSeqDefEQ (TACLET)

• getOfSeqReverse (TACLET)

• getOfSeqReverseEQ (TACLET)

• getOfSeqSingleton (TACLET)

• getOfSeqSingletonConcrete (TACLET)

• getOfSeqSingletonEQ (TACLET)

• getOfSeqSub (TACLET)

• getOfSeqSubEQ (TACLET)

• getOfSeqUpd (TACLET)

• getOfSwap (TACLET)

• inDomainOfMapForeach (TACLET)

• infiniteUnionUnused (TACLET)

• lenOfSeqEmptyEQ (TACLET)

• lenOfSeqSingleton (TACLET)

• lenOfSeqSingletonEQ (TACLET)

• maxAxiom (TACLET)

• minAxiom (TACLET)

• narrowSelectArrayType (TACLET)

• narrowSelectType (TACLET)

• prod_empty (TACLET)

• prod_one (TACLET)

• reachEndOfUniquePath (TACLET)

• reachEndOfUniquePath2 (TACLET)

• selectOfStore (TACLET)

• selectOfStoreEQ (TACLET)

• seqGetAlphaCast (TACLET)

• seqNPerm (PREDICATE)

• simplifySelectOfStore (TACLET)

• simplifySelectOfStoreEQ (TACLET)

• sum_empty (TACLET)

• sum_zero (TACLET)

• wd_Heap_Reference (TACLET)

• wd_Heap_Reference_Array (TACLET)

• wd_Heap_Reference_Created (TACLET)

• wd_Heap_Reference_Static (TACLET)

• wd_Seq_Get (TACLET)

• wd_Type_Cast (TACLET)

• wd_Type_ExactInstance (TACLET)

• wd_Type_Instance (TACLET)

• wellFormedStoreObject (TACLET)

• wellFormedStoreObjectEQ (TACLET)

alphaObj

• allocateInstance (TACLET)

• allocateInstanceWithLength (TACLET)

• class_being_initialized_is_prepared (TACLET)

• class_erroneous_excludes_class_in_init (TACLET)

• class_initialized_excludes_class_init_in_progress (TACLET)

• erroneous_class_has_no_initialized_sub_class (TACLET)

• initialized_class_is_not_erroneous (TACLET)

• initialized_class_is_prepared (TACLET)

• superclasses_of_initialized_classes_are_initialized (TACLET)

• superclasses_of_initialized_classes_are_prepared (TACLET)

any

• Map (SORT)

• Pair (SORT)

• alphaObj (SORT)

• applyOnElementary (TACLET)

• applyOnPV (TACLET)

• applyOnRigidTerm (TACLET)

• applySkip1 (TACLET)

• array2seqDef (TACLET)

• arrayStoreValid (PREDICATE)

• assertSafe (TACLET)

• assertSafeWithMessage (TACLET)

• assignableDefinition (TACLET)

• betaObj (SORT)

• castTrueImpliesOriginalTrue (TACLET)

• castedGetAny (TACLET)

• defIsFinite (TACLET)

• defMapSingleton (TACLET)

• defOfEmpty (TACLET)

• defOfSeqConcat (TACLET)

• defOfSeqRemove (TACLET)

• defOfSeqReverse (TACLET)

• defOfSeqSingleton (TACLET)

• defOfSeqSub (TACLET)

• defOfSeqSwap (TACLET)

• defOfSeqUpd (TACLET)

• defSeq2Map (TACLET)

• definitionOfNewOnHeap (TACLET)

• definitionOfObjectIsomorphic (TACLET)

• definitionOfObjectsIsomorphic (TACLET)

• definitionOfSameTypes (TACLET)

• definitionSeqdefWorkaround (TACLET)

• definitionSeqdefWorkaround2 (TACLET)

• dismissNonSelectedField (TACLET)

• dismissNonSelectedFieldEQ (TACLET)

• dropEffectlessStores (TACLET)

• eqSameSeq (TACLET)

• eqSeqConcat4 (TACLET)

• eqSeqConcat4EQ (TACLET)

• eqSeqConcat5 (TACLET)

• eqSeqConcat5EQ (TACLET)

• eqSeqDef (TACLET)

• eqSeqDef2 (TACLET)

• eqSeqReverse (TACLET)

• eqSeqReverse2 (TACLET)

• eqSeqSingleton (TACLET)

• eqSeqSingleton2 (TACLET)

• equalUnique (TACLET)

• equalityToSelect (TACLET)

• equalityToSeqGetAndSeqLen (TACLET)

• equalityToSeqGetAndSeqLenLeft (TACLET)

• equalityToSeqGetAndSeqLenRight (TACLET)

• exact_instance_known_dynamic_type (TACLET)

• getAnyOfArray2seq (TACLET)

• getAnyOfNPermInv (TACLET)

• getOfSeq2Map (TACLET)

• getOfSeqDef (TACLET)

• getOfSeqDefEQ (TACLET)

• getOfSeqSingleton (TACLET)

• getOfSeqSingletonConcrete (TACLET)

• getOfSeqSingletonEQ (TACLET)

• getOfSeqUpd (TACLET)

• hideAuxiliaryEq (TACLET)

• hideAuxiliaryEqConcrete (TACLET)

• hideAuxiliaryEqConcrete2 (TACLET)

• ifEqualsInteger (TACLET)

• ifEqualsNull (TACLET)

• ifEqualsTRUE (TACLET)

• inDomain (PREDICATE)

• indexOfSeqConcatFirst (TACLET)

• indexOfSeqConcatSecond (TACLET)

• indexOfSeqSingleton (TACLET)

• indexOfSeqSub (TACLET)

• instanceof_known_dynamic_type (TACLET)

• instanceof_known_dynamic_type_2 (TACLET)

• instanceof_not_compatible (TACLET)

• instanceof_not_compatible_2 (TACLET)

• instanceof_not_compatible_3 (TACLET)

• instanceof_not_compatible_4 (TACLET)

• instanceof_not_compatible_5 (TACLET)

• instanceof_static_type (TACLET)

• instanceof_static_type_2 (TACLET)

• lenOfSeqDef (TACLET)

• lenOfSeqDefEQ (TACLET)

• lenOfSeqUpd (TACLET)

• loopScopeInvDia (TACLET)

• measuredBy (PREDICATE)

• measuredByCheck (TACLET)

• measuredByCheck (PREDICATE)

• measuredByCheckEmpty (TACLET)

• memsetEmpty (TACLET)

• observerDependency (TACLET)

• observerDependencyEQ (TACLET)

• prec (PREDICATE)

• precOfIntPair (TACLET)

• precOfPair (TACLET)

• precOfPairInt (TACLET)

• precOfSeq (TACLET)

• reachDependenciesStore (TACLET)

• reachDependenciesStoreEQ (TACLET)

• reachDependenciesStoreSimple (TACLET)

• reachDependenciesStoreSimpleEQ (TACLET)

• sameType (PREDICATE)

• sameTypeFalse (TACLET)

• sameTypeTrue (TACLET)

• schiffl_lemma_2 (TACLET)

• schiffl_thm_1 (TACLET)

• selectOfMemset (TACLET)

• selectOfMemsetEQ (TACLET)

• seqDefOfSeq (TACLET)

• seqDef_empty (TACLET)

• seqDef_induction_lower (TACLET)

• seqDef_induction_lower_concrete (TACLET)

• seqDef_induction_upper (TACLET)

• seqDef_induction_upper_concrete (TACLET)

• seqDef_lower_equals_upper (TACLET)

• seqDef_one_summand (TACLET)

• seqDef_split (TACLET)

• seqDef_split_in_three (TACLET)

• seqGetAlphaCast (TACLET)

• seqIndexOf (TACLET)

• seqNPerm (PREDICATE)

• seqNPermDefLeft (TACLET)

• seqNPermDefReplace (TACLET)

• seqNPermRange (TACLET)

• seqNPermRight (TACLET)

• seqOutsideValue (TACLET)

• seqPermCountsInt (TACLET)

• seqPermDef (TACLET)

• seqPermDefLeft (TACLET)

• seqPermExists (TACLET)

• seqPermForall (TACLET)

• seqSelfDefinition (TACLET)

• seqSelfDefinitionEQ2 (TACLET)

• seqnormalizeDef (TACLET)

• sequentialToParallel1 (TACLET)

• simplifySelectOfMemset (TACLET)

• simplifySelectOfMemsetEQ (TACLET)

• simplifyUpdate1 (TACLET)

• subSeqCompleteSeqDef (TACLET)

• subSeqCompleteSeqDefEQ (TACLET)

• subSeqHeadSeqDef (TACLET)

• subSeqHeadSeqDefEQ (TACLET)

• subSeqSingleton (TACLET)

• subSeqSingleton2 (TACLET)

• subSeqSingleton2EQ (TACLET)

• subSeqSingletonEQ (TACLET)

• subSeqTailEQL (TACLET)

• subSeqTailEQR (TACLET)

• subSeqTailL (TACLET)

• subSeqTailR (TACLET)

• threeBranchLoopScopeInvRuleDia (TACLET)

• wd (TRANSFORMER)

beta

• castedGetAny (TACLET)

• elementOfInfiniteUnion2Vars (TACLET)

• elementOfInfiniteUnion2VarsEQ (TACLET)

• narrowSelectArrayType (TACLET)

• narrowSelectType (TACLET)

• pullOutSelect (TACLET)

• selectOfAnon (TACLET)

• selectOfAnonEQ (TACLET)

• selectOfCreate (TACLET)

• selectOfCreateEQ (TACLET)

• selectOfMemset (TACLET)

• selectOfMemsetEQ (TACLET)

• selectOfStore (TACLET)

• selectOfStoreEQ (TACLET)

• simplifySelectOfAnon (TACLET)

• simplifySelectOfAnonEQ (TACLET)

• simplifySelectOfCreate (TACLET)

• simplifySelectOfCreateEQ (TACLET)

• simplifySelectOfMemset (TACLET)

• simplifySelectOfMemsetEQ (TACLET)

• simplifySelectOfStore (TACLET)

• simplifySelectOfStoreEQ (TACLET)

• wellFormedMemsetArrayPrimitive (TACLET)

• wellFormedStorePrimitive (TACLET)

• wellFormedStorePrimitiveArray (TACLET)

• wellFormedStorePrimitiveEQ (TACLET)

betaObj

• erroneous_class_has_no_initialized_sub_class (TACLET)

• superclasses_of_initialized_classes_are_initialized (TACLET)

• superclasses_of_initialized_classes_are_prepared (TACLET)

boolean

• Map (SORT)

• NonSingleton (SORT)

• PermissionOwnerList (SORT)

• all_bool (TACLET)

• allocateInstance (TACLET)

• allocateInstanceWithLength (TACLET)

• apply_eq_boolean_rigid (TACLET)

• apply_eq_boolean_rigid_2 (TACLET)

• assertSafe (TACLET)

• assertSafeWithMessage (TACLET)

• assignableDefinition (TACLET)

• assignment_to_primitive_array_component_transaction (TACLET)

• assignment_to_reference_array_component_transaction (TACLET)

• betaObj (SORT)

• boolean (SORT)

• castTrueImpliesOriginalTrue (TACLET)

• class_being_initialized_is_prepared (TACLET)

• class_erroneous_excludes_class_in_init (TACLET)

• class_initialized_excludes_class_init_in_progress (TACLET)

• createdInHeapToElementOf (TACLET)

• createdInHeapWithAllFields (TACLET)

• createdInHeapWithAllFieldsEQ (TACLET)

• createdInHeapWithArrayRange (TACLET)

• createdInHeapWithArrayRangeEQ (TACLET)

• createdInHeapWithSingleton (TACLET)

• createdInHeapWithSingletonEQ (TACLET)

• createdOnHeapImpliesCreatedOnPermissions (TACLET)

• defInDomainImpliesCreated (TACLET)

• definitionOfNewOnHeap (TACLET)

• elementOfFreshLocs (TACLET)

• erroneous_class_has_no_initialized_sub_class (TACLET)

• ex_bool (TACLET)

• exact_instance_definition_boolean (TACLET)

• ifthenelse_equals_1 (TACLET)

• ifthenelse_equals_2 (TACLET)

• initialized_class_is_not_erroneous (TACLET)

• initialized_class_is_prepared (TACLET)

• intersectAllFieldsFreshLocs (TACLET)

• maxAxiom (TACLET)

• minAxiom (TACLET)

• nullCreated (TACLET)

• onlyCreatedObjectsAreInLocSets (TACLET)

• onlyCreatedObjectsAreInLocSetsEQ (TACLET)

• onlyCreatedObjectsAreObserved (TACLET)

• onlyCreatedObjectsAreObservedInLocSets (TACLET)

• onlyCreatedObjectsAreObservedInLocSetsEQ (TACLET)

• onlyCreatedObjectsAreReferenced (TACLET)

• only_created_objects_are_reachable (TACLET)

• prod_one (TACLET)

• reach_does_not_depend_on_fresh_locs (TACLET)

• reach_does_not_depend_on_fresh_locs_EQ (TACLET)

• readPermissionAfterTransferRead (TACLET)

• readPermissionAfterTransferReadEQ (TACLET)

• readPermissionAfterTransferWrite (TACLET)

• readPermissionAfterTransferWriteEQ (TACLET)

• real (SORT)

• referencedObjectIsCreatedRight (TACLET)

• referencedObjectIsCreatedRightEQ (TACLET)

• selectCreatedOfAnon (TACLET)

• selectCreatedOfAnonAsFormula (TACLET)

• selectCreatedOfAnonAsFormulaEQ (TACLET)

• selectCreatedOfAnonEQ (TACLET)

• sum_zero (TACLET)

• superclasses_of_initialized_classes_are_initialized (TACLET)

• superclasses_of_initialized_classes_are_prepared (TACLET)

• transferPermission_empty (TACLET)

• transferPermission_slice (TACLET)

• wd_Heap_Reference (TACLET)

• wd_Heap_Reference_Array (TACLET)

• wd_Heap_Store (TACLET)

• wd_LocSet_AllElemsArr (TACLET)

• wd_LocSet_AllElemsArrLocsets (TACLET)

• wellFormedMemsetArrayObject (TACLET)

• wellFormedStoreArray (TACLET)

• wellFormedStoreObject (TACLET)

• wellFormedStoreObjectEQ (TACLET)

deltaObject

• accDefinition (TACLET)

• onlyCreatedObjectsAreObserved (TACLET)

• onlyCreatedObjectsAreReferenced (TACLET)

• referencedObjectIsCreatedRight (TACLET)

• referencedObjectIsCreatedRightEQ (TACLET)

• wellFormedMemsetArrayObject (TACLET)

• wellFormedStoreArray (TACLET)

• wellFormedStoreObject (TACLET)

• wellFormedStoreObjectEQ (TACLET)

double

• acosIsNaN (TACLET)

• acosRange (TACLET)

• asinIsNaN (TACLET)

• asineIsZero (TACLET)

• asineRange (TACLET)

• atan2IsNaN (TACLET)

• atan2Range (TACLET)

• atanIsNaN (TACLET)

• atanIsZero (TACLET)

• atanRange (TACLET)

• cosIsNaN (TACLET)

• cosIsNaNAlt (TACLET)

• cosIsNotNaN (TACLET)

• cosRange (TACLET)

• cosRange2 (TACLET)

• cosRangeAlt (TACLET)

• doubleIsInfinite (PREDICATE)

• doubleIsNaN (PREDICATE)

• doubleIsNegative (PREDICATE)

• doubleIsNice (PREDICATE)

• doubleIsNormal (PREDICATE)

• doubleIsPositive (PREDICATE)

• doubleIsSubnormal (PREDICATE)

• doubleIsZero (PREDICATE)

• eqDouble (PREDICATE)

• expIsInfinite (TACLET)

• expIsNaN (TACLET)

• expIsZero (TACLET)

• geqDouble (PREDICATE)

• gtDouble (PREDICATE)

• java.lang.Math (SORT)

• leqDouble (PREDICATE)

• ltDouble (PREDICATE)

• niceDouble (TACLET)

• powIsInfinite1 (TACLET)

• powIsInfinite2 (TACLET)

• powIsNaN1 (TACLET)

• powIsNaN2 (TACLET)

• powIsNaN3 (TACLET)

• powIsNotNaN (TACLET)

• powIsOne (TACLET)

• powIsZero1 (TACLET)

• powIsZero2 (TACLET)

• sinIsNaN (TACLET)

• sinIsNotNaN (TACLET)

• sinRange2 (TACLET)

• sinRange3 (TACLET)

• sineIsNaNAlt (TACLET)

• sineIsZero (TACLET)

• sineRange (TACLET)

• sineRangeAlt (TACLET)

• sqrtIsInfinite (TACLET)

• sqrtIsNaN (TACLET)

• sqrtIsNotNaN (TACLET)

• sqrtIsSmaller (TACLET)

• sqrtIsZero (TACLET)

• tanIsNaN (TACLET)

• tanIsZero (TACLET)

float

• castLongToFloatAddition2 (TACLET)

• eqFloat (PREDICATE)

• floatIsInfinite (PREDICATE)

• floatIsNaN (PREDICATE)

• floatIsNegative (PREDICATE)

• floatIsNice (PREDICATE)

• floatIsNormal (PREDICATE)

• floatIsPositive (PREDICATE)

• floatIsSubnormal (PREDICATE)

• floatIsZero (PREDICATE)

• geqFloat (PREDICATE)

• gtFloat (PREDICATE)

• intLongToFloatAddition1 (TACLET)

• intToFloatAddition (TACLET)

• java.lang.Math (SORT)

• leqFloat (PREDICATE)

• ltFloat (PREDICATE)

• niceFloat (TACLET)

• wideningCastIntToFloat (TACLET)

• wideningCastLongToFloat (TACLET)

fp

• double (SORT)

• float (SORT)

int

• LocSet (SORT)

• NonSingleton (SORT)

• PermissionOwnerList (SORT)

• RegEx (SORT)

• alphaObj (SORT)

• andJIntDef (TACLET)

• array2seqDef (TACLET)

• assignment_to_primitive_array_component_transaction (TACLET)

• assignment_to_reference_array_component_transaction (TACLET)

• binaryAndOne (TACLET)

• binaryAndSymm (TACLET)

• binaryAndZeroLeft (TACLET)

• binaryAndZeroRight (TACLET)

• binaryOrGte (TACLET)

• binaryOrInInt (TACLET)

• binaryOrNeutralLeft (TACLET)

• binaryOrNeutralRight (TACLET)

• binaryOrSign (TACLET)

• bprod_find (TACLET)

• bprod_split (TACLET)

• bsum_equal_except_one_index (TACLET)

• bsum_positive_lower_bound_element (TACLET)

• bsum_split (TACLET)

• cancel_equation (TACLET)

• cancel_gtNeg (TACLET)

• cancel_gtPos (TACLET)

• castedGetAny (TACLET)

• charListHeader (FILE)

• checkPermissionOwner (PREDICATE)

• checkPermissionOwner_empty (TACLET)

• checkPermissionOwner_nonempty (TACLET)

• concatRepeatContraction1 (TACLET)

• concatRepeatContraction2 (TACLET)

• concatRepeatContraction2Sym (TACLET)

• concatRepeatContraction3 (TACLET)

• concatRepeatContraction3Sym (TACLET)

• contains (TACLET)

• containsAxiomAntec (TACLET)

• containsAxiomSucc (TACLET)

• createdInHeapWithArrayRange (TACLET)

• createdInHeapWithArrayRangeEQ (TACLET)

• defIsFinite (TACLET)

• defOfEmpty (TACLET)

• defOfSeqConcat (TACLET)

• defOfSeqNPermInv (TACLET)

• defOfSeqRemove (TACLET)

• defOfSeqReverse (TACLET)

• defOfSeqSingleton (TACLET)

• defOfSeqSub (TACLET)

• defOfSeqSwap (TACLET)

• defOfSeqUpd (TACLET)

• defSeq2Map (TACLET)

• definitionAllElementsOfArray (TACLET)

• definitionAllElementsOfArray2 (TACLET)

• definitionAllElementsOfArrayLocsets (TACLET)

• definitionOfNewOnHeap (TACLET)

• definitionOfObjectIsomorphic (TACLET)

• definitionOfObjectsIsomorphic (TACLET)

• definitionOfSameTypes (TACLET)

• definitionSeqdefWorkaround (TACLET)

• definitionSeqdefWorkaround2 (TACLET)

• disjointArrayRangeAllFields1 (TACLET)

• disjointArrayRangeAllFields2 (TACLET)

• disjointArrayRanges (TACLET)

• disjointInfiniteUnion (TACLET)

• disjointInfiniteUnion_2 (TACLET)

• divAddMultDenom (TACLET)

• divGreatestDNeg (TACLET)

• divGreatestDPos (TACLET)

• divIncreasingNeg (TACLET)

• divIncreasingPos (TACLET)

• divLeastDNeg (TACLET)

• divLeastDPos (TACLET)

• div_exists (TACLET)

• div_unique1 (TACLET)

• div_unique2 (TACLET)

• elementOfArrayRange (TACLET)

• elementOfArrayRangeConcrete (TACLET)

• elementOfArrayRangeEQ (TACLET)

• eqSameSeq (TACLET)

• eqSeqDef (TACLET)

• eqSeqDef2 (TACLET)

• eqSeqReverse (TACLET)

• eqSeqReverse2 (TACLET)

• equalityToSeqGetAndSeqLen (TACLET)

• equalityToSeqGetAndSeqLenLeft (TACLET)

• equalityToSeqGetAndSeqLenRight (TACLET)

• exact_instance_definition_int (TACLET)

• geq (PREDICATE)

• getAnyOfArray2seq (TACLET)

• getAnyOfNPermInv (TACLET)

• getJavaCardTransient (TACLET)

• getOfArray2seq (TACLET)

• getOfNPermInv (TACLET)

• getOfRemoveAny (TACLET)

• getOfRemoveAnyConcrete1 (TACLET)

• getOfRemoveAnyConcrete2 (TACLET)

• getOfRemoveInt (TACLET)

• getOfSeq2Map (TACLET)

• getOfSeqConcat (TACLET)

• getOfSeqConcatEQ (TACLET)

• getOfSeqDef (TACLET)

• getOfSeqDefEQ (TACLET)

• getOfSeqReverse (TACLET)

• getOfSeqReverseEQ (TACLET)

• getOfSeqSingleton (TACLET)

• getOfSeqSingletonEQ (TACLET)

• getOfSeqSub (TACLET)

• getOfSeqSubEQ (TACLET)

• getOfSeqUpd (TACLET)

• getOfSwap (TACLET)

• gt (PREDICATE)

• inByte (PREDICATE)

• inChar (PREDICATE)

• inDomainOfSeq2Map (TACLET)

• inInt (PREDICATE)

• inLong (PREDICATE)

• inRangeByte (PREDICATE)

• inRangeChar (PREDICATE)

• inRangeInt (PREDICATE)

• inRangeLong (PREDICATE)

• inRangeShort (PREDICATE)

• inShort (PREDICATE)

• indexOf (TACLET)

• indexOfSeqConcatFirst (TACLET)

• indexOfSeqConcatSecond (TACLET)

• indexOfSeqSub (TACLET)

• indexOfStr (TACLET)

• insertPermissionOwner (TACLET)

• javaShiftLeftIntDef (TACLET)

• javaShiftLeftLongDef (TACLET)

• javaShiftRightIntDef (TACLET)

• javaShiftRightLongDef (TACLET)

• jdivAddMultDenom (TACLET)

• jdivMultDenom1 (TACLET)

• jdivMultDenom2 (TACLET)

• jdiv_uniqueNegNeg (TACLET)

• jdiv_uniqueNegPos (TACLET)

• jdiv_uniquePosNeg (TACLET)

• jdiv_uniquePosPos (TACLET)

• jmodAddMultDenomZero (TACLET)

• jmodAltZero (TACLET)

• jmodDivisible (TACLET)

• jmodDivisibleRep (TACLET)

• jmodUnique1 (TACLET)

• jmodUnique2 (TACLET)

• jmodjmod (TACLET)

• lastIndexOf (TACLET)

• lastIndexOfStr (TACLET)

• lenOfRemove (TACLET)

• lenOfSeqDef (TACLET)

• lenOfSeqDefEQ (TACLET)

• lenOfSeqSub (TACLET)

• lenOfSeqSubEQ (TACLET)

• lenOfSeqUpd (TACLET)

• lenOfSwap (TACLET)

• lengthReplace (TACLET)

• lengthReplaceEQ (TACLET)

• leq (PREDICATE)

• logPowIdentity (TACLET)

• logProdIdentity (TACLET)

• logProdIdentityConcrete (TACLET)

• lt (PREDICATE)

• mapSize (FILE)

• maxAxiom (TACLET)

• minAxiom (TACLET)

• mod_homoEq (TACLET)

• moduloByteFixpointInline (TACLET)

• moduloCharFixpointInline (TACLET)

• moduloIntFixpointInline (TACLET)

• moduloLongFixpointInline (TACLET)

• moduloShortFixpointInline (TACLET)

• narrowSelectArrayType (TACLET)

• nonNull (PREDICATE)

• nonNull (TACLET)

• nullIsNotNonNull (TACLET)

• only_created_objects_are_reachable (TACLET)

• orJIntDef (TACLET)

• orJintInInt (TACLET)

• powDef (TACLET)

• precOfInt (TACLET)

• precOfIntPair (TACLET)

• precOfPairInt (TACLET)

• precOfSeq (TACLET)

• reach (PREDICATE)

• reachAddOne (TACLET)

• reachAddOne2 (TACLET)

• reachDefinition (TACLET)

• reachDependenciesAnon (TACLET)

• reachDependenciesAnonCoarse (TACLET)

• reachDependenciesStore (TACLET)

• reachDependenciesStoreEQ (TACLET)

• reachDependenciesStoreSimple (TACLET)

• reachDependenciesStoreSimpleEQ (TACLET)

• reachDoesNotDependOnCreatedness (TACLET)

• reachEndOfUniquePath (TACLET)

• reachEndOfUniquePath2 (TACLET)

• reachNull (TACLET)

• reachNull2 (TACLET)

• reachUniquePathSameSteps (TACLET)

• reach_does_not_depend_on_fresh_locs (TACLET)

• reach_does_not_depend_on_fresh_locs_EQ (TACLET)

• real (SORT)

• regExConcatAxiom (TACLET)

• regExConcatRepeatLeft (TACLET)

• regExConcatRepeatRight (TACLET)

• removeZeros (TACLET)

• repeatAxiom (TACLET)

• repeatMatchEmpty (TACLET)

• repeatPlusAxiom (TACLET)

• repeatRepeatContraction (TACLET)

• repeatStarAxiom (TACLET)

• replaceConcat (TACLET)

• replaceCons (TACLET)

• replaceDef (TACLET)

• replaceEmpty (TACLET)

• replaceSingleton (TACLET)

• replaceSubstring (TACLET)

• schiffl_lemma_2 (TACLET)

• schiffl_thm_1 (TACLET)

• seqDefOfSeq (TACLET)

• seqDef_empty (TACLET)

• seqDef_induction_lower (TACLET)

• seqDef_induction_lower_concrete (TACLET)

• seqDef_induction_upper (TACLET)

• seqDef_induction_upper_concrete (TACLET)

• seqDef_lower_equals_upper (TACLET)

• seqDef_one_summand (TACLET)

• seqDef_split (TACLET)

• seqDef_split_in_three (TACLET)

• seqGetAlphaCast (TACLET)

• seqGetSInvS (TACLET)

• seqIndexOf (TACLET)

• seqNPerm (PREDICATE)

• seqNPermComp (TACLET)

• seqNPermDefLeft (TACLET)

• seqNPermDefReplace (TACLET)

• seqNPermInjective (TACLET)

• seqNPermRange (TACLET)

• seqNPermRight (TACLET)

• seqNPermSingleton (TACLET)

• seqNPermSwapNPerm (TACLET)

• seqOutsideValue (TACLET)

• seqPermCountsInt (TACLET)

• seqPermDef (TACLET)

• seqPermDefLeft (TACLET)

• seqPermExists (TACLET)

• seqPermForall (TACLET)

• seqPermFromSwap (TACLET)

• seqSelfDefinition (TACLET)

• seqSelfDefinitionEQ2 (TACLET)

• seqSwapPreservesSeqPerm (TACLET)

• seqSwapPreservesSeqPermEQ (TACLET)

• seqnormalizeDef (TACLET)

• shiftLeftDef (TACLET)

• shiftLeftPositiveShiftDef (TACLET)

• shiftRightDef (TACLET)

• shiftRightPositiveShiftDef (TACLET)

• subSeqCompleteSeqDef (TACLET)

• subSeqCompleteSeqDefEQ (TACLET)

• subSeqConcat (TACLET)

• subSeqConcatEQ (TACLET)

• subSeqEmpty (TACLET)

• subSeqHeadSeqDef (TACLET)

• subSeqHeadSeqDefEQ (TACLET)

• subSeqSingleton2 (TACLET)

• subSeqSingleton2EQ (TACLET)

• subSeqTailEQL (TACLET)

• subSeqTailEQR (TACLET)

• substringSubstring (TACLET)

• substringSubstring2 (TACLET)

• transferPermission_empty (TACLET)

• transferPermission_slice (TACLET)

• unsignedShiftRightJintDef (TACLET)

• wellFormedMemsetArrayObject (TACLET)

• wellFormedMemsetArrayPrimitive (TACLET)

• wellFormedStoreArray (TACLET)

• wellFormedStorePrimitiveArray (TACLET)

• wellOrderLeqInt (PREDICATE)

• xorJIntDef (TACLET)

java.lang.Object

• abortJavaCardTransactionBox (TACLET)

• abortJavaCardTransactionDiamond (TACLET)

• allocateInstance (TACLET)

• allocateInstanceWithLength (TACLET)

• alphaObj (SORT)

• assertSafe (TACLET)

• assertSafeWithMessage (TACLET)

• assignableDefinition (TACLET)

• assignment_to_primitive_array_component_transaction (TACLET)

• assignment_to_reference_array_component_transaction (TACLET)

• createdInHeapToElementOf (TACLET)

• createdInHeapWithAllFields (TACLET)

• createdInHeapWithAllFieldsEQ (TACLET)

• createdInHeapWithArrayRange (TACLET)

• createdInHeapWithArrayRangeEQ (TACLET)

• createdInHeapWithSingleton (TACLET)

• createdInHeapWithSingletonEQ (TACLET)

• createdOnHeapImpliesCreatedOnPermissions (TACLET)

• defInDomainImpliesCreated (TACLET)

• definitionOfNewOnHeap (TACLET)

• definitionOfObjectIsomorphic (TACLET)

• definitionOfObjectsIsomorphic (TACLET)

• deltaObject (SORT)

• elementOfFreshLocs (TACLET)

• getJavaCardTransient (TACLET)

• intersectAllFieldsFreshLocs (TACLET)

• java.io.Serializable (SORT)

• java.lang.Cloneable (SORT)

• java.lang.Math (SORT)

• nullCreated (TACLET)

• onlyCreatedObjectsAreInLocSets (TACLET)

• onlyCreatedObjectsAreInLocSetsEQ (TACLET)

• onlyCreatedObjectsAreObserved (TACLET)

• onlyCreatedObjectsAreObservedInLocSets (TACLET)

• onlyCreatedObjectsAreObservedInLocSetsEQ (TACLET)

• onlyCreatedObjectsAreReferenced (TACLET)

• only_created_objects_are_reachable (TACLET)

• reach_does_not_depend_on_fresh_locs (TACLET)

• reach_does_not_depend_on_fresh_locs_EQ (TACLET)

• referencedObjectIsCreatedRight (TACLET)

• referencedObjectIsCreatedRightEQ (TACLET)

• selectCreatedOfAnon (TACLET)

• selectCreatedOfAnonAsFormula (TACLET)

• selectCreatedOfAnonAsFormulaEQ (TACLET)

• selectCreatedOfAnonEQ (TACLET)

• selectOfAnon (TACLET)

• selectOfAnonEQ (TACLET)

• selectOfCreate (TACLET)

• selectOfCreateEQ (TACLET)

• selectOfMemset (TACLET)

• selectOfMemsetEQ (TACLET)

• selectOfStore (TACLET)

• selectOfStoreEQ (TACLET)

• setJavaCardTransient (TACLET)

• simplifySelectOfAnon (TACLET)

• simplifySelectOfAnonEQ (TACLET)

• simplifySelectOfCreate (TACLET)

• simplifySelectOfCreateEQ (TACLET)

• simplifySelectOfMemset (TACLET)

• simplifySelectOfMemsetEQ (TACLET)

• simplifySelectOfStore (TACLET)

• simplifySelectOfStoreEQ (TACLET)

• wd_Heap_Reference (TACLET)

• wd_Heap_Reference_Array (TACLET)

• wd_Heap_Reference_Created (TACLET)

• wd_Heap_Store (TACLET)

• wd_LocSet_AllElemsArr (TACLET)

• wd_LocSet_AllElemsArrLocsets (TACLET)

• wellFormedMemsetArrayObject (TACLET)

• wellFormedStoreArray (TACLET)

• wellFormedStoreObject (TACLET)

• wellFormedStoreObjectEQ (TACLET)

numbers

• binaryAnd_literals (TACLET)

• binaryOr_literals (TACLET)

• binaryXOr_literals (TACLET)

• equalCharacters (TACLET)

• ifEqualsInteger (TACLET)

• java.lang.Math (SORT)

• real (SORT)

• shiftleft_literals (TACLET)

• shiftright_literals (TACLET)

• translate0 (TACLET)

• translate1 (TACLET)

• translate2 (TACLET)

• translate3 (TACLET)

• translate4 (TACLET)

• translate5 (TACLET)

• translate6 (TACLET)

• translate7 (TACLET)

• translate8 (TACLET)

• translate9 (TACLET)

• translateNegLit (TACLET)

acc

• acc (PREDICATE)

arrayStoreValid

• arrayStoreValid (PREDICATE)

assignable

• assignable (PREDICATE)

checkPermissionOwner

• checkPermissionOwner (PREDICATE)

clContains

• clContains (PREDICATE)

clEndsWith

• clEndsWith (PREDICATE)

clStartsWith

• clStartsWith (PREDICATE)

createdInHeap

• createdInHeap (PREDICATE)

disjoint

• disjoint (PREDICATE)

doubleIsInfinite

• doubleIsInfinite (PREDICATE)

doubleIsNaN

• doubleIsNaN (PREDICATE)

doubleIsNegative

• doubleIsNegative (PREDICATE)

doubleIsNice

• doubleIsNice (PREDICATE)

doubleIsNormal

• doubleIsNormal (PREDICATE)

doubleIsPositive

• doubleIsPositive (PREDICATE)

doubleIsSubnormal

• doubleIsSubnormal (PREDICATE)

doubleIsZero

• doubleIsZero (PREDICATE)

elementOf

• elementOf (PREDICATE)

eqDouble

• eqDouble (PREDICATE)

eqFloat

• eqFloat (PREDICATE)

floatIsInfinite

• floatIsInfinite (PREDICATE)

floatIsNaN

• floatIsNaN (PREDICATE)

floatIsNegative

• floatIsNegative (PREDICATE)

floatIsNice

• floatIsNice (PREDICATE)

floatIsNormal

• floatIsNormal (PREDICATE)

floatIsPositive

• floatIsPositive (PREDICATE)

floatIsSubnormal

• floatIsSubnormal (PREDICATE)

floatIsZero

• floatIsZero (PREDICATE)

geq

• geq (PREDICATE)

geqDouble

• geqDouble (PREDICATE)

geqFloat

• geqFloat (PREDICATE)

gt

• gt (PREDICATE)

gtDouble

• gtDouble (PREDICATE)

gtFloat

• gtFloat (PREDICATE)

inByte

• inByte (PREDICATE)

inChar

• inChar (PREDICATE)

inDomain

• inDomain (PREDICATE)

inDomainImpliesCreated

• inDomainImpliesCreated (PREDICATE)

inInt

• inInt (PREDICATE)

inLong

• inLong (PREDICATE)

inRangeByte

• inRangeByte (PREDICATE)

inRangeChar

• inRangeChar (PREDICATE)

inRangeInt

• inRangeInt (PREDICATE)

inRangeLong

• inRangeLong (PREDICATE)

inRangeShort

• inRangeShort (PREDICATE)

inShort

• inShort (PREDICATE)

isFinite

• isFinite (PREDICATE)

leq

• leq (PREDICATE)

leqDouble

• leqDouble (PREDICATE)

leqFloat

• leqFloat (PREDICATE)

lt

• lt (PREDICATE)

ltDouble

• ltDouble (PREDICATE)

ltFloat

• ltFloat (PREDICATE)

match

• match (PREDICATE)

measuredBy

• measuredBy (PREDICATE)

measuredByCheck

• measuredByCheck (PREDICATE)

measuredByEmpty

• measuredByEmpty (PREDICATE)

newObjectsIsomorphic

• newObjectsIsomorphic (PREDICATE)

newOnHeap

• newOnHeap (PREDICATE)

nonEmptyPermission

• nonEmptyPermission (PREDICATE)

nonNull

• nonNull (PREDICATE)

objectIsomorphic

• objectIsomorphic (PREDICATE)

objectsIsomorphic

• objectsIsomorphic (PREDICATE)

permissionsFor

• permissionsFor (PREDICATE)

prec

• prec (PREDICATE)

reach

• reach (PREDICATE)

readPermission

• readPermission (PREDICATE)

readPermissionObject

• readPermissionObject (PREDICATE)

readPermissionOwe

• readPermissionOwe (PREDICATE)

readPermissionOwe2

• readPermissionOwe2 (PREDICATE)

sameType

• sameType (PREDICATE)

sameTypes

• sameTypes (PREDICATE)

seqNPerm

• seqNPerm (PREDICATE)

seqPerm

• seqPerm (PREDICATE)

ssubsort

• ssubsort (PREDICATE)

subset

• subset (PREDICATE)

twoPermissions

• twoPermissions (PREDICATE)

wellFormed

• wellFormed (PREDICATE)

wellOrderLeqInt

• wellOrderLeqInt (PREDICATE)

writePermission

• writePermission (PREDICATE)

writePermissionObject

• writePermissionObject (PREDICATE)

#

• real (SORT)

0

• real (SORT)

1

• real (SORT)

2

• real (SORT)

3

• real (SORT)

4

• real (SORT)

5

• real (SORT)

6

• real (SORT)

7

• real (SORT)

8

• real (SORT)

9

• real (SORT)

C

• real (SORT)

DFP

• java.lang.Math (SORT)

FALSE

• boolean (SORT)

FP

• java.lang.Math (SORT)

TRUE

• boolean (SORT)

Z

• real (SORT)

absDouble

• java.lang.Math (SORT)

absFloat

• java.lang.Math (SORT)

acosDouble

• java.lang.Math (SORT)

add

• real (SORT)

addDouble

• java.lang.Math (SORT)

addFloat

• java.lang.Math (SORT)

addJint

• real (SORT)

addJlong

• real (SORT)

allElementsOfArray

• LocSet (SORT)

allElementsOfArrayLocsets

• LocSet (SORT)

allFields

• LocSet (SORT)

allLocs

• LocSet (SORT)

allObjects

• LocSet (SORT)

alt

• RegEx (SORT)

andJint

• real (SORT)

andJlong

• real (SORT)

anon

• alphaObj (SORT)

anySORT

• alphSub (SORT)

arr

• alphaObj (SORT)

array2seq

• seqNPerm (PREDICATE)

arrayRange

• LocSet (SORT)

asinDouble

• java.lang.Math (SORT)

atan2Double

• java.lang.Math (SORT)

atanDouble

• java.lang.Math (SORT)

atom

• Free (SORT)

binaryAnd

• real (SORT)

binaryOr

• real (SORT)

binaryXOr

• real (SORT)

bitwiseNegateJint

• real (SORT)

bitwiseNegateJlong

• real (SORT)

bprod

• real (SORT)

bsum

• real (SORT)

byte_HALFRANGE

• real (SORT)

byte_MAX

• real (SORT)

byte_MIN

• real (SORT)

byte_RANGE

• real (SORT)

char_MAX

• real (SORT)

char_MIN

• real (SORT)

char_RANGE

• real (SORT)

checkedAddInt

• real (SORT)

checkedAddLong

• real (SORT)

checkedBitwiseAndInt

• real (SORT)

checkedBitwiseAndLong

• real (SORT)

checkedBitwiseNegateInt

• real (SORT)

checkedBitwiseNegateLong

• real (SORT)

checkedBitwiseOrInt

• real (SORT)

checkedBitwiseOrLong

• real (SORT)

checkedBitwiseXOrInt

• real (SORT)

checkedBitwiseXOrLong

• real (SORT)

checkedDivInt

• real (SORT)

checkedDivLong

• real (SORT)

checkedMulInt

• real (SORT)

checkedMulLong

• real (SORT)

checkedShiftLeftInt

• real (SORT)

checkedShiftLeftLong

• real (SORT)

checkedShiftRightInt

• real (SORT)

checkedShiftRightLong

• real (SORT)

checkedSubInt

• real (SORT)

checkedSubLong

• real (SORT)

checkedUnaryMinusInt

• real (SORT)

checkedUnaryMinusLong

• real (SORT)

checkedUnsignedShiftRightInt

• real (SORT)

checkedUnsignedShiftRightLong

• real (SORT)

clHashCode

• charListHeader (FILE)

clIndexOfChar

• charListHeader (FILE)

clIndexOfCl

• charListHeader (FILE)

clLastIndexOfChar

• charListHeader (FILE)

clLastIndexOfCl

• charListHeader (FILE)

clRemoveZeros

• charListHeader (FILE)

clReplace

• charListHeader (FILE)

clTranslateInt

• charListHeader (FILE)

consPermissionOwnerList

• PermissionOwnerList (SORT)

cosDouble

• java.lang.Math (SORT)

create

• alphaObj (SORT)

currentThread

• PermissionOwnerList (SORT)

div

• real (SORT)

divDouble

• java.lang.Math (SORT)

divFloat

• java.lang.Math (SORT)

divJint

• real (SORT)

divJlong

• real (SORT)

empty

• LocSet (SORT)

emptyPermission

• PermissionOwnerList (SORT)

emptyPermissionOwnerList

• PermissionOwnerList (SORT)

expDouble

• java.lang.Math (SORT)

first

• Pair (SORT)

freshLocs

• LocSet (SORT)

index

• real (SORT)

infiniteUnion

• LocSet (SORT)

initFullPermission

• PermissionOwnerList (SORT)

insertPermissionOwner

• PermissionOwnerList (SORT)

int_HALFRANGE

• real (SORT)

int_MAX

• real (SORT)

int_MIN

• real (SORT)

int_RANGE

• real (SORT)

intersect

• LocSet (SORT)

javaAddDouble

• java.lang.Math (SORT)

javaAddDoubleForbiddenResult

• java.lang.Math (SORT)

javaAddFloat

• java.lang.Math (SORT)

javaAddFloatForbiddenResult

• java.lang.Math (SORT)

javaAddInt

• real (SORT)

javaAddIntOverFlow

• real (SORT)

javaAddLong

• real (SORT)

javaAddLongOverFlow

• real (SORT)

javaBitwiseAndInt

• real (SORT)

javaBitwiseAndLong

• real (SORT)

javaBitwiseNegateInt

• real (SORT)

javaBitwiseNegateLong

• real (SORT)

javaBitwiseOrInt

• real (SORT)

javaBitwiseOrIntOverFlow

• real (SORT)

javaBitwiseOrLong

• real (SORT)

javaBitwiseXOrInt

• real (SORT)

javaBitwiseXOrLong

• real (SORT)

javaCastByte

• real (SORT)

javaCastByteOverFlow

• real (SORT)

javaCastChar

• real (SORT)

javaCastCharOverFlow

• real (SORT)

javaCastInt

• real (SORT)

javaCastIntOverFlow

• real (SORT)

javaCastLong

• real (SORT)

javaCastLongOverFlow

• real (SORT)

javaCastShort

• real (SORT)

javaCastShortOverFlow

• real (SORT)

javaDivDouble

• java.lang.Math (SORT)

javaDivDoubleForbiddenResult

• java.lang.Math (SORT)

javaDivFloat

• java.lang.Math (SORT)

javaDivFloatForbiddenResult

• java.lang.Math (SORT)

javaDivInt

• real (SORT)

javaDivIntOverFlow

• real (SORT)

javaDivLong

• real (SORT)

javaDivLongOverFlow

• real (SORT)

javaMaxDouble

• java.lang.Math (SORT)

javaMaxFloat

• java.lang.Math (SORT)

javaMinDouble

• java.lang.Math (SORT)

javaMinFloat

• java.lang.Math (SORT)

javaMod

• real (SORT)

javaModDouble

• java.lang.Math (SORT)

javaModFloat

• java.lang.Math (SORT)

javaModOverFlow

• real (SORT)

javaMulDouble

• java.lang.Math (SORT)

javaMulDoubleForbiddenResult

• java.lang.Math (SORT)

javaMulFloat

• java.lang.Math (SORT)

javaMulFloatForbiddenResult

• java.lang.Math (SORT)

javaMulInt

• real (SORT)

javaMulIntOverFlow

• real (SORT)

javaMulLong

• real (SORT)

javaMulLongOverFlow

• real (SORT)

javaShiftLeftInt

• real (SORT)

javaShiftLeftLong

• real (SORT)

javaShiftRightInt

• real (SORT)

javaShiftRightLong

• real (SORT)

javaSubDouble

• java.lang.Math (SORT)

javaSubDoubleForbiddenResult

• java.lang.Math (SORT)

javaSubFloat

• java.lang.Math (SORT)

javaSubFloatForbiddenResult

• java.lang.Math (SORT)

javaSubInt

• real (SORT)

javaSubIntOverFlow

• real (SORT)

javaSubLong

• real (SORT)

javaSubLongOverFlow

• real (SORT)

javaUnaryMinusDouble

• java.lang.Math (SORT)

javaUnaryMinusFloat

• java.lang.Math (SORT)

javaUnaryMinusInt

• real (SORT)

javaUnaryMinusIntOverFlow

• real (SORT)

javaUnaryMinusLong

• real (SORT)

javaUnaryMinusLongOverFlow

• real (SORT)

javaUnsignedShiftRightInt

• real (SORT)

javaUnsignedShiftRightLong

• real (SORT)

javaUnsignedShiftRightOverFlow

• real (SORT)

jdiv

• real (SORT)

jmod

• real (SORT)

length

• alphaObj (SORT)

log

• real (SORT)

long_HALFRANGE

• real (SORT)

long_MAX

• real (SORT)

long_MIN

• real (SORT)

long_RANGE

• real (SORT)

mapEmpty

• Map (SORT)

mapForeach

• Map (SORT)

mapGet

• Map (SORT)

mapOverride

• Map (SORT)

mapRemove

• Map (SORT)

mapSingleton

• Map (SORT)

mapSize

• mapSize (FILE)

mapUndef

• Map (SORT)

mapUpdate

• Map (SORT)

max

• real (SORT)

memset

• alphaObj (SORT)

min

• real (SORT)

mod

• real (SORT)

modJint

• real (SORT)

modJlong

• real (SORT)

moduloByte

• real (SORT)

moduloChar

• real (SORT)

moduloInt

• real (SORT)

moduloLong

• real (SORT)

moduloShort

• real (SORT)

mul

• real (SORT)

mulDouble

• java.lang.Math (SORT)

mulFloat

• java.lang.Math (SORT)

mulJint

• real (SORT)

mulJlong

• real (SORT)

neg

• real (SORT)

negDouble

• java.lang.Math (SORT)

negFloat

• java.lang.Math (SORT)

neglit

• real (SORT)

null

• alphaObj (SORT)

opt

• RegEx (SORT)

orJint

• real (SORT)

orJlong

• real (SORT)

owner1

• PermissionOwnerList (SORT)

owner2

• PermissionOwnerList (SORT)

owner3

• PermissionOwnerList (SORT)

owner4

• PermissionOwnerList (SORT)

pair

• Pair (SORT)

pow

• real (SORT)

powDouble

• java.lang.Math (SORT)

prod

• real (SORT)

regEx

• RegEx (SORT)

regExConcat

• RegEx (SORT)

repeat

• RegEx (SORT)

repeatPlus

• RegEx (SORT)

repeatStar

• RegEx (SORT)

returnPermission

• PermissionOwnerList (SORT)

returnPermissionOwner

• PermissionOwnerList (SORT)

second

• Pair (SORT)

seq2map

• Map (SORT)

seqConcat

• seqNPerm (PREDICATE)

seqDef

• seqNPerm (PREDICATE)

seqEmpty

• seqNPerm (PREDICATE)

seqGetOutside

• seqNPerm (PREDICATE)

seqIndexOf

• seqNPerm (PREDICATE)

seqLen

• seqNPerm (PREDICATE)

seqNPermInv

• seqNPerm (PREDICATE)

seqRemove

• seqNPerm (PREDICATE)

seqReverse

• seqNPerm (PREDICATE)

seqSingleton

• seqNPerm (PREDICATE)

seqSub

• seqNPerm (PREDICATE)

seqSwap

• seqNPerm (PREDICATE)

seqUpd

• seqNPerm (PREDICATE)

seq_def_workaround

• seqNPerm (PREDICATE)

seq_def_workaround2

• seqNPerm (PREDICATE)

setMinus

• LocSet (SORT)

shiftleft

• real (SORT)

shiftleftJint

• real (SORT)

shiftleftJlong

• real (SORT)

shiftleftPositiveShift

• real (SORT)

shiftright

• real (SORT)

shiftrightJint

• real (SORT)

shiftrightJlong

• real (SORT)

shiftrightPositiveShift

• real (SORT)

short_HALFRANGE

• real (SORT)

short_MAX

• real (SORT)

short_MIN

• real (SORT)

short_RANGE

• real (SORT)

sinDouble

• java.lang.Math (SORT)

singleton

• LocSet (SORT)

slice

• PermissionOwnerList (SORT)

slice1

• PermissionOwnerList (SORT)

slice2

• PermissionOwnerList (SORT)

sqrtDouble

• java.lang.Math (SORT)

store

• alphaObj (SORT)

sub

• real (SORT)

subDouble

• java.lang.Math (SORT)

subFloat

• java.lang.Math (SORT)

subJint

• real (SORT)

subJlong

• real (SORT)

sum

• real (SORT)

tanDouble

• java.lang.Math (SORT)

transferPermission

• PermissionOwnerList (SORT)

unaryMinusJint

• real (SORT)

unaryMinusJlong

• real (SORT)

undefinedLog

• real (SORT)

undefinedPow

• real (SORT)

union

• LocSet (SORT)

unsignedshift

• real (SORT)

unsignedshiftrightJint

• real (SORT)

unsignedshiftrightJlong

• real (SORT)

values

• seqNPerm (PREDICATE)

xorJint

• real (SORT)

xorJlong

• real (SORT)

F

• F (TRANSFORMER)

T

• T (TRANSFORMER)

WD

• WD (TRANSFORMER)

wd

• wd (TRANSFORMER)

alpha

• andLeft (TACLET)

• impRight (TACLET)

• notLeft (TACLET)

• notRight (TACLET)

• orRight (TACLET)

apply_auxiliary_eq

• applyEqReverse (TACLET)

apply_equations

• applyEq (TACLET)

• applyEqRigid (TACLET)

• apply_eq_boolean (TACLET)

• apply_eq_boolean_2 (TACLET)

• apply_eq_boolean_rigid (TACLET)

• apply_eq_boolean_rigid_2 (TACLET)

• apply_eq_monomials (TACLET)

• apply_eq_monomials_rigid (TACLET)

apply_equations_andOr

• applyEq_and_gen0 (TACLET)

• applyEq_and_gen1 (TACLET)

• applyEq_and_gen2 (TACLET)

• applyEq_and_gen3 (TACLET)

• applyEq_and_int0 (TACLET)

• applyEq_and_int1 (TACLET)

• applyEq_and_int2 (TACLET)

• applyEq_and_int3 (TACLET)

• applyEq_and_int4 (TACLET)

• applyEq_and_int5 (TACLET)

• applyEq_and_int6 (TACLET)

• applyEq_and_int7 (TACLET)

• applyEq_or_gen0 (TACLET)

• applyEq_or_gen1 (TACLET)

• applyEq_or_gen2 (TACLET)

• applyEq_or_gen3 (TACLET)

• applyEq_or_int0 (TACLET)

• applyEq_or_int1 (TACLET)

• applyEq_or_int2 (TACLET)

• applyEq_or_int3 (TACLET)

• applyEq_or_int4 (TACLET)

• applyEq_or_int5 (TACLET)

• applyEq_or_int6 (TACLET)

• applyEq_or_int7 (TACLET)

apply_select_eq

• applyEq (TACLET)

auto_induction

• auto_int_induction_geq_1 (TACLET)

• auto_int_induction_geq_2 (TACLET)

• auto_int_induction_geq_3 (TACLET)

• auto_int_induction_geq_5 (TACLET)

• auto_int_induction_geq_6 (TACLET)

• auto_int_induction_geq_Left1 (TACLET)

• auto_int_induction_geq_Left2 (TACLET)

• auto_int_induction_gt_1 (TACLET)

• auto_int_induction_gt_2 (TACLET)

• auto_int_induction_gt_3 (TACLET)

• auto_int_induction_gt_5 (TACLET)

• auto_int_induction_gt_6 (TACLET)

• auto_int_induction_gt_Left1 (TACLET)

• auto_int_induction_gt_Left2 (TACLET)

auto_induction_lemma

• autoInductGEQ_Lemma_1 (TACLET)

• autoInductGEQ_Lemma_2 (TACLET)

• autoInductGEQ_Lemma_3 (TACLET)

• autoInductGEQ_Lemma_5 (TACLET)

• autoInductGEQ_Lemma_6 (TACLET)

• autoInductGT_Lemma_1 (TACLET)

• autoInductGT_Lemma_2 (TACLET)

• autoInductGT_Lemma_3 (TACLET)

• autoInductGT_Lemma_5 (TACLET)

• autoInductGT_Lemma_6 (TACLET)

beta

• andRight (TACLET)

• doubleImpLeft (TACLET)

• equiv_left (TACLET)

• equiv_right (TACLET)

• impLeft (TACLET)

• orLeft (TACLET)

boolean_cases

• all_bool (TACLET)

• ex_bool (TACLET)

boxDiamondConv

• boxToDiamond (TACLET)

• boxToDiamondTransaction (TACLET)

• diamondToBox (TACLET)

• diamondToBoxTransaction (TACLET)

cast_deletion

• castDel (TACLET)

charLiteral_to_intLiteral

• charLiteral_to_int (TACLET)

classAxiom

• createdInHeapToElementOf (TACLET)

closure

• close (TACLET)

• closeFalse (TACLET)

• closeTrue (TACLET)

• closeType (TACLET)

• closeTypeSwitched (TACLET)

cnf_andAssoc

• shift_paren_and (TACLET)

cnf_andComm

• commute_and (TACLET)

• commute_and_2 (TACLET)

cnf_dist

• cnf_rightDist (TACLET)

cnf_expandIfThenElse

• cnf_eqv (TACLET)

• ifthenelse_to_or_for (TACLET)

• ifthenelse_to_or_for2 (TACLET)

• ifthenelse_to_or_left (TACLET)

• ifthenelse_to_or_left2 (TACLET)

• ifthenelse_to_or_right (TACLET)

• ifthenelse_to_or_right2 (TACLET)

cnf_orAssoc

• shift_paren_or (TACLET)

cnf_orComm

• commute_or (TACLET)

• commute_or_2 (TACLET)

cnf_setComm

• commuteDisjoint (TACLET)

• commuteIntersection (TACLET)

• commuteIntersection_2 (TACLET)

• commuteUnion (TACLET)

• commuteUnion_2 (TACLET)

comprehension_split

• bprod_find (TACLET)

• bsum_split (TACLET)

comprehensions

• bprod_equal_one_right (TACLET)

• bprod_equal_zero_right (TACLET)

• bsum_equal_split1 (TACLET)

• bsum_equal_split2 (TACLET)

• bsum_equal_split3 (TACLET)

• bsum_equal_split4 (TACLET)

• bsum_zero_right (TACLET)

• definitionOfNewOnHeap (TACLET)

• definitionOfObjectIsomorphic (TACLET)

• definitionOfObjectsIsomorphic (TACLET)

• definitionOfSameTypes (TACLET)

• equal_bprod1 (TACLET)

• equal_bprod2 (TACLET)

• equal_bprod3 (TACLET)

• equal_bsum1 (TACLET)

• equal_bsum2 (TACLET)

• equal_bsum3 (TACLET)

comprehensions_high_costs

• equal_bprod5 (TACLET)

• equal_bsum5 (TACLET)

concrete

• allFieldsSubsetOf (TACLET)

• applySkip1 (TACLET)

• binaryAndZeroLeft (TACLET)

• binaryAndZeroRight (TACLET)

• binaryOrNeutralLeft (TACLET)

• binaryOrNeutralRight (TACLET)

• boolean_equal (TACLET)

• boolean_equal_2 (TACLET)

• boolean_not_equal_1 (TACLET)

• boolean_not_equal_2 (TACLET)

• bprod_lower_equals_upper (TACLET)

• bprod_one (TACLET)

• bprod_one_factor_concrete1 (TACLET)

• bprod_one_factor_concrete2 (TACLET)

• bsum_lower_equals_upper (TACLET)

• bsum_one_summand_concrete1 (TACLET)

• bsum_one_summand_concrete2 (TACLET)

• bsum_zero (TACLET)

• castTrueImpliesOriginalTrue (TACLET)

• checkPermissionOwner_empty (TACLET)

• concatRepeatContraction1 (TACLET)

• concatRepeatContraction2 (TACLET)

• concatRepeatContraction2Sym (TACLET)

• concatRepeatContraction3 (TACLET)

• concatRepeatContraction3Sym (TACLET)

• concrete_and_1 (TACLET)

• concrete_and_2 (TACLET)

• concrete_and_3 (TACLET)

• concrete_and_4 (TACLET)

• concrete_eq_1 (TACLET)

• concrete_eq_2 (TACLET)

• concrete_eq_3 (TACLET)

• concrete_eq_4 (TACLET)

• concrete_impl_1 (TACLET)

• concrete_impl_2 (TACLET)

• concrete_impl_3 (TACLET)

• concrete_impl_4 (TACLET)

• concrete_not_1 (TACLET)

• concrete_not_2 (TACLET)

• concrete_or_1 (TACLET)

• concrete_or_2 (TACLET)

• concrete_or_3 (TACLET)

• concrete_or_4 (TACLET)

• concrete_or_5 (TACLET)

• createdInHeapWithEmpty (TACLET)

• createdInHeapWithObserver (TACLET)

• createdInHeapWithObserverEQ (TACLET)

• createdInHeapWithSelect (TACLET)

• createdInHeapWithSelectEQ (TACLET)

• createdInHeapWithSetMinusFreshLocs (TACLET)

• createdInHeapWithSetMinusFreshLocsEQ (TACLET)

• definitionSeqdefWorkaround (TACLET)

• definitionSeqdefWorkaround2 (TACLET)

• disjointAllFields (TACLET)

• disjointAllFields_2 (TACLET)

• disjointAllObjects (TACLET)

• disjointWithEmpty (TACLET)

• div_one (TACLET)

• double_not (TACLET)

• dropEffectlessStores (TACLET)

• elementOfAllFields (TACLET)

• elementOfAllLocs (TACLET)

• elementOfAllObjects (TACLET)

• elementOfEmpty (TACLET)

• elementOfFreshLocs (TACLET)

• elementOfGuardedSet (TACLET)

• emptyEqualsSingleton (TACLET)

• eqClose (TACLET)

• eq_and (TACLET)

• eq_and_2 (TACLET)

• eq_eq (TACLET)

• eq_imp (TACLET)

• eq_or (TACLET)

• eq_or_2 (TACLET)

• equalUnique (TACLET)

• expandInByte (TACLET)

• expandInByte (TACLET)

• expandInChar (TACLET)

• expandInChar (TACLET)

• expandInInt (TACLET)

• expandInInt (TACLET)

• expandInLong (TACLET)

• expandInLong (TACLET)

• expandInShort (TACLET)

• expandInShort (TACLET)

• false_right (TACLET)

• false_to_not_true (TACLET)

• firstOfPair (TACLET)

• getOfSeqSingletonConcrete (TACLET)

• hideAuxiliaryEq (TACLET)

• hideAuxiliaryEqConcrete (TACLET)

• hideAuxiliaryEqConcrete2 (TACLET)

• ifExthenelse1_eq (TACLET)

• ifExthenelse1_eq2 (TACLET)

• ifExthenelse1_eq2_for (TACLET)

• ifExthenelse1_eq2_for_phi (TACLET)

• ifExthenelse1_eq2_phi (TACLET)

• ifExthenelse1_eq_for (TACLET)

• ifExthenelse1_eq_for_phi (TACLET)

• ifExthenelse1_eq_phi (TACLET)

• ifExthenelse1_false (TACLET)

• ifExthenelse1_false_for (TACLET)

• ifExthenelse1_min (TACLET)

• ifExthenelse1_min_for (TACLET)

• ifthenelse_concrete (TACLET)

• ifthenelse_concrete2 (TACLET)

• ifthenelse_concrete3 (TACLET)

• ifthenelse_concrete4 (TACLET)

• ifthenelse_equals (TACLET)

• ifthenelse_false (TACLET)

• ifthenelse_false_for (TACLET)

• ifthenelse_same_branches (TACLET)

• ifthenelse_same_branches_for (TACLET)

• ifthenelse_true (TACLET)

• ifthenelse_true_for (TACLET)

• inDomainOfMapEmpty (TACLET)

• indexOfSeqSingleton (TACLET)

• infiniteUnionUnused (TACLET)

• insert_constant_value (TACLET)

• instanceof_not_compatible (TACLET)

• instanceof_not_compatible_2 (TACLET)

• instanceof_not_compatible_3 (TACLET)

• instanceof_not_compatible_4 (TACLET)

• instanceof_not_compatible_5 (TACLET)

• instanceof_static_type (TACLET)

• instanceof_static_type_2 (TACLET)

• intersectWithAllLocs (TACLET)

• intersectWithAllLocsRight (TACLET)

• intersectWithEmpty (TACLET)

• intersectWithEmptyRight (TACLET)

• intersectWithItself (TACLET)

• intersectionSetMinusItself (TACLET)

• intersectionSetMinusItself_2 (TACLET)

• irrflConcrete1 (TACLET)

• irrflConcrete2 (TACLET)

• jdiv_one (TACLET)

• jmodNumZero (TACLET)

• lenOfSeqEmpty (TACLET)

• lenOfSeqEmptyEQ (TACLET)

• lenOfSeqSingleton (TACLET)

• lenOfSeqSingletonEQ (TACLET)

• memsetEmpty (TACLET)

• moduloByteIsInByte (TACLET)

• moduloByteIsInRangeByte (TACLET)

• moduloCharIsInChar (TACLET)

• moduloCharIsInRangeChar (TACLET)

• moduloIntIsInInt (TACLET)

• moduloIntIsInRangeInt (TACLET)

• moduloLongIsInLong (TACLET)

• moduloLongIsInRangeLong (TACLET)

• moduloShortIsInRangeShort (TACLET)

• moduloShortIsInShort (TACLET)

• neq_and (TACLET)

• neq_and_2 (TACLET)

• neq_and_3 (TACLET)

• neq_and_4 (TACLET)

• neq_or (TACLET)

• neq_or_2 (TACLET)

• neq_or_3 (TACLET)

• neq_or_4 (TACLET)

• nonNullZero (TACLET)

• nullIsNotNonNull (TACLET)

• optEmpty (TACLET)

• polyMod_zero (TACLET)

• powMonoConcreteRight (TACLET)

• prod_empty (TACLET)

• prod_one (TACLET)

• readPermissionEmpty (TACLET)

• readPermissionObject (TACLET)

• referencedObjectIsCreatedRight (TACLET)

• referencedObjectIsCreatedRightEQ (TACLET)

• regExAxiom (TACLET)

• regExConcatAltLeft (TACLET)

• regExConcatAltRight (TACLET)

• regExConcatConcreteStringLeft (TACLET)

• regExConcatConcreteStringRight (TACLET)

• regExConcatOptLeft (TACLET)

• regExConcatOptRight (TACLET)

• repeatOnce (TACLET)

• repeatRepeatContraction (TACLET)

• repeatZero (TACLET)

• returnPermission_empty (TACLET)

• sameTypeFalse (TACLET)

• sameTypeTrue (TACLET)

• secondOfPair (TACLET)

• seqConcatWithSeqEmpty1 (TACLET)

• seqConcatWithSeqEmpty2 (TACLET)

• seqNPermEmpty (TACLET)

• seqNPermSingletonConrete (TACLET)

• seqPermRefl (TACLET)

• seqReverseOfSeqEmpty (TACLET)

• setMinusItself (TACLET)

• setMinusWithAllLocs (TACLET)

• setMinusWithEmpty1 (TACLET)

• setMinusWithEmpty2 (TACLET)

• simplifySelectOfAnon (TACLET)

• simplifySelectOfAnonEQ (TACLET)

• simplifySelectOfCreate (TACLET)

• simplifySelectOfCreateEQ (TACLET)

• simplifySelectOfMemset (TACLET)

• simplifySelectOfMemsetEQ (TACLET)

• simplifySelectOfStore (TACLET)

• simplifySelectOfStoreEQ (TACLET)

• singletonEqualsEmpty (TACLET)

• sortsDisjoint1 (TACLET)

• sortsDisjoint2 (TACLET)

• subSeqComplete (TACLET)

• subSeqCompleteSeqDef (TACLET)

• subSeqCompleteSeqDefEQ (TACLET)

• subSeqEmpty (TACLET)

• subSeqHeadSeqDef (TACLET)

• subSeqHeadSeqDefEQ (TACLET)

• subSeqSingleton (TACLET)

• subSeqSingletonEQ (TACLET)

• subSeqTailEQL (TACLET)

• subSeqTailEQR (TACLET)

• subSeqTailL (TACLET)

• subSeqTailR (TACLET)

• subsetOfEmpty (TACLET)

• subsetOfIntersectWithItSelf1 (TACLET)

• subsetOfIntersectWithItSelf2 (TACLET)

• subsetOfIntersectWithItSelfEQ1 (TACLET)

• subsetOfIntersectWithItSelfEQ2 (TACLET)

• subsetOfItself (TACLET)

• subsetOfUnionWithItSelf1 (TACLET)

• subsetOfUnionWithItSelf2 (TACLET)

• subsetOfUnionWithItSelfEQ1 (TACLET)

• subsetOfUnionWithItSelfEQ2 (TACLET)

• subsetWithAllLocs (TACLET)

• subsetWithAllLocs2 (TACLET)

• subsetWithEmpty (TACLET)

• sum_empty (TACLET)

• sum_zero (TACLET)

• transferPermission_empty (TACLET)

• true_left (TACLET)

• typeEqDerived (TACLET)

• typeEqDerived2 (TACLET)

• unionWithAllLocs (TACLET)

• unionWithAllLocsRight (TACLET)

• unionWithEmpty (TACLET)

• unionWithEmptyRight (TACLET)

• unionWithItself (TACLET)

• wellFormedAnon (TACLET)

• wellFormedAnonEQ (TACLET)

• wellFormedCreate (TACLET)

• wellFormedStorePrimitive (TACLET)

• wellFormedStorePrimitiveArray (TACLET)

• wellFormedStorePrimitiveEQ (TACLET)

• writePermissionEmpty (TACLET)

• writePermissionObject (TACLET)

confluence_restricted

• class_being_initialized_is_prepared (TACLET)

• class_erroneous_excludes_class_in_init (TACLET)

• class_initialized_excludes_class_init_in_progress (TACLET)

• erroneous_class_has_no_initialized_sub_class (TACLET)

• initialized_class_is_not_erroneous (TACLET)

• initialized_class_is_prepared (TACLET)

conjNormalForm

• associativeLawIntersect (TACLET)

• associativeLawUnion (TACLET)

• cnf_eqv (TACLET)

• cnf_rightDist (TACLET)

• commute_and (TACLET)

• commute_and_2 (TACLET)

• commute_or (TACLET)

• commute_or_2 (TACLET)

• ifthenelse_to_or_for (TACLET)

• ifthenelse_to_or_for2 (TACLET)

• ifthenelse_to_or_left (TACLET)

• ifthenelse_to_or_left2 (TACLET)

• ifthenelse_to_or_right (TACLET)

• ifthenelse_to_or_right2 (TACLET)

• shift_paren_and (TACLET)

• shift_paren_or (TACLET)

cut

• cut (TACLET)

cut_direct

• cut_direct (TACLET)

defOpsReplace

• replaceDef (TACLET)

defOpsReplaceInline

• replaceCons (TACLET)

defOpsSeqEquality

• equalityToSeqGetAndSeqLen (TACLET)

defOpsStartsEndsWith

• endsWith (TACLET)

• startsWith (TACLET)

defOps_div

• div_axiom (TACLET)

defOps_divModPullOut

• polyDiv_pullOut (TACLET)

• polyMod_pullOut (TACLET)

defOps_expandJNumericOp

• expand_addJint (TACLET)

• expand_addJlong (TACLET)

• expand_divJint (TACLET)

• expand_divJlong (TACLET)

• expand_modJint (TACLET)

• expand_modJlong (TACLET)

• expand_moduloByte (TACLET)

• expand_moduloChar (TACLET)

• expand_moduloInteger (TACLET)

• expand_moduloLong (TACLET)