internlm/Lean-Github huggingface dataset:
Theorem: Execution.Step.Exec.unprocessed_eq
Proof state before:
case h
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
i : ID
⊢ i ∈ unprocessed s₂ ↔ i ∈ unprocessed s₁ \ {rcn e}
Tactic:
simp [State.unprocessed, Equivalent.obj?_rcn_eq e.equiv, and_assoc, e.progress_eq]
Proof state after:
case h
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
i : ID
⊢ i ∈ s₂.rtr[Component.rcn] → (i ∉ Set.insert (rcn e) s₁.progress ↔ i ∉ s₁.progress ∧ ¬i = rcn e)
Theorem: Execution.Step.Exec.unprocessed_eq
Proof state before:
case h
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
i : ID
⊢ i ∈ s₂.rtr[Component.rcn] → (i ∉ Set.insert (rcn e) s₁.progress ↔ i ∉ s₁.progress ∧ ¬i = rcn e)
Tactic:
intro _
Proof state after:
case h
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
i : ID
a✝ : i ∈ s₂.rtr[Component.rcn]
⊢ i ∉ Set.insert (rcn e) s₁.progress ↔ i ∉ s₁.progress ∧ ¬i = rcn e
Theorem: Execution.Step.Exec.unprocessed_eq
Proof state before:
case h
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
i : ID
a✝ : i ∈ s₂.rtr[Component.rcn]
⊢ i ∉ Set.insert (rcn e) s₁.progress ↔ i ∉ s₁.progress ∧ ¬i = rcn e
Tactic:
simp [Set.insert]
Proof state after:
case h
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
i : ID
a✝ : i ∈ s₂.rtr[Component.rcn]
⊢ ¬(i = rcn e ∨ i ∈ s₁.progress) ↔ i ∉ s₁.progress ∧ ¬i = rcn e
Theorem: Execution.Step.Exec.unprocessed_eq
Proof state before:
case h
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
i : ID
a✝ : i ∈ s₂.rtr[Component.rcn]
⊢ ¬(i = rcn e ∨ i ∈ s₁.progress) ↔ i ∉ s₁.progress ∧ ¬i = rcn e
Tactic:
push_neg
Proof state after:
case h
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
i : ID
a✝ : i ∈ s₂.rtr[Component.rcn]
⊢ i ≠ rcn e ∧ i ∉ s₁.progress ↔ i ∉ s₁.progress ∧ i ≠ rcn e
Theorem: Execution.Step.Exec.unprocessed_eq
Proof state before:
case h
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
i : ID
a✝ : i ∈ s₂.rtr[Component.rcn]
⊢ i ≠ rcn e ∧ i ∉ s₁.progress ↔ i ∉ s₁.progress ∧ i ≠ rcn e
Tactic:
simp [and_comm]
Proof state after:
no goals
Theorem: Execution.Step.Exec.unprocessed_ssubset
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
⊢ unprocessed s₂ ⊂ unprocessed s₁
Tactic:
simp [e.unprocessed_eq, Set.ssubset_iff_subset_ne]
Proof state after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
⊢ rcn e ∈ unprocessed s₁
Theorem: Execution.Step.Exec.unprocessed_ssubset
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
⊢ rcn e ∈ unprocessed s₁
Tactic:
exact e.rcn_mem_unprocessed
Proof state after:
no goals
Theorem: Execution.Step.Exec.indep_restriction_eq
Proof state before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
cpt : Component.Valued
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
ho : s₁.rtr[Component.rcn][i] = some rcn
⊢ input.restriction s₁ rcn cpt = input.restriction s₂ rcn cpt
Tactic:
simp [input.restriction]
Proof state after:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
cpt : Component.Valued
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
ho : s₁.rtr[Component.rcn][i] = some rcn
⊢ Partial.restrict (s₁.rtr[Component.val cpt]) {i | { cpt := cpt, id := i } ∈ rcn.deps Kind.in} =
    Partial.restrict (s₂.rtr[Component.val cpt]) {i | { cpt := cpt, id := i } ∈ rcn.deps Kind.in}
Theorem: Execution.Step.Exec.indep_restriction_eq
Proof state before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
cpt : Component.Valued
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
ho : s₁.rtr[Component.rcn][i] = some rcn
⊢ Partial.restrict (s₁.rtr[Component.val cpt]) {i | { cpt := cpt, id := i } ∈ rcn.deps Kind.in} =
    Partial.restrict (s₂.rtr[Component.val cpt]) {i | { cpt := cpt, id := i } ∈ rcn.deps Kind.in}
Tactic:
apply Partial.ext_restrict
Proof state after:
case h
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
cpt : Component.Valued
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
ho : s₁.rtr[Component.rcn][i] = some rcn
⊢ ∀ a ∈ {i | { cpt := cpt, id := i } ∈ rcn.deps Kind.in}, s₁.rtr[Component.val cpt][a] = s₂.rtr[Component.val cpt][a]
Theorem: Execution.Step.Exec.indep_restriction_eq
Proof state before:
case h
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
cpt : Component.Valued
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
ho : s₁.rtr[Component.rcn][i] = some rcn
⊢ ∀ a ∈ {i | { cpt := cpt, id := i } ∈ rcn.deps Kind.in}, s₁.rtr[Component.val cpt][a] = s₂.rtr[Component.val cpt][a]
Tactic:
intro _ hd
Proof state after:
case h
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
cpt : Component.Valued
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
ho : s₁.rtr[Component.rcn][i] = some rcn
a✝ : Component.idType (Component.val cpt)
hd : a✝ ∈ {i | { cpt := cpt, id := i } ∈ rcn.deps Kind.in}
⊢ s₁.rtr[Component.val cpt][a✝] = s₂.rtr[Component.val cpt][a✝]
Theorem: Execution.Step.Exec.indep_restriction_eq
Proof state before:
case h
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
cpt : Component.Valued
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
ho : s₁.rtr[Component.rcn][i] = some rcn
a✝ : Component.idType (Component.val cpt)
hd : a✝ ∈ {i | { cpt := cpt, id := i } ∈ rcn.deps Kind.in}
⊢ s₁.rtr[Component.val cpt][a✝] = s₂.rtr[Component.val cpt][a✝]
Tactic:
exact e.applied_rtr_eq ▸ e.apply.preserves_unchanged $ State.target_not_mem_indep_output ho hi hd
Proof state after:
no goals
Theorem: Execution.Step.Exec.indep_input_eq
Proof state before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
h₁ : s₁.rtr[Component.rcn][i] = some rcn
h₂ : s₂.rtr[Component.rcn][i] = some rcn
⊢ input s₁ i = input s₂ i
Tactic:
simp [input, h₁, h₂]
Proof state after:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
h₁ : s₁.rtr[Component.rcn][i] = some rcn
h₂ : s₂.rtr[Component.rcn][i] = some rcn
⊢ ((fun cpt => input.restriction s₁ rcn cpt) = fun cpt => input.restriction s₂ rcn cpt) ∧ s₁.tag = s₂.tag
Theorem: Execution.Step.Exec.indep_input_eq
Proof state before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
h₁ : s₁.rtr[Component.rcn][i] = some rcn
h₂ : s₂.rtr[Component.rcn][i] = some rcn
⊢ ((fun cpt => input.restriction s₁ rcn cpt) = fun cpt => input.restriction s₂ rcn cpt) ∧ s₁.tag = s₂.tag
Tactic:
refine ⟨?_, e.preserves_tag⟩
Proof state after:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
h₁ : s₁.rtr[Component.rcn][i] = some rcn
h₂ : s₂.rtr[Component.rcn][i] = some rcn
⊢ (fun cpt => input.restriction s₁ rcn cpt) = fun cpt => input.restriction s₂ rcn cpt
Theorem: Execution.Step.Exec.indep_input_eq
Proof state before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
h₁ : s₁.rtr[Component.rcn][i] = some rcn
h₂ : s₂.rtr[Component.rcn][i] = some rcn
⊢ (fun cpt => input.restriction s₁ rcn cpt) = fun cpt => input.restriction s₂ rcn cpt
Tactic:
ext1
Proof state after:
case h
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
h₁ : s₁.rtr[Component.rcn][i] = some rcn
h₂ : s₂.rtr[Component.rcn][i] = some rcn
x✝ : Component.Valued
⊢ input.restriction s₁ rcn x✝ = input.restriction s₂ rcn x✝
Theorem: Execution.Step.Exec.indep_input_eq
Proof state before:
case h
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
h₁ : s₁.rtr[Component.rcn][i] = some rcn
h₂ : s₂.rtr[Component.rcn][i] = some rcn
x✝ : Component.Valued
⊢ input.restriction s₁ rcn x✝ = input.restriction s₂ rcn x✝
Tactic:
exact e.indep_restriction_eq hi h₁
Proof state after:
no goals
Theorem: Execution.Step.Exec.indep_output_eq
Proof state before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
⊢ output s₁ i = output s₂ i
Tactic:
simp [output]
Proof state after:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
⊢ (match s₁.rtr[Component.rcn][i], [], fun x => x.body (input s₁ i) with
    | some x, x_1, f => f x
    | none, y, x => y) =
    match s₂.rtr[Component.rcn][i], [], fun x => x.body (input s₂ i) with
    | some x, x_1, f => f x
    | none, y, x => y
Theorem: Execution.Step.Exec.indep_output_eq
Proof state before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
⊢ (match s₁.rtr[Component.rcn][i], [], fun x => x.body (input s₁ i) with
    | some x, x_1, f => f x
    | none, y, x => y) =
    match s₂.rtr[Component.rcn][i], [], fun x => x.body (input s₂ i) with
    | some x, x_1, f => f x
    | none, y, x => y
Tactic:
have he := Equivalent.obj?_rcn_eq e.equiv
Proof state after:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
he : s₁.rtr[Component.rcn] = s₂.rtr[Component.rcn]
⊢ (match s₁.rtr[Component.rcn][i], [], fun x => x.body (input s₁ i) with
    | some x, x_1, f => f x
    | none, y, x => y) =
    match s₂.rtr[Component.rcn][i], [], fun x => x.body (input s₂ i) with
    | some x, x_1, f => f x
    | none, y, x => y
Theorem: Execution.Step.Exec.indep_output_eq
Proof state before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
he : s₁.rtr[Component.rcn] = s₂.rtr[Component.rcn]
⊢ (match s₁.rtr[Component.rcn][i], [], fun x => x.body (input s₁ i) with
    | some x, x_1, f => f x
    | none, y, x => y) =
    match s₂.rtr[Component.rcn][i], [], fun x => x.body (input s₂ i) with
    | some x, x_1, f => f x
    | none, y, x => y
Tactic:
cases h : s₁.rtr[.rcn][i] <;> simp [he ▸ h]
Proof state after:
case some
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
he : s₁.rtr[Component.rcn] = s₂.rtr[Component.rcn]
val✝ : Component.type α Component.rcn
h : s₁.rtr[Component.rcn][i] = some val✝
⊢ val✝.body (input s₁ i) = val✝.body (input s₂ i)
Theorem: Execution.Step.Exec.indep_output_eq
Proof state before:
case some
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
he : s₁.rtr[Component.rcn] = s₂.rtr[Component.rcn]
val✝ : Component.type α Component.rcn
h : s₁.rtr[Component.rcn][i] = some val✝
⊢ val✝.body (input s₁ i) = val✝.body (input s₂ i)
Tactic:
simp [e.indep_input_eq hi h $ he ▸ h]
Proof state after:
no goals
Theorem: Execution.Step.Exec.indep_comm
Proof state before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₑ s₁
e₁₂ : s₁ ↓ₑ s₁₂
e₂ : s ↓ₑ s₂
e₂₁ : s₂ ↓ₑ s₂₁
hr₁ : Execution.Step.Exec.rcn e₁ = Execution.Step.Exec.rcn e₂₁
hr₂ : Execution.Step.Exec.rcn e₂ = Execution.Step.Exec.rcn e₁₂
hi : Execution.Step.Exec.rcn e₁ ≮[s.rtr]≯ Execution.Step.Exec.rcn e₂
⊢ s₁₂ = s₂₁
Tactic:
have ho₁ := e₁.indep_output_eq hi
Proof state after:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₑ s₁
e₁₂ : s₁ ↓ₑ s₁₂
e₂ : s ↓ₑ s₂
e₂₁ : s₂ ↓ₑ s₂₁
hr₁ : Execution.Step.Exec.rcn e₁ = Execution.Step.Exec.rcn e₂₁
hr₂ : Execution.Step.Exec.rcn e₂ = Execution.Step.Exec.rcn e₁₂
hi : Execution.Step.Exec.rcn e₁ ≮[s.rtr]≯ Execution.Step.Exec.rcn e₂
ho₁ : output s (Execution.Step.Exec.rcn e₂) = output s₁ (Execution.Step.Exec.rcn e₂)
⊢ s₁₂ = s₂₁
Theorem: Execution.Step.Exec.indep_comm
Proof state before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₑ s₁
e₁₂ : s₁ ↓ₑ s₁₂
e₂ : s ↓ₑ s₂
e₂₁ : s₂ ↓ₑ s₂₁
hr₁ : Execution.Step.Exec.rcn e₁ = Execution.Step.Exec.rcn e₂₁
hr₂ : Execution.Step.Exec.rcn e₂ = Execution.Step.Exec.rcn e₁₂
hi : Execution.Step.Exec.rcn e₁ ≮[s.rtr]≯ Execution.Step.Exec.rcn e₂
ho₁ : output s (Execution.Step.Exec.rcn e₂) = output s₁ (Execution.Step.Exec.rcn e₂)
⊢ s₁₂ = s₂₁
Tactic:
have ho₂ := e₂.indep_output_eq hi.symm
Proof state after:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₑ s₁
e₁₂ : s₁ ↓ₑ s₁₂
e₂ : s ↓ₑ s₂
e₂₁ : s₂ ↓ₑ s₂₁
hr₁ : Execution.Step.Exec.rcn e₁ = Execution.Step.Exec.rcn e₂₁
hr₂ : Execution.Step.Exec.rcn e₂ = Execution.Step.Exec.rcn e₁₂
hi : Execution.Step.Exec.rcn e₁ ≮[s.rtr]≯ Execution.Step.Exec.rcn e₂
ho₁ : output s (Execution.Step.Exec.rcn e₂) = output s₁ (Execution.Step.Exec.rcn e₂)
ho₂ : output s (Execution.Step.Exec.rcn e₁) = output s₂ (Execution.Step.Exec.rcn e₁)
⊢ s₁₂ = s₂₁
Theorem: Execution.Step.Exec.indep_comm
Proof state before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₑ s₁
e₁₂ : s₁ ↓ₑ s₁₂
e₂ : s ↓ₑ s₂
e₂₁ : s₂ ↓ₑ s₂₁
hr₁ : Execution.Step.Exec.rcn e₁ = Execution.Step.Exec.rcn e₂₁
hr₂ : Execution.Step.Exec.rcn e₂ = Execution.Step.Exec.rcn e₁₂
hi : Execution.Step.Exec.rcn e₁ ≮[s.rtr]≯ Execution.Step.Exec.rcn e₂
ho₁ : output s (Execution.Step.Exec.rcn e₂) = output s₁ (Execution.Step.Exec.rcn e₂)
ho₂ : output s (Execution.Step.Exec.rcn e₁) = output s₂ (Execution.Step.Exec.rcn e₁)
⊢ s₁₂ = s₂₁
Tactic:
cases e₁
Proof state after:
case mk
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
s₁₂ s₂ s₂₁ : State α
e₂ : s ↓ₑ s₂
e₂₁ : s₂ ↓ₑ s₂₁
rcn✝ : ID
s₂✝ : State α
a✝² : Allows s rcn✝
a✝¹ : Triggers s rcn✝
a✝ : s -[output s rcn✝]→ s₂✝
e₁₂ : (record s₂✝ rcn✝) ↓ₑ s₁₂
hr₂ : Execution.Step.Exec.rcn e₂ = Execution.Step.Exec.rcn e₁₂
ho₁ : output s (Execution.Step.Exec.rcn e₂) = output (record s₂✝ rcn✝) (Execution.Step.Exec.rcn e₂)
hr₁ : Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝) = Execution.Step.Exec.rcn e₂₁
hi : Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝) ≮[s.rtr]≯ Execution.Step.Exec.rcn e₂
ho₂ : output s (Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝)) = output s₂ (Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝))
⊢ s₁₂ = s₂₁
Theorem: Execution.Step.Exec.indep_comm
Proof state before:
case mk
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
s₁₂ s₂ s₂₁ : State α
e₂ : s ↓ₑ s₂
e₂₁ : s₂ ↓ₑ s₂₁
rcn✝ : ID
s₂✝ : State α
a✝² : Allows s rcn✝
a✝¹ : Triggers s rcn✝
a✝ : s -[output s rcn✝]→ s₂✝
e₁₂ : (record s₂✝ rcn✝) ↓ₑ s₁₂
hr₂ : Execution.Step.Exec.rcn e₂ = Execution.Step.Exec.rcn e₁₂
ho₁ : output s (Execution.Step.Exec.rcn e₂) = output (record s₂✝ rcn✝) (Execution.Step.Exec.rcn e₂)
hr₁ : Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝) = Execution.Step.Exec.rcn e₂₁
hi : Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝) ≮[s.rtr]≯ Execution.Step.Exec.rcn e₂
ho₂ : output s (Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝)) = output s₂ (Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝))
⊢ s₁₂ = s₂₁
Tactic:
cases e₁₂
Proof state after:
case mk.mk
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
s₂ s₂₁ : State α
e₂ : s ↓ₑ s₂
e₂₁ : s₂ ↓ₑ s₂₁
rcn✝¹ : ID
s₂✝¹ : State α
a✝⁵ : Allows s rcn✝¹
a✝⁴ : Triggers s rcn✝¹
a✝³ : s -[output s rcn✝¹]→ s₂✝¹
ho₁ : output s (Execution.Step.Exec.rcn e₂) = output (record s₂✝¹ rcn✝¹) (Execution.Step.Exec.rcn e₂)
hr₁ : Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a✝³) = Execution.Step.Exec.rcn e₂₁
hi : Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a✝³) ≮[s.rtr]≯ Execution.Step.Exec.rcn e₂
ho₂ : output s (Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a✝³)) = output s₂ (Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a✝³))
rcn✝ : ID
s₂✝ : State α
a✝² : Allows (record s₂✝¹ rcn✝¹) rcn✝
a✝¹ : Triggers (record s₂✝¹ rcn✝¹) rcn✝
a✝ : (record s₂✝¹ rcn✝¹) -[output (record s₂✝¹ rcn✝¹) rcn✝]→ s₂✝
hr₂ : Execution.Step.Exec.rcn e₂ = Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝)
⊢ record s₂✝ rcn✝ = s₂₁
Theorem: Execution.Step.Exec.indep_comm
Proof state before:
case mk.mk
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
s₂ s₂₁ : State α
e₂ : s ↓ₑ s₂
e₂₁ : s₂ ↓ₑ s₂₁
rcn✝¹ : ID
s₂✝¹ : State α
a✝⁵ : Allows s rcn✝¹
a✝⁴ : Triggers s rcn✝¹
a✝³ : s -[output s rcn✝¹]→ s₂✝¹
ho₁ : output s (Execution.Step.Exec.rcn e₂) = output (record s₂✝¹ rcn✝¹) (Execution.Step.Exec.rcn e₂)
hr₁ : Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a✝³) = Execution.Step.Exec.rcn e₂₁
hi : Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a✝³) ≮[s.rtr]≯ Execution.Step.Exec.rcn e₂
ho₂ : output s (Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a✝³)) = output s₂ (Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a✝³))
rcn✝ : ID
s₂✝ : State α
a✝² : Allows (record s₂✝¹ rcn✝¹) rcn✝
a✝¹ : Triggers (record s₂✝¹ rcn✝¹) rcn✝
a✝ : (record s₂✝¹ rcn✝¹) -[output (record s₂✝¹ rcn✝¹) rcn✝]→ s₂✝
hr₂ : Execution.Step.Exec.rcn e₂ = Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝)
⊢ record s₂✝ rcn✝ = s₂₁
Tactic:
cases e₂
Proof state after:
case mk.mk.mk
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
s₂₁ : State α
rcn✝² : ID
s₂✝² : State α
a✝⁸ : Allows s rcn✝²
a✝⁷ : Triggers s rcn✝²
a✝⁶ : s -[output s rcn✝²]→ s₂✝²
rcn✝¹ : ID
s₂✝¹ : State α
a✝⁵ : Allows (record s₂✝² rcn✝²) rcn✝¹
a✝⁴ : Triggers (record s₂✝² rcn✝²) rcn✝¹
a✝³ : (record s₂✝² rcn✝²) -[output (record s₂✝² rcn✝²) rcn✝¹]→ s₂✝¹
rcn✝ : ID
s₂✝ : State α
a✝² : Allows s rcn✝
a✝¹ : Triggers s rcn✝
a✝ : s -[output s rcn✝]→ s₂✝
e₂₁ : (record s₂✝ rcn✝) ↓ₑ s₂₁
hr₁ : Execution.Step.Exec.rcn (mk a✝⁸ a✝⁷ a✝⁶) = Execution.Step.Exec.rcn e₂₁
ho₂ :
  output s (Execution.Step.Exec.rcn (mk a✝⁸ a✝⁷ a✝⁶)) =
    output (record s₂✝ rcn✝) (Execution.Step.Exec.rcn (mk a✝⁸ a✝⁷ a✝⁶))
ho₁ :
  output s (Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝)) =
    output (record s₂✝² rcn✝²) (Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝))
hi : Execution.Step.Exec.rcn (mk a✝⁸ a✝⁷ a✝⁶) ≮[s.rtr]≯ Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝)
hr₂ : Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝) = Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a✝³)
⊢ record s₂✝¹ rcn✝¹ = s₂₁
Theorem: Execution.Step.Exec.indep_comm
Proof state before:
case mk.mk.mk
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
s₂₁ : State α
rcn✝² : ID
s₂✝² : State α
a✝⁸ : Allows s rcn✝²
a✝⁷ : Triggers s rcn✝²
a✝⁶ : s -[output s rcn✝²]→ s₂✝²
rcn✝¹ : ID
s₂✝¹ : State α
a✝⁵ : Allows (record s₂✝² rcn✝²) rcn✝¹
a✝⁴ : Triggers (record s₂✝² rcn✝²) rcn✝¹
a✝³ : (record s₂✝² rcn✝²) -[output (record s₂✝² rcn✝²) rcn✝¹]→ s₂✝¹
rcn✝ : ID
s₂✝ : State α
a✝² : Allows s rcn✝
a✝¹ : Triggers s rcn✝
a✝ : s -[output s rcn✝]→ s₂✝
e₂₁ : (record s₂✝ rcn✝) ↓ₑ s₂₁
hr₁ : Execution.Step.Exec.rcn (mk a✝⁸ a✝⁷ a✝⁶) = Execution.Step.Exec.rcn e₂₁
ho₂ :
  output s (Execution.Step.Exec.rcn (mk a✝⁸ a✝⁷ a✝⁶)) =
    output (record s₂✝ rcn✝) (Execution.Step.Exec.rcn (mk a✝⁸ a✝⁷ a✝⁶))
ho₁ :
  output s (Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝)) =
    output (record s₂✝² rcn✝²) (Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝))
hi : Execution.Step.Exec.rcn (mk a✝⁸ a✝⁷ a✝⁶) ≮[s.rtr]≯ Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝)
hr₂ : Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝) = Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a✝³)
⊢ record s₂✝¹ rcn✝¹ = s₂₁
Tactic:
cases e₂₁
Proof state after:
case mk.mk.mk.mk
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn✝³ : ID
s₂✝³ : State α
a✝¹¹ : Allows s rcn✝³
a✝¹⁰ : Triggers s rcn✝³
a✝⁹ : s -[output s rcn✝³]→ s₂✝³
rcn✝² : ID
s₂✝² : State α
a✝⁸ : Allows (record s₂✝³ rcn✝³) rcn✝²
a✝⁷ : Triggers (record s₂✝³ rcn✝³) rcn✝²
a✝⁶ : (record s₂✝³ rcn✝³) -[output (record s₂✝³ rcn✝³) rcn✝²]→ s₂✝²
rcn✝¹ : ID
s₂✝¹ : State α
a✝⁵ : Allows s rcn✝¹
a✝⁴ : Triggers s rcn✝¹
a✝³ : s -[output s rcn✝¹]→ s₂✝¹
ho₂ :
  output s (Execution.Step.Exec.rcn (mk a✝¹¹ a✝¹⁰ a✝⁹)) =
    output (record s₂✝¹ rcn✝¹) (Execution.Step.Exec.rcn (mk a✝¹¹ a✝¹⁰ a✝⁹))
ho₁ :
  output s (Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a✝³)) =
    output (record s₂✝³ rcn✝³) (Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a✝³))
hi : Execution.Step.Exec.rcn (mk a✝¹¹ a✝¹⁰ a✝⁹) ≮[s.rtr]≯ Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a✝³)
hr₂ : Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a✝³) = Execution.Step.Exec.rcn (mk a✝⁸ a✝⁷ a✝⁶)
rcn✝ : ID
s₂✝ : State α
a✝² : Allows (record s₂✝¹ rcn✝¹) rcn✝
a✝¹ : Triggers (record s₂✝¹ rcn✝¹) rcn✝
a✝ : (record s₂✝¹ rcn✝¹) -[output (record s₂✝¹ rcn✝¹) rcn✝]→ s₂✝
hr₁ : Execution.Step.Exec.rcn (mk a✝¹¹ a✝¹⁰ a✝⁹) = Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝)
⊢ record s₂✝² rcn✝² = record s₂✝ rcn✝
Theorem: Execution.Step.Exec.indep_comm
Proof state before:
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
s₁₂ : State α
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
a₁₂ : (record s₁ rcn₁) -[output (record s₁ rcn₁) rcn₂]→ s₁₂
rcn✝¹ : ID
s₂ : State α
a✝³ : Allows s rcn✝¹
a✝² : Triggers s rcn✝¹
a₂ : s -[output s rcn✝¹]→ s₂
ho₂ :
  output s (Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁)) =
    output (record s₂ rcn✝¹) (Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁))
ho₁ :
  output s (Execution.Step.Exec.rcn (mk a✝³ a✝² a₂)) = output (record s₁ rcn₁) (Execution.Step.Exec.rcn (mk a✝³ a✝² a₂))
hi : Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁) ≮[s.rtr]≯ Execution.Step.Exec.rcn (mk a✝³ a✝² a₂)
hr₂ : Execution.Step.Exec.rcn (mk a✝³ a✝² a₂) = Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a₁₂)
rcn✝ : ID
s₂₁ : State α
a✝¹ : Allows (record s₂ rcn✝¹) rcn✝
a✝ : Triggers (record s₂ rcn✝¹) rcn✝
a₂₁ : (record s₂ rcn✝¹) -[output (record s₂ rcn✝¹) rcn✝]→ s₂₁
hr₁ : Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁) = Execution.Step.Exec.rcn (mk a✝¹ a✝ a₂₁)
⊢ record s₁₂ rcn₂ = record s₂₁ rcn✝
Tactic:
case _ rcn₁ s₁ _ _ a₁ rcn₂ s₁₂ _ _ a₁₂ _ s₂ _ _ a₂ _ s₂₁ _ _ a₂₁ => 
  cases hr₁; cases hr₂; simp [Exec.rcn] at *
  have ⟨z₁₂, f₁₂⟩ := Apply.RTC.construct s₁ (s.output rcn₂)
  have ⟨z₂₁, f₂₁⟩ := Apply.RTC.construct s₂ (s.output rcn₁)
  rw [←ho₁] at a₁₂; rw [←ho₂] at a₂₁
  cases f₁₂.comm_record a₁₂; cases f₂₁.comm_record a₂₁
  rw [record_comm]; congr
  exact Apply.RTC.disjoint_targets_comm (s.indep_output_disjoint_targets hi) a₁ f₁₂ a₂ f₂₁
Proof state after:
no goals
Theorem: Execution.Step.Exec.indep_comm
Proof state before:
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
s₁₂ : State α
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
a₁₂ : (record s₁ rcn₁) -[output (record s₁ rcn₁) rcn₂]→ s₁₂
rcn✝¹ : ID
s₂ : State α
a✝³ : Allows s rcn✝¹
a✝² : Triggers s rcn✝¹
a₂ : s -[output s rcn✝¹]→ s₂
ho₂ :
  output s (Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁)) =
    output (record s₂ rcn✝¹) (Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁))
ho₁ :
  output s (Execution.Step.Exec.rcn (mk a✝³ a✝² a₂)) = output (record s₁ rcn₁) (Execution.Step.Exec.rcn (mk a✝³ a✝² a₂))
hi : Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁) ≮[s.rtr]≯ Execution.Step.Exec.rcn (mk a✝³ a✝² a₂)
hr₂ : Execution.Step.Exec.rcn (mk a✝³ a✝² a₂) = Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a₁₂)
rcn✝ : ID
s₂₁ : State α
a✝¹ : Allows (record s₂ rcn✝¹) rcn✝
a✝ : Triggers (record s₂ rcn✝¹) rcn✝
a₂₁ : (record s₂ rcn✝¹) -[output (record s₂ rcn✝¹) rcn✝]→ s₂₁
hr₁ : Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁) = Execution.Step.Exec.rcn (mk a✝¹ a✝ a₂₁)
⊢ record s₁₂ rcn₂ = record s₂₁ rcn✝
Tactic:
cases hr₁
Proof state after:
case refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
s₁₂ : State α
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
a₁₂ : (record s₁ rcn₁) -[output (record s₁ rcn₁) rcn₂]→ s₁₂
rcn✝ : ID
s₂ : State α
a✝³ : Allows s rcn✝
a✝² : Triggers s rcn✝
a₂ : s -[output s rcn✝]→ s₂
ho₂ :
  output s (Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁)) = output (record s₂ rcn✝) (Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁))
ho₁ :
  output s (Execution.Step.Exec.rcn (mk a✝³ a✝² a₂)) = output (record s₁ rcn₁) (Execution.Step.Exec.rcn (mk a✝³ a✝² a₂))
hi : Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁) ≮[s.rtr]≯ Execution.Step.Exec.rcn (mk a✝³ a✝² a₂)
hr₂ : Execution.Step.Exec.rcn (mk a✝³ a✝² a₂) = Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a₁₂)
s₂₁ : State α
a✝¹ : Allows (record s₂ rcn✝) rcn₁
a✝ : Triggers (record s₂ rcn✝) rcn₁
a₂₁ : (record s₂ rcn✝) -[output (record s₂ rcn✝) rcn₁]→ s₂₁
⊢ record s₁₂ rcn₂ = record s₂₁ rcn₁