the property retrieve ar v = retrieve (bsimp ar) (decode erase(bsimp(ar)) code(v)) if |- v : r does not hold

test of retrieve r v = retrieve (bsimp r) (decode bsimp r code v)

removed C(c) The retrieve and code in the previous version is still not correct and will crash. no prob now.

The C(Char) construct is incompatible with the code and retrieve in Fahad's thesis. This causes the exception. Two ways of fixing this: delete C(C) construct (easy way around) or amend retrieve code etc. since the C(C) construct is intended for decoding Pred, and we don't use pred now, we shall delete this. This is the last veersion that contains C(CHAR)

exp and proof

augmented version of proof sketch

pf

found the difference: caused by flats in ders_simp, the alts is at top most level , so no fuse and bits stay at the alts level whereas in ders + singele simp, the alts that should be the final top-level alts is not at the topmost level initially before simplification so it is opened up and bits fused. later it finds out itself the top level only aalts remaining, but the fuse is not reversible we do not know what happened either.

random test failed on the new simplification function. ("super_blexing_simp")

correctness test with enumeration