fact: Definition srs : Srs := [((sz, sz), (st, sr)); ((sz, st), (sl' 1, sm)) ] ++ flat_map enc_Instruction (combine (seq 1 (length mm)) mm) ++ flat_map (fun p => [ ((sl' p, sb), (sl, sb' p)); ((sl' p, sm), (sl, sm' p)); ((sb' p, sb), (sb, sb' p)); ((sb' p, sm), (sb, sm' p)); ((sb' p, sr), (sb, sr' p)); ((sm' p, sb), (sm, sb' p)); ((sm' p, sr), (sm, sr' p))]) (seq 0 state_bound) ++ flat_map (fun p => [ ((sb, sr' p), (sb' p, sr)); ((sm, sr' p), (sm' p, sr)); ((sb, sb' p), (sb' p, sb)); ((sm, sb' p), (sm' p, sb)); ((sl, sb' p), (sl' p, sb)); ((sb, sm' p), (sb' p, sm)); ((sl, sm' p), (sl' p, sm))]) (seq 0 state_bound) ++ map (fun p => ((sz, sl' p), (so, so))) (seq (S (length mm)) (state_bound - S (length mm))) ++ [((sz, sl' 0), (so, so)); ((sz, so), (so, so)); ((so, sb), (so, so)); ((so, sm), (so, so)); ((so, sr), (so, so)); ((so, sz), (so, so))].
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun