theorem NFA.SlotsValidOfRangeMap (slots : Array Capture.SlotGroup) (h : List.map (fun (i : Nat) => (i, i.div 2)) (List.range slots.size) = slots.toList) : Slots.Valid slots

instance NFA.instLEProdNat : LE Capture.SlotGroup

Equations

• NFA.instLEProdNat = { le := Prod.Lex (fun (x1 x2 : Nat) => x1 < x2) fun (x1 x2 : Nat) => x1 ≤ x2 }

instance NFA.instLTProdNat : LT Capture.SlotGroup

Equations

• NFA.instLTProdNat = { lt := Prod.Lex (fun (x1 x2 : Nat) => x1 < x2) fun (x1 x2 : Nat) => x1 < x2 }

theorem NFA.toSlots_valid (captures : Array Capture) (h : Capture.valid captures) : Slots.Valid (Capture.toSlots captures)