def Compiler.Lemmas.isAppendOfState (sid : NFA.Unchecked.StateID) (state : NFA.Unchecked.State) (s1 s2 : Array NFA.Unchecked.State) : Prop

Equations

• Compiler.Lemmas.isAppendOfState sid state s1 s2 = (s2 = s1 ++ #[state] ∧ s2[sid]? = some state)

def Compiler.Lemmas.isAppendOfStateID (sid : NFA.Unchecked.StateID) (s1 s2 : Array NFA.Unchecked.State) : Prop

Equations

• Compiler.Lemmas.isAppendOfStateID sid s1 s2 = ∃ (state : NFA.Unchecked.State), Compiler.Lemmas.isAppendOfState sid state s1 s2

def Compiler.Lemmas.assignableP (sid : NFA.Unchecked.StateID) (s1 s2 : Array NFA.Unchecked.State) : Prop

Equations

• Compiler.Lemmas.assignableP sid s1 s2 = (Compiler.Lemmas.patchAssignable s2 sid ∧ Compiler.Lemmas.isAppendOfStateID sid s1 s2)

def Compiler.Lemmas.assignableP2 (sid : NFA.Unchecked.StateID) (s1 s2 : Array NFA.Unchecked.State) : Prop

Equations

• Compiler.Lemmas.assignableP2 sid s1 s2 = (Compiler.Lemmas.patch2Assignable s2 sid ∧ Compiler.Lemmas.isAppendOfStateID sid s1 s2)

def Compiler.Lemmas.pushPostCond (prevsid : NFA.Unchecked.State) (prevs : Array NFA.Unchecked.State) (sid : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) : Prop

Equations

• Compiler.Lemmas.pushPostCond prevsid prevs sid s = (Compiler.Lemmas.stateIdNextOfLt prevs sid s ∧ Compiler.Lemmas.isAppendOfState sid prevsid prevs s ∧ sid = prevs.size)

def Compiler.Lemmas.pushPostCond' (prevsid : NFA.Unchecked.State) (prevs : Array NFA.Unchecked.State) (r : ThompsonRef) (s : Array NFA.Unchecked.State) : Prop

Equations

• Compiler.Lemmas.pushPostCond' prevsid prevs r s = (Compiler.Lemmas.tRefNextOfLt prevs r s ∧ Compiler.Lemmas.isAppendOfState r.end prevsid prevs s ∧ r.end = prevs.size)

@[simp]

theorem Compiler.Lemmas.isAppend_of_isAppendOfState {sid1 : NFA.Unchecked.StateID} {s1 s2 : Array NFA.Unchecked.State} (h : isAppendOfStateID sid1 s1 s2) : isAppend s1 s2

@[simp]

theorem Compiler.Lemmas.isAppend_of_assignableP {sid1 : NFA.Unchecked.StateID} {s1 s2 : Array NFA.Unchecked.State} (h : assignableP sid1 s1 s2) : isAppend s1 s2

@[simp]

theorem Compiler.Lemmas.isAppend_of_assignableP2 {sid1 : NFA.Unchecked.StateID} {s1 s2 : Array NFA.Unchecked.State} (h : assignableP2 sid1 s1 s2) : isAppend s1 s2

theorem Compiler.Lemmas.push_spec (sid : NFA.Unchecked.State) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ NextOfLt states ∧ sid.nextOf ≤ states.size⌝⦄ Code.push sid ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜pushPostCond sid states r s⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.push_lift_spec (sid : NFA.Unchecked.State) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ NextOfLt states ∧ sid.nextOf ≤ states.size⌝⦄ liftM (Code.push sid) ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜pushPostCond sid states r s⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.push_run_spec (sid : NFA.Unchecked.State) (states : Array NFA.Unchecked.State) (h1 : NextOfLt states) (h2 : sid.nextOf ≤ states.size) (h3 : State.patchAssignable sid) : ⦃⌜True⌝⦄ StateT.run (Code.push sid) states ⦃(fun (r : NFA.Unchecked.StateID × Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r.fst r.snd ∧ assignableIf states r.snd ∧ assignableP r.fst states r.snd⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.push_run_lift_spec (sid : NFA.Unchecked.State) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜s.fst = states ∧ NextOfLt states ∧ sid.nextOf ≤ states.size ∧ State.patchAssignable sid⌝⦄ liftM (Code.push sid states) ⦃(fun (r : NFA.Unchecked.StateID × Array NFA.Unchecked.State) (x : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜stateIdNextOfLt states r.fst r.snd ∧ assignableIf states r.snd ∧ assignableP r.fst states r.snd⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

@[simp]

theorem Compiler.Lemmas.push'_lt (state : NFA.Unchecked.State) (states : Array NFA.Unchecked.State) : states.size < (Code.push' state states).snd.size

theorem Compiler.Lemmas.push'_spec (sid : NFA.Unchecked.State) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ NextOfLt states ∧ sid.nextOf ≤ states.size⌝⦄ Code.push' sid ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜pushPostCond' sid states r s⌝, PUnit.unit)⦄

@[simp]

theorem Compiler.Lemmas.append_of_push {state : NFA.Unchecked.State} (s s_1 : Array NFA.Unchecked.State) (r : NFA.Unchecked.StateID) (h_1 : r < s_1.size) (h_2 : s_1 = s.push state) (h_3 : s_1[r]? = some state) : ∃ (state : NFA.Unchecked.State), s_1 = s.push state ∧ s_1[r]? = some state

@[simp]

theorem Compiler.Lemmas.assignableIfP_of_push {state : NFA.Unchecked.State} (s s_1 : Array NFA.Unchecked.State) (r : NFA.Unchecked.StateID) (h_1 : r < s_1.size) (hs : State.patchAssignable state) (h_2 : s_1 = s.push state) (h_3 : s_1[r]? = some state) : (∃ (state : NFA.Unchecked.State), s_1 = s.push state ∧ s_1[r]? = some state) ∧ (∀ (sid : Fin s_1.size), patchAssignable s ↑sid → patchAssignable s_1 ↑sid) ∧ ∀ (sid : Fin s_1.size), ¬↑sid = s.size → patch2Assignable s ↑sid → patch2Assignable s_1 ↑sid

@[simp]

theorem Compiler.Lemmas.assignableIfP_of_push' {state : NFA.Unchecked.State} (s s_1 : Array NFA.Unchecked.State) (r : ThompsonRef) (h_2 : r.end < s_1.size) (hs : State.patchAssignable state) (h_4 : s_1 = s.push state) (h_5 : s_1[r.end]? = some state) : (∃ (state : NFA.Unchecked.State), s_1 = s.push state ∧ s_1[r.end]? = some state) ∧ (∀ (sid : Fin s_1.size), patchAssignable s ↑sid → patchAssignable s_1 ↑sid) ∧ ∀ (sid : Fin s_1.size), ¬↑sid = s.size → patch2Assignable s ↑sid → patch2Assignable s_1 ↑sid

theorem Compiler.Lemmas.add_match_spec (pattern_id : NFA.PatternID) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ NextOfLt states⌝⦄ Code.add_match pattern_id ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s ∧ assignableIf states s⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.add_match_lift_spec (pattern_id : NFA.PatternID) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) : ⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ NextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.add_match pattern_id) ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(stateIdNextOfLt states r s.fst ∧ assignableIf states s.fst) ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.add_union_spec (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ NextOfLt states⌝⦄ Code.add_union ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s ∧ assignableIf states s ∧ assignableP r states s⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.add_union_lift_spec (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ NextOfLt states⌝⦄ liftM Code.add_union ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s ∧ assignableIf states s ∧ assignableP r states s⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.add_union_lift_spec' (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) : ⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ NextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM Code.add_union ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(stateIdNextOfLt states r s.fst ∧ assignableIf states s.fst ∧ assignableP r states s.fst) ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.add_union_reverse_spec (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ NextOfLt states⌝⦄ Code.add_union_reverse ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s ∧ assignableP r states s⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.add_union_reverse_lift_spec (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ NextOfLt states⌝⦄ liftM Code.add_union_reverse ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s ∧ assignableP r states s⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.add_backrefence_spec (case_insensitive : Bool) (b : Nat) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ NextOfLt states⌝⦄ Code.add_backrefence case_insensitive b ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s ∧ assignableIf states s ∧ assignableP r states s⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.add_backrefence_lift_spec (case_insensitive : Bool) (b : Nat) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ NextOfLt states⌝⦄ liftM (Code.add_backrefence case_insensitive b) ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s ∧ assignableIf states s ∧ assignableP r states s⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_range_spec (start «end» : UInt32) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ NextOfLt states⌝⦄ Code.c_range start «end» ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLt states r s ∧ assignableIf states s ∧ assignableP r.end states s⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.add_empty_spec (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ NextOfLt states⌝⦄ Code.add_empty ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s ∧ assignableIf states s ∧ assignableP r states s⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.add_empty_lift_spec (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ NextOfLt states⌝⦄ liftM Code.add_empty ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s ∧ assignableIf states s ∧ assignableP r states s⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.add_empty_lift_spec' (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) : ⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ NextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM Code.add_empty ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(stateIdNextOfLt states r s.fst ∧ assignableIf states s.fst ∧ assignableP r states s.fst) ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.add_fail_spec (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ NextOfLt states⌝⦄ Code.add_fail ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s ∧ assignableIf states s ∧ isAppendOfStateID r states s⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.add_fail_lift_spec (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ NextOfLt states⌝⦄ liftM Code.add_fail ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s ∧ assignableIf states s ∧ isAppendOfStateID r states s⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.eat_next_of_le {mode : NFA.Unchecked.EatMode} (states : Array NFA.Unchecked.State) (h : mode.nextOf < states.size) : (NFA.Unchecked.State.Eat mode 0).nextOf ≤ states.size

@[simp]

theorem Compiler.Lemmas.patch2Assignable_of_eat_state {mode : NFA.Unchecked.EatMode} (states : Array NFA.Unchecked.State) (sid sid' : NFA.Unchecked.StateID) (hlt : sid < states.size) (heq : states[sid]? = some (NFA.Unchecked.State.Eat mode sid')) : patch2Assignable states sid

theorem Compiler.Lemmas.add_eat_spec (mode : NFA.Unchecked.EatMode) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ NextOfLt states ∧ mode.nextOf < states.size⌝⦄ Code.add_eat mode ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s ∧ assignableIf states s ∧ assignableP2 r states s⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.add_eat_lift_spec (mode : NFA.Unchecked.EatMode) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ NextOfLt states ∧ mode.nextOf < states.size⌝⦄ liftM (Code.add_eat mode) ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s ∧ assignableIf states s ∧ assignableP2 r states s⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

@[simp]

theorem Compiler.Lemmas.patch2Assignable_of_state {state : NFA.Unchecked.State} (states : Array NFA.Unchecked.State) (sid : NFA.Unchecked.StateID) (hlt : sid < states.size) (h : State.patch2Assignable state) (heq : states[sid]? = some state) : patch2Assignable states sid

@[simp]

theorem Compiler.Lemmas.patch2Assignable_of_add_change_state (states : Array NFA.Unchecked.State) (sid : NFA.Unchecked.StateID) (hlt : sid < states.size) (heq : states[sid]? = some (NFA.Unchecked.State.ChangeFrameStep 0 0)) : patch2Assignable states sid

theorem Compiler.Lemmas.add_change_state_spec (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ NextOfLt states ∧ 0 < states.size⌝⦄ Code.add_change_state ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s ∧ assignableIf states s ∧ assignableP2 r states s⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.add_change_state_lift_spec (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ NextOfLt states ∧ 0 < states.size⌝⦄ liftM Code.add_change_state ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s ∧ assignableIf states s ∧ assignableP2 r states s⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.add_remove_state_spec (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ NextOfLt states⌝⦄ Code.add_remove_state ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s ∧ assignableIf states s ∧ assignableP r states s⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.add_remove_state_lift_spec (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ NextOfLt states⌝⦄ liftM Code.add_remove_state ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s ∧ assignableIf states s ∧ assignableP r states s⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.add_next_char_spec (offset : Nat) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ NextOfLt states⌝⦄ Code.add_next_char offset ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s ∧ assignableIf states s ∧ assignableP r states s⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.add_next_char_lift_spec (offset : Nat) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) : ⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ NextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.add_next_char offset) ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(stateIdNextOfLt states r s.fst ∧ assignableIf states s.fst ∧ assignableP r states s.fst) ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_empty_spec (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ NextOfLt states⌝⦄ Code.c_empty ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLt states r s ∧ assignableP r.end states s⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_empty_lift_spec (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) : ⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ NextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM Code.c_empty ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(tRefNextOfLt states r s.fst ∧ assignableP r.end states s.fst) ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.add_sparse_spec (trans : Array NFA.Unchecked.Transition) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ NextOfLt states ∧ ∀ (i : Nat) (x : i < trans.size), trans[i].next ≤ states.size⌝⦄ Code.add_sparse trans ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s ∧ assignableIf states s ∧ patchAssignable s r⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_unicode_class_spec (cls : Regex.Syntax.ClassUnicode) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ NextOfLt states⌝⦄ Code.c_unicode_class cls ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLt states r s ∧ assignableIf states s ∧ patchAssignable s r.end⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_unicode_class_lift_spec (cls : Regex.Syntax.ClassUnicode) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) : ⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ NextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_unicode_class cls) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(tRefNextOfLt states r s.fst ∧ assignableIf states s.fst ∧ patchAssignable s.fst r.end) ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_literal_spec (c : Char) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ NextOfLt states⌝⦄ Code.c_literal c ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLt states r s ∧ assignableIf states s ∧ assignableP r.end states s⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_literal_lift_spec (c : Char) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) : ⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ NextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_literal c) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(tRefNextOfLt states r s.fst ∧ assignableIf states s.fst ∧ assignableP r.end states s.fst) ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_look_spec (look : Regex.Syntax.Look) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ NextOfLt states⌝⦄ Code.c_look look ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLt states r s ∧ assignableP r.end states s⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_look_lift_spec (look : Regex.Syntax.Look) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) : ⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ NextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_look look) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(tRefNextOfLt states r s.fst ∧ assignableP r.end states s.fst) ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_possessive_spec (tref : ThompsonRef) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ tref.start < states.size ∧ tref.end < states.size ∧ NextOfLt states ∧ patchAssignable states tref.end⌝⦄ Code.c_possessive tref ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLt states r s ∧ assignableIf states s ∧ patchAssignable s r.end⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_possessive_lift_spec (tref : ThompsonRef) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) : ⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ tref.start < states.size ∧ tref.end < states.size ∧ NextOfLt states ∧ patchAssignable states tref.end) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_possessive tref) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(tRefNextOfLt states r s.fst ∧ assignableIf states s.fst ∧ patchAssignable s.fst r.end) ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.tref_le_of_lt_spec {captures : Array NFA.Capture} (states : Array NFA.Unchecked.State) (tref : ThompsonRef) : ⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(tRefNextOfLt states tref s.fst ∧ assignableIf states s.fst ∧ patchAssignable s.fst tref.end) ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝⦄ EStateM.pure tref ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(tRefNextOfLeLt states r s.fst ∧ assignableIf states s.fst ∧ patchAssignable s.fst r.end) ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_possessive_le_lift_spec (tref : ThompsonRef) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) : ⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ tref.start < states.size ∧ tref.end < states.size ∧ NextOfLt states ∧ patchAssignable states tref.end) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_possessive tref) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(tRefNextOfLeLt states r s.fst ∧ assignableIf states s.fst ∧ patchAssignable s.fst r.end) ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_cap'_start_spec (group : Nat) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) : ⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜s.fst = states ∧ NextOfLt states ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ Code.c_cap' NFA.Capture.Role.Start group ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜stateIdNextOfLt states r s.fst ∧ assignableIf states s.fst ∧ assignableP r states s.fst ∧ cMemAndValid captures s.snd.fst ∧ { role := NFA.Capture.Role.Start, group := group } ∈ s.snd.fst⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_cap'_end_spec (group : Nat) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) (h : ∃ (c : NFA.Capture), c ∈ captures ∧ c.role = NFA.Capture.Role.Start ∧ c.group = group) : ⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜s.fst = states ∧ NextOfLt states ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ Code.c_cap' NFA.Capture.Role.End group ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜stateIdNextOfLt states r s.fst ∧ assignableIf states s.fst ∧ assignableP r states s.fst ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_back_ref_spec (case_insensitive : Bool) (n : Nat) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ NextOfLt states⌝⦄ Code.c_back_ref case_insensitive n ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLt states r s ∧ assignableIf states s ∧ patchAssignable s r.end⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_back_ref_lift_spec (case_insensitive : Bool) (n : Nat) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) : ⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ NextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_back_ref case_insensitive n) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(tRefNextOfLt states r s.fst ∧ assignableIf states s.fst ∧ patchAssignable s.fst r.end) ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_lookaround_PositiveLookahead_spec (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ tRefLt compiled states ∧ NextOfLt states ∧ patchAssignable states compiled.end⌝⦄ Code.c_lookaround_PositiveLookahead compiled ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLeLt states r s ∧ assignableIf states s ∧ patchAssignable s r.end⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_lookaround_PositiveLookahead_lift_spec (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) : ⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ tRefLt compiled states ∧ NextOfLt states ∧ patchAssignable states compiled.end) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_lookaround_PositiveLookahead compiled) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(tRefNextOfLeLt states r s.fst ∧ assignableIf states s.fst ∧ patchAssignable s.fst r.end) ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_lookaround_NegativeLookahead_spec (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ tRefLt compiled states ∧ NextOfLt states ∧ patchAssignable states compiled.end⌝⦄ Code.c_lookaround_NegativeLookahead compiled ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLeLt states r s ∧ assignableIf states s ∧ patchAssignable s r.end⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_lookaround_NegativeLookahead_lift_spec (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) : ⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ tRefLt compiled states ∧ NextOfLt states ∧ patchAssignable states compiled.end) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_lookaround_NegativeLookahead compiled) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(tRefNextOfLeLt states r s.fst ∧ assignableIf states s.fst ∧ patchAssignable s.fst r.end) ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_lookaround_PositiveLookbehind_spec (next_char : NFA.Unchecked.StateID) (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ next_char < states.size ∧ tRefLt compiled states ∧ NextOfLt states ∧ patchAssignable states next_char ∧ patchAssignable states compiled.end⌝⦄ Code.c_lookaround_PositiveLookbehind next_char compiled ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLeLt states r s ∧ assignableIf states s ∧ patchAssignable s r.end⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_lookaround_PositiveLookbehind_lift_spec (next_char : NFA.Unchecked.StateID) (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) : ⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ next_char < states.size ∧ tRefLt compiled states ∧ NextOfLt states ∧ patchAssignable states next_char ∧ patchAssignable states compiled.end) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_lookaround_PositiveLookbehind next_char compiled) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(tRefNextOfLeLt states r s.fst ∧ assignableIf states s.fst ∧ patchAssignable s.fst r.end) ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_lookaround_NegativeLookbehind_spec (next_char : NFA.Unchecked.StateID) (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ next_char < states.size ∧ tRefLt compiled states ∧ NextOfLt states ∧ patchAssignable states next_char ∧ patchAssignable states compiled.end⌝⦄ Code.c_lookaround_NegativeLookbehind next_char compiled ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLeLt states r s ∧ assignableIf states s ∧ patchAssignable s r.end⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_lookaround_NegativeLookbehind_lift_spec (next_char : NFA.Unchecked.StateID) (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) : ⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ next_char < states.size ∧ tRefLt compiled states ∧ NextOfLt states ∧ patchAssignable states next_char ∧ patchAssignable states compiled.end) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_lookaround_NegativeLookbehind next_char compiled) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(tRefNextOfLeLt states r s.fst ∧ assignableIf states s.fst ∧ patchAssignable s.fst r.end) ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_repetition_0_some_1_false_spec (union : NFA.Unchecked.StateID) (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ union < states.size ∧ tRefLt compiled states ∧ NextOfLt states ∧ patchAssignable states union ∧ patchAssignable states compiled.end⌝⦄ Code.c_repetition_0_some_1_false union compiled ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLeLt states r s ∧ assignableIf states s ∧ patchAssignable s r.end⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_repetition_0_some_1_false_lift_spec (union : NFA.Unchecked.StateID) (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) : ⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ union < states.size ∧ tRefLt compiled states ∧ NextOfLt states ∧ patchAssignable states union ∧ patchAssignable states compiled.end) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_repetition_0_some_1_false union compiled) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(tRefNextOfLeLt states r s.fst ∧ assignableIf states s.fst ∧ patchAssignable s.fst r.end) ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_repetition_0_some_1_true_spec (union : NFA.Unchecked.StateID) (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ union < states.size ∧ tRefLt compiled states ∧ NextOfLt states ∧ patchAssignable states union ∧ patchAssignable states compiled.end⌝⦄ Code.c_repetition_0_some_1_true union compiled ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLeLt states r s ∧ assignableIf states s ∧ patchAssignable s r.end⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_repetition_0_some_1_true_lift_spec (union : NFA.Unchecked.StateID) (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) : ⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ union < states.size ∧ tRefLt compiled states ∧ NextOfLt states ∧ patchAssignable states union ∧ patchAssignable states compiled.end) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_repetition_0_some_1_true union compiled) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(tRefNextOfLeLt states r s.fst ∧ assignableIf states s.fst ∧ patchAssignable s.fst r.end) ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_repetition_0_none_spec (union : NFA.Unchecked.StateID) (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ union < states.size ∧ tRefLt compiled states ∧ NextOfLt states ∧ patchAssignable states union ∧ patchAssignable states compiled.end⌝⦄ Code.c_repetition_0_none union compiled ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLeLt states r s ∧ assignableIf states s ∧ patchAssignable s r.end⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_repetition_0_none_lift_spec (union : NFA.Unchecked.StateID) (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) : ⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ union < states.size ∧ tRefLt compiled states ∧ NextOfLt states ∧ patchAssignable states union ∧ patchAssignable states compiled.end) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_repetition_0_none union compiled) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(tRefNextOfLeLt states r s.fst ∧ assignableIf states s.fst ∧ patchAssignable s.fst r.end) ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.greedy_union_spec (greedy : Bool) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ NextOfLt states⌝⦄ if greedy = true then liftM Code.add_union else liftM Code.add_union_reverse ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s ∧ assignableIf states s ∧ patchAssignable s r⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_at_least_0_pre_spec (compiled : ThompsonRef) (greedy : Bool) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ tRefLt compiled states ∧ NextOfLt states ∧ patchAssignable states compiled.end⌝⦄ Code.c_at_least_0_pre compiled greedy ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s ∧ assignableIf states s ∧ patchAssignable s r⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_at_least_0_pre_lift_spec (compiled : ThompsonRef) (greedy : Bool) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) : ⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ tRefLt compiled states ∧ NextOfLt states ∧ patchAssignable states compiled.end) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_at_least_0_pre compiled greedy) ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(stateIdNextOfLt states r s.fst ∧ assignableIf states s.fst ∧ patchAssignable s.fst r) ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_at_least_set_spec (possible_empty_capture_group : Option Nat) (greedy : Bool) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) {groups : Array Nat} : ⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜s.fst = states ∧ s.snd.fst = captures ∧ s.snd.snd = groups⌝⦄ Code.c_at_least_set possible_empty_capture_group greedy ⦃(fun (x : Unit) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜states = s.fst ∧ s.snd.fst = captures ∧ groups.size ≤ s.snd.snd.size ∧ assignableIf states s.fst⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_at_least_0_post_spec (compiled : ThompsonRef) (plus : NFA.Unchecked.StateID) (greedy possessive : Bool) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ plus < states.size ∧ compiled.start < states.size ∧ NextOfLt states ∧ patchAssignable states compiled.end ∧ patchAssignable states plus⌝⦄ Code.c_at_least_0_post compiled plus greedy possessive ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLeLt states r s ∧ assignableIf states s ∧ patchAssignable s r.end⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_at_least_0_post_lift_spec (compiled : ThompsonRef) (plus : NFA.Unchecked.StateID) (greedy possessive : Bool) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) : ⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ plus < states.size ∧ compiled.start < states.size ∧ NextOfLt states ∧ patchAssignable states compiled.end ∧ patchAssignable states plus) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_at_least_0_post compiled plus greedy possessive) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(tRefNextOfLeLt states r s.fst ∧ assignableIf states s.fst ∧ patchAssignable s.fst r.end) ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_at_least_0_spec (compiled : ThompsonRef) (possible_empty_capture_group : Option Nat) (greedy : Bool) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) : ⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜s.fst = states ∧ tRefLt compiled states ∧ NextOfLt states ∧ patchAssignable states compiled.end ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ Code.c_at_least_0 compiled possible_empty_capture_group greedy ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜stateIdNextOfLt states r s.fst ∧ assignableIf states s.fst ∧ patchAssignable s.fst r ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_at_least_1_pre_spec (greedy : Bool) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ NextOfLt states⌝⦄ Code.c_at_least_1_pre greedy ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s ∧ assignableIf states s ∧ patchAssignable s r⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_at_least_1_pre_lift_spec (greedy : Bool) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) : ⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ NextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_at_least_1_pre greedy) ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(stateIdNextOfLt states r s.fst ∧ assignableIf states s.fst ∧ patchAssignable s.fst r) ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_at_least_1_post_spec (compiled : ThompsonRef) (union : NFA.Unchecked.StateID) (possessive : Bool) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ union < states.size ∧ tRefLt compiled states ∧ NextOfLt states ∧ patchAssignable states compiled.end ∧ patchAssignable states union⌝⦄ Code.c_at_least_1_post compiled union possessive ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLeLt states r s ∧ assignableIf states s ∧ patchAssignable s r.end⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_at_least_1_post_lift_spec (compiled : ThompsonRef) (union : NFA.Unchecked.StateID) (possessive : Bool) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) : ⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ union < states.size ∧ tRefLt compiled states ∧ NextOfLt states ∧ patchAssignable states compiled.end ∧ patchAssignable states union) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_at_least_1_post compiled union possessive) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(tRefNextOfLeLt states r s.fst ∧ assignableIf states s.fst ∧ patchAssignable s.fst r.end) ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_at_least_1_spec (possible_empty_capture_group : Option Nat) (greedy : Bool) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) : ⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ NextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ Code.c_at_least_1 possible_empty_capture_group greedy ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜stateIdNextOfLt states r s.fst ∧ assignableIf states s.fst ∧ patchAssignable s.fst r ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_at_least_2_spec («prefix» last : ThompsonRef) (greedy possessive : Bool) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ tRefLt «prefix» states ∧ tRefLt last states ∧ NextOfLt states ∧ patchAssignable states «prefix».end ∧ patchAssignable states last.end⌝⦄ Code.c_at_least_2 «prefix» last greedy possessive ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLeLt states r s ∧ assignableIf states s ∧ patchAssignable s r.end⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄

theorem Compiler.Lemmas.c_at_least_2_lift_spec («prefix» last : ThompsonRef) (greedy possessive : Bool) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) : ⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ tRefLt «prefix» states ∧ tRefLt last states ∧ NextOfLt states ∧ patchAssignable states «prefix».end ∧ patchAssignable states last.end) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_at_least_2 «prefix» last greedy possessive) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(tRefNextOfLeLt states r s.fst ∧ assignableIf states s.fst ∧ patchAssignable s.fst r.end) ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄