Class de.uka.ilkd.key.proof.proverules.ProveRulesTest

all > de.uka.ilkd.key.proof.proverules > ProveRulesTest
196

tests
0

failures
0

ignored
15m31.53s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 4.507s passed
powPositiveConcrete data()[101] 4.602s passed
powGeq1Concrete data()[102] 4.619s passed
pow2InIntLower data()[103] 4.576s passed
pow2InIntUpper data()[104] 4.576s passed
logSelfConcrete data()[105] 4.591s passed
log1Concrete data()[106] 4.547s passed
logProduct data()[107] 4.620s passed
logTimesBaseConcrete data()[108] 4.592s passed
logProdIdentity data()[109] 4.598s passed
moduloByteIsInByte data()[10] 4.708s passed
logProdIdentityConcrete data()[110] 4.582s passed
logPowIdentity data()[111] 4.544s passed
logPowIdentityConcrete data()[112] 4.544s passed
logPositive data()[113] 4.644s passed
logPositiveConcrete data()[114] 4.555s passed
logMono data()[115] 4.663s passed
logMonoConcrete data()[116] 4.506s passed
powLogLess data()[117] 4.642s passed
powLogMore2 data()[118] 4.637s passed
logLessThanPow data()[119] 4.716s passed
moduloCharIsInChar data()[11] 4.749s passed
logLessThanPowConcrete data()[120] 4.535s passed
logSqueeze data()[121] 4.558s passed
ifthenelse_equals data()[122] 4.595s passed
ifthenelse_equals_1 data()[123] 4.451s passed
ifthenelse_equals_2 data()[124] 4.525s passed
disjointWithSingleton1 data()[125] 4.589s passed
disjointWithSingleton2 data()[126] 4.549s passed
disjointArrayRanges data()[127] 4.573s passed
disjointArrayRangeAllFields1 data()[128] 4.580s passed
disjointArrayRangeAllFields2 data()[129] 4.554s passed
div_unique1 data()[12] 4.794s passed
seqSelfDefinition data()[130] 4.539s passed
seqOutsideValue data()[131] 4.547s passed
castedGetAny data()[132] 4.581s passed
seqGetAlphaCast data()[133] 4.556s passed
getOfSeqSingleton data()[134] 4.584s passed
getOfSeqSingletonConcrete data()[135] 4.628s passed
getOfSeqConcat data()[136] 4.559s passed
getOfSeqSub data()[137] 4.528s passed
getOfSeqReverse data()[138] 4.564s passed
lenOfSeqEmpty data()[139] 4.568s passed
div_unique2 data()[13] 4.809s passed
lenOfSeqSingleton data()[140] 4.589s passed
lenOfSeqConcat data()[141] 4.546s passed
lenOfSeqSub data()[142] 4.465s passed
lenOfSeqReverse data()[143] 4.510s passed
equalityToSeqGetAndSeqLenLeft data()[144] 4.556s passed
equalityToSeqGetAndSeqLenRight data()[145] 4.512s passed
getOfSeqSingletonEQ data()[146] 4.458s passed
getOfSeqConcatEQ data()[147] 4.607s passed
getOfSeqSubEQ data()[148] 4.452s passed
getOfSeqReverseEQ data()[149] 4.435s passed
div_exists data()[14] 5.095s passed
lenOfSeqEmptyEQ data()[150] 4.636s passed
lenOfSeqSingletonEQ data()[151] 4.395s passed
lenOfSeqConcatEQ data()[152] 4.409s passed
lenOfSeqSubEQ data()[153] 4.544s passed
lenOfSeqReverseEQ data()[154] 4.555s passed
getOfSeqDefEQ data()[155] 4.413s passed
lenOfSeqDefEQ data()[156] 4.467s passed
seqConcatWithSeqEmpty1 data()[157] 4.359s passed
seqConcatWithSeqEmpty2 data()[158] 4.386s passed
seqReverseOfSeqEmpty data()[159] 4.473s passed
div_one data()[15] 4.703s passed
subSeqComplete data()[160] 4.390s passed
subSeqTailR data()[161] 4.495s passed
subSeqTailL data()[162] 4.461s passed
subSeqTailEQR data()[163] 4.459s passed
subSeqTailEQL data()[164] 4.474s passed
seqDef_split data()[165] 4.520s passed
seqDef_induction_upper data()[166] 4.588s passed
seqDef_induction_upper_concrete data()[167] 4.513s passed
seqDef_induction_lower data()[168] 4.640s passed
seqDef_induction_lower_concrete data()[169] 4.596s passed
jdiv_one data()[16] 4.719s passed
seqDef_split_in_three data()[170] 4.988s passed
seqDef_empty data()[171] 4.412s passed
seqDef_one_summand data()[172] 4.455s passed
seqDef_lower_equals_upper data()[173] 4.550s passed
seqDefOfSeq data()[174] 4.582s passed
seqSelfDefinitionEQ2 data()[175] 4.558s passed
indexOfSeqSingleton data()[176] 4.498s passed
indexOfSeqConcatFirst data()[177] 4.559s passed
indexOfSeqConcatSecond data()[178] 4.633s passed
indexOfSeqSub data()[179] 4.624s passed
div_zero data()[17] 4.732s passed
lenOfArray2seq data()[180] 4.474s passed
getAnyOfArray2seq data()[181] 4.432s passed
getOfArray2seq data()[182] 4.527s passed
getAnyOfNPermInv data()[183] 4.555s passed
seqNPermRange data()[184] 4.691s passed
seqPermTrans data()[185] 4.657s passed
seqPermRefl data()[186] 4.617s passed
seqPermSplit data()[187] 4.601s passed
seqNPermRight data()[188] 5.144s passed
seqPermFromSwap data()[189] 4.714s passed
divResZero1 data()[18] 4.654s passed
seqPermTransAlt0 data()[190] 4.726s passed
seqPermTransAlt1 data()[191] 4.507s passed
seqPermTransAlt2 data()[192] 4.562s passed
seqPermTransAlt3 data()[193] 4.623s passed
schiffl_lemma_2 data()[194] 28.827s passed
schiffl_thm_1 data()[195] 5.792s passed
eqSameSeq data()[196] 4.786s passed
divResZero2 data()[19] 4.683s passed
eqTermCut data()[1] 5.873s passed
divResOne1 data()[20] 4.669s passed
divResOne2 data()[21] 4.650s passed
div_cancel1 data()[22] 4.674s passed
div_cancel2 data()[23] 4.669s passed
divAddMultDenom data()[24] 4.679s passed
divMinus data()[25] 4.753s passed
divMinusDenom data()[26] 4.730s passed
divLeastDPos data()[27] 4.607s passed
divLeastDNeg data()[28] 4.718s passed
divGreatestDPos data()[29] 4.624s passed
equivAllRight data()[2] 5.254s passed
divGreatestDNeg data()[30] 4.628s passed
divIncreasingPos data()[31] 4.590s passed
divIncreasingNeg data()[32] 4.575s passed
jdiv_zero data()[33] 4.566s passed
jdivPulloutMinusNum data()[34] 4.648s passed
jdivPulloutMinusDenom data()[35] 4.809s passed
jdiv_uniquePosPos data()[36] 4.653s passed
jdiv_uniquePosNeg data()[37] 4.645s passed
jdiv_uniqueNegPos data()[38] 4.642s passed
jdiv_uniqueNegNeg data()[39] 4.613s passed
irrflConcrete1 data()[3] 4.948s passed
jdivMultDenom1 data()[40] 4.721s passed
jdivMultDenom2 data()[41] 4.629s passed
mod_geZero data()[42] 4.664s passed
mod_lessDenom data()[43] 4.592s passed
jmod_NumPos data()[44] 4.631s passed
jmod_NumNeg data()[45] 4.585s passed
jmod_geZero data()[46] 4.636s passed
jmodNumZero data()[47] 4.633s passed
jmod_pulloutminusNum data()[48] 4.648s passed
jmod_pulloutminusDenom data()[49] 4.641s passed
irrflConcrete2 data()[4] 4.875s passed
jmodUnique1 data()[50] 4.805s passed
jmodUnique2 data()[51] 4.837s passed
intDivRem data()[52] 4.623s passed
jmodjmod data()[53] 4.719s passed
jmodDivisible data()[54] 4.642s passed
jmodDivisibleRep data()[55] 4.570s passed
jdivAddMultDenom data()[56] 5.049s passed
jmodAltZero data()[57] 4.650s passed
jmodAddMultDenomZero data()[58] 4.594s passed
polyDiv_zero data()[59] 4.653s passed
cancel_gtPos data()[5] 4.976s passed
polyMod_ltdivDenom data()[60] 4.751s passed
bsum_empty data()[61] 4.631s passed
bsum_induction_upper data()[62] 4.661s passed
bsum_induction_lower data()[63] 4.638s passed
bsum_num_of_bounds data()[64] 4.587s passed
bsum_num_of_bounds2 data()[65] 4.671s passed
bsum_induction_upper2 data()[66] 4.579s passed
bsum_induction_upper_concrete data()[67] 4.593s passed
bsum_induction_upper_concrete_2 data()[68] 4.626s passed
bsum_induction_upper2_concrete data()[69] 4.597s passed
cancel_gtNeg data()[6] 4.832s passed
bsum_induction_lower_concrete data()[70] 4.593s passed
bsum_induction_lower2 data()[71] 4.537s passed
bsum_induction_lower2_concrete data()[72] 4.577s passed
bsum_positive data()[73] 4.684s passed
bsum_upper_bound data()[74] 4.671s passed
bsum_lower_bound data()[75] 4.643s passed
bsum_positive_lower_bound_element data()[76] 4.625s passed
bsum_sub_same_index data()[77] 4.600s passed
bsum_less_same_index data()[78] 4.660s passed
bsum_equal_except_one_index data()[79] 4.694s passed
moduloIntIsInInt data()[7] 4.762s passed
bsum_num_of_is_max data()[80] 4.598s passed
bsum_num_of_is_max2 data()[81] 4.745s passed
bsum_num_of_is_max3 data()[82] 4.696s passed
bsum_num_of_is_max4 data()[83] 4.629s passed
bsum_num_of_lt_max data()[84] 4.576s passed
bsum_num_of_lt_max2 data()[85] 4.556s passed
bsum_num_of_lt_max3 data()[86] 4.658s passed
bsum_num_of_lt_max4 data()[87] 4.539s passed
bsum_num_of_gt0 data()[88] 4.563s passed
bsum_num_of_gt0_alt data()[89] 4.554s passed
moduloLongIsInLong data()[8] 4.742s passed
bsum_add_concrete data()[90] 4.500s passed
bprod_all_positive data()[91] 4.568s passed
bprod_split data()[92] 4.633s passed
powConcrete0 data()[93] 4.508s passed
powConcrete1 data()[94] 4.571s passed
powSplitFactor data()[95] 4.586s passed
powAdd data()[96] 4.534s passed
powMono data()[97] 4.517s passed
powMonoConcrete data()[98] 4.488s passed
powMonoConcreteRight data()[99] 4.549s passed
moduloShortIsInShort data()[9] 4.747s passed

Standard output

14:35:33,039 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.5
14:35:33,073 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
14:35:33,100 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
14:35:33,240 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
14:35:33,241 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
14:35:33,258 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
14:35:33,258 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
14:35:33,259 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
14:35:33,285 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
14:35:33,291 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
14:35:33,292 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@7c22d4f - End of configuration.
14:35:33,293 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@5f59185e - Registering current configuration as safe fallback point

786        WARN  Test worker     d.u.i.k.s.ProofSettings   No proof-settings could be loaded, using defaults java.io.FileNotFoundException: /home/runner/.key/proof-settings.props (No such file or directory)
	at java.base/java.io.FileInputStream.open0(Native Method)

Standard error

#2 = split-prop
de.uka.ilkd.key.macros.scripts.MacroCommand$Parameters@1d271570
#2 = allRight
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@5b22a9a4
#2 = allRight
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@632e009c
#2 = split-prop
de.uka.ilkd.key.macros.scripts.MacroCommand$Parameters@662920ae
#2 = seqPermDefLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@3e9635d8
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@38574fcd
#2 = exLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@10ec4d23
#2 = split-prop
de.uka.ilkd.key.macros.scripts.MacroCommand$Parameters@692bfc26
#2 = seqNPermRange
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@218fc60c
var = iv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@19fd77b8
occ = 1
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@19fd77b8
with = v_x_0
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@19fd77b8
#2 = impLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@c66a8b9
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@24245789
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@2e13124b
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@1a34e23c
var = iv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@46f40151
occ = 1
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@46f40151
with = v_y_0
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@46f40151
#2 = impLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@4e899355
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@2046609d
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@6f1454d7
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@5f6c16eb
#2 = seqNPermDefLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@50545b27
var = iv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@72e88e92
occ = 2
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@72e88e92
with = v_x_0
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@72e88e92
#2 = impLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@63cf8b55
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@f33d8bd
#2 = exLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@7e811c5e
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@73ad10c2
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@411aa589
var = iv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@18b2cddd
occ = 2
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@18b2cddd
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@18b2cddd
with = v_y_0
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@18b2cddd
#2 = impLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@2075b83
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@475c80ae
#2 = exLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@113e67df
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@cebba96
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@1d3ad28c
var = iv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@4845d035
occ = 1
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@4845d035
with = jv_0
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@4845d035
#2 = impLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@683af88c
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@2533f22c
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@754489fd
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@46f714ca
#2 = castAdd
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@3ae781f1
formula = equals(any::seqGet(s_0,jv_0),v_x_0)
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@3ae781f1
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@3ae781f1
var = iv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@7dec8e8a
occ = 1
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@7dec8e8a
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@7dec8e8a
with = jv_1
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@7dec8e8a
#2 = impLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@185d16e8
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@6d083963
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@75e276f4
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@5d8ec5b0
#2 = castAdd
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@5d84c518
formula = equals(any::seqGet(s_0,jv_1),v_y_0)
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@5d84c518
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@5d84c518
var = iv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@1ed2b998
with = v_x_0
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@1ed2b998
#2 = impLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@725c1162
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@5ac35c93
var = iv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@4291447d
with = v_y_0
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@4291447d
#2 = impLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@74431e4b
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@269d1f46
#2 = equals(v_x_0,v_y_0)
de.uka.ilkd.key.macros.scripts.CutCommand$Parameters@6b0d6ff9
var = v_r
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@1c45799c
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@1c45799c
with = seqSwap(s_0,v_x_0,jv_0)
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@1c45799c
#2 = andRight
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@61b5b673
#2 = andRight
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@41a49e3d
#2 = andRight
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@40164f35
#2 = andRight
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@1d32e89a
#2 = lenOfSwap
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@37a4d4a4
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@3dd88cf2
#2 = seqNPermSwapNPerm
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@5bf3cd93
var = iv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@58d4ee4d
occ = 1
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@58d4ee4d
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@58d4ee4d
with = v_x_0
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@58d4ee4d
var = jv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@6ea2b512
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@6ea2b512
with = jv_0
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@6ea2b512
#2 = impLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@4ff5d133
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@2a1af9c3
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@2f3364c1
#2 = allRight
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@11bfbc1e
#2 = impRight
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@7ed8b2b2
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@2ea16ff9
var = iv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@769cfb75
with = v_iv_0
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@769cfb75
#2 = impLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@7eb011c4
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@4d1c37cb
#2 = getOfSwap
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@6d9a89cf
#2 = ifthenelse_negated
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@3fba9c95
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@1ff0c0c1
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@1ff0c0c1
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@52eca6d1
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@6c63ba60
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@7bbaf889
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@afbed24
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@afbed24
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@7e207300
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@4028ca69
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@4028ca69
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@83f1c5
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@1c318434
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@7d6fe840
#2 = getOfSwap
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@2afb18ba
#2 = ifthenelse_negated
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@14018bb8
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@13145dc6
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@13145dc6
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@77062c6c
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@2db54db9
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@3e56ffb8
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@3909a54e
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@3909a54e
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@6f4d1f18
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@6f5975b7
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@19b9bc74
#2 = getOfSwap
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@56b01c23
#2 = ifthenelse_negated
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@7099396f
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@9b5c53d
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@9b5c53d
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@4a822275
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@3b7412b0
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@7b5dd0f6
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@6027bcbf
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@6027bcbf
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@7e77ba1e
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@1ef01665
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@25b93e6a
#2 = equals(int::cast(any::seqGet(s_0,v_x_0)),int::cast(any::seqGet(s_0,v_y_0)))
de.uka.ilkd.key.macros.scripts.CutCommand$Parameters@500dc22
#2 = seqNPermInjective
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@51043f58
var = iv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@373bbb1e
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@373bbb1e
with = v_x_0
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@373bbb1e
var = jv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@1de039d0
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@1de039d0
with = v_y_0
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@1de039d0
#2 = impLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@33e60976
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@75c87c70
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@48c75993
#2 = equals(int::cast(any::seqGet(s_0,v_x_0)),v_x_0)
de.uka.ilkd.key.macros.scripts.CutCommand$Parameters@3055e51a
var = v_r
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@3e496d42
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@3e496d42
with = seqSwap(s_0,v_y_0,jv_1)
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@3e496d42
#2 = andRight
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@54c4f428
#2 = andRight
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@31ef0c61
#2 = andRight
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@52501de
#2 = andRight
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@7fc6f09a
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@590f68b
#2 = seqNPermSwapNPerm
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@734fcd2b
var = iv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@5f85d5c5
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@5f85d5c5
with = v_y_0
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@5f85d5c5
var = jv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@5a082130
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@5a082130
with = jv_1
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@5a082130
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@63e97d00
#2 = allRight
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@636be6f8
#2 = impRight
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@4028770e
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@1a1cf274
var = iv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@218a4858
with = v_iv_0
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@218a4858
#2 = impLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@3e24a278
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@5d5b40dc
#2 = getOfSwap
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@1cf838ab
#2 = ifthenelse_negated
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@4996cd36
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@e1d4922
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@e1d4922
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@bce6e65
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@33def1a3
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@543225a3
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@1025956f
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@1025956f
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@204762a
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@315158da
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@315158da
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@a4437c9
var = iv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@49969a19
with = v_y_0
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@49969a19
#2 = impLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@17806593
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@3a2bc4f4
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@18375a8b
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@698cfabe
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@348665b4
#2 = getOfSwap
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@26b2e1be
#2 = ifthenelse_negated
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@6aba310e
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@3208928f
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@3208928f
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@5c38ebee
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@5f1860f3
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@28d453c8
#2 = equals(int::cast(any::seqGet(s_0,v_y_0)),v_y_0)
de.uka.ilkd.key.macros.scripts.CutCommand$Parameters@44576a9c
var = v_r
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@7468bafb
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@7468bafb
with = seqSwap(s_0,v_x_0,jv_0)
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@7468bafb
#2 = andRight
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@7b978aaf
#2 = andRight
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@40919eda
#2 = andRight
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@406a48dc
#2 = andRight
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@43137c3b
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@66602d68
#2 = seqNPermSwapNPerm
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@11b5a7e9
var = iv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@21d61268
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@21d61268
with = v_x_0
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@21d61268
var = jv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@1c1d6bb5
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@1c1d6bb5
with = jv_0
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@1c1d6bb5
#2 = impLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@459682bf
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@56cd776f
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@1641399c
#2 = allRight
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@374f4e20
#2 = impRight
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@27e3447d
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@1da3696d
var = iv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@1167b473
with = v_iv_0
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@1167b473
#2 = impLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@47b7f58c
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@6be08515
#2 = getOfSwap
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@3697e8e5
#2 = ifthenelse_negated
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@68481cd5
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@138a21c7
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@138a21c7
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@a7ac1c3
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@4dc91e53
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@7f5a8ea0
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@7a642c9e
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@7a642c9e
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@48b0a304
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@4d41a93b
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@4d41a93b
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@3af9e1e7
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@1df19a23
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@2a2c7cf0
#2 = getOfSwap
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@59019b5e
#2 = ifthenelse_negated
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@1ce0b2f2
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@4c6a8814
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@4c6a8814
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@df6b131
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@4e87e40d
#2 = getOfSwap
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@5ab925a2
#2 = ifthenelse_negated
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@46ad4880
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@4caaa26e
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@4caaa26e
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@2b1d642e
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@18ea42fd
#2 = equals(int::cast(any::seqGet(s_0,v_x_0)),v_y_0)
de.uka.ilkd.key.macros.scripts.CutCommand$Parameters@5c4cb4dd
var = v_r
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@24563eec
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@24563eec
with = seqSwap(seqSwap(s_0,jv_0,v_x_0),jv_0,v_y_0)
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@24563eec
#2 = andRight
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@70364b18
#2 = andRight
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@7b407c35
#2 = andRight
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@b48c8f3
#2 = andRight
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@5c2336cf
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@71948a11
#2 = seqNPermSwapNPerm
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@c3e5f7
var = iv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@5382eb09
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@5382eb09
with = jv_0
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@5382eb09
var = jv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@5a2a77e8
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@5a2a77e8
with = v_x_0
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@5a2a77e8
#2 = impLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@6531f912
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@45bdfdf3
#2 = seqNPermSwapNPerm
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@7b129ce1
formula = seqNPerm(seqSwap(s_0,jv_0,v_x_0))
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@7b129ce1
var = iv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@68b622fb
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@68b622fb
with = jv_0
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@68b622fb
var = jv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@f8e0063
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@f8e0063
with = v_y_0
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@f8e0063
#2 = impLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@7daad7a5
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@78329a11
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@46d4a9e3
#2 = allRight
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@309ba449
#2 = impRight
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@7f56ca14
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@7ca95c13
var = iv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@4e09d0ee
with = v_iv_0
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@4e09d0ee
#2 = impLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@7cebbdf1
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@2a0fac1
#2 = getOfSwap
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@74d679e5
#2 = ifthenelse_negated
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@11424783
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@257608a
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@257608a
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@63de8080
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@6fbdce89
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@5cd07593
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@5d983106
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@5d983106
#2 = getOfSwap
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@66d9d891
#2 = ifthenelse_negated
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@7ad5c54d
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@2411385d
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@2411385d
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@3368f476
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@1c80560a
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@410c0c78
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@77577132
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@77577132
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@5ecb888d
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@7729662c
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@7729662c
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@8a57895
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@6fbda864
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@f8f67e9
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@2b1f59b8
#2 = getOfSwap
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@2949bbe5
#2 = ifthenelse_negated
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@78cae5ed
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@2600c96
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@2600c96
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@35f596d6
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@43a0efa3
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@74e51012
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@780f1e0d
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@780f1e0d
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@6e4a8e9b
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@111c1c13
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@1ceff6e0
#2 = getOfSwap
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@7e8a2456
#2 = ifthenelse_negated
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@744529dd
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@6f49d658
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@6f49d658
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@12ada7dd
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@25600198
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@53341b49
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@14111259
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@14111259
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@da593e6
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@377c77ee
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@377c77ee
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@789ae1b6
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@368f43f0
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@6247d644
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@3a61e009
#2 = getOfSwap
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@11557213
#2 = ifthenelse_negated
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@1da7e1b6
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@1b218485
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@1b218485
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@69f0f6d
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@52d03f35
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@7df76ae3
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@2e0dcbff
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@2e0dcbff
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@3d6bfe8d
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@50c58006
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@50c58006
#2 = getOfSwap
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@6d1570a4
#2 = ifthenelse_negated
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@72775aca
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@e4e2132
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@e4e2132
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@362d91de
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@63f5aff2
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@3b974f5e
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@df23db2
#2 = getOfSwap
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@15571cf5
#2 = ifthenelse_negated
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@46f1871a
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@70e3eb8c
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@70e3eb8c
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@3e0ebe98
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@6bf36e26
#2 = equals(int::seqGet(s_0,v_y_0),v_x_0)
de.uka.ilkd.key.macros.scripts.CutCommand$Parameters@471a2b7f
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@d4159b5
#2 = seqNPermSwapNPerm
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@55c57185
var = iv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@1238e8fd
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@1238e8fd
with = jv_1
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@1238e8fd
var = jv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@32efb41c
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@32efb41c
with = v_y_0
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@32efb41c
#2 = impLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@2ec785ee
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@228fee9e
#2 = seqNPermSwapNPerm
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@1df2735e
formula = seqNPerm(seqSwap(s_0,jv_1,v_y_0))
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@1df2735e
var = iv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@6acbc920
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@6acbc920
with = jv_1
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@6acbc920
var = jv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@1e67293c
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@1e67293c
with = v_x_0
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@1e67293c
#2 = impLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@34429d36
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@24a86194
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@66ee2925
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@60ea4d39
#2 = seqNPermSwapNPerm
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@10793e50
formula = seqNPerm(s_0)
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@10793e50
var = iv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@35453a90
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@35453a90
with = v_x_0
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@35453a90
var = jv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@113f509
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@113f509
with = jv_0
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@113f509
#2 = impLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@fc01bd9
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@7d547686
#2 = seqNPermSwapNPerm
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@7eb73cf8
formula = seqNPerm(seqSwap(s_0,v_x_0,jv_0))
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@7eb73cf8
var = iv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@23d08e0a
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@23d08e0a
with = v_y_0
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@23d08e0a
var = jv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@338bb603
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@338bb603
with = jv_1
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@338bb603
var = v_r
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@4b8faf9
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@4b8faf9
with = seqSwap(seqSwap(s_0,v_x_0,jv_0),v_y_0,jv_1)
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@4b8faf9
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@1841c5ad
#2 = split-prop
de.uka.ilkd.key.macros.scripts.MacroCommand$Parameters@4c89bc58
#2 = schiffl_lemma_2
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@5e4370e4
formula = seqPerm(f_s,f_t)
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@5e4370e4
var = x
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@785624a
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@785624a
with = f_x
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@785624a
var = y
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@65d8a5eb
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@65d8a5eb
with = f_y
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@65d8a5eb
#2 = impLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@26d7640d
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@780d9f92
#2 = exLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@439fabbe
#2 = split-prop
de.uka.ilkd.key.macros.scripts.MacroCommand$Parameters@26d75ff8
#2 = seqPermDef
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@d505d9c
occ = 1
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@d505d9c
#2 = andRight
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@3abca535
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@fc95f79
var = s
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@2a78c847
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@2a78c847
with = r_0
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@2a78c847
#2 = andRight
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@4bc1c7b3
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@52d3153f
#2 = allRight
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@363805fb
#2 = impRight
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@3ebb924e
var = iv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@34d16ecc
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@34d16ecc
with = iv_0
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@34d16ecc
#2 = impLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@4ca73921
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@5e9cd7f4
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@5319abae
#2 = seqNPermRange
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@3769e124
var = iv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@76e095ba
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@76e095ba
with = iv_0
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@76e095ba
#2 = impLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@176cce5e
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@4542b548
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@d6813b0
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@2b4874b4
#2 = seqNPermRange
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@a3cface
var = iv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@58a4d69
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@58a4d69
with = f_x
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@58a4d69
#2 = impLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@3e3c7aee
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@44577933
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@5386a77
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@46fd5aa0
#2 = seqNPermRange
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@7e0ae2e2
var = iv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@de763d5
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@de763d5
with = f_y
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@de763d5
#2 = impLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@4ad2b272
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@40e5bccd
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@5db0653a
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@7853e93a
#2 = getOfSeqDef
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@612902ab
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@612902ab
#2 = getOfSeqDef
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@6543d8d
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@6154eda
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@6154eda
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@590f03ed
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@590f03ed
#2 = sub_zero_2
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@ed13cfb
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@ed13cfb
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@77b7fb0f
occ = 2
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@77b7fb0f
#2 = andLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@23a99b1e
#2 = sub_zero_2
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@919ed8f
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@919ed8f
#2 = add_zero_right
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@6f0b45f3
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@6f0b45f3
#2 = add_zero_right
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@954267
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@954267
#2 = add_zero_right
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@189c88c9
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@189c88c9
#2 = add_zero_right
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@5eaf7bc0
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@5eaf7bc0
#2 = add_zero_right
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@6b3e993b
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@6b3e993b
#2 = add_zero_right
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@41126841
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@41126841
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@3db46a6a
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@3db46a6a
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@550ae2d1
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@550ae2d1
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@11eae02b
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@1ddceffb
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@41efaebf
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@41efaebf
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@7650e664
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@54403053
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@54403053
#2 = seqNPermInjective
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@34c8aa59
var = iv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@3d5dc340
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@3d5dc340
with = iv_0
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@3d5dc340
var = jv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@61fa7bc
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@61fa7bc
with = f_y
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@61fa7bc
#2 = impLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@2e1cda5d
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@64112755
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@317e1605
#2 = ifthenelse_split
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@737e6d2d
occ = 0
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@737e6d2d
#2 = seqNPermInjective
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@ea0d45b
var = iv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@7f9f2a3e
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@7f9f2a3e
with = iv_0
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@7f9f2a3e
var = jv
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@477733ea
#2 = hide
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@477733ea
with = f_x
de.uka.ilkd.key.macros.scripts.InstantiateCommand$Parameters@477733ea
#2 = impLeft
de.uka.ilkd.key.macros.scripts.RuleCommand$Parameters@2ec6b024
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@4662aa9b
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@176f46bc
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@3033e8e6
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@2504fa0e
#2 = branch
de.uka.ilkd.key.macros.scripts.TryCloseCommand$TryCloseArguments@f2175d7