Decision #436 — library/core/src/iter/range.rs:900
Status: no_witness
Truth table
| row | c0 br 2930 | c1 br 2931 | c2 br 2937 | c3 br 2938 | outcome |
|---|---|---|---|---|---|
| 18006 | T | * | * | * | T |
| 18007 | T | * | * | * | T |
| 18008 | T | * | * | * | T |
| 18009 | T | * | T | F | T |
| 18010 | T | * | * | * | T |
| 18011 | T | * | * | * | T |
| 18012 | T | * | * | * | T |
| 18013 | T | * | T | F | T |
| 18014 | T | * | * | * | T |
| 18015 | T | * | * | * | T |
| 18016 | T | * | * | * | T |
| 18017 | T | * | T | F | T |
| 18018 | T | * | * | * | T |
| 18019 | T | * | * | * | T |
| 18020 | T | * | * | * | T |
| 18021 | T | * | T | F | T |
| 18022 | T | * | * | * | T |
| 18023 | T | * | * | * | T |
| 18024 | T | * | * | * | T |
| 18025 | T | * | T | F | T |
| 18026 | T | * | * | * | T |
| 18027 | T | * | * | * | T |
| 18028 | T | * | * | * | T |
| 18029 | T | * | T | F | T |
| 18030 | T | * | * | * | T |
| 18031 | T | * | * | * | T |
| 18032 | T | * | * | * | T |
| 18033 | T | * | T | F | T |
| 18034 | T | * | * | * | T |
| 18035 | T | * | * | * | T |
| 18036 | T | * | * | * | T |
| 18037 | T | * | T | F | T |
| 25724 | T | * | * | * | T |
| 25725 | T | * | * | * | T |
| 25726 | T | * | * | * | T |
| 25727 | T | * | T | F | T |
| 25728 | T | * | * | * | T |
| 25729 | T | * | * | * | T |
| 25730 | T | * | * | * | T |
| 25731 | T | * | T | F | T |
| 25732 | T | * | * | * | T |
| 25733 | T | * | * | * | T |
| 25734 | T | * | * | * | T |
| 25735 | T | * | T | F | T |
| 25736 | T | * | * | * | T |
| 25737 | T | * | * | * | T |
| 25738 | T | * | * | * | T |
| 25739 | T | * | T | F | T |
| 25740 | T | * | * | * | T |
| 25741 | T | * | * | * | T |
| 25742 | T | * | * | * | T |
| 25743 | T | * | T | F | T |
| 25744 | T | * | * | * | T |
| 25745 | T | * | * | * | T |
| 25746 | T | * | * | * | T |
| 25747 | T | * | T | F | T |
| 25748 | T | * | * | * | T |
| 25749 | T | * | * | * | T |
| 25750 | T | * | * | * | T |
| 25751 | T | * | T | F | T |
| 25752 | T | * | * | * | T |
| 25753 | T | * | * | * | T |
| 25754 | T | * | * | * | T |
| 25755 | T | * | T | F | T |
| 31417 | T | * | * | * | T |
| 31418 | T | * | T | T | T |
| 31419 | T | * | * | * | T |
| 31420 | T | * | T | T | T |
| 31421 | T | * | * | * | T |
| 31422 | T | * | T | T | T |
| 31423 | T | * | * | * | T |
| 31424 | T | * | T | T | T |
| 31425 | T | * | * | * | T |
| 31426 | T | * | T | T | T |
| 31427 | T | * | * | * | T |
| 31428 | T | * | T | T | T |
| 31429 | T | * | * | * | T |
| 31430 | T | * | T | T | T |
| 31431 | T | * | * | * | T |
| 31432 | T | * | T | T | T |
| 31433 | T | * | * | * | T |
| 31434 | T | * | T | T | T |
| 31435 | T | * | * | * | T |
| 31436 | T | * | T | T | T |
| 31437 | T | * | * | * | T |
| 31438 | T | * | T | T | T |
| 31439 | T | * | * | * | T |
| 31440 | T | * | T | T | T |
| 31441 | T | * | * | * | T |
| 31442 | T | * | T | T | T |
| 31443 | T | * | * | * | T |
| 31444 | T | * | T | T | T |
| 31445 | T | * | * | * | T |
| 31446 | T | * | T | T | T |
| 31447 | T | * | * | * | T |
| 31448 | T | * | T | T | T |
| 31449 | T | * | * | * | T |
| 31450 | T | * | T | T | T |
| 31451 | T | * | * | * | T |
| 31452 | T | * | T | T | T |
| 31453 | T | * | * | * | T |
| 31454 | T | * | T | T | T |
| 31455 | T | * | * | * | T |
| 31456 | T | * | T | T | T |
| 31457 | T | * | * | * | T |
| 31458 | T | * | T | T | T |
| 31459 | T | * | * | * | T |
| 31460 | T | * | T | T | T |
| 31461 | T | * | * | * | T |
| 31462 | T | * | T | T | T |
| 31463 | T | * | * | * | T |
| 31464 | T | * | T | T | T |
| 31465 | T | * | * | * | T |
| 31466 | T | * | T | T | T |
| 31467 | T | * | * | * | T |
| 31468 | T | * | T | T | T |
| 31469 | T | * | * | * | T |
| 31470 | T | * | T | T | T |
| 31471 | T | * | * | * | T |
| 31472 | T | * | T | T | T |
| 37355 | T | * | * | * | T |
| 37356 | T | * | T | T | T |
| 37357 | T | * | * | * | T |
| 37358 | T | * | T | T | T |
| 37359 | T | * | * | * | T |
| 37360 | T | * | T | T | T |
| 37361 | T | * | * | * | T |
| 37362 | T | * | T | T | T |
| 37363 | T | * | * | * | T |
| 37364 | T | * | T | T | T |
| 37365 | T | * | * | * | T |
| 37366 | T | * | T | T | T |
| 37367 | T | * | * | * | T |
| 37368 | T | * | T | T | T |
| 37369 | T | * | * | * | T |
| 37370 | T | * | T | T | T |
| 37371 | T | * | * | * | T |
| 37372 | T | * | T | T | T |
| 37373 | T | * | * | * | T |
| 37374 | T | * | T | T | T |
| 37375 | T | * | * | * | T |
| 37376 | T | * | T | T | T |
| 37377 | T | * | * | * | T |
| 37378 | T | * | T | T | T |
| 37379 | T | * | * | * | T |
| 37380 | T | * | T | T | T |
| 37381 | T | * | * | * | T |
| 37382 | T | * | T | T | T |
| 37383 | T | * | * | * | T |
| 37384 | T | * | T | T | T |
| 37385 | T | * | * | * | T |
| 37386 | T | * | T | T | T |
| 37387 | T | * | * | * | T |
| 37388 | T | * | T | T | T |
| 37389 | T | * | * | * | T |
| 37390 | T | * | T | T | T |
| 37391 | T | * | * | * | T |
| 37392 | T | * | T | T | T |
| 37393 | T | * | * | * | T |
| 37394 | T | * | T | T | T |
| 37395 | T | * | * | * | T |
| 37396 | T | * | T | T | T |
| 37397 | T | * | * | * | T |
| 37398 | T | * | T | T | T |
| 37399 | T | * | * | * | T |
| 37400 | T | * | T | T | T |
| 37401 | T | * | * | * | T |
| 37402 | T | * | T | T | T |
| 37403 | T | * | * | * | T |
| 37404 | T | * | T | T | T |
| 37405 | T | * | * | * | T |
| 37406 | T | * | T | T | T |
| 37407 | T | * | * | * | T |
| 37408 | T | * | T | T | T |
| 37409 | T | * | * | * | T |
| 37410 | T | * | T | T | T |
| 59433 | T | * | * | * | T |
| 59434 | T | * | * | * | T |
| 59435 | T | * | * | * | T |
| 59436 | T | * | T | F | T |
| 59437 | T | * | * | * | T |
| 59438 | T | * | * | * | T |
| 59439 | T | * | * | * | T |
| 59440 | T | * | T | F | T |
| 59441 | T | * | * | * | T |
| 59442 | T | * | * | * | T |
| 59443 | T | * | * | * | T |
| 59444 | T | * | T | F | T |
| 59445 | T | * | * | * | T |
| 59446 | T | * | * | * | T |
| 59447 | T | * | * | * | T |
| 59448 | T | * | T | F | T |
| 59449 | T | * | * | * | T |
| 59450 | T | * | * | * | T |
| 59451 | T | * | * | * | T |
| 59452 | T | * | T | F | T |
| 59453 | T | * | * | * | T |
| 59454 | T | * | * | * | T |
| 59455 | T | * | * | * | T |
| 59456 | T | * | T | F | T |
| 59457 | T | * | * | * | T |
| 59458 | T | * | * | * | T |
| 59459 | T | * | * | * | T |
| 59460 | T | * | T | F | T |
| 59461 | T | * | * | * | T |
| 59462 | T | * | * | * | T |
| 59463 | T | * | * | * | T |
| 59464 | T | * | T | F | T |
| 59465 | T | * | * | * | T |
| 59466 | T | * | * | * | T |
| 59467 | T | * | * | * | T |
| 59468 | T | * | T | F | T |
| 59469 | T | * | * | * | T |
| 59470 | T | * | * | * | T |
| 59471 | T | * | * | * | T |
| 59472 | T | * | T | F | T |
| 59473 | T | * | * | * | T |
| 59474 | T | * | * | * | T |
| 59475 | T | * | * | * | T |
| 59476 | T | * | T | F | T |
| 59477 | T | * | * | * | T |
| 59478 | T | * | * | * | T |
| 59479 | T | * | * | * | T |
| 59480 | T | * | T | F | T |
| 69205 | T | * | * | * | T |
| 69206 | T | * | * | * | T |
| 69207 | T | * | * | * | T |
| 69208 | T | * | T | F | T |
| 69209 | T | * | * | * | T |
| 69210 | T | * | * | * | T |
| 69211 | T | * | * | * | T |
| 69212 | T | * | T | F | T |
| 69213 | T | * | * | * | T |
| 69214 | T | * | * | * | T |
| 69215 | T | * | * | * | T |
| 69216 | T | * | T | F | T |
| 69217 | T | * | * | * | T |
| 69218 | T | * | * | * | T |
| 69219 | T | * | * | * | T |
| 69220 | T | * | T | F | T |
| 69221 | T | * | * | * | T |
| 69222 | T | * | * | * | T |
| 69223 | T | * | * | * | T |
| 69224 | T | * | T | F | T |
| 69225 | T | * | * | * | T |
| 69226 | T | * | * | * | T |
| 69227 | T | * | * | * | T |
| 69228 | T | * | T | F | T |
| 69229 | T | * | * | * | T |
| 69230 | T | * | * | * | T |
| 69231 | T | * | * | * | T |
| 69232 | T | * | T | F | T |
| 69233 | T | * | * | * | T |
| 69234 | T | * | * | * | T |
| 69235 | T | * | * | * | T |
| 69236 | T | * | T | F | T |
| 69237 | T | * | * | * | T |
| 69238 | T | * | * | * | T |
| 69239 | T | * | * | * | T |
| 69240 | T | * | T | F | T |
| 69241 | T | * | * | * | T |
| 69242 | T | * | * | * | T |
| 69243 | T | * | * | * | T |
| 69244 | T | * | T | F | T |
| 69245 | T | * | * | * | T |
| 69246 | T | * | * | * | T |
| 69247 | T | * | * | * | T |
| 69248 | T | * | T | F | T |
| 69249 | T | * | * | * | T |
| 69250 | T | * | * | * | T |
| 69251 | T | * | * | * | T |
| 69252 | T | * | T | F | T |
| 106948 | T | * | * | * | T |
| 106949 | T | * | * | * | T |
| 106950 | T | * | * | * | T |
| 106951 | T | * | T | F | T |
| 106952 | T | * | * | * | T |
| 106953 | T | * | * | * | T |
| 106954 | T | * | * | * | T |
| 106955 | T | * | T | F | T |
| 106956 | T | * | * | * | T |
| 106957 | T | * | * | * | T |
| 106958 | T | * | * | * | T |
| 106959 | T | * | T | F | T |
| 106960 | T | * | * | * | T |
| 106961 | T | * | * | * | T |
| 106962 | T | * | * | * | T |
| 106963 | T | * | T | F | T |
| 106964 | T | * | * | * | T |
| 106965 | T | * | * | * | T |
| 106966 | T | * | * | * | T |
| 106967 | T | * | T | F | T |
| 106968 | T | * | * | * | T |
| 106969 | T | * | * | * | T |
| 106970 | T | * | * | * | T |
| 106971 | T | * | T | F | T |
| 106972 | T | * | * | * | T |
| 106973 | T | * | * | * | T |
| 106974 | T | * | * | * | T |
| 106975 | T | * | T | F | T |
| 106976 | T | * | * | * | T |
| 106977 | T | * | * | * | T |
| 106978 | T | * | * | * | T |
| 106979 | T | * | T | F | T |
| 106980 | T | * | * | * | T |
| 106981 | T | * | * | * | T |
| 106982 | T | * | * | * | T |
| 106983 | T | * | T | F | T |
| 106984 | T | * | * | * | T |
| 106985 | T | * | * | * | T |
| 106986 | T | * | * | * | T |
| 106987 | T | * | T | F | T |
| 106988 | T | * | * | * | T |
| 106989 | T | * | * | * | T |
| 106990 | T | * | * | * | T |
| 106991 | T | * | T | F | T |
| 106992 | T | * | * | * | T |
| 106993 | T | * | * | * | T |
| 106994 | T | * | * | * | T |
| 106995 | T | * | T | F | T |
| 106996 | T | * | * | * | T |
| 106997 | T | * | * | * | T |
| 106998 | T | * | * | * | T |
| 106999 | T | * | T | F | T |
| 107000 | T | * | * | * | T |
| 107001 | T | * | * | * | T |
| 107002 | T | * | * | * | T |
| 107003 | T | * | T | F | T |
| 107004 | T | * | * | * | T |
| 107005 | T | * | * | * | T |
| 107006 | T | * | * | * | T |
| 107007 | T | * | T | F | T |
| 107008 | T | * | * | * | T |
| 107009 | T | * | * | * | T |
| 107010 | T | * | * | * | T |
| 107011 | T | * | T | F | T |
| 107012 | T | * | * | * | T |
| 107013 | T | * | * | * | T |
| 107014 | T | * | * | * | T |
| 107015 | T | * | T | F | T |
| 107016 | T | * | * | * | T |
| 107017 | T | * | * | * | T |
| 107018 | T | * | * | * | T |
| 107019 | T | * | T | F | T |
| 107020 | T | * | * | * | T |
| 107021 | T | * | * | * | T |
| 107022 | T | * | * | * | T |
| 107023 | T | * | T | F | T |
| 107024 | T | * | * | * | T |
| 107025 | T | * | * | * | T |
| 107026 | T | * | * | * | T |
| 107027 | T | * | T | F | T |
| 107028 | T | * | * | * | T |
| 107029 | T | * | * | * | T |
| 107030 | T | * | * | * | T |
| 107031 | T | * | T | F | T |
| 107032 | T | * | * | * | T |
| 107033 | T | * | * | * | T |
| 107034 | T | * | * | * | T |
| 107035 | T | * | T | F | T |
| 107036 | T | * | * | * | T |
| 107037 | T | * | * | * | T |
| 107038 | T | * | * | * | T |
| 107039 | T | * | T | F | T |
| 107040 | T | * | * | * | T |
| 107041 | T | * | * | * | T |
| 107042 | T | * | * | * | T |
| 107043 | T | * | T | F | T |
| 125811 | T | * | * | * | T |
| 125812 | T | * | * | * | T |
| 125813 | T | * | * | * | T |
| 125814 | T | * | T | F | T |
| 125815 | T | * | * | * | T |
| 125816 | T | * | * | * | T |
| 125817 | T | * | * | * | T |
| 125818 | T | * | T | F | T |
| 125819 | T | * | * | * | T |
| 125820 | T | * | * | * | T |
| 125821 | T | * | * | * | T |
| 125822 | T | * | T | F | T |
| 125823 | T | * | * | * | T |
| 125824 | T | * | * | * | T |
| 125825 | T | * | * | * | T |
| 125826 | T | * | T | F | T |
| 125827 | T | * | * | * | T |
| 125828 | T | * | * | * | T |
| 125829 | T | * | * | * | T |
| 125830 | T | * | T | F | T |
| 125831 | T | * | * | * | T |
| 125832 | T | * | * | * | T |
| 125833 | T | * | * | * | T |
| 125834 | T | * | T | F | T |
| 125835 | T | * | * | * | T |
| 125836 | T | * | * | * | T |
| 125837 | T | * | * | * | T |
| 125838 | T | * | T | F | T |
| 125839 | T | * | * | * | T |
| 125840 | T | * | * | * | T |
| 125841 | T | * | * | * | T |
| 125842 | T | * | T | F | T |
| 125843 | T | * | * | * | T |
| 125844 | T | * | * | * | T |
| 125845 | T | * | * | * | T |
| 125846 | T | * | T | F | T |
| 125847 | T | * | * | * | T |
| 125848 | T | * | * | * | T |
| 125849 | T | * | * | * | T |
| 125850 | T | * | T | F | T |
| 125851 | T | * | * | * | T |
| 125852 | T | * | * | * | T |
| 125853 | T | * | * | * | T |
| 125854 | T | * | T | F | T |
| 125855 | T | * | * | * | T |
| 125856 | T | * | * | * | T |
| 125857 | T | * | * | * | T |
| 125858 | T | * | T | F | T |
| 125859 | T | * | * | * | T |
| 125860 | T | * | * | * | T |
| 125861 | T | * | * | * | T |
| 125862 | T | * | T | F | T |
| 125863 | T | * | * | * | T |
| 125864 | T | * | * | * | T |
| 125865 | T | * | * | * | T |
| 125866 | T | * | T | F | T |
| 125867 | T | * | * | * | T |
| 125868 | T | * | * | * | T |
| 125869 | T | * | * | * | T |
| 125870 | T | * | T | F | T |
| 125871 | T | * | * | * | T |
| 125872 | T | * | * | * | T |
| 125873 | T | * | * | * | T |
| 125874 | T | * | T | F | T |
| 125875 | T | * | * | * | T |
| 125876 | T | * | * | * | T |
| 125877 | T | * | * | * | T |
| 125878 | T | * | T | F | T |
| 125879 | T | * | * | * | T |
| 125880 | T | * | * | * | T |
| 125881 | T | * | * | * | T |
| 125882 | T | * | T | F | T |
| 125883 | T | * | * | * | T |
| 125884 | T | * | * | * | T |
| 125885 | T | * | * | * | T |
| 125886 | T | * | T | F | T |
| 125887 | T | * | * | * | T |
| 125888 | T | * | * | * | T |
| 125889 | T | * | * | * | T |
| 125890 | T | * | T | F | T |
| 125891 | T | * | * | * | T |
| 125892 | T | * | * | * | T |
| 125893 | T | * | * | * | T |
| 125894 | T | * | T | F | T |
| 125895 | T | * | * | * | T |
| 125896 | T | * | * | * | T |
| 125897 | T | * | * | * | T |
| 125898 | T | * | T | F | T |
| 125899 | T | * | * | * | T |
| 125900 | T | * | * | * | T |
| 125901 | T | * | * | * | T |
| 125902 | T | * | T | F | T |
| 125903 | T | * | * | * | T |
| 125904 | T | * | * | * | T |
| 125905 | T | * | * | * | T |
| 125906 | T | * | T | F | T |
Independent-effect pairs
All 4 conditions live in scry_octagon::join — 4 br_if
c0(branch2930): GAP view gap →c1(branch2931): DEAD view gap →c2(branch2937): GAP view gap →c3(branch2938): GAP view gap →