pomdp
observables v, h endobservables
module vehicle
v: [0..12] init 12;
[c0] v=12 -> (v'=0);
[c0] v=0 -> (v'=1);
[c1] v=0 -> (v'=2);
[c2] v=0 -> (v'=3);
[c1] v=1 -> (v'=4);
[c2] v=1 -> (v'=5);
[c0] v=2 -> (v'=4);
[c2] v=2 -> (v'=6);
[c0] v=3 -> (v'=5);
[c1] v=3 -> (v'=6);
[c1] v=4 -> (v'=7);
[c2] v=4 -> (v'=8);
[c0] v=5 -> (v'=7);
[c2] v=5 -> (v'=9);
[c0] v=6 -> (v'=8);
[c1] v=6 -> (v'=9);
[c1] v=7 -> (v'=10);
[c1] v=8 -> (v'=10);
[c1] v=9 -> (v'=10);
[c0] v=10 -> (v'=11);
[c1] v=10 -> (v'=11);
[c2] v=10 -> (v'=11);
[c0] v=11 -> (v'=11);
[c1] v=11 -> (v'=11);
[c2] v=11 -> (v'=11);
endmodule
module driver
u : [0..6] init 3;
h : [0..2] init 0;
[c0] u=3 & v=12 ->0.1428571428571428:(u'=0)&(h'=0)+0.1428571428571428:(u'=1)&(h'=0)+0.1428571428571428:(u'=2)&(h'=0)+0.1428571428571428:(u'=3)&(h'=0)+0.1428571428571428:(u'=4)&(h'=0)+0.1428571428571428:(u'=5)&(h'=0)+0.1428571428571428:(u'=6)&(h'=0);
[c0] u=0 & v=0 -> 0.30898673520641067869:(u'=0)&(h'=1) +0.43939345120311446014:(u'=1)&(h'=1) +0.19450909322973192195:(u'=2)&(h'=1) +0.02680395152338755152:(u'=3)&(h'=1) +0.0011498212312096522079:(u'=4)&(h'=1) +1.5354455087369958091e-05:(u'=5)&(h'=1) +6.3827976791975726098e-08:(u'=6)&(h'=1) +0.00011642294215262604805:(u'=0)&(h'=2) +0.0037614345599554120311:(u'=1)&(h'=2) +0.015875055576409027175:(u'=2)&(h'=2) +0.0087523323728912211933:(u'=3)&(h'=2) +0.00063034621989866530204:(u'=4)&(h'=2) +5.9303634069355602054e-06:(u'=5)&(h'=2) +7.2883675433195704392e-09:(u'=6)&(h'=2);
[c1] u=0 & v=0 -> 0.28800890320137989553:(u'=0)&(h'=1) +0.39127148090681562742:(u'=1)&(h'=1) +0.23524678749708249903:(u'=2)&(h'=1) +0.062595402361519864032:(u'=3)&(h'=1) +0.0073711355208192080868:(u'=4)&(h'=1) +0.00038414889033507043517:(u'=5)&(h'=1) +8.8600872097344950546e-06:(u'=6)&(h'=1) +0.00022781225663809947764:(u'=0)&(h'=2) +0.0062521201720977612887:(u'=1)&(h'=2) +0.0081308165543853734569:(u'=2)&(h'=2) +0.0005010691020410522941:(u'=3)&(h'=2) +1.4632471889146019239e-06:(u'=4)&(h'=2) +2.0248571431128738473e-10:(u'=5)&(h'=2) +1.3277848016935405698e-15:(u'=6)&(h'=2);
[c2] u=0 & v=0 -> 0.21288772333811173398:(u'=0)&(h'=1) +0.18421276765925165275:(u'=1)&(h'=1) +0.048776838768533573032:(u'=2)&(h'=1) +0.0039521405915898134148:(u'=3)&(h'=1) +9.7988685926075837392e-05:(u'=4)&(h'=1) +7.434372100498882646e-07:(u'=5)&(h'=1) +1.7259867910456124629e-09:(u'=6)&(h'=1) +9.0729726941287742103e-05:(u'=0)&(h'=2) +0.011725605468126109113:(u'=1)&(h'=2) +0.17502644687673363233:(u'=2)&(h'=2) +0.30175522664888276836:(u'=3)&(h'=2) +0.060088124862662128933:(u'=4)&(h'=2) +0.0013819910397660074928:(u'=5)&(h'=2) +3.6711702784259513425e-06:(u'=6)&(h'=2);
[c0] u=1 & v=0 -> 0.10668110075909956191:(u'=0)&(h'=1) +0.31873347543022956252:(u'=1)&(h'=1) +0.29644249066083361299:(u'=2)&(h'=1) +0.085827371813468833484:(u'=3)&(h'=1) +0.0077354175135099468782:(u'=4)&(h'=1) +0.00021702726133448495727:(u'=5)&(h'=1) +1.8954721420207443197e-06:(u'=6)&(h'=1) +3.647244319482400611e-05:(u'=0)&(h'=2) +0.0039160743170279684044:(u'=1)&(h'=2) +0.054926736634011666394:(u'=2)&(h'=2) +0.10063834185533120091:(u'=3)&(h'=2) +0.024087401502441981721:(u'=4)&(h'=2) +0.00075311835869592668857:(u'=5)&(h'=2) +3.0759786785181408682e-06:(u'=6)&(h'=2);
[c1] u=1 & v=0 -> 0.13450302223441032434:(u'=0)&(h'=1) +0.30970390674024439459:(u'=1)&(h'=1) +0.31559822445964225146:(u'=2)&(h'=1) +0.14232973647246216498:(u'=3)&(h'=1) +0.028407300530203190292:(u'=4)&(h'=1) +0.0025092129080946292546:(u'=5)&(h'=1) +9.8088543707617963617e-05:(u'=6)&(h'=1) +1.5314917822066659124e-05:(u'=0)&(h'=2) +0.0036344210244367105601:(u'=1)&(h'=2) +0.040870732017625872878:(u'=2)&(h'=2) +0.021779415039548489369:(u'=3)&(h'=2) +0.00054996698698170593065:(u'=4)&(h'=2) +6.5808750526704745294e-07:(u'=5)&(h'=2) +3.7315329800401052319e-11:(u'=6)&(h'=2);
[c2] u=1 & v=0 -> 0.079913264970475544891:(u'=0)&(h'=1) +0.15841179036699215565:(u'=1)&(h'=1) +0.096090608303711633198:(u'=2)&(h'=1) +0.017836071132617405122:(u'=3)&(h'=1) +0.0010130765468966131896:(u'=4)&(h'=1) +1.7608004468539763617e-05:(u'=5)&(h'=1) +9.3648932408789295583e-08:(u'=6)&(h'=1) +3.7943387171404232187e-06:(u'=0)&(h'=2) +0.0014860163339211935902:(u'=1)&(h'=2) +0.06721927041888171861:(u'=2)&(h'=2) +0.35119371193869536318:(u'=3)&(h'=2) +0.21192509856364877274:(u'=4)&(h'=2) +0.014770689945178029634:(u'=5)&(h'=2) +0.00011890548686346597961:(u'=6)&(h'=2);
[c0] u=2 & v=0 -> 0.015584210442122797824:(u'=0)&(h'=1) +0.097825356661324663898:(u'=1)&(h'=1) +0.1911572002171130491:(u'=2)&(h'=1) +0.11627931567224426834:(u'=3)&(h'=1) +0.022018455840963842979:(u'=4)&(h'=1) +0.0012979077779776174942:(u'=5)&(h'=1) +2.3816250889918073793e-05:(u'=6)&(h'=1) +2.6810743303148094259e-06:(u'=0)&(h'=2) +0.00095667858209287810756:(u'=1)&(h'=2) +0.044593345087592162201:(u'=2)&(h'=2) +0.27153189787407333577:(u'=3)&(h'=2) +0.21598244958483320266:(u'=4)&(h'=2) +0.022442067968721640669:(u'=5)&(h'=2) +0.00030461696572036626313:(u'=6)&(h'=2);
[c1] u=2 & v=0 -> 0.039930307842923180861:(u'=0)&(h'=1) +0.15583308175631960246:(u'=1)&(h'=1) +0.26914721288136983501:(u'=2)&(h'=1) +0.20572797011644505805:(u'=3)&(h'=1) +0.069593715219360571811:(u'=4)&(h'=1) +0.010418853439346153697:(u'=5)&(h'=1) +0.00069030824836099132381:(u'=6)&(h'=1) +1.8781879021858003016e-07:(u'=0)&(h'=2) +0.00038541617639479533366:(u'=1)&(h'=2) +0.037478090285502960177:(u'=2)&(h'=2) +0.17269572317882314616:(u'=3)&(h'=2) +0.037708766506962573817:(u'=4)&(h'=2) +0.00039017522116869846494:(u'=5)&(h'=2) +1.9130823229311818931e-07:(u'=6)&(h'=2);
[c2] u=2 & v=0 -> 0.013402499283233363855:(u'=0)&(h'=1) +0.060863081644350724986:(u'=1)&(h'=1) +0.084575952184433769721:(u'=2)&(h'=1) +0.035963724870661427369:(u'=3)&(h'=1) +0.0046795840269372238063:(u'=4)&(h'=1) +0.0001863265084809737212:(u'=5)&(h'=1) +2.2702142982740675402e-06:(u'=6)&(h'=1) +9.44983427385831633e-08:(u'=0)&(h'=2) +0.00011215367014677117335:(u'=1)&(h'=2) +0.015373951747493629777:(u'=2)&(h'=2) +0.2434110348713768579:(u'=3)&(h'=2) +0.44512064484406832499:(u'=4)&(h'=2) +0.094015170445171783453:(u'=5)&(h'=2) +0.0022935111910040175374:(u'=6)&(h'=2);
[c0] u=3 & v=0 -> 0.0010875840841770762803:(u'=0)&(h'=1) +0.014343526005252731081:(u'=1)&(h'=1) +0.058887293184594846629:(u'=2)&(h'=1) +0.075259242715132998458:(u'=3)&(h'=1) +0.029941301957836990305:(u'=4)&(h'=1) +0.0037081227609795535706:(u'=5)&(h'=1) +0.00014295854221701008338:(u'=6)&(h'=1) +4.7272840539632717558e-08:(u'=0)&(h'=2) +5.6058312966395032202e-05:(u'=1)&(h'=2) +0.0086839067693035391915:(u'=2)&(h'=2) +0.17572642918985531546:(u'=3)&(h'=2) +0.46452149986395729897:(u'=4)&(h'=2) +0.16040627687414271696:(u'=5)&(h'=2) +0.0072357524667429635318:(u'=6)&(h'=2);
[c1] u=3 & v=0 -> 0.0064288336052728900852:(u'=0)&(h'=1) +0.042523749025810499147:(u'=1)&(h'=1) +0.12448130537344875846:(u'=2)&(h'=1) +0.16126864912655680673:(u'=3)&(h'=1) +0.092463214742646279709:(u'=4)&(h'=1) +0.023461796100624592032:(u'=5)&(h'=1) +0.0026346731771567603181:(u'=6)&(h'=1) +2.9830839452188160494e-10:(u'=0)&(h'=2) +5.2933024424401851974e-06:(u'=1)&(h'=2) +0.0044508663937534156604:(u'=2)&(h'=2) +0.17734502974759325244:(u'=3)&(h'=2) +0.33484984322019772929:(u'=4)&(h'=2) +0.02995972296354193834:(u'=5)&(h'=2) +0.00012702292264618158775:(u'=6)&(h'=2);
[c2] u=3 & v=0 -> 0.001159485712318920024:(u'=0)&(h'=1) +0.012062381624449931491:(u'=1)&(h'=1) +0.038399497394709727893:(u'=2)&(h'=1) +0.037406134257301493218:(u'=3)&(h'=1) +0.011150258330049237637:(u'=4)&(h'=1) +0.001017072338609832172:(u'=5)&(h'=1) +2.838857344195669331e-05:(u'=6)&(h'=1) +1.2088645214868658098e-09:(u'=0)&(h'=2) +4.347791828870032126e-06:(u'=1)&(h'=2) +0.0018061032651615588178:(u'=2)&(h'=2) +0.086656099918943421678:(u'=3)&(h'=2) +0.48021799041089147098:(u'=4)&(h'=2) +0.30736926491229626945:(u'=5)&(h'=2) +0.022722974261132771606:(u'=6)&(h'=2);
[c0] u=4 & v=0 -> 5.4756168979187192132e-05:(u'=0)&(h'=1) +0.0015172340567196165341:(u'=1)&(h'=1) +0.013087138400114533415:(u'=2)&(h'=1) +0.035140617845505331407:(u'=3)&(h'=1) +0.029372889805008368241:(u'=4)&(h'=1) +0.0076428712586563774325:(u'=5)&(h'=1) +0.00061906891477895545535:(u'=6)&(h'=1) +3.1265050791239630961e-10:(u'=0)&(h'=2) +1.2321358431801388432e-06:(u'=1)&(h'=2) +0.00063431480503624542832:(u'=2)&(h'=2) +0.04265774641040743359:(u'=3)&(h'=2) +0.37474666086245284058:(u'=4)&(h'=2) +0.43005543344980712295:(u'=5)&(h'=2) +0.064470035574040213122:(u'=6)&(h'=2);
[c1] u=4 & v=0 -> 0.00065621050867103200652:(u'=0)&(h'=1) +0.0073567314371043423388:(u'=1)&(h'=1) +0.036500587081744147178:(u'=2)&(h'=1) +0.080147139002573211664:(u'=3)&(h'=1) +0.077884211034385850136:(u'=4)&(h'=1) +0.03349531391112322426:(u'=5)&(h'=1) +0.0063751719977752033947:(u'=6)&(h'=1) +6.4780445064108874949e-14:(u'=0)&(h'=2) +9.9397507923181241725e-09:(u'=1)&(h'=2) +7.2270935978299393333e-05:(u'=2)&(h'=2) +0.024900523483498686328:(u'=3)&(h'=2) +0.40654618515944784818:(u'=4)&(h'=2) +0.31453423162056914908:(u'=5)&(h'=2) +0.011531413887313489083:(u'=6)&(h'=2);
[c2] u=4 & v=0 -> 7.5763995221547560566e-05:(u'=0)&(h'=1) +0.0018056353499900079911:(u'=1)&(h'=1) +0.013168067432434813965:(u'=2)&(h'=1) +0.029385889947837955799:(u'=3)&(h'=1) +0.020066908316406725094:(u'=4)&(h'=1) +0.0041932127508689104323:(u'=5)&(h'=1) +0.00026812551379252856773:(u'=6)&(h'=1) +8.0924389931295820504e-12:(u'=0)&(h'=2) +8.8200765912586724263e-08:(u'=1)&(h'=2) +0.00011103195952037395048:(u'=2)&(h'=2) +0.016143822651773213905:(u'=3)&(h'=2) +0.27111121111221087032:(u'=4)&(h'=2) +0.52586141027245159041:(u'=5)&(h'=2) +0.11780883248863321944:(u'=6)&(h'=2);
[c0] u=5 & v=0 -> 2.1981317726021309722e-06:(u'=0)&(h'=1) +0.00012796750338896860084:(u'=1)&(h'=1) +0.0023190934833383328346:(u'=2)&(h'=1) +0.01308306198944987099:(u'=3)&(h'=1) +0.022975931508274247128:(u'=4)&(h'=1) +0.012560572709265090119:(u'=5)&(h'=1) +0.0021375601328322280104:(u'=6)&(h'=1) +9.5962479399716750941e-13:(u'=0)&(h'=2) +1.2568169857543658047e-08:(u'=1)&(h'=2) +2.1502523264459663671e-05:(u'=2)&(h'=2) +0.0048056663430471524209:(u'=3)&(h'=2) +0.14030224048590858588:(u'=4)&(h'=2) +0.53508453814497702883:(u'=5)&(h'=2) +0.26657965447535209025:(u'=6)&(h'=2);
[c1] u=5 & v=0 -> 5.3879239700666423855e-05:(u'=0)&(h'=1) +0.0010237774039232444816:(u'=1)&(h'=1) +0.0086092010038132781719:(u'=2)&(h'=1) +0.032040064521721665913:(u'=3)&(h'=1) +0.052771221007733036534:(u'=4)&(h'=1) +0.038465743419082952526:(u'=5)&(h'=1) +0.012408644555557631073:(u'=6)&(h'=1) +2.4808877203328967875e-18:(u'=0)&(h'=2) +3.2916148458884736423e-12:(u'=1)&(h'=2) +2.0695100040225614324e-07:(u'=2)&(h'=2) +0.00061657038735794030687:(u'=3)&(h'=2) +0.08704712060273858687:(u'=4)&(h'=2) +0.58234824613775559854:(u'=5)&(h'=2) +0.18461532476632336319:(u'=6)&(h'=2);
[c2] u=5 & v=0 -> 3.5457451481830273805e-06:(u'=0)&(h'=1) +0.00019358612003289482379:(u'=1)&(h'=1) +0.0032341914631950643109:(u'=2)&(h'=1) +0.016534156728950904353:(u'=3)&(h'=1) +0.025865637473291860915:(u'=4)&(h'=1) +0.012381952546896503667:(u'=5)&(h'=1) +0.0018137603216692491613:(u'=6)&(h'=1) +3.0555119081292784825e-14:(u'=0)&(h'=2) +1.0092034238171203973e-09:(u'=1)&(h'=2) +3.8499596284443942138e-06:(u'=2)&(h'=2) +0.0016963535078133116368:(u'=3)&(h'=2) +0.086329509329428996689:(u'=4)&(h'=2) +0.50744024658729325328:(u'=5)&(h'=2) +0.34450320920741733799:(u'=6)&(h'=2);
[c0] u=6 & v=0 -> 6.7455947713482173986e-08:(u'=0)&(h'=1) +8.250735547749958666e-06:(u'=1)&(h'=1) +0.00031415043949103044771:(u'=2)&(h'=1) +0.0037235334621175861756:(u'=3)&(h'=1) +0.013738693524761079814:(u'=4)&(h'=1) +0.015780043474792962432:(u'=5)&(h'=1) +0.0056421358693466861639:(u'=6)&(h'=1) +1.5539389413024312026e-15:(u'=0)&(h'=2) +6.7635648651969406084e-11:(u'=1)&(h'=2) +3.8456005595035226408e-07:(u'=2)&(h'=2) +0.00028562715148627301027:(u'=3)&(h'=2) +0.027712876652176910569:(u'=4)&(h'=2) +0.35124530862695552136:(u'=5)&(h'=2) +0.58154892797968327223:(u'=6)&(h'=2);
[c1] u=6 & v=0 -> 3.8331939036190968096e-06:(u'=0)&(h'=1) +0.00012344890158254252441:(u'=1)&(h'=1) +0.0017594903849019129152:(u'=2)&(h'=1) +0.011098385153376697301:(u'=3)&(h'=1) +0.030981747724546947198:(u'=4)&(h'=1) +0.038275886742083271852:(u'=5)&(h'=1) +0.020927523340190757467:(u'=6)&(h'=1) +2.1026035649475159804e-23:(u'=0)&(h'=2) +2.4122906513234438168e-16:(u'=1)&(h'=2) +1.3114703785293425693e-10:(u'=2)&(h'=2) +3.37865581854651664e-06:(u'=3)&(h'=2) +0.0041246398594724587375:(u'=4)&(h'=2) +0.23860785180142857209:(u'=5)&(h'=2) +0.65409381411154732255:(u'=6)&(h'=2);
[c2] u=6 & v=0 -> 1.0347605875277509927e-07:(u'=0)&(h'=1) +1.2942140034963387635e-05:(u'=1)&(h'=1) +0.00049533284114802115638:(u'=2)&(h'=1) +0.0058011348961660479454:(u'=3)&(h'=1) +0.020789958304953448653:(u'=4)&(h'=1) +0.022799172523960860304:(u'=5)&(h'=1) +0.0076508443067248559782:(u'=6)&(h'=1) +7.1309757202914564879e-17:(u'=0)&(h'=2) +7.1374898652235863099e-12:(u'=1)&(h'=2) +8.2513455898901673386e-08:(u'=2)&(h'=2) +0.0001101759426512162617:(u'=3)&(h'=2) +0.016991491341202983462:(u'=4)&(h'=2) +0.30266273179613667477:(u'=5)&(h'=2) +0.62268602991036881011:(u'=6)&(h'=2);
[c0] u=0 & v=1 -> (u'=0)&(h'=0);
[c1] u=0 & v=1 -> 0.28800890320137989553:(u'=0)&(h'=1) +0.39127148090681562742:(u'=1)&(h'=1) +0.23524678749708249903:(u'=2)&(h'=1) +0.062595402361519864032:(u'=3)&(h'=1) +0.0073711355208192080868:(u'=4)&(h'=1) +0.00038414889033507043517:(u'=5)&(h'=1) +8.8600872097344950546e-06:(u'=6)&(h'=1) +0.00022781225663809947764:(u'=0)&(h'=2) +0.0062521201720977612887:(u'=1)&(h'=2) +0.0081308165543853734569:(u'=2)&(h'=2) +0.0005010691020410522941:(u'=3)&(h'=2) +1.4632471889146019239e-06:(u'=4)&(h'=2) +2.0248571431128738473e-10:(u'=5)&(h'=2) +1.3277848016935405698e-15:(u'=6)&(h'=2);
[c2] u=0 & v=1 -> (u'=0)&(h'=2);
[c0] u=1 & v=1 -> (u'=1)&(h'=0);
[c1] u=1 & v=1 -> 0.13450302223441032434:(u'=0)&(h'=1) +0.30970390674024439459:(u'=1)&(h'=1) +0.31559822445964225146:(u'=2)&(h'=1) +0.14232973647246216498:(u'=3)&(h'=1) +0.028407300530203190292:(u'=4)&(h'=1) +0.0025092129080946292546:(u'=5)&(h'=1) +9.8088543707617963617e-05:(u'=6)&(h'=1) +1.5314917822066659124e-05:(u'=0)&(h'=2) +0.0036344210244367105601:(u'=1)&(h'=2) +0.040870732017625872878:(u'=2)&(h'=2) +0.021779415039548489369:(u'=3)&(h'=2) +0.00054996698698170593065:(u'=4)&(h'=2) +6.5808750526704745294e-07:(u'=5)&(h'=2) +3.7315329800401052319e-11:(u'=6)&(h'=2);
[c2] u=1 & v=1 -> (u'=1)&(h'=2);
[c0] u=2 & v=1 -> (u'=2)&(h'=0);
[c1] u=2 & v=1 -> 0.039930307842923180861:(u'=0)&(h'=1) +0.15583308175631960246:(u'=1)&(h'=1) +0.26914721288136983501:(u'=2)&(h'=1) +0.20572797011644505805:(u'=3)&(h'=1) +0.069593715219360571811:(u'=4)&(h'=1) +0.010418853439346153697:(u'=5)&(h'=1) +0.00069030824836099132381:(u'=6)&(h'=1) +1.8781879021858003016e-07:(u'=0)&(h'=2) +0.00038541617639479533366:(u'=1)&(h'=2) +0.037478090285502960177:(u'=2)&(h'=2) +0.17269572317882314616:(u'=3)&(h'=2) +0.037708766506962573817:(u'=4)&(h'=2) +0.00039017522116869846494:(u'=5)&(h'=2) +1.9130823229311818931e-07:(u'=6)&(h'=2);
[c2] u=2 & v=1 -> (u'=2)&(h'=2);
[c0] u=3 & v=1 -> (u'=3)&(h'=0);
[c1] u=3 & v=1 -> 0.0064288336052728900852:(u'=0)&(h'=1) +0.042523749025810499147:(u'=1)&(h'=1) +0.12448130537344875846:(u'=2)&(h'=1) +0.16126864912655680673:(u'=3)&(h'=1) +0.092463214742646279709:(u'=4)&(h'=1) +0.023461796100624592032:(u'=5)&(h'=1) +0.0026346731771567603181:(u'=6)&(h'=1) +2.9830839452188160494e-10:(u'=0)&(h'=2) +5.2933024424401851974e-06:(u'=1)&(h'=2) +0.0044508663937534156604:(u'=2)&(h'=2) +0.17734502974759325244:(u'=3)&(h'=2) +0.33484984322019772929:(u'=4)&(h'=2) +0.02995972296354193834:(u'=5)&(h'=2) +0.00012702292264618158775:(u'=6)&(h'=2);
[c2] u=3 & v=1 -> (u'=3)&(h'=2);
[c0] u=4 & v=1 -> (u'=4)&(h'=0);
[c1] u=4 & v=1 -> 0.00065621050867103200652:(u'=0)&(h'=1) +0.0073567314371043423388:(u'=1)&(h'=1) +0.036500587081744147178:(u'=2)&(h'=1) +0.080147139002573211664:(u'=3)&(h'=1) +0.077884211034385850136:(u'=4)&(h'=1) +0.03349531391112322426:(u'=5)&(h'=1) +0.0063751719977752033947:(u'=6)&(h'=1) +6.4780445064108874949e-14:(u'=0)&(h'=2) +9.9397507923181241725e-09:(u'=1)&(h'=2) +7.2270935978299393333e-05:(u'=2)&(h'=2) +0.024900523483498686328:(u'=3)&(h'=2) +0.40654618515944784818:(u'=4)&(h'=2) +0.31453423162056914908:(u'=5)&(h'=2) +0.011531413887313489083:(u'=6)&(h'=2);
[c2] u=4 & v=1 -> (u'=4)&(h'=2);
[c0] u=5 & v=1 -> (u'=5)&(h'=0);
[c1] u=5 & v=1 -> 5.3879239700666423855e-05:(u'=0)&(h'=1) +0.0010237774039232444816:(u'=1)&(h'=1) +0.0086092010038132781719:(u'=2)&(h'=1) +0.032040064521721665913:(u'=3)&(h'=1) +0.052771221007733036534:(u'=4)&(h'=1) +0.038465743419082952526:(u'=5)&(h'=1) +0.012408644555557631073:(u'=6)&(h'=1) +2.4808877203328967875e-18:(u'=0)&(h'=2) +3.2916148458884736423e-12:(u'=1)&(h'=2) +2.0695100040225614324e-07:(u'=2)&(h'=2) +0.00061657038735794030687:(u'=3)&(h'=2) +0.08704712060273858687:(u'=4)&(h'=2) +0.58234824613775559854:(u'=5)&(h'=2) +0.18461532476632336319:(u'=6)&(h'=2);
[c2] u=5 & v=1 -> (u'=5)&(h'=2);
[c0] u=6 & v=1 -> (u'=6)&(h'=0);
[c1] u=6 & v=1 -> 3.8331939036190968096e-06:(u'=0)&(h'=1) +0.00012344890158254252441:(u'=1)&(h'=1) +0.0017594903849019129152:(u'=2)&(h'=1) +0.011098385153376697301:(u'=3)&(h'=1) +0.030981747724546947198:(u'=4)&(h'=1) +0.038275886742083271852:(u'=5)&(h'=1) +0.020927523340190757467:(u'=6)&(h'=1) +2.1026035649475159804e-23:(u'=0)&(h'=2) +2.4122906513234438168e-16:(u'=1)&(h'=2) +1.3114703785293425693e-10:(u'=2)&(h'=2) +3.37865581854651664e-06:(u'=3)&(h'=2) +0.0041246398594724587375:(u'=4)&(h'=2) +0.23860785180142857209:(u'=5)&(h'=2) +0.65409381411154732255:(u'=6)&(h'=2);
[c2] u=6 & v=1 -> (u'=6)&(h'=2);
[c0] u=0 & v=2 -> (u'=0)&(h'=2);
[c1] u=0 & v=2 -> (u'=0)&(h'=0);
[c2] u=0 & v=2 -> 0.21288772333811173398:(u'=0)&(h'=1) +0.18421276765925165275:(u'=1)&(h'=1) +0.048776838768533573032:(u'=2)&(h'=1) +0.0039521405915898134148:(u'=3)&(h'=1) +9.7988685926075837392e-05:(u'=4)&(h'=1) +7.434372100498882646e-07:(u'=5)&(h'=1) +1.7259867910456124629e-09:(u'=6)&(h'=1) +9.0729726941287742103e-05:(u'=0)&(h'=2) +0.011725605468126109113:(u'=1)&(h'=2) +0.17502644687673363233:(u'=2)&(h'=2) +0.30175522664888276836:(u'=3)&(h'=2) +0.060088124862662128933:(u'=4)&(h'=2) +0.0013819910397660074928:(u'=5)&(h'=2) +3.6711702784259513425e-06:(u'=6)&(h'=2);
[c0] u=1 & v=2 -> (u'=1)&(h'=2);
[c1] u=1 & v=2 -> (u'=1)&(h'=0);
[c2] u=1 & v=2 -> 0.079913264970475544891:(u'=0)&(h'=1) +0.15841179036699215565:(u'=1)&(h'=1) +0.096090608303711633198:(u'=2)&(h'=1) +0.017836071132617405122:(u'=3)&(h'=1) +0.0010130765468966131896:(u'=4)&(h'=1) +1.7608004468539763617e-05:(u'=5)&(h'=1) +9.3648932408789295583e-08:(u'=6)&(h'=1) +3.7943387171404232187e-06:(u'=0)&(h'=2) +0.0014860163339211935902:(u'=1)&(h'=2) +0.06721927041888171861:(u'=2)&(h'=2) +0.35119371193869536318:(u'=3)&(h'=2) +0.21192509856364877274:(u'=4)&(h'=2) +0.014770689945178029634:(u'=5)&(h'=2) +0.00011890548686346597961:(u'=6)&(h'=2);
[c0] u=2 & v=2 -> (u'=2)&(h'=2);
[c1] u=2 & v=2 -> (u'=2)&(h'=0);
[c2] u=2 & v=2 -> 0.013402499283233363855:(u'=0)&(h'=1) +0.060863081644350724986:(u'=1)&(h'=1) +0.084575952184433769721:(u'=2)&(h'=1) +0.035963724870661427369:(u'=3)&(h'=1) +0.0046795840269372238063:(u'=4)&(h'=1) +0.0001863265084809737212:(u'=5)&(h'=1) +2.2702142982740675402e-06:(u'=6)&(h'=1) +9.44983427385831633e-08:(u'=0)&(h'=2) +0.00011215367014677117335:(u'=1)&(h'=2) +0.015373951747493629777:(u'=2)&(h'=2) +0.2434110348713768579:(u'=3)&(h'=2) +0.44512064484406832499:(u'=4)&(h'=2) +0.094015170445171783453:(u'=5)&(h'=2) +0.0022935111910040175374:(u'=6)&(h'=2);
[c0] u=3 & v=2 -> (u'=3)&(h'=2);
[c1] u=3 & v=2 -> (u'=3)&(h'=0);
[c2] u=3 & v=2 -> 0.001159485712318920024:(u'=0)&(h'=1) +0.012062381624449931491:(u'=1)&(h'=1) +0.038399497394709727893:(u'=2)&(h'=1) +0.037406134257301493218:(u'=3)&(h'=1) +0.011150258330049237637:(u'=4)&(h'=1) +0.001017072338609832172:(u'=5)&(h'=1) +2.838857344195669331e-05:(u'=6)&(h'=1) +1.2088645214868658098e-09:(u'=0)&(h'=2) +4.347791828870032126e-06:(u'=1)&(h'=2) +0.0018061032651615588178:(u'=2)&(h'=2) +0.086656099918943421678:(u'=3)&(h'=2) +0.48021799041089147098:(u'=4)&(h'=2) +0.30736926491229626945:(u'=5)&(h'=2) +0.022722974261132771606:(u'=6)&(h'=2);
[c0] u=4 & v=2 -> (u'=4)&(h'=2);
[c1] u=4 & v=2 -> (u'=4)&(h'=0);
[c2] u=4 & v=2 -> 7.5763995221547560566e-05:(u'=0)&(h'=1) +0.0018056353499900079911:(u'=1)&(h'=1) +0.013168067432434813965:(u'=2)&(h'=1) +0.029385889947837955799:(u'=3)&(h'=1) +0.020066908316406725094:(u'=4)&(h'=1) +0.0041932127508689104323:(u'=5)&(h'=1) +0.00026812551379252856773:(u'=6)&(h'=1) +8.0924389931295820504e-12:(u'=0)&(h'=2) +8.8200765912586724263e-08:(u'=1)&(h'=2) +0.00011103195952037395048:(u'=2)&(h'=2) +0.016143822651773213905:(u'=3)&(h'=2) +0.27111121111221087032:(u'=4)&(h'=2) +0.52586141027245159041:(u'=5)&(h'=2) +0.11780883248863321944:(u'=6)&(h'=2);
[c0] u=5 & v=2 -> (u'=5)&(h'=2);
[c1] u=5 & v=2 -> (u'=5)&(h'=0);
[c2] u=5 & v=2 -> 3.5457451481830273805e-06:(u'=0)&(h'=1) +0.00019358612003289482379:(u'=1)&(h'=1) +0.0032341914631950643109:(u'=2)&(h'=1) +0.016534156728950904353:(u'=3)&(h'=1) +0.025865637473291860915:(u'=4)&(h'=1) +0.012381952546896503667:(u'=5)&(h'=1) +0.0018137603216692491613:(u'=6)&(h'=1) +3.0555119081292784825e-14:(u'=0)&(h'=2) +1.0092034238171203973e-09:(u'=1)&(h'=2) +3.8499596284443942138e-06:(u'=2)&(h'=2) +0.0016963535078133116368:(u'=3)&(h'=2) +0.086329509329428996689:(u'=4)&(h'=2) +0.50744024658729325328:(u'=5)&(h'=2) +0.34450320920741733799:(u'=6)&(h'=2);
[c0] u=6 & v=2 -> (u'=6)&(h'=2);
[c1] u=6 & v=2 -> (u'=6)&(h'=0);
[c2] u=6 & v=2 -> 1.0347605875277509927e-07:(u'=0)&(h'=1) +1.2942140034963387635e-05:(u'=1)&(h'=1) +0.00049533284114802115638:(u'=2)&(h'=1) +0.0058011348961660479454:(u'=3)&(h'=1) +0.020789958304953448653:(u'=4)&(h'=1) +0.022799172523960860304:(u'=5)&(h'=1) +0.0076508443067248559782:(u'=6)&(h'=1) +7.1309757202914564879e-17:(u'=0)&(h'=2) +7.1374898652235863099e-12:(u'=1)&(h'=2) +8.2513455898901673386e-08:(u'=2)&(h'=2) +0.0001101759426512162617:(u'=3)&(h'=2) +0.016991491341202983462:(u'=4)&(h'=2) +0.30266273179613667477:(u'=5)&(h'=2) +0.62268602991036881011:(u'=6)&(h'=2);
[c0] u=0 & v=3 -> 0.30898673520641067869:(u'=0)&(h'=1) +0.43939345120311446014:(u'=1)&(h'=1) +0.19450909322973192195:(u'=2)&(h'=1) +0.02680395152338755152:(u'=3)&(h'=1) +0.0011498212312096522079:(u'=4)&(h'=1) +1.5354455087369958091e-05:(u'=5)&(h'=1) +6.3827976791975726098e-08:(u'=6)&(h'=1) +0.00011642294215262604805:(u'=0)&(h'=2) +0.0037614345599554120311:(u'=1)&(h'=2) +0.015875055576409027175:(u'=2)&(h'=2) +0.0087523323728912211933:(u'=3)&(h'=2) +0.00063034621989866530204:(u'=4)&(h'=2) +5.9303634069355602054e-06:(u'=5)&(h'=2) +7.2883675433195704392e-09:(u'=6)&(h'=2);
[c1] u=0 & v=3 -> (u'=0)&(h'=2);
[c2] u=0 & v=3 -> (u'=0)&(h'=0);
[c0] u=1 & v=3 -> 0.10668110075909956191:(u'=0)&(h'=1) +0.31873347543022956252:(u'=1)&(h'=1) +0.29644249066083361299:(u'=2)&(h'=1) +0.085827371813468833484:(u'=3)&(h'=1) +0.0077354175135099468782:(u'=4)&(h'=1) +0.00021702726133448495727:(u'=5)&(h'=1) +1.8954721420207443197e-06:(u'=6)&(h'=1) +3.647244319482400611e-05:(u'=0)&(h'=2) +0.0039160743170279684044:(u'=1)&(h'=2) +0.054926736634011666394:(u'=2)&(h'=2) +0.10063834185533120091:(u'=3)&(h'=2) +0.024087401502441981721:(u'=4)&(h'=2) +0.00075311835869592668857:(u'=5)&(h'=2) +3.0759786785181408682e-06:(u'=6)&(h'=2);
[c1] u=1 & v=3 -> (u'=1)&(h'=2);
[c2] u=1 & v=3 -> (u'=1)&(h'=0);
[c0] u=2 & v=3 -> 0.015584210442122797824:(u'=0)&(h'=1) +0.097825356661324663898:(u'=1)&(h'=1) +0.1911572002171130491:(u'=2)&(h'=1) +0.11627931567224426834:(u'=3)&(h'=1) +0.022018455840963842979:(u'=4)&(h'=1) +0.0012979077779776174942:(u'=5)&(h'=1) +2.3816250889918073793e-05:(u'=6)&(h'=1) +2.6810743303148094259e-06:(u'=0)&(h'=2) +0.00095667858209287810756:(u'=1)&(h'=2) +0.044593345087592162201:(u'=2)&(h'=2) +0.27153189787407333577:(u'=3)&(h'=2) +0.21598244958483320266:(u'=4)&(h'=2) +0.022442067968721640669:(u'=5)&(h'=2) +0.00030461696572036626313:(u'=6)&(h'=2);
[c1] u=2 & v=3 -> (u'=2)&(h'=2);
[c2] u=2 & v=3 -> (u'=2)&(h'=0);
[c0] u=3 & v=3 -> 0.0010875840841770762803:(u'=0)&(h'=1) +0.014343526005252731081:(u'=1)&(h'=1) +0.058887293184594846629:(u'=2)&(h'=1) +0.075259242715132998458:(u'=3)&(h'=1) +0.029941301957836990305:(u'=4)&(h'=1) +0.0037081227609795535706:(u'=5)&(h'=1) +0.00014295854221701008338:(u'=6)&(h'=1) +4.7272840539632717558e-08:(u'=0)&(h'=2) +5.6058312966395032202e-05:(u'=1)&(h'=2) +0.0086839067693035391915:(u'=2)&(h'=2) +0.17572642918985531546:(u'=3)&(h'=2) +0.46452149986395729897:(u'=4)&(h'=2) +0.16040627687414271696:(u'=5)&(h'=2) +0.0072357524667429635318:(u'=6)&(h'=2);
[c1] u=3 & v=3 -> (u'=3)&(h'=2);
[c2] u=3 & v=3 -> (u'=3)&(h'=0);
[c0] u=4 & v=3 -> 5.4756168979187192132e-05:(u'=0)&(h'=1) +0.0015172340567196165341:(u'=1)&(h'=1) +0.013087138400114533415:(u'=2)&(h'=1) +0.035140617845505331407:(u'=3)&(h'=1) +0.029372889805008368241:(u'=4)&(h'=1) +0.0076428712586563774325:(u'=5)&(h'=1) +0.00061906891477895545535:(u'=6)&(h'=1) +3.1265050791239630961e-10:(u'=0)&(h'=2) +1.2321358431801388432e-06:(u'=1)&(h'=2) +0.00063431480503624542832:(u'=2)&(h'=2) +0.04265774641040743359:(u'=3)&(h'=2) +0.37474666086245284058:(u'=4)&(h'=2) +0.43005543344980712295:(u'=5)&(h'=2) +0.064470035574040213122:(u'=6)&(h'=2);
[c1] u=4 & v=3 -> (u'=4)&(h'=2);
[c2] u=4 & v=3 -> (u'=4)&(h'=0);
[c0] u=5 & v=3 -> 2.1981317726021309722e-06:(u'=0)&(h'=1) +0.00012796750338896860084:(u'=1)&(h'=1) +0.0023190934833383328346:(u'=2)&(h'=1) +0.01308306198944987099:(u'=3)&(h'=1) +0.022975931508274247128:(u'=4)&(h'=1) +0.012560572709265090119:(u'=5)&(h'=1) +0.0021375601328322280104:(u'=6)&(h'=1) +9.5962479399716750941e-13:(u'=0)&(h'=2) +1.2568169857543658047e-08:(u'=1)&(h'=2) +2.1502523264459663671e-05:(u'=2)&(h'=2) +0.0048056663430471524209:(u'=3)&(h'=2) +0.14030224048590858588:(u'=4)&(h'=2) +0.53508453814497702883:(u'=5)&(h'=2) +0.26657965447535209025:(u'=6)&(h'=2);
[c1] u=5 & v=3 -> (u'=5)&(h'=2);
[c2] u=5 & v=3 -> (u'=5)&(h'=0);
[c0] u=6 & v=3 -> 6.7455947713482173986e-08:(u'=0)&(h'=1) +8.250735547749958666e-06:(u'=1)&(h'=1) +0.00031415043949103044771:(u'=2)&(h'=1) +0.0037235334621175861756:(u'=3)&(h'=1) +0.013738693524761079814:(u'=4)&(h'=1) +0.015780043474792962432:(u'=5)&(h'=1) +0.0056421358693466861639:(u'=6)&(h'=1) +1.5539389413024312026e-15:(u'=0)&(h'=2) +6.7635648651969406084e-11:(u'=1)&(h'=2) +3.8456005595035226408e-07:(u'=2)&(h'=2) +0.00028562715148627301027:(u'=3)&(h'=2) +0.027712876652176910569:(u'=4)&(h'=2) +0.35124530862695552136:(u'=5)&(h'=2) +0.58154892797968327223:(u'=6)&(h'=2);
[c1] u=6 & v=3 -> (u'=6)&(h'=2);
[c2] u=6 & v=3 -> (u'=6)&(h'=0);
[c0] u=0 & v=4 -> (u'=0)&(h'=0);
[c1] u=0 & v=4 -> 0.30898673520641067869:(u'=0)&(h'=1) +0.43939345120311446014:(u'=1)&(h'=1) +0.19450909322973192195:(u'=2)&(h'=1) +0.02680395152338755152:(u'=3)&(h'=1) +0.0011498212312096522079:(u'=4)&(h'=1) +1.5354455087369958091e-05:(u'=5)&(h'=1) +6.3827976791975726098e-08:(u'=6)&(h'=1) +0.00011642294215262604805:(u'=0)&(h'=2) +0.0037614345599554120311:(u'=1)&(h'=2) +0.015875055576409027175:(u'=2)&(h'=2) +0.0087523323728912211933:(u'=3)&(h'=2) +0.00063034621989866530204:(u'=4)&(h'=2) +5.9303634069355602054e-06:(u'=5)&(h'=2) +7.2883675433195704392e-09:(u'=6)&(h'=2);
[c2] u=0 & v=4 -> 0.21288772333811173398:(u'=0)&(h'=1) +0.18421276765925165275:(u'=1)&(h'=1) +0.048776838768533573032:(u'=2)&(h'=1) +0.0039521405915898134148:(u'=3)&(h'=1) +9.7988685926075837392e-05:(u'=4)&(h'=1) +7.434372100498882646e-07:(u'=5)&(h'=1) +1.7259867910456124629e-09:(u'=6)&(h'=1) +9.0729726941287742103e-05:(u'=0)&(h'=2) +0.011725605468126109113:(u'=1)&(h'=2) +0.17502644687673363233:(u'=2)&(h'=2) +0.30175522664888276836:(u'=3)&(h'=2) +0.060088124862662128933:(u'=4)&(h'=2) +0.0013819910397660074928:(u'=5)&(h'=2) +3.6711702784259513425e-06:(u'=6)&(h'=2);
[c0] u=1 & v=4 -> (u'=1)&(h'=0);
[c1] u=1 & v=4 -> 0.10668110075909956191:(u'=0)&(h'=1) +0.31873347543022956252:(u'=1)&(h'=1) +0.29644249066083361299:(u'=2)&(h'=1) +0.085827371813468833484:(u'=3)&(h'=1) +0.0077354175135099468782:(u'=4)&(h'=1) +0.00021702726133448495727:(u'=5)&(h'=1) +1.8954721420207443197e-06:(u'=6)&(h'=1) +3.647244319482400611e-05:(u'=0)&(h'=2) +0.0039160743170279684044:(u'=1)&(h'=2) +0.054926736634011666394:(u'=2)&(h'=2) +0.10063834185533120091:(u'=3)&(h'=2) +0.024087401502441981721:(u'=4)&(h'=2) +0.00075311835869592668857:(u'=5)&(h'=2) +3.0759786785181408682e-06:(u'=6)&(h'=2);
[c2] u=1 & v=4 -> 0.079913264970475544891:(u'=0)&(h'=1) +0.15841179036699215565:(u'=1)&(h'=1) +0.096090608303711633198:(u'=2)&(h'=1) +0.017836071132617405122:(u'=3)&(h'=1) +0.0010130765468966131896:(u'=4)&(h'=1) +1.7608004468539763617e-05:(u'=5)&(h'=1) +9.3648932408789295583e-08:(u'=6)&(h'=1) +3.7943387171404232187e-06:(u'=0)&(h'=2) +0.0014860163339211935902:(u'=1)&(h'=2) +0.06721927041888171861:(u'=2)&(h'=2) +0.35119371193869536318:(u'=3)&(h'=2) +0.21192509856364877274:(u'=4)&(h'=2) +0.014770689945178029634:(u'=5)&(h'=2) +0.00011890548686346597961:(u'=6)&(h'=2);
[c0] u=2 & v=4 -> (u'=2)&(h'=0);
[c1] u=2 & v=4 -> 0.015584210442122797824:(u'=0)&(h'=1) +0.097825356661324663898:(u'=1)&(h'=1) +0.1911572002171130491:(u'=2)&(h'=1) +0.11627931567224426834:(u'=3)&(h'=1) +0.022018455840963842979:(u'=4)&(h'=1) +0.0012979077779776174942:(u'=5)&(h'=1) +2.3816250889918073793e-05:(u'=6)&(h'=1) +2.6810743303148094259e-06:(u'=0)&(h'=2) +0.00095667858209287810756:(u'=1)&(h'=2) +0.044593345087592162201:(u'=2)&(h'=2) +0.27153189787407333577:(u'=3)&(h'=2) +0.21598244958483320266:(u'=4)&(h'=2) +0.022442067968721640669:(u'=5)&(h'=2) +0.00030461696572036626313:(u'=6)&(h'=2);
[c2] u=2 & v=4 -> 0.013402499283233363855:(u'=0)&(h'=1) +0.060863081644350724986:(u'=1)&(h'=1) +0.084575952184433769721:(u'=2)&(h'=1) +0.035963724870661427369:(u'=3)&(h'=1) +0.0046795840269372238063:(u'=4)&(h'=1) +0.0001863265084809737212:(u'=5)&(h'=1) +2.2702142982740675402e-06:(u'=6)&(h'=1) +9.44983427385831633e-08:(u'=0)&(h'=2) +0.00011215367014677117335:(u'=1)&(h'=2) +0.015373951747493629777:(u'=2)&(h'=2) +0.2434110348713768579:(u'=3)&(h'=2) +0.44512064484406832499:(u'=4)&(h'=2) +0.094015170445171783453:(u'=5)&(h'=2) +0.0022935111910040175374:(u'=6)&(h'=2);
[c0] u=3 & v=4 -> (u'=3)&(h'=0);
[c1] u=3 & v=4 -> 0.0010875840841770762803:(u'=0)&(h'=1) +0.014343526005252731081:(u'=1)&(h'=1) +0.058887293184594846629:(u'=2)&(h'=1) +0.075259242715132998458:(u'=3)&(h'=1) +0.029941301957836990305:(u'=4)&(h'=1) +0.0037081227609795535706:(u'=5)&(h'=1) +0.00014295854221701008338:(u'=6)&(h'=1) +4.7272840539632717558e-08:(u'=0)&(h'=2) +5.6058312966395032202e-05:(u'=1)&(h'=2) +0.0086839067693035391915:(u'=2)&(h'=2) +0.17572642918985531546:(u'=3)&(h'=2) +0.46452149986395729897:(u'=4)&(h'=2) +0.16040627687414271696:(u'=5)&(h'=2) +0.0072357524667429635318:(u'=6)&(h'=2);
[c2] u=3 & v=4 -> 0.001159485712318920024:(u'=0)&(h'=1) +0.012062381624449931491:(u'=1)&(h'=1) +0.038399497394709727893:(u'=2)&(h'=1) +0.037406134257301493218:(u'=3)&(h'=1) +0.011150258330049237637:(u'=4)&(h'=1) +0.001017072338609832172:(u'=5)&(h'=1) +2.838857344195669331e-05:(u'=6)&(h'=1) +1.2088645214868658098e-09:(u'=0)&(h'=2) +4.347791828870032126e-06:(u'=1)&(h'=2) +0.0018061032651615588178:(u'=2)&(h'=2) +0.086656099918943421678:(u'=3)&(h'=2) +0.48021799041089147098:(u'=4)&(h'=2) +0.30736926491229626945:(u'=5)&(h'=2) +0.022722974261132771606:(u'=6)&(h'=2);
[c0] u=4 & v=4 -> (u'=4)&(h'=0);
[c1] u=4 & v=4 -> 5.4756168979187192132e-05:(u'=0)&(h'=1) +0.0015172340567196165341:(u'=1)&(h'=1) +0.013087138400114533415:(u'=2)&(h'=1) +0.035140617845505331407:(u'=3)&(h'=1) +0.029372889805008368241:(u'=4)&(h'=1) +0.0076428712586563774325:(u'=5)&(h'=1) +0.00061906891477895545535:(u'=6)&(h'=1) +3.1265050791239630961e-10:(u'=0)&(h'=2) +1.2321358431801388432e-06:(u'=1)&(h'=2) +0.00063431480503624542832:(u'=2)&(h'=2) +0.04265774641040743359:(u'=3)&(h'=2) +0.37474666086245284058:(u'=4)&(h'=2) +0.43005543344980712295:(u'=5)&(h'=2) +0.064470035574040213122:(u'=6)&(h'=2);
[c2] u=4 & v=4 -> 7.5763995221547560566e-05:(u'=0)&(h'=1) +0.0018056353499900079911:(u'=1)&(h'=1) +0.013168067432434813965:(u'=2)&(h'=1) +0.029385889947837955799:(u'=3)&(h'=1) +0.020066908316406725094:(u'=4)&(h'=1) +0.0041932127508689104323:(u'=5)&(h'=1) +0.00026812551379252856773:(u'=6)&(h'=1) +8.0924389931295820504e-12:(u'=0)&(h'=2) +8.8200765912586724263e-08:(u'=1)&(h'=2) +0.00011103195952037395048:(u'=2)&(h'=2) +0.016143822651773213905:(u'=3)&(h'=2) +0.27111121111221087032:(u'=4)&(h'=2) +0.52586141027245159041:(u'=5)&(h'=2) +0.11780883248863321944:(u'=6)&(h'=2);
[c0] u=5 & v=4 -> (u'=5)&(h'=0);
[c1] u=5 & v=4 -> 2.1981317726021309722e-06:(u'=0)&(h'=1) +0.00012796750338896860084:(u'=1)&(h'=1) +0.0023190934833383328346:(u'=2)&(h'=1) +0.01308306198944987099:(u'=3)&(h'=1) +0.022975931508274247128:(u'=4)&(h'=1) +0.012560572709265090119:(u'=5)&(h'=1) +0.0021375601328322280104:(u'=6)&(h'=1) +9.5962479399716750941e-13:(u'=0)&(h'=2) +1.2568169857543658047e-08:(u'=1)&(h'=2) +2.1502523264459663671e-05:(u'=2)&(h'=2) +0.0048056663430471524209:(u'=3)&(h'=2) +0.14030224048590858588:(u'=4)&(h'=2) +0.53508453814497702883:(u'=5)&(h'=2) +0.26657965447535209025:(u'=6)&(h'=2);
[c2] u=5 & v=4 -> 3.5457451481830273805e-06:(u'=0)&(h'=1) +0.00019358612003289482379:(u'=1)&(h'=1) +0.0032341914631950643109:(u'=2)&(h'=1) +0.016534156728950904353:(u'=3)&(h'=1) +0.025865637473291860915:(u'=4)&(h'=1) +0.012381952546896503667:(u'=5)&(h'=1) +0.0018137603216692491613:(u'=6)&(h'=1) +3.0555119081292784825e-14:(u'=0)&(h'=2) +1.0092034238171203973e-09:(u'=1)&(h'=2) +3.8499596284443942138e-06:(u'=2)&(h'=2) +0.0016963535078133116368:(u'=3)&(h'=2) +0.086329509329428996689:(u'=4)&(h'=2) +0.50744024658729325328:(u'=5)&(h'=2) +0.34450320920741733799:(u'=6)&(h'=2);
[c0] u=6 & v=4 -> (u'=6)&(h'=0);
[c1] u=6 & v=4 -> 6.7455947713482173986e-08:(u'=0)&(h'=1) +8.250735547749958666e-06:(u'=1)&(h'=1) +0.00031415043949103044771:(u'=2)&(h'=1) +0.0037235334621175861756:(u'=3)&(h'=1) +0.013738693524761079814:(u'=4)&(h'=1) +0.015780043474792962432:(u'=5)&(h'=1) +0.0056421358693466861639:(u'=6)&(h'=1) +1.5539389413024312026e-15:(u'=0)&(h'=2) +6.7635648651969406084e-11:(u'=1)&(h'=2) +3.8456005595035226408e-07:(u'=2)&(h'=2) +0.00028562715148627301027:(u'=3)&(h'=2) +0.027712876652176910569:(u'=4)&(h'=2) +0.35124530862695552136:(u'=5)&(h'=2) +0.58154892797968327223:(u'=6)&(h'=2);
[c2] u=6 & v=4 -> 1.0347605875277509927e-07:(u'=0)&(h'=1) +1.2942140034963387635e-05:(u'=1)&(h'=1) +0.00049533284114802115638:(u'=2)&(h'=1) +0.0058011348961660479454:(u'=3)&(h'=1) +0.020789958304953448653:(u'=4)&(h'=1) +0.022799172523960860304:(u'=5)&(h'=1) +0.0076508443067248559782:(u'=6)&(h'=1) +7.1309757202914564879e-17:(u'=0)&(h'=2) +7.1374898652235863099e-12:(u'=1)&(h'=2) +8.2513455898901673386e-08:(u'=2)&(h'=2) +0.0001101759426512162617:(u'=3)&(h'=2) +0.016991491341202983462:(u'=4)&(h'=2) +0.30266273179613667477:(u'=5)&(h'=2) +0.62268602991036881011:(u'=6)&(h'=2);
[c0] u=0 & v=5 -> 0.28800890320137989553:(u'=0)&(h'=1) +0.39127148090681562742:(u'=1)&(h'=1) +0.23524678749708249903:(u'=2)&(h'=1) +0.062595402361519864032:(u'=3)&(h'=1) +0.0073711355208192080868:(u'=4)&(h'=1) +0.00038414889033507043517:(u'=5)&(h'=1) +8.8600872097344950546e-06:(u'=6)&(h'=1) +0.00022781225663809947764:(u'=0)&(h'=2) +0.0062521201720977612887:(u'=1)&(h'=2) +0.0081308165543853734569:(u'=2)&(h'=2) +0.0005010691020410522941:(u'=3)&(h'=2) +1.4632471889146019239e-06:(u'=4)&(h'=2) +2.0248571431128738473e-10:(u'=5)&(h'=2) +1.3277848016935405698e-15:(u'=6)&(h'=2);
[c1] u=0 & v=5 -> (u'=0)&(h'=0);
[c2] u=0 & v=5 -> 0.21288772333811173398:(u'=0)&(h'=1) +0.18421276765925165275:(u'=1)&(h'=1) +0.048776838768533573032:(u'=2)&(h'=1) +0.0039521405915898134148:(u'=3)&(h'=1) +9.7988685926075837392e-05:(u'=4)&(h'=1) +7.434372100498882646e-07:(u'=5)&(h'=1) +1.7259867910456124629e-09:(u'=6)&(h'=1) +9.0729726941287742103e-05:(u'=0)&(h'=2) +0.011725605468126109113:(u'=1)&(h'=2) +0.17502644687673363233:(u'=2)&(h'=2) +0.30175522664888276836:(u'=3)&(h'=2) +0.060088124862662128933:(u'=4)&(h'=2) +0.0013819910397660074928:(u'=5)&(h'=2) +3.6711702784259513425e-06:(u'=6)&(h'=2);
[c0] u=1 & v=5 -> 0.13450302223441032434:(u'=0)&(h'=1) +0.30970390674024439459:(u'=1)&(h'=1) +0.31559822445964225146:(u'=2)&(h'=1) +0.14232973647246216498:(u'=3)&(h'=1) +0.028407300530203190292:(u'=4)&(h'=1) +0.0025092129080946292546:(u'=5)&(h'=1) +9.8088543707617963617e-05:(u'=6)&(h'=1) +1.5314917822066659124e-05:(u'=0)&(h'=2) +0.0036344210244367105601:(u'=1)&(h'=2) +0.040870732017625872878:(u'=2)&(h'=2) +0.021779415039548489369:(u'=3)&(h'=2) +0.00054996698698170593065:(u'=4)&(h'=2) +6.5808750526704745294e-07:(u'=5)&(h'=2) +3.7315329800401052319e-11:(u'=6)&(h'=2);
[c1] u=1 & v=5 -> (u'=1)&(h'=0);
[c2] u=1 & v=5 -> 0.079913264970475544891:(u'=0)&(h'=1) +0.15841179036699215565:(u'=1)&(h'=1) +0.096090608303711633198:(u'=2)&(h'=1) +0.017836071132617405122:(u'=3)&(h'=1) +0.0010130765468966131896:(u'=4)&(h'=1) +1.7608004468539763617e-05:(u'=5)&(h'=1) +9.3648932408789295583e-08:(u'=6)&(h'=1) +3.7943387171404232187e-06:(u'=0)&(h'=2) +0.0014860163339211935902:(u'=1)&(h'=2) +0.06721927041888171861:(u'=2)&(h'=2) +0.35119371193869536318:(u'=3)&(h'=2) +0.21192509856364877274:(u'=4)&(h'=2) +0.014770689945178029634:(u'=5)&(h'=2) +0.00011890548686346597961:(u'=6)&(h'=2);
[c0] u=2 & v=5 -> 0.039930307842923180861:(u'=0)&(h'=1) +0.15583308175631960246:(u'=1)&(h'=1) +0.26914721288136983501:(u'=2)&(h'=1) +0.20572797011644505805:(u'=3)&(h'=1) +0.069593715219360571811:(u'=4)&(h'=1) +0.010418853439346153697:(u'=5)&(h'=1) +0.00069030824836099132381:(u'=6)&(h'=1) +1.8781879021858003016e-07:(u'=0)&(h'=2) +0.00038541617639479533366:(u'=1)&(h'=2) +0.037478090285502960177:(u'=2)&(h'=2) +0.17269572317882314616:(u'=3)&(h'=2) +0.037708766506962573817:(u'=4)&(h'=2) +0.00039017522116869846494:(u'=5)&(h'=2) +1.9130823229311818931e-07:(u'=6)&(h'=2);
[c1] u=2 & v=5 -> (u'=2)&(h'=0);
[c2] u=2 & v=5 -> 0.013402499283233363855:(u'=0)&(h'=1) +0.060863081644350724986:(u'=1)&(h'=1) +0.084575952184433769721:(u'=2)&(h'=1) +0.035963724870661427369:(u'=3)&(h'=1) +0.0046795840269372238063:(u'=4)&(h'=1) +0.0001863265084809737212:(u'=5)&(h'=1) +2.2702142982740675402e-06:(u'=6)&(h'=1) +9.44983427385831633e-08:(u'=0)&(h'=2) +0.00011215367014677117335:(u'=1)&(h'=2) +0.015373951747493629777:(u'=2)&(h'=2) +0.2434110348713768579:(u'=3)&(h'=2) +0.44512064484406832499:(u'=4)&(h'=2) +0.094015170445171783453:(u'=5)&(h'=2) +0.0022935111910040175374:(u'=6)&(h'=2);
[c0] u=3 & v=5 -> 0.0064288336052728900852:(u'=0)&(h'=1) +0.042523749025810499147:(u'=1)&(h'=1) +0.12448130537344875846:(u'=2)&(h'=1) +0.16126864912655680673:(u'=3)&(h'=1) +0.092463214742646279709:(u'=4)&(h'=1) +0.023461796100624592032:(u'=5)&(h'=1) +0.0026346731771567603181:(u'=6)&(h'=1) +2.9830839452188160494e-10:(u'=0)&(h'=2) +5.2933024424401851974e-06:(u'=1)&(h'=2) +0.0044508663937534156604:(u'=2)&(h'=2) +0.17734502974759325244:(u'=3)&(h'=2) +0.33484984322019772929:(u'=4)&(h'=2) +0.02995972296354193834:(u'=5)&(h'=2) +0.00012702292264618158775:(u'=6)&(h'=2);
[c1] u=3 & v=5 -> (u'=3)&(h'=0);
[c2] u=3 & v=5 -> 0.001159485712318920024:(u'=0)&(h'=1) +0.012062381624449931491:(u'=1)&(h'=1) +0.038399497394709727893:(u'=2)&(h'=1) +0.037406134257301493218:(u'=3)&(h'=1) +0.011150258330049237637:(u'=4)&(h'=1) +0.001017072338609832172:(u'=5)&(h'=1) +2.838857344195669331e-05:(u'=6)&(h'=1) +1.2088645214868658098e-09:(u'=0)&(h'=2) +4.347791828870032126e-06:(u'=1)&(h'=2) +0.0018061032651615588178:(u'=2)&(h'=2) +0.086656099918943421678:(u'=3)&(h'=2) +0.48021799041089147098:(u'=4)&(h'=2) +0.30736926491229626945:(u'=5)&(h'=2) +0.022722974261132771606:(u'=6)&(h'=2);
[c0] u=4 & v=5 -> 0.00065621050867103200652:(u'=0)&(h'=1) +0.0073567314371043423388:(u'=1)&(h'=1) +0.036500587081744147178:(u'=2)&(h'=1) +0.080147139002573211664:(u'=3)&(h'=1) +0.077884211034385850136:(u'=4)&(h'=1) +0.03349531391112322426:(u'=5)&(h'=1) +0.0063751719977752033947:(u'=6)&(h'=1) +6.4780445064108874949e-14:(u'=0)&(h'=2) +9.9397507923181241725e-09:(u'=1)&(h'=2) +7.2270935978299393333e-05:(u'=2)&(h'=2) +0.024900523483498686328:(u'=3)&(h'=2) +0.40654618515944784818:(u'=4)&(h'=2) +0.31453423162056914908:(u'=5)&(h'=2) +0.011531413887313489083:(u'=6)&(h'=2);
[c1] u=4 & v=5 -> (u'=4)&(h'=0);
[c2] u=4 & v=5 -> 7.5763995221547560566e-05:(u'=0)&(h'=1) +0.0018056353499900079911:(u'=1)&(h'=1) +0.013168067432434813965:(u'=2)&(h'=1) +0.029385889947837955799:(u'=3)&(h'=1) +0.020066908316406725094:(u'=4)&(h'=1) +0.0041932127508689104323:(u'=5)&(h'=1) +0.00026812551379252856773:(u'=6)&(h'=1) +8.0924389931295820504e-12:(u'=0)&(h'=2) +8.8200765912586724263e-08:(u'=1)&(h'=2) +0.00011103195952037395048:(u'=2)&(h'=2) +0.016143822651773213905:(u'=3)&(h'=2) +0.27111121111221087032:(u'=4)&(h'=2) +0.52586141027245159041:(u'=5)&(h'=2) +0.11780883248863321944:(u'=6)&(h'=2);
[c0] u=5 & v=5 -> 5.3879239700666423855e-05:(u'=0)&(h'=1) +0.0010237774039232444816:(u'=1)&(h'=1) +0.0086092010038132781719:(u'=2)&(h'=1) +0.032040064521721665913:(u'=3)&(h'=1) +0.052771221007733036534:(u'=4)&(h'=1) +0.038465743419082952526:(u'=5)&(h'=1) +0.012408644555557631073:(u'=6)&(h'=1) +2.4808877203328967875e-18:(u'=0)&(h'=2) +3.2916148458884736423e-12:(u'=1)&(h'=2) +2.0695100040225614324e-07:(u'=2)&(h'=2) +0.00061657038735794030687:(u'=3)&(h'=2) +0.08704712060273858687:(u'=4)&(h'=2) +0.58234824613775559854:(u'=5)&(h'=2) +0.18461532476632336319:(u'=6)&(h'=2);
[c1] u=5 & v=5 -> (u'=5)&(h'=0);
[c2] u=5 & v=5 -> 3.5457451481830273805e-06:(u'=0)&(h'=1) +0.00019358612003289482379:(u'=1)&(h'=1) +0.0032341914631950643109:(u'=2)&(h'=1) +0.016534156728950904353:(u'=3)&(h'=1) +0.025865637473291860915:(u'=4)&(h'=1) +0.012381952546896503667:(u'=5)&(h'=1) +0.0018137603216692491613:(u'=6)&(h'=1) +3.0555119081292784825e-14:(u'=0)&(h'=2) +1.0092034238171203973e-09:(u'=1)&(h'=2) +3.8499596284443942138e-06:(u'=2)&(h'=2) +0.0016963535078133116368:(u'=3)&(h'=2) +0.086329509329428996689:(u'=4)&(h'=2) +0.50744024658729325328:(u'=5)&(h'=2) +0.34450320920741733799:(u'=6)&(h'=2);
[c0] u=6 & v=5 -> 3.8331939036190968096e-06:(u'=0)&(h'=1) +0.00012344890158254252441:(u'=1)&(h'=1) +0.0017594903849019129152:(u'=2)&(h'=1) +0.011098385153376697301:(u'=3)&(h'=1) +0.030981747724546947198:(u'=4)&(h'=1) +0.038275886742083271852:(u'=5)&(h'=1) +0.020927523340190757467:(u'=6)&(h'=1) +2.1026035649475159804e-23:(u'=0)&(h'=2) +2.4122906513234438168e-16:(u'=1)&(h'=2) +1.3114703785293425693e-10:(u'=2)&(h'=2) +3.37865581854651664e-06:(u'=3)&(h'=2) +0.0041246398594724587375:(u'=4)&(h'=2) +0.23860785180142857209:(u'=5)&(h'=2) +0.65409381411154732255:(u'=6)&(h'=2);
[c1] u=6 & v=5 -> (u'=6)&(h'=0);
[c2] u=6 & v=5 -> 1.0347605875277509927e-07:(u'=0)&(h'=1) +1.2942140034963387635e-05:(u'=1)&(h'=1) +0.00049533284114802115638:(u'=2)&(h'=1) +0.0058011348961660479454:(u'=3)&(h'=1) +0.020789958304953448653:(u'=4)&(h'=1) +0.022799172523960860304:(u'=5)&(h'=1) +0.0076508443067248559782:(u'=6)&(h'=1) +7.1309757202914564879e-17:(u'=0)&(h'=2) +7.1374898652235863099e-12:(u'=1)&(h'=2) +8.2513455898901673386e-08:(u'=2)&(h'=2) +0.0001101759426512162617:(u'=3)&(h'=2) +0.016991491341202983462:(u'=4)&(h'=2) +0.30266273179613667477:(u'=5)&(h'=2) +0.62268602991036881011:(u'=6)&(h'=2);
[c0] u=0 & v=6 -> 0.28800890320137989553:(u'=0)&(h'=1) +0.39127148090681562742:(u'=1)&(h'=1) +0.23524678749708249903:(u'=2)&(h'=1) +0.062595402361519864032:(u'=3)&(h'=1) +0.0073711355208192080868:(u'=4)&(h'=1) +0.00038414889033507043517:(u'=5)&(h'=1) +8.8600872097344950546e-06:(u'=6)&(h'=1) +0.00022781225663809947764:(u'=0)&(h'=2) +0.0062521201720977612887:(u'=1)&(h'=2) +0.0081308165543853734569:(u'=2)&(h'=2) +0.0005010691020410522941:(u'=3)&(h'=2) +1.4632471889146019239e-06:(u'=4)&(h'=2) +2.0248571431128738473e-10:(u'=5)&(h'=2) +1.3277848016935405698e-15:(u'=6)&(h'=2);
[c1] u=0 & v=6 -> 0.30898673520641067869:(u'=0)&(h'=1) +0.43939345120311446014:(u'=1)&(h'=1) +0.19450909322973192195:(u'=2)&(h'=1) +0.02680395152338755152:(u'=3)&(h'=1) +0.0011498212312096522079:(u'=4)&(h'=1) +1.5354455087369958091e-05:(u'=5)&(h'=1) +6.3827976791975726098e-08:(u'=6)&(h'=1) +0.00011642294215262604805:(u'=0)&(h'=2) +0.0037614345599554120311:(u'=1)&(h'=2) +0.015875055576409027175:(u'=2)&(h'=2) +0.0087523323728912211933:(u'=3)&(h'=2) +0.00063034621989866530204:(u'=4)&(h'=2) +5.9303634069355602054e-06:(u'=5)&(h'=2) +7.2883675433195704392e-09:(u'=6)&(h'=2);
[c2] u=0 & v=6 -> (u'=0)&(h'=0);
[c0] u=1 & v=6 -> 0.13450302223441032434:(u'=0)&(h'=1) +0.30970390674024439459:(u'=1)&(h'=1) +0.31559822445964225146:(u'=2)&(h'=1) +0.14232973647246216498:(u'=3)&(h'=1) +0.028407300530203190292:(u'=4)&(h'=1) +0.0025092129080946292546:(u'=5)&(h'=1) +9.8088543707617963617e-05:(u'=6)&(h'=1) +1.5314917822066659124e-05:(u'=0)&(h'=2) +0.0036344210244367105601:(u'=1)&(h'=2) +0.040870732017625872878:(u'=2)&(h'=2) +0.021779415039548489369:(u'=3)&(h'=2) +0.00054996698698170593065:(u'=4)&(h'=2) +6.5808750526704745294e-07:(u'=5)&(h'=2) +3.7315329800401052319e-11:(u'=6)&(h'=2);
[c1] u=1 & v=6 -> 0.10668110075909956191:(u'=0)&(h'=1) +0.31873347543022956252:(u'=1)&(h'=1) +0.29644249066083361299:(u'=2)&(h'=1) +0.085827371813468833484:(u'=3)&(h'=1) +0.0077354175135099468782:(u'=4)&(h'=1) +0.00021702726133448495727:(u'=5)&(h'=1) +1.8954721420207443197e-06:(u'=6)&(h'=1) +3.647244319482400611e-05:(u'=0)&(h'=2) +0.0039160743170279684044:(u'=1)&(h'=2) +0.054926736634011666394:(u'=2)&(h'=2) +0.10063834185533120091:(u'=3)&(h'=2) +0.024087401502441981721:(u'=4)&(h'=2) +0.00075311835869592668857:(u'=5)&(h'=2) +3.0759786785181408682e-06:(u'=6)&(h'=2);
[c2] u=1 & v=6 -> (u'=1)&(h'=0);
[c0] u=2 & v=6 -> 0.039930307842923180861:(u'=0)&(h'=1) +0.15583308175631960246:(u'=1)&(h'=1) +0.26914721288136983501:(u'=2)&(h'=1) +0.20572797011644505805:(u'=3)&(h'=1) +0.069593715219360571811:(u'=4)&(h'=1) +0.010418853439346153697:(u'=5)&(h'=1) +0.00069030824836099132381:(u'=6)&(h'=1) +1.8781879021858003016e-07:(u'=0)&(h'=2) +0.00038541617639479533366:(u'=1)&(h'=2) +0.037478090285502960177:(u'=2)&(h'=2) +0.17269572317882314616:(u'=3)&(h'=2) +0.037708766506962573817:(u'=4)&(h'=2) +0.00039017522116869846494:(u'=5)&(h'=2) +1.9130823229311818931e-07:(u'=6)&(h'=2);
[c1] u=2 & v=6 -> 0.015584210442122797824:(u'=0)&(h'=1) +0.097825356661324663898:(u'=1)&(h'=1) +0.1911572002171130491:(u'=2)&(h'=1) +0.11627931567224426834:(u'=3)&(h'=1) +0.022018455840963842979:(u'=4)&(h'=1) +0.0012979077779776174942:(u'=5)&(h'=1) +2.3816250889918073793e-05:(u'=6)&(h'=1) +2.6810743303148094259e-06:(u'=0)&(h'=2) +0.00095667858209287810756:(u'=1)&(h'=2) +0.044593345087592162201:(u'=2)&(h'=2) +0.27153189787407333577:(u'=3)&(h'=2) +0.21598244958483320266:(u'=4)&(h'=2) +0.022442067968721640669:(u'=5)&(h'=2) +0.00030461696572036626313:(u'=6)&(h'=2);
[c2] u=2 & v=6 -> (u'=2)&(h'=0);
[c0] u=3 & v=6 -> 0.0064288336052728900852:(u'=0)&(h'=1) +0.042523749025810499147:(u'=1)&(h'=1) +0.12448130537344875846:(u'=2)&(h'=1) +0.16126864912655680673:(u'=3)&(h'=1) +0.092463214742646279709:(u'=4)&(h'=1) +0.023461796100624592032:(u'=5)&(h'=1) +0.0026346731771567603181:(u'=6)&(h'=1) +2.9830839452188160494e-10:(u'=0)&(h'=2) +5.2933024424401851974e-06:(u'=1)&(h'=2) +0.0044508663937534156604:(u'=2)&(h'=2) +0.17734502974759325244:(u'=3)&(h'=2) +0.33484984322019772929:(u'=4)&(h'=2) +0.02995972296354193834:(u'=5)&(h'=2) +0.00012702292264618158775:(u'=6)&(h'=2);
[c1] u=3 & v=6 -> 0.0010875840841770762803:(u'=0)&(h'=1) +0.014343526005252731081:(u'=1)&(h'=1) +0.058887293184594846629:(u'=2)&(h'=1) +0.075259242715132998458:(u'=3)&(h'=1) +0.029941301957836990305:(u'=4)&(h'=1) +0.0037081227609795535706:(u'=5)&(h'=1) +0.00014295854221701008338:(u'=6)&(h'=1) +4.7272840539632717558e-08:(u'=0)&(h'=2) +5.6058312966395032202e-05:(u'=1)&(h'=2) +0.0086839067693035391915:(u'=2)&(h'=2) +0.17572642918985531546:(u'=3)&(h'=2) +0.46452149986395729897:(u'=4)&(h'=2) +0.16040627687414271696:(u'=5)&(h'=2) +0.0072357524667429635318:(u'=6)&(h'=2);
[c2] u=3 & v=6 -> (u'=3)&(h'=0);
[c0] u=4 & v=6 -> 0.00065621050867103200652:(u'=0)&(h'=1) +0.0073567314371043423388:(u'=1)&(h'=1) +0.036500587081744147178:(u'=2)&(h'=1) +0.080147139002573211664:(u'=3)&(h'=1) +0.077884211034385850136:(u'=4)&(h'=1) +0.03349531391112322426:(u'=5)&(h'=1) +0.0063751719977752033947:(u'=6)&(h'=1) +6.4780445064108874949e-14:(u'=0)&(h'=2) +9.9397507923181241725e-09:(u'=1)&(h'=2) +7.2270935978299393333e-05:(u'=2)&(h'=2) +0.024900523483498686328:(u'=3)&(h'=2) +0.40654618515944784818:(u'=4)&(h'=2) +0.31453423162056914908:(u'=5)&(h'=2) +0.011531413887313489083:(u'=6)&(h'=2);
[c1] u=4 & v=6 -> 5.4756168979187192132e-05:(u'=0)&(h'=1) +0.0015172340567196165341:(u'=1)&(h'=1) +0.013087138400114533415:(u'=2)&(h'=1) +0.035140617845505331407:(u'=3)&(h'=1) +0.029372889805008368241:(u'=4)&(h'=1) +0.0076428712586563774325:(u'=5)&(h'=1) +0.00061906891477895545535:(u'=6)&(h'=1) +3.1265050791239630961e-10:(u'=0)&(h'=2) +1.2321358431801388432e-06:(u'=1)&(h'=2) +0.00063431480503624542832:(u'=2)&(h'=2) +0.04265774641040743359:(u'=3)&(h'=2) +0.37474666086245284058:(u'=4)&(h'=2) +0.43005543344980712295:(u'=5)&(h'=2) +0.064470035574040213122:(u'=6)&(h'=2);
[c2] u=4 & v=6 -> (u'=4)&(h'=0);
[c0] u=5 & v=6 -> 5.3879239700666423855e-05:(u'=0)&(h'=1) +0.0010237774039232444816:(u'=1)&(h'=1) +0.0086092010038132781719:(u'=2)&(h'=1) +0.032040064521721665913:(u'=3)&(h'=1) +0.052771221007733036534:(u'=4)&(h'=1) +0.038465743419082952526:(u'=5)&(h'=1) +0.012408644555557631073:(u'=6)&(h'=1) +2.4808877203328967875e-18:(u'=0)&(h'=2) +3.2916148458884736423e-12:(u'=1)&(h'=2) +2.0695100040225614324e-07:(u'=2)&(h'=2) +0.00061657038735794030687:(u'=3)&(h'=2) +0.08704712060273858687:(u'=4)&(h'=2) +0.58234824613775559854:(u'=5)&(h'=2) +0.18461532476632336319:(u'=6)&(h'=2);
[c1] u=5 & v=6 -> 2.1981317726021309722e-06:(u'=0)&(h'=1) +0.00012796750338896860084:(u'=1)&(h'=1) +0.0023190934833383328346:(u'=2)&(h'=1) +0.01308306198944987099:(u'=3)&(h'=1) +0.022975931508274247128:(u'=4)&(h'=1) +0.012560572709265090119:(u'=5)&(h'=1) +0.0021375601328322280104:(u'=6)&(h'=1) +9.5962479399716750941e-13:(u'=0)&(h'=2) +1.2568169857543658047e-08:(u'=1)&(h'=2) +2.1502523264459663671e-05:(u'=2)&(h'=2) +0.0048056663430471524209:(u'=3)&(h'=2) +0.14030224048590858588:(u'=4)&(h'=2) +0.53508453814497702883:(u'=5)&(h'=2) +0.26657965447535209025:(u'=6)&(h'=2);
[c2] u=5 & v=6 -> (u'=5)&(h'=0);
[c0] u=6 & v=6 -> 3.8331939036190968096e-06:(u'=0)&(h'=1) +0.00012344890158254252441:(u'=1)&(h'=1) +0.0017594903849019129152:(u'=2)&(h'=1) +0.011098385153376697301:(u'=3)&(h'=1) +0.030981747724546947198:(u'=4)&(h'=1) +0.038275886742083271852:(u'=5)&(h'=1) +0.020927523340190757467:(u'=6)&(h'=1) +2.1026035649475159804e-23:(u'=0)&(h'=2) +2.4122906513234438168e-16:(u'=1)&(h'=2) +1.3114703785293425693e-10:(u'=2)&(h'=2) +3.37865581854651664e-06:(u'=3)&(h'=2) +0.0041246398594724587375:(u'=4)&(h'=2) +0.23860785180142857209:(u'=5)&(h'=2) +0.65409381411154732255:(u'=6)&(h'=2);
[c1] u=6 & v=6 -> 6.7455947713482173986e-08:(u'=0)&(h'=1) +8.250735547749958666e-06:(u'=1)&(h'=1) +0.00031415043949103044771:(u'=2)&(h'=1) +0.0037235334621175861756:(u'=3)&(h'=1) +0.013738693524761079814:(u'=4)&(h'=1) +0.015780043474792962432:(u'=5)&(h'=1) +0.0056421358693466861639:(u'=6)&(h'=1) +1.5539389413024312026e-15:(u'=0)&(h'=2) +6.7635648651969406084e-11:(u'=1)&(h'=2) +3.8456005595035226408e-07:(u'=2)&(h'=2) +0.00028562715148627301027:(u'=3)&(h'=2) +0.027712876652176910569:(u'=4)&(h'=2) +0.35124530862695552136:(u'=5)&(h'=2) +0.58154892797968327223:(u'=6)&(h'=2);
[c2] u=6 & v=6 -> (u'=6)&(h'=0);
[c0] u=0 & v=7 -> (u'=0)&(h'=0);
[c1] u=0 & v=7 -> 0.21288772333811173398:(u'=0)&(h'=1) +0.18421276765925165275:(u'=1)&(h'=1) +0.048776838768533573032:(u'=2)&(h'=1) +0.0039521405915898134148:(u'=3)&(h'=1) +9.7988685926075837392e-05:(u'=4)&(h'=1) +7.434372100498882646e-07:(u'=5)&(h'=1) +1.7259867910456124629e-09:(u'=6)&(h'=1) +9.0729726941287742103e-05:(u'=0)&(h'=2) +0.011725605468126109113:(u'=1)&(h'=2) +0.17502644687673363233:(u'=2)&(h'=2) +0.30175522664888276836:(u'=3)&(h'=2) +0.060088124862662128933:(u'=4)&(h'=2) +0.0013819910397660074928:(u'=5)&(h'=2) +3.6711702784259513425e-06:(u'=6)&(h'=2);
[c2] u=0 & v=7 -> (u'=0)&(h'=0);
[c0] u=1 & v=7 -> (u'=1)&(h'=0);
[c1] u=1 & v=7 -> 0.079913264970475544891:(u'=0)&(h'=1) +0.15841179036699215565:(u'=1)&(h'=1) +0.096090608303711633198:(u'=2)&(h'=1) +0.017836071132617405122:(u'=3)&(h'=1) +0.0010130765468966131896:(u'=4)&(h'=1) +1.7608004468539763617e-05:(u'=5)&(h'=1) +9.3648932408789295583e-08:(u'=6)&(h'=1) +3.7943387171404232187e-06:(u'=0)&(h'=2) +0.0014860163339211935902:(u'=1)&(h'=2) +0.06721927041888171861:(u'=2)&(h'=2) +0.35119371193869536318:(u'=3)&(h'=2) +0.21192509856364877274:(u'=4)&(h'=2) +0.014770689945178029634:(u'=5)&(h'=2) +0.00011890548686346597961:(u'=6)&(h'=2);
[c2] u=1 & v=7 -> (u'=1)&(h'=0);
[c0] u=2 & v=7 -> (u'=2)&(h'=0);
[c1] u=2 & v=7 -> 0.013402499283233363855:(u'=0)&(h'=1) +0.060863081644350724986:(u'=1)&(h'=1) +0.084575952184433769721:(u'=2)&(h'=1) +0.035963724870661427369:(u'=3)&(h'=1) +0.0046795840269372238063:(u'=4)&(h'=1) +0.0001863265084809737212:(u'=5)&(h'=1) +2.2702142982740675402e-06:(u'=6)&(h'=1) +9.44983427385831633e-08:(u'=0)&(h'=2) +0.00011215367014677117335:(u'=1)&(h'=2) +0.015373951747493629777:(u'=2)&(h'=2) +0.2434110348713768579:(u'=3)&(h'=2) +0.44512064484406832499:(u'=4)&(h'=2) +0.094015170445171783453:(u'=5)&(h'=2) +0.0022935111910040175374:(u'=6)&(h'=2);
[c2] u=2 & v=7 -> (u'=2)&(h'=0);
[c0] u=3 & v=7 -> (u'=3)&(h'=0);
[c1] u=3 & v=7 -> 0.001159485712318920024:(u'=0)&(h'=1) +0.012062381624449931491:(u'=1)&(h'=1) +0.038399497394709727893:(u'=2)&(h'=1) +0.037406134257301493218:(u'=3)&(h'=1) +0.011150258330049237637:(u'=4)&(h'=1) +0.001017072338609832172:(u'=5)&(h'=1) +2.838857344195669331e-05:(u'=6)&(h'=1) +1.2088645214868658098e-09:(u'=0)&(h'=2) +4.347791828870032126e-06:(u'=1)&(h'=2) +0.0018061032651615588178:(u'=2)&(h'=2) +0.086656099918943421678:(u'=3)&(h'=2) +0.48021799041089147098:(u'=4)&(h'=2) +0.30736926491229626945:(u'=5)&(h'=2) +0.022722974261132771606:(u'=6)&(h'=2);
[c2] u=3 & v=7 -> (u'=3)&(h'=0);
[c0] u=4 & v=7 -> (u'=4)&(h'=0);
[c1] u=4 & v=7 -> 7.5763995221547560566e-05:(u'=0)&(h'=1) +0.0018056353499900079911:(u'=1)&(h'=1) +0.013168067432434813965:(u'=2)&(h'=1) +0.029385889947837955799:(u'=3)&(h'=1) +0.020066908316406725094:(u'=4)&(h'=1) +0.0041932127508689104323:(u'=5)&(h'=1) +0.00026812551379252856773:(u'=6)&(h'=1) +8.0924389931295820504e-12:(u'=0)&(h'=2) +8.8200765912586724263e-08:(u'=1)&(h'=2) +0.00011103195952037395048:(u'=2)&(h'=2) +0.016143822651773213905:(u'=3)&(h'=2) +0.27111121111221087032:(u'=4)&(h'=2) +0.52586141027245159041:(u'=5)&(h'=2) +0.11780883248863321944:(u'=6)&(h'=2);
[c2] u=4 & v=7 -> (u'=4)&(h'=0);
[c0] u=5 & v=7 -> (u'=5)&(h'=0);
[c1] u=5 & v=7 -> 3.5457451481830273805e-06:(u'=0)&(h'=1) +0.00019358612003289482379:(u'=1)&(h'=1) +0.0032341914631950643109:(u'=2)&(h'=1) +0.016534156728950904353:(u'=3)&(h'=1) +0.025865637473291860915:(u'=4)&(h'=1) +0.012381952546896503667:(u'=5)&(h'=1) +0.0018137603216692491613:(u'=6)&(h'=1) +3.0555119081292784825e-14:(u'=0)&(h'=2) +1.0092034238171203973e-09:(u'=1)&(h'=2) +3.8499596284443942138e-06:(u'=2)&(h'=2) +0.0016963535078133116368:(u'=3)&(h'=2) +0.086329509329428996689:(u'=4)&(h'=2) +0.50744024658729325328:(u'=5)&(h'=2) +0.34450320920741733799:(u'=6)&(h'=2);
[c2] u=5 & v=7 -> (u'=5)&(h'=0);
[c0] u=6 & v=7 -> (u'=6)&(h'=0);
[c1] u=6 & v=7 -> 1.0347605875277509927e-07:(u'=0)&(h'=1) +1.2942140034963387635e-05:(u'=1)&(h'=1) +0.00049533284114802115638:(u'=2)&(h'=1) +0.0058011348961660479454:(u'=3)&(h'=1) +0.020789958304953448653:(u'=4)&(h'=1) +0.022799172523960860304:(u'=5)&(h'=1) +0.0076508443067248559782:(u'=6)&(h'=1) +7.1309757202914564879e-17:(u'=0)&(h'=2) +7.1374898652235863099e-12:(u'=1)&(h'=2) +8.2513455898901673386e-08:(u'=2)&(h'=2) +0.0001101759426512162617:(u'=3)&(h'=2) +0.016991491341202983462:(u'=4)&(h'=2) +0.30266273179613667477:(u'=5)&(h'=2) +0.62268602991036881011:(u'=6)&(h'=2);
[c2] u=6 & v=7 -> (u'=6)&(h'=0);
[c0] u=0 & v=8 -> (u'=0)&(h'=0);
[c1] u=0 & v=8 -> 0.30898673520641067869:(u'=0)&(h'=1) +0.43939345120311446014:(u'=1)&(h'=1) +0.19450909322973192195:(u'=2)&(h'=1) +0.02680395152338755152:(u'=3)&(h'=1) +0.0011498212312096522079:(u'=4)&(h'=1) +1.5354455087369958091e-05:(u'=5)&(h'=1) +6.3827976791975726098e-08:(u'=6)&(h'=1) +0.00011642294215262604805:(u'=0)&(h'=2) +0.0037614345599554120311:(u'=1)&(h'=2) +0.015875055576409027175:(u'=2)&(h'=2) +0.0087523323728912211933:(u'=3)&(h'=2) +0.00063034621989866530204:(u'=4)&(h'=2) +5.9303634069355602054e-06:(u'=5)&(h'=2) +7.2883675433195704392e-09:(u'=6)&(h'=2);
[c2] u=0 & v=8 -> (u'=0)&(h'=0);
[c0] u=1 & v=8 -> (u'=1)&(h'=0);
[c1] u=1 & v=8 -> 0.10668110075909956191:(u'=0)&(h'=1) +0.31873347543022956252:(u'=1)&(h'=1) +0.29644249066083361299:(u'=2)&(h'=1) +0.085827371813468833484:(u'=3)&(h'=1) +0.0077354175135099468782:(u'=4)&(h'=1) +0.00021702726133448495727:(u'=5)&(h'=1) +1.8954721420207443197e-06:(u'=6)&(h'=1) +3.647244319482400611e-05:(u'=0)&(h'=2) +0.0039160743170279684044:(u'=1)&(h'=2) +0.054926736634011666394:(u'=2)&(h'=2) +0.10063834185533120091:(u'=3)&(h'=2) +0.024087401502441981721:(u'=4)&(h'=2) +0.00075311835869592668857:(u'=5)&(h'=2) +3.0759786785181408682e-06:(u'=6)&(h'=2);
[c2] u=1 & v=8 -> (u'=1)&(h'=0);
[c0] u=2 & v=8 -> (u'=2)&(h'=0);
[c1] u=2 & v=8 -> 0.015584210442122797824:(u'=0)&(h'=1) +0.097825356661324663898:(u'=1)&(h'=1) +0.1911572002171130491:(u'=2)&(h'=1) +0.11627931567224426834:(u'=3)&(h'=1) +0.022018455840963842979:(u'=4)&(h'=1) +0.0012979077779776174942:(u'=5)&(h'=1) +2.3816250889918073793e-05:(u'=6)&(h'=1) +2.6810743303148094259e-06:(u'=0)&(h'=2) +0.00095667858209287810756:(u'=1)&(h'=2) +0.044593345087592162201:(u'=2)&(h'=2) +0.27153189787407333577:(u'=3)&(h'=2) +0.21598244958483320266:(u'=4)&(h'=2) +0.022442067968721640669:(u'=5)&(h'=2) +0.00030461696572036626313:(u'=6)&(h'=2);
[c2] u=2 & v=8 -> (u'=2)&(h'=0);
[c0] u=3 & v=8 -> (u'=3)&(h'=0);
[c1] u=3 & v=8 -> 0.0010875840841770762803:(u'=0)&(h'=1) +0.014343526005252731081:(u'=1)&(h'=1) +0.058887293184594846629:(u'=2)&(h'=1) +0.075259242715132998458:(u'=3)&(h'=1) +0.029941301957836990305:(u'=4)&(h'=1) +0.0037081227609795535706:(u'=5)&(h'=1) +0.00014295854221701008338:(u'=6)&(h'=1) +4.7272840539632717558e-08:(u'=0)&(h'=2) +5.6058312966395032202e-05:(u'=1)&(h'=2) +0.0086839067693035391915:(u'=2)&(h'=2) +0.17572642918985531546:(u'=3)&(h'=2) +0.46452149986395729897:(u'=4)&(h'=2) +0.16040627687414271696:(u'=5)&(h'=2) +0.0072357524667429635318:(u'=6)&(h'=2);
[c2] u=3 & v=8 -> (u'=3)&(h'=0);
[c0] u=4 & v=8 -> (u'=4)&(h'=0);
[c1] u=4 & v=8 -> 5.4756168979187192132e-05:(u'=0)&(h'=1) +0.0015172340567196165341:(u'=1)&(h'=1) +0.013087138400114533415:(u'=2)&(h'=1) +0.035140617845505331407:(u'=3)&(h'=1) +0.029372889805008368241:(u'=4)&(h'=1) +0.0076428712586563774325:(u'=5)&(h'=1) +0.00061906891477895545535:(u'=6)&(h'=1) +3.1265050791239630961e-10:(u'=0)&(h'=2) +1.2321358431801388432e-06:(u'=1)&(h'=2) +0.00063431480503624542832:(u'=2)&(h'=2) +0.04265774641040743359:(u'=3)&(h'=2) +0.37474666086245284058:(u'=4)&(h'=2) +0.43005543344980712295:(u'=5)&(h'=2) +0.064470035574040213122:(u'=6)&(h'=2);
[c2] u=4 & v=8 -> (u'=4)&(h'=0);
[c0] u=5 & v=8 -> (u'=5)&(h'=0);
[c1] u=5 & v=8 -> 2.1981317726021309722e-06:(u'=0)&(h'=1) +0.00012796750338896860084:(u'=1)&(h'=1) +0.0023190934833383328346:(u'=2)&(h'=1) +0.01308306198944987099:(u'=3)&(h'=1) +0.022975931508274247128:(u'=4)&(h'=1) +0.012560572709265090119:(u'=5)&(h'=1) +0.0021375601328322280104:(u'=6)&(h'=1) +9.5962479399716750941e-13:(u'=0)&(h'=2) +1.2568169857543658047e-08:(u'=1)&(h'=2) +2.1502523264459663671e-05:(u'=2)&(h'=2) +0.0048056663430471524209:(u'=3)&(h'=2) +0.14030224048590858588:(u'=4)&(h'=2) +0.53508453814497702883:(u'=5)&(h'=2) +0.26657965447535209025:(u'=6)&(h'=2);
[c2] u=5 & v=8 -> (u'=5)&(h'=0);
[c0] u=6 & v=8 -> (u'=6)&(h'=0);
[c1] u=6 & v=8 -> 6.7455947713482173986e-08:(u'=0)&(h'=1) +8.250735547749958666e-06:(u'=1)&(h'=1) +0.00031415043949103044771:(u'=2)&(h'=1) +0.0037235334621175861756:(u'=3)&(h'=1) +0.013738693524761079814:(u'=4)&(h'=1) +0.015780043474792962432:(u'=5)&(h'=1) +0.0056421358693466861639:(u'=6)&(h'=1) +1.5539389413024312026e-15:(u'=0)&(h'=2) +6.7635648651969406084e-11:(u'=1)&(h'=2) +3.8456005595035226408e-07:(u'=2)&(h'=2) +0.00028562715148627301027:(u'=3)&(h'=2) +0.027712876652176910569:(u'=4)&(h'=2) +0.35124530862695552136:(u'=5)&(h'=2) +0.58154892797968327223:(u'=6)&(h'=2);
[c2] u=6 & v=8 -> (u'=6)&(h'=0);
[c0] u=0 & v=9 -> (u'=0)&(h'=0);
[c1] u=0 & v=9 -> 0.28800890320137989553:(u'=0)&(h'=1) +0.39127148090681562742:(u'=1)&(h'=1) +0.23524678749708249903:(u'=2)&(h'=1) +0.062595402361519864032:(u'=3)&(h'=1) +0.0073711355208192080868:(u'=4)&(h'=1) +0.00038414889033507043517:(u'=5)&(h'=1) +8.8600872097344950546e-06:(u'=6)&(h'=1) +0.00022781225663809947764:(u'=0)&(h'=2) +0.0062521201720977612887:(u'=1)&(h'=2) +0.0081308165543853734569:(u'=2)&(h'=2) +0.0005010691020410522941:(u'=3)&(h'=2) +1.4632471889146019239e-06:(u'=4)&(h'=2) +2.0248571431128738473e-10:(u'=5)&(h'=2) +1.3277848016935405698e-15:(u'=6)&(h'=2);
[c2] u=0 & v=9 -> (u'=0)&(h'=0);
[c0] u=1 & v=9 -> (u'=1)&(h'=0);
[c1] u=1 & v=9 -> 0.13450302223441032434:(u'=0)&(h'=1) +0.30970390674024439459:(u'=1)&(h'=1) +0.31559822445964225146:(u'=2)&(h'=1) +0.14232973647246216498:(u'=3)&(h'=1) +0.028407300530203190292:(u'=4)&(h'=1) +0.0025092129080946292546:(u'=5)&(h'=1) +9.8088543707617963617e-05:(u'=6)&(h'=1) +1.5314917822066659124e-05:(u'=0)&(h'=2) +0.0036344210244367105601:(u'=1)&(h'=2) +0.040870732017625872878:(u'=2)&(h'=2) +0.021779415039548489369:(u'=3)&(h'=2) +0.00054996698698170593065:(u'=4)&(h'=2) +6.5808750526704745294e-07:(u'=5)&(h'=2) +3.7315329800401052319e-11:(u'=6)&(h'=2);
[c2] u=1 & v=9 -> (u'=1)&(h'=0);
[c0] u=2 & v=9 -> (u'=2)&(h'=0);
[c1] u=2 & v=9 -> 0.039930307842923180861:(u'=0)&(h'=1) +0.15583308175631960246:(u'=1)&(h'=1) +0.26914721288136983501:(u'=2)&(h'=1) +0.20572797011644505805:(u'=3)&(h'=1) +0.069593715219360571811:(u'=4)&(h'=1) +0.010418853439346153697:(u'=5)&(h'=1) +0.00069030824836099132381:(u'=6)&(h'=1) +1.8781879021858003016e-07:(u'=0)&(h'=2) +0.00038541617639479533366:(u'=1)&(h'=2) +0.037478090285502960177:(u'=2)&(h'=2) +0.17269572317882314616:(u'=3)&(h'=2) +0.037708766506962573817:(u'=4)&(h'=2) +0.00039017522116869846494:(u'=5)&(h'=2) +1.9130823229311818931e-07:(u'=6)&(h'=2);
[c2] u=2 & v=9 -> (u'=2)&(h'=0);
[c0] u=3 & v=9 -> (u'=3)&(h'=0);
[c1] u=3 & v=9 -> 0.0064288336052728900852:(u'=0)&(h'=1) +0.042523749025810499147:(u'=1)&(h'=1) +0.12448130537344875846:(u'=2)&(h'=1) +0.16126864912655680673:(u'=3)&(h'=1) +0.092463214742646279709:(u'=4)&(h'=1) +0.023461796100624592032:(u'=5)&(h'=1) +0.0026346731771567603181:(u'=6)&(h'=1) +2.9830839452188160494e-10:(u'=0)&(h'=2) +5.2933024424401851974e-06:(u'=1)&(h'=2) +0.0044508663937534156604:(u'=2)&(h'=2) +0.17734502974759325244:(u'=3)&(h'=2) +0.33484984322019772929:(u'=4)&(h'=2) +0.02995972296354193834:(u'=5)&(h'=2) +0.00012702292264618158775:(u'=6)&(h'=2);
[c2] u=3 & v=9 -> (u'=3)&(h'=0);
[c0] u=4 & v=9 -> (u'=4)&(h'=0);
[c1] u=4 & v=9 -> 0.00065621050867103200652:(u'=0)&(h'=1) +0.0073567314371043423388:(u'=1)&(h'=1) +0.036500587081744147178:(u'=2)&(h'=1) +0.080147139002573211664:(u'=3)&(h'=1) +0.077884211034385850136:(u'=4)&(h'=1) +0.03349531391112322426:(u'=5)&(h'=1) +0.0063751719977752033947:(u'=6)&(h'=1) +6.4780445064108874949e-14:(u'=0)&(h'=2) +9.9397507923181241725e-09:(u'=1)&(h'=2) +7.2270935978299393333e-05:(u'=2)&(h'=2) +0.024900523483498686328:(u'=3)&(h'=2) +0.40654618515944784818:(u'=4)&(h'=2) +0.31453423162056914908:(u'=5)&(h'=2) +0.011531413887313489083:(u'=6)&(h'=2);
[c2] u=4 & v=9 -> (u'=4)&(h'=0);
[c0] u=5 & v=9 -> (u'=5)&(h'=0);
[c1] u=5 & v=9 -> 5.3879239700666423855e-05:(u'=0)&(h'=1) +0.0010237774039232444816:(u'=1)&(h'=1) +0.0086092010038132781719:(u'=2)&(h'=1) +0.032040064521721665913:(u'=3)&(h'=1) +0.052771221007733036534:(u'=4)&(h'=1) +0.038465743419082952526:(u'=5)&(h'=1) +0.012408644555557631073:(u'=6)&(h'=1) +2.4808877203328967875e-18:(u'=0)&(h'=2) +3.2916148458884736423e-12:(u'=1)&(h'=2) +2.0695100040225614324e-07:(u'=2)&(h'=2) +0.00061657038735794030687:(u'=3)&(h'=2) +0.08704712060273858687:(u'=4)&(h'=2) +0.58234824613775559854:(u'=5)&(h'=2) +0.18461532476632336319:(u'=6)&(h'=2);
[c2] u=5 & v=9 -> (u'=5)&(h'=0);
[c0] u=6 & v=9 -> (u'=6)&(h'=0);
[c1] u=6 & v=9 -> 3.8331939036190968096e-06:(u'=0)&(h'=1) +0.00012344890158254252441:(u'=1)&(h'=1) +0.0017594903849019129152:(u'=2)&(h'=1) +0.011098385153376697301:(u'=3)&(h'=1) +0.030981747724546947198:(u'=4)&(h'=1) +0.038275886742083271852:(u'=5)&(h'=1) +0.020927523340190757467:(u'=6)&(h'=1) +2.1026035649475159804e-23:(u'=0)&(h'=2) +2.4122906513234438168e-16:(u'=1)&(h'=2) +1.3114703785293425693e-10:(u'=2)&(h'=2) +3.37865581854651664e-06:(u'=3)&(h'=2) +0.0041246398594724587375:(u'=4)&(h'=2) +0.23860785180142857209:(u'=5)&(h'=2) +0.65409381411154732255:(u'=6)&(h'=2);
[c2] u=6 & v=9 -> (u'=6)&(h'=0);
[c0] u=0 & v=10 -> (u'=0)&(h'=0);
[c1] u=0 & v=10 -> (u'=0)&(h'=0);
[c2] u=0 & v=10 -> (u'=0)&(h'=0);
[c0] u=1 & v=10 -> (u'=1)&(h'=0);
[c1] u=1 & v=10 -> (u'=1)&(h'=0);
[c2] u=1 & v=10 -> (u'=1)&(h'=0);
[c0] u=2 & v=10 -> (u'=2)&(h'=0);
[c1] u=2 & v=10 -> (u'=2)&(h'=0);
[c2] u=2 & v=10 -> (u'=2)&(h'=0);
[c0] u=3 & v=10 -> (u'=3)&(h'=0);
[c1] u=3 & v=10 -> (u'=3)&(h'=0);
[c2] u=3 & v=10 -> (u'=3)&(h'=0);
[c0] u=4 & v=10 -> (u'=4)&(h'=0);
[c1] u=4 & v=10 -> (u'=4)&(h'=0);
[c2] u=4 & v=10 -> (u'=4)&(h'=0);
[c0] u=5 & v=10 -> (u'=5)&(h'=0);
[c1] u=5 & v=10 -> (u'=5)&(h'=0);
[c2] u=5 & v=10 -> (u'=5)&(h'=0);
[c0] u=6 & v=10 -> (u'=6)&(h'=0);
[c1] u=6 & v=10 -> (u'=6)&(h'=0);
[c2] u=6 & v=10 -> (u'=6)&(h'=0);
[c0] u=0 & v=11 -> (u'=0)&(h'=0);
[c1] u=0 & v=11 -> (u'=0)&(h'=0);
[c2] u=0 & v=11 -> (u'=0)&(h'=0);
[c0] u=1 & v=11 -> (u'=1)&(h'=0);
[c1] u=1 & v=11 -> (u'=1)&(h'=0);
[c2] u=1 & v=11 -> (u'=1)&(h'=0);
[c0] u=2 & v=11 -> (u'=2)&(h'=0);
[c1] u=2 & v=11 -> (u'=2)&(h'=0);
[c2] u=2 & v=11 -> (u'=2)&(h'=0);
[c0] u=3 & v=11 -> (u'=3)&(h'=0);
[c1] u=3 & v=11 -> (u'=3)&(h'=0);
[c2] u=3 & v=11 -> (u'=3)&(h'=0);
[c0] u=4 & v=11 -> (u'=4)&(h'=0);
[c1] u=4 & v=11 -> (u'=4)&(h'=0);
[c2] u=4 & v=11 -> (u'=4)&(h'=0);
[c0] u=5 & v=11 -> (u'=5)&(h'=0);
[c1] u=5 & v=11 -> (u'=5)&(h'=0);
[c2] u=5 & v=11 -> (u'=5)&(h'=0);
[c0] u=6 & v=11 -> (u'=6)&(h'=0);
[c1] u=6 & v=11 -> (u'=6)&(h'=0);
[c2] u=6 & v=11 -> (u'=6)&(h'=0);
endmodule
label "end" = v=11;
rewards "satisfaction"
[c0] v=0& u=0: 0.058283;
[c1] v=0& u=0: 0.04534;
[c2] v=0& u=0: 0.55007;
[c0] v=0& u=1: 0.36872;
[c1] v=0& u=1: 0.20055;
[c2] v=0& u=1: 0.64672;
[c0] v=0& u=2: 1.1116;
[c1] v=0& u=2: 0.74598;
[c2] v=0& u=2: 0.80033;
[c0] v=0& u=3: 1.6333;
[c1] v=0& u=3: 1.6402;
[c2] v=0& u=3: 0.89878;
[c0] v=0& u=4: 1.8251;
[c1] v=0& u=4: 2.2728;
[c2] v=0& u=4: 0.93104;
[c0] v=0& u=5: 1.8936;
[c1] v=0& u=5: 2.5639;
[c2] v=0& u=5: 0.93997;
[c0] v=0& u=6: 1.9216;
[c1] v=0& u=6: 2.6905;
[c2] v=0& u=6: 0.94245;
[c1] v=1& u=0: 0.04534;
[c2] v=1& u=0: 5;
[c1] v=1& u=1: 0.20055;
[c2] v=1& u=1: 5;
[c1] v=1& u=2: 0.74598;
[c2] v=1& u=2: 5;
[c1] v=1& u=3: 1.6402;
[c2] v=1& u=3: 5;
[c1] v=1& u=4: 2.2728;
[c2] v=1& u=4: 5;
[c1] v=1& u=5: 2.5639;
[c2] v=1& u=5: 5;
[c1] v=1& u=6: 2.6905;
[c2] v=1& u=6: 5;
[c0] v=2& u=0: 5;
[c2] v=2& u=0: 0.55007;
[c0] v=2& u=1: 5;
[c2] v=2& u=1: 0.64672;
[c0] v=2& u=2: 5;
[c2] v=2& u=2: 0.80033;
[c0] v=2& u=3: 5;
[c2] v=2& u=3: 0.89878;
[c0] v=2& u=4: 5;
[c2] v=2& u=4: 0.93104;
[c0] v=2& u=5: 5;
[c2] v=2& u=5: 0.93997;
[c0] v=2& u=6: 5;
[c2] v=2& u=6: 0.94245;
[c0] v=3& u=0: 0.058283;
[c1] v=3& u=0: 5;
[c0] v=3& u=1: 0.36872;
[c1] v=3& u=1: 5;
[c0] v=3& u=2: 1.1116;
[c1] v=3& u=2: 5;
[c0] v=3& u=3: 1.6333;
[c1] v=3& u=3: 5;
[c0] v=3& u=4: 1.8251;
[c1] v=3& u=4: 5;
[c0] v=3& u=5: 1.8936;
[c1] v=3& u=5: 5;
[c0] v=3& u=6: 1.9216;
[c1] v=3& u=6: 5;
[c1] v=4& u=0: 0.058283;
[c2] v=4& u=0: 0.55007;
[c1] v=4& u=1: 0.36872;
[c2] v=4& u=1: 0.64672;
[c1] v=4& u=2: 1.1116;
[c2] v=4& u=2: 0.80033;
[c1] v=4& u=3: 1.6333;
[c2] v=4& u=3: 0.89878;
[c1] v=4& u=4: 1.8251;
[c2] v=4& u=4: 0.93104;
[c1] v=4& u=5: 1.8936;
[c2] v=4& u=5: 0.93997;
[c1] v=4& u=6: 1.9216;
[c2] v=4& u=6: 0.94245;
[c0] v=5& u=0: 0.04534;
[c2] v=5& u=0: 0.55007;
[c0] v=5& u=1: 0.20055;
[c2] v=5& u=1: 0.64672;
[c0] v=5& u=2: 0.74598;
[c2] v=5& u=2: 0.80033;
[c0] v=5& u=3: 1.6402;
[c2] v=5& u=3: 0.89878;
[c0] v=5& u=4: 2.2728;
[c2] v=5& u=4: 0.93104;
[c0] v=5& u=5: 2.5639;
[c2] v=5& u=5: 0.93997;
[c0] v=5& u=6: 2.6905;
[c2] v=5& u=6: 0.94245;
[c0] v=6& u=0: 0.04534;
[c1] v=6& u=0: 0.058283;
[c0] v=6& u=1: 0.20055;
[c1] v=6& u=1: 0.36872;
[c0] v=6& u=2: 0.74598;
[c1] v=6& u=2: 1.1116;
[c0] v=6& u=3: 1.6402;
[c1] v=6& u=3: 1.6333;
[c0] v=6& u=4: 2.2728;
[c1] v=6& u=4: 1.8251;
[c0] v=6& u=5: 2.5639;
[c1] v=6& u=5: 1.8936;
[c0] v=6& u=6: 2.6905;
[c1] v=6& u=6: 1.9216;
[c1] v=7& u=0: 0.55007;
[c1] v=7& u=1: 0.64672;
[c1] v=7& u=2: 0.80033;
[c1] v=7& u=3: 0.89878;
[c1] v=7& u=4: 0.93104;
[c1] v=7& u=5: 0.93997;
[c1] v=7& u=6: 0.94245;
[c1] v=8& u=0: 0.058283;
[c1] v=8& u=1: 0.36872;
[c1] v=8& u=2: 1.1116;
[c1] v=8& u=3: 1.6333;
[c1] v=8& u=4: 1.8251;
[c1] v=8& u=5: 1.8936;
[c1] v=8& u=6: 1.9216;
[c1] v=9& u=0: 0.04534;
[c1] v=9& u=1: 0.20055;
[c1] v=9& u=2: 0.74598;
[c1] v=9& u=3: 1.6402;
[c1] v=9& u=4: 2.2728;
[c1] v=9& u=5: 2.5639;
[c1] v=9& u=6: 2.6905;
endrewards
rewards "destinationTrust"
v=10 & u=0 :1;
v=10 & u=1 :2;
v=10 & u=2 :3;
v=10 & u=3 :4;
v=10 & u=4 :5;
v=10 & u=5 :6;
v=10 & u=6 :7;
endrewards
rewards "averageTrust"
v=0 & u=0 : (0+1)/5;
v=0 & u=1 : (1+1)/5;
v=0 & u=2 : (2+1)/5;
v=0 & u=3 : (3+1)/5;
v=0 & u=4 : (4+1)/5;
v=0 & u=5 : (5+1)/5;
v=0 & u=6 : (6+1)/5;
v=1 & u=0 : (0+1)/5;
v=1 & u=1 : (1+1)/5;
v=1 & u=2 : (2+1)/5;
v=1 & u=3 : (3+1)/5;
v=1 & u=4 : (4+1)/5;
v=1 & u=5 : (5+1)/5;
v=1 & u=6 : (6+1)/5;
v=2 & u=0 : (0+1)/5;
v=2 & u=1 : (1+1)/5;
v=2 & u=2 : (2+1)/5;
v=2 & u=3 : (3+1)/5;
v=2 & u=4 : (4+1)/5;
v=2 & u=5 : (5+1)/5;
v=2 & u=6 : (6+1)/5;
v=3 & u=0 : (0+1)/5;
v=3 & u=1 : (1+1)/5;
v=3 & u=2 : (2+1)/5;
v=3 & u=3 : (3+1)/5;
v=3 & u=4 : (4+1)/5;
v=3 & u=5 : (5+1)/5;
v=3 & u=6 : (6+1)/5;
v=4 & u=0 : (0+1)/5;
v=4 & u=1 : (1+1)/5;
v=4 & u=2 : (2+1)/5;
v=4 & u=3 : (3+1)/5;
v=4 & u=4 : (4+1)/5;
v=4 & u=5 : (5+1)/5;
v=4 & u=6 : (6+1)/5;
v=5 & u=0 : (0+1)/5;
v=5 & u=1 : (1+1)/5;
v=5 & u=2 : (2+1)/5;
v=5 & u=3 : (3+1)/5;
v=5 & u=4 : (4+1)/5;
v=5 & u=5 : (5+1)/5;
v=5 & u=6 : (6+1)/5;
v=6 & u=0 : (0+1)/5;
v=6 & u=1 : (1+1)/5;
v=6 & u=2 : (2+1)/5;
v=6 & u=3 : (3+1)/5;
v=6 & u=4 : (4+1)/5;
v=6 & u=5 : (5+1)/5;
v=6 & u=6 : (6+1)/5;
v=7 & u=0 : (0+1)/5;
v=7 & u=1 : (1+1)/5;
v=7 & u=2 : (2+1)/5;
v=7 & u=3 : (3+1)/5;
v=7 & u=4 : (4+1)/5;
v=7 & u=5 : (5+1)/5;
v=7 & u=6 : (6+1)/5;
v=8 & u=0 : (0+1)/5;
v=8 & u=1 : (1+1)/5;
v=8 & u=2 : (2+1)/5;
v=8 & u=3 : (3+1)/5;
v=8 & u=4 : (4+1)/5;
v=8 & u=5 : (5+1)/5;
v=8 & u=6 : (6+1)/5;
v=9 & u=0 : (0+1)/5;
v=9 & u=1 : (1+1)/5;
v=9 & u=2 : (2+1)/5;
v=9 & u=3 : (3+1)/5;
v=9 & u=4 : (4+1)/5;
v=9 & u=5 : (5+1)/5;
v=9 & u=6 : (6+1)/5;
v=10 & u=0 : (0+1)/5;
v=10 & u=1 : (1+1)/5;
v=10 & u=2 : (2+1)/5;
v=10 & u=3 : (3+1)/5;
v=10 & u=4 : (4+1)/5;
v=10 & u=5 : (5+1)/5;
v=10 & u=6 : (6+1)/5;
endrewards
rewards "min_takeoverTimes_V2"
v=1 & h=1 :1;
v=2 & h=1 :1;
v=3 & h=1 :1;
v=4 & h=1 :1;
v=5 & h=1 :1;
v=6 & h=1 :1;
v=7 & h=1 :1;
v=8 & h=1 :1;
v=9 & h=1 :1;
v=10 & h=1 :1;
endrewards
rewards "distance"
[c0] v=0: 0.686;
[c1] v=0: 0.434;
[c2] v=0: 0.637;
[c1] v=1: 0.759;
[c2] v=1: 0.775;
[c0] v=2: 0.944;
[c2] v=2: 0.862;
[c0] v=3: 0.795;
[c1] v=3: 0.908;
[c1] v=4: 0.675;
[c2] v=4: 0.873;
[c0] v=5: 1.147;
[c2] v=5: 1.319;
[c0] v=6: 1.07;
[c1] v=6: 1.085;
[c1] v=7: 0.604;
[c1] v=8: 0.339;
[c1] v=9: 0.633;
endrewards
rewards "energyConsumption"
[c0] v=0 & u=0 : 0.686*0.029142+0.8575*0.97086;
[c1] v=0 & u=0 : 0.434*0.015113+0.5425*0.98489;
[c2] v=0 & u=0 : 0.637*0.55007+0.79625*0.44993;
[c0] v=0 & u=1 : 0.686*0.18436+0.8575*0.81564;
[c1] v=0 & u=1 : 0.434*0.066851+0.5425*0.93315;
[c2] v=0 & u=1 : 0.637*0.64672+0.79625*0.35328;
[c0] v=0 & u=2 : 0.686*0.55581+0.8575*0.44419;
[c1] v=0 & u=2 : 0.434*0.24866+0.5425*0.75134;
[c2] v=0 & u=2 : 0.637*0.80033+0.79625*0.19967;
[c0] v=0 & u=3 : 0.686*0.81663+0.8575*0.18337;
[c1] v=0 & u=3 : 0.434*0.54674+0.5425*0.45326;
[c2] v=0 & u=3 : 0.637*0.89878+0.79625*0.10122;
[c0] v=0 & u=4 : 0.686*0.91257+0.8575*0.087435;
[c1] v=0 & u=4 : 0.434*0.75758+0.5425*0.24242;
[c2] v=0 & u=4 : 0.637*0.93104+0.79625*0.068964;
[c0] v=0 & u=5 : 0.686*0.94679+0.8575*0.053206;
[c1] v=0 & u=5 : 0.434*0.85463+0.5425*0.14537;
[c2] v=0 & u=5 : 0.637*0.93997+0.79625*0.060027;
[c0] v=0 & u=6 : 0.686*0.96079+0.8575*0.039207;
[c1] v=0 & u=6 : 0.434*0.89683+0.5425*0.10317;
[c2] v=0 & u=6 : 0.637*0.94245+0.79625*0.057549;
[c1] v=1 & u=0 : 0.759*0.015113+0.94875*0.98489;
[c2] v=1 & u=0: 0.775;
[c1] v=1 & u=1 : 0.759*0.066851+0.94875*0.93315;
[c2] v=1 & u=1: 0.775;
[c1] v=1 & u=2 : 0.759*0.24866+0.94875*0.75134;
[c2] v=1 & u=2: 0.775;
[c1] v=1 & u=3 : 0.759*0.54674+0.94875*0.45326;
[c2] v=1 & u=3: 0.775;
[c1] v=1 & u=4 : 0.759*0.75758+0.94875*0.24242;
[c2] v=1 & u=4: 0.775;
[c1] v=1 & u=5 : 0.759*0.85463+0.94875*0.14537;
[c2] v=1 & u=5: 0.775;
[c1] v=1 & u=6 : 0.759*0.89683+0.94875*0.10317;
[c2] v=1 & u=6: 0.775;
[c0] v=2 & u=0: 0.944;
[c2] v=2 & u=0 : 0.862*0.55007+1.0775*0.44993;
[c0] v=2 & u=1: 0.944;
[c2] v=2 & u=1 : 0.862*0.64672+1.0775*0.35328;
[c0] v=2 & u=2: 0.944;
[c2] v=2 & u=2 : 0.862*0.80033+1.0775*0.19967;
[c0] v=2 & u=3: 0.944;
[c2] v=2 & u=3 : 0.862*0.89878+1.0775*0.10122;
[c0] v=2 & u=4: 0.944;
[c2] v=2 & u=4 : 0.862*0.93104+1.0775*0.068964;
[c0] v=2 & u=5: 0.944;
[c2] v=2 & u=5 : 0.862*0.93997+1.0775*0.060027;
[c0] v=2 & u=6: 0.944;
[c2] v=2 & u=6 : 0.862*0.94245+1.0775*0.057549;
[c0] v=3 & u=0 : 0.795*0.029142+0.99375*0.97086;
[c1] v=3 & u=0: 0.908;
[c0] v=3 & u=1 : 0.795*0.18436+0.99375*0.81564;
[c1] v=3 & u=1: 0.908;
[c0] v=3 & u=2 : 0.795*0.55581+0.99375*0.44419;
[c1] v=3 & u=2: 0.908;
[c0] v=3 & u=3 : 0.795*0.81663+0.99375*0.18337;
[c1] v=3 & u=3: 0.908;
[c0] v=3 & u=4 : 0.795*0.91257+0.99375*0.087435;
[c1] v=3 & u=4: 0.908;
[c0] v=3 & u=5 : 0.795*0.94679+0.99375*0.053206;
[c1] v=3 & u=5: 0.908;
[c0] v=3 & u=6 : 0.795*0.96079+0.99375*0.039207;
[c1] v=3 & u=6: 0.908;
[c1] v=4 & u=0 : 0.675*0.029142+0.84375*0.97086;
[c2] v=4 & u=0 : 0.873*0.55007+1.0913*0.44993;
[c1] v=4 & u=1 : 0.675*0.18436+0.84375*0.81564;
[c2] v=4 & u=1 : 0.873*0.64672+1.0913*0.35328;
[c1] v=4 & u=2 : 0.675*0.55581+0.84375*0.44419;
[c2] v=4 & u=2 : 0.873*0.80033+1.0913*0.19967;
[c1] v=4 & u=3 : 0.675*0.81663+0.84375*0.18337;
[c2] v=4 & u=3 : 0.873*0.89878+1.0913*0.10122;
[c1] v=4 & u=4 : 0.675*0.91257+0.84375*0.087435;
[c2] v=4 & u=4 : 0.873*0.93104+1.0913*0.068964;
[c1] v=4 & u=5 : 0.675*0.94679+0.84375*0.053206;
[c2] v=4 & u=5 : 0.873*0.93997+1.0913*0.060027;
[c1] v=4 & u=6 : 0.675*0.96079+0.84375*0.039207;
[c2] v=4 & u=6 : 0.873*0.94245+1.0913*0.057549;
[c0] v=5 & u=0 : 1.147*0.015113+1.4338*0.98489;
[c2] v=5 & u=0 : 1.319*0.55007+1.6487*0.44993;
[c0] v=5 & u=1 : 1.147*0.066851+1.4338*0.93315;
[c2] v=5 & u=1 : 1.319*0.64672+1.6487*0.35328;
[c0] v=5 & u=2 : 1.147*0.24866+1.4338*0.75134;
[c2] v=5 & u=2 : 1.319*0.80033+1.6487*0.19967;
[c0] v=5 & u=3 : 1.147*0.54674+1.4338*0.45326;
[c2] v=5 & u=3 : 1.319*0.89878+1.6487*0.10122;
[c0] v=5 & u=4 : 1.147*0.75758+1.4338*0.24242;
[c2] v=5 & u=4 : 1.319*0.93104+1.6487*0.068964;
[c0] v=5 & u=5 : 1.147*0.85463+1.4338*0.14537;
[c2] v=5 & u=5 : 1.319*0.93997+1.6487*0.060027;
[c0] v=5 & u=6 : 1.147*0.89683+1.4338*0.10317;
[c2] v=5 & u=6 : 1.319*0.94245+1.6487*0.057549;
[c0] v=6 & u=0 : 1.07*0.015113+1.3375*0.98489;
[c1] v=6 & u=0 : 1.085*0.029142+1.3562*0.97086;
[c0] v=6 & u=1 : 1.07*0.066851+1.3375*0.93315;
[c1] v=6 & u=1 : 1.085*0.18436+1.3562*0.81564;
[c0] v=6 & u=2 : 1.07*0.24866+1.3375*0.75134;
[c1] v=6 & u=2 : 1.085*0.55581+1.3562*0.44419;
[c0] v=6 & u=3 : 1.07*0.54674+1.3375*0.45326;
[c1] v=6 & u=3 : 1.085*0.81663+1.3562*0.18337;
[c0] v=6 & u=4 : 1.07*0.75758+1.3375*0.24242;
[c1] v=6 & u=4 : 1.085*0.91257+1.3562*0.087435;
[c0] v=6 & u=5 : 1.07*0.85463+1.3375*0.14537;
[c1] v=6 & u=5 : 1.085*0.94679+1.3562*0.053206;
[c0] v=6 & u=6 : 1.07*0.89683+1.3375*0.10317;
[c1] v=6 & u=6 : 1.085*0.96079+1.3562*0.039207;
[c1] v=7 & u=0 : 0.604*0.55007+0.755*0.44993;
[c1] v=7 & u=1 : 0.604*0.64672+0.755*0.35328;
[c1] v=7 & u=2 : 0.604*0.80033+0.755*0.19967;
[c1] v=7 & u=3 : 0.604*0.89878+0.755*0.10122;
[c1] v=7 & u=4 : 0.604*0.93104+0.755*0.068964;
[c1] v=7 & u=5 : 0.604*0.93997+0.755*0.060027;
[c1] v=7 & u=6 : 0.604*0.94245+0.755*0.057549;
[c1] v=8 & u=0 : 0.339*0.029142+0.42375*0.97086;
[c1] v=8 & u=1 : 0.339*0.18436+0.42375*0.81564;
[c1] v=8 & u=2 : 0.339*0.55581+0.42375*0.44419;
[c1] v=8 & u=3 : 0.339*0.81663+0.42375*0.18337;
[c1] v=8 & u=4 : 0.339*0.91257+0.42375*0.087435;
[c1] v=8 & u=5 : 0.339*0.94679+0.42375*0.053206;
[c1] v=8 & u=6 : 0.339*0.96079+0.42375*0.039207;
[c1] v=9 & u=0 : 0.633*0.015113+0.79125*0.98489;
[c1] v=9 & u=1 : 0.633*0.066851+0.79125*0.93315;
[c1] v=9 & u=2 : 0.633*0.24866+0.79125*0.75134;
[c1] v=9 & u=3 : 0.633*0.54674+0.79125*0.45326;
[c1] v=9 & u=4 : 0.633*0.75758+0.79125*0.24242;
[c1] v=9 & u=5 : 0.633*0.85463+0.79125*0.14537;
[c1] v=9 & u=6 : 0.633*0.89683+0.79125*0.10317;
endrewards
rewards "averageEnergyConsumptionRate"
[c0] v=0 & u=0 : 1*0.029142/4+1.25*0.97086/4;
[c1] v=0 & u=0 : 1*0.015113/4+1.25*0.98489/4;
[c2] v=0 & u=0 : 1*0.55007/4+1.25*0.44993/4;
[c0] v=0 & u=1 : 1*0.18436/4+1.25*0.81564/4;
[c1] v=0 & u=1 : 1*0.066851/4+1.25*0.93315/4;
[c2] v=0 & u=1 : 1*0.64672/4+1.25*0.35328/4;
[c0] v=0 & u=2 : 1*0.55581/4+1.25*0.44419/4;
[c1] v=0 & u=2 : 1*0.24866/4+1.25*0.75134/4;
[c2] v=0 & u=2 : 1*0.80033/4+1.25*0.19967/4;
[c0] v=0 & u=3 : 1*0.81663/4+1.25*0.18337/4;
[c1] v=0 & u=3 : 1*0.54674/4+1.25*0.45326/4;
[c2] v=0 & u=3 : 1*0.89878/4+1.25*0.10122/4;
[c0] v=0 & u=4 : 1*0.91257/4+1.25*0.087435/4;
[c1] v=0 & u=4 : 1*0.75758/4+1.25*0.24242/4;
[c2] v=0 & u=4 : 1*0.93104/4+1.25*0.068964/4;
[c0] v=0 & u=5 : 1*0.94679/4+1.25*0.053206/4;
[c1] v=0 & u=5 : 1*0.85463/4+1.25*0.14537/4;
[c2] v=0 & u=5 : 1*0.93997/4+1.25*0.060027/4;
[c0] v=0 & u=6 : 1*0.96079/4+1.25*0.039207/4;
[c1] v=0 & u=6 : 1*0.89683/4+1.25*0.10317/4;
[c2] v=0 & u=6 : 1*0.94245/4+1.25*0.057549/4;
[c1] v=1 & u=0 : 1*0.015113/4+1.25*0.98489/4;
[c2] v=1 & u=0: 1/4;
[c1] v=1 & u=1 : 1*0.066851/4+1.25*0.93315/4;
[c2] v=1 & u=1: 1/4;
[c1] v=1 & u=2 : 1*0.24866/4+1.25*0.75134/4;
[c2] v=1 & u=2: 1/4;
[c1] v=1 & u=3 : 1*0.54674/4+1.25*0.45326/4;
[c2] v=1 & u=3: 1/4;
[c1] v=1 & u=4 : 1*0.75758/4+1.25*0.24242/4;
[c2] v=1 & u=4: 1/4;
[c1] v=1 & u=5 : 1*0.85463/4+1.25*0.14537/4;
[c2] v=1 & u=5: 1/4;
[c1] v=1 & u=6 : 1*0.89683/4+1.25*0.10317/4;
[c2] v=1 & u=6: 1/4;
[c0] v=2 & u=0: 1/4;
[c2] v=2 & u=0 : 1*0.55007/4+1.25*0.44993/4;
[c0] v=2 & u=1: 1/4;
[c2] v=2 & u=1 : 1*0.64672/4+1.25*0.35328/4;
[c0] v=2 & u=2: 1/4;
[c2] v=2 & u=2 : 1*0.80033/4+1.25*0.19967/4;
[c0] v=2 & u=3: 1/4;
[c2] v=2 & u=3 : 1*0.89878/4+1.25*0.10122/4;
[c0] v=2 & u=4: 1/4;
[c2] v=2 & u=4 : 1*0.93104/4+1.25*0.068964/4;
[c0] v=2 & u=5: 1/4;
[c2] v=2 & u=5 : 1*0.93997/4+1.25*0.060027/4;
[c0] v=2 & u=6: 1/4;
[c2] v=2 & u=6 : 1*0.94245/4+1.25*0.057549/4;
[c0] v=3 & u=0 : 1*0.029142/4+1.25*0.97086/4;
[c1] v=3 & u=0: 1/4;
[c0] v=3 & u=1 : 1*0.18436/4+1.25*0.81564/4;
[c1] v=3 & u=1: 1/4;
[c0] v=3 & u=2 : 1*0.55581/4+1.25*0.44419/4;
[c1] v=3 & u=2: 1/4;
[c0] v=3 & u=3 : 1*0.81663/4+1.25*0.18337/4;
[c1] v=3 & u=3: 1/4;
[c0] v=3 & u=4 : 1*0.91257/4+1.25*0.087435/4;
[c1] v=3 & u=4: 1/4;
[c0] v=3 & u=5 : 1*0.94679/4+1.25*0.053206/4;
[c1] v=3 & u=5: 1/4;
[c0] v=3 & u=6 : 1*0.96079/4+1.25*0.039207/4;
[c1] v=3 & u=6: 1/4;
[c1] v=4 & u=0 : 1*0.029142/4+1.25*0.97086/4;
[c2] v=4 & u=0 : 1*0.55007/4+1.25*0.44993/4;
[c1] v=4 & u=1 : 1*0.18436/4+1.25*0.81564/4;
[c2] v=4 & u=1 : 1*0.64672/4+1.25*0.35328/4;
[c1] v=4 & u=2 : 1*0.55581/4+1.25*0.44419/4;
[c2] v=4 & u=2 : 1*0.80033/4+1.25*0.19967/4;
[c1] v=4 & u=3 : 1*0.81663/4+1.25*0.18337/4;
[c2] v=4 & u=3 : 1*0.89878/4+1.25*0.10122/4;
[c1] v=4 & u=4 : 1*0.91257/4+1.25*0.087435/4;
[c2] v=4 & u=4 : 1*0.93104/4+1.25*0.068964/4;
[c1] v=4 & u=5 : 1*0.94679/4+1.25*0.053206/4;
[c2] v=4 & u=5 : 1*0.93997/4+1.25*0.060027/4;
[c1] v=4 & u=6 : 1*0.96079/4+1.25*0.039207/4;
[c2] v=4 & u=6 : 1*0.94245/4+1.25*0.057549/4;
[c0] v=5 & u=0 : 1*0.015113/4+1.25*0.98489/4;
[c2] v=5 & u=0 : 1*0.55007/4+1.25*0.44993/4;
[c0] v=5 & u=1 : 1*0.066851/4+1.25*0.93315/4;
[c2] v=5 & u=1 : 1*0.64672/4+1.25*0.35328/4;
[c0] v=5 & u=2 : 1*0.24866/4+1.25*0.75134/4;
[c2] v=5 & u=2 : 1*0.80033/4+1.25*0.19967/4;
[c0] v=5 & u=3 : 1*0.54674/4+1.25*0.45326/4;
[c2] v=5 & u=3 : 1*0.89878/4+1.25*0.10122/4;
[c0] v=5 & u=4 : 1*0.75758/4+1.25*0.24242/4;
[c2] v=5 & u=4 : 1*0.93104/4+1.25*0.068964/4;
[c0] v=5 & u=5 : 1*0.85463/4+1.25*0.14537/4;
[c2] v=5 & u=5 : 1*0.93997/4+1.25*0.060027/4;
[c0] v=5 & u=6 : 1*0.89683/4+1.25*0.10317/4;
[c2] v=5 & u=6 : 1*0.94245/4+1.25*0.057549/4;
[c0] v=6 & u=0 : 1*0.015113/4+1.25*0.98489/4;
[c1] v=6 & u=0 : 1*0.029142/4+1.25*0.97086/4;
[c0] v=6 & u=1 : 1*0.066851/4+1.25*0.93315/4;
[c1] v=6 & u=1 : 1*0.18436/4+1.25*0.81564/4;
[c0] v=6 & u=2 : 1*0.24866/4+1.25*0.75134/4;
[c1] v=6 & u=2 : 1*0.55581/4+1.25*0.44419/4;
[c0] v=6 & u=3 : 1*0.54674/4+1.25*0.45326/4;
[c1] v=6 & u=3 : 1*0.81663/4+1.25*0.18337/4;
[c0] v=6 & u=4 : 1*0.75758/4+1.25*0.24242/4;
[c1] v=6 & u=4 : 1*0.91257/4+1.25*0.087435/4;
[c0] v=6 & u=5 : 1*0.85463/4+1.25*0.14537/4;
[c1] v=6 & u=5 : 1*0.94679/4+1.25*0.053206/4;
[c0] v=6 & u=6 : 1*0.89683/4+1.25*0.10317/4;
[c1] v=6 & u=6 : 1*0.96079/4+1.25*0.039207/4;
[c1] v=7 & u=0 : 1*0.55007/4+1.25*0.44993/4;
[c1] v=7 & u=1 : 1*0.64672/4+1.25*0.35328/4;
[c1] v=7 & u=2 : 1*0.80033/4+1.25*0.19967/4;
[c1] v=7 & u=3 : 1*0.89878/4+1.25*0.10122/4;
[c1] v=7 & u=4 : 1*0.93104/4+1.25*0.068964/4;
[c1] v=7 & u=5 : 1*0.93997/4+1.25*0.060027/4;
[c1] v=7 & u=6 : 1*0.94245/4+1.25*0.057549/4;
[c1] v=8 & u=0 : 1*0.029142/4+1.25*0.97086/4;
[c1] v=8 & u=1 : 1*0.18436/4+1.25*0.81564/4;
[c1] v=8 & u=2 : 1*0.55581/4+1.25*0.44419/4;
[c1] v=8 & u=3 : 1*0.81663/4+1.25*0.18337/4;
[c1] v=8 & u=4 : 1*0.91257/4+1.25*0.087435/4;
[c1] v=8 & u=5 : 1*0.94679/4+1.25*0.053206/4;
[c1] v=8 & u=6 : 1*0.96079/4+1.25*0.039207/4;
[c1] v=9 & u=0 : 1*0.015113/4+1.25*0.98489/4;
[c1] v=9 & u=1 : 1*0.066851/4+1.25*0.93315/4;
[c1] v=9 & u=2 : 1*0.24866/4+1.25*0.75134/4;
[c1] v=9 & u=3 : 1*0.54674/4+1.25*0.45326/4;
[c1] v=9 & u=4 : 1*0.75758/4+1.25*0.24242/4;
[c1] v=9 & u=5 : 1*0.85463/4+1.25*0.14537/4;
[c1] v=9 & u=6 : 1*0.89683/4+1.25*0.10317/4;
endrewards