Theorem: Reactor.Refresh.deterministic (ReactorModel/Execution/Theorems/Reactor.lean)

State before:
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
⊢ rtr₁ = rtr₂
Tactic:
have e := Equivalent.trans (Equivalent.symm rf₁.equiv) rf₂.equiv
State after:
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
⊢ rtr₁ = rtr₂

State before:
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
⊢ rtr₁ = rtr₂
Tactic:
apply ext_obj? e
State after:
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
⊢ ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂

State before:
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
⊢ ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
Tactic:
intro cpt _ _ _ ho₁ ho₂
State after:
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
cpt : Component.Valued
i✝ : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₁[Component.val cpt][i✝] = some o₁✝
ho₂ : rtr₂[Component.val cpt][i✝] = some o₂✝
⊢ o₁✝ = o₂✝

State before:
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
cpt : Component.Valued
i✝ : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₁[Component.val cpt][i✝] = some o₁✝
ho₂ : rtr₂[Component.val cpt][i✝] = some o₂✝
⊢ o₁✝ = o₂✝
Tactic:
cases cpt
State after:
case inp
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
i✝ : Component.idType (Component.val Component.Valued.inp)
o₁✝ o₂✝ : Component.type α (Component.val Component.Valued.inp)
ho₁ : rtr₁[Component.val Component.Valued.inp][i✝] = some o₁✝
ho₂ : rtr₂[Component.val Component.Valued.inp][i✝] = some o₂✝
⊢ o₁✝ = o₂✝

case out
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
i✝ : Component.idType (Component.val Component.Valued.out)
o₁✝ o₂✝ : Component.type α (Component.val Component.Valued.out)
ho₁ : rtr₁[Component.val Component.Valued.out][i✝] = some o₁✝
ho₂ : rtr₂[Component.val Component.Valued.out][i✝] = some o₂✝
⊢ o₁✝ = o₂✝

case stv
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
i✝ : Component.idType (Component.val Component.Valued.stv)
o₁✝ o₂✝ : Component.type α (Component.val Component.Valued.stv)
ho₁ : rtr₁[Component.val Component.Valued.stv][i✝] = some o₁✝
ho₂ : rtr₂[Component.val Component.Valued.stv][i✝] = some o₂✝
⊢ o₁✝ = o₂✝

case act
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
i✝ : Component.idType (Component.val Component.Valued.act)
o₁✝ o₂✝ : Component.type α (Component.val Component.Valued.act)
ho₁ : rtr₁[Component.val Component.Valued.act][i✝] = some o₁✝
ho₂ : rtr₂[Component.val Component.Valued.act][i✝] = some o₂✝
⊢ o₁✝ = o₂✝

State before:
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
i✝ : Component.idType (Component.val Component.Valued.stv)
o₁✝ o₂✝ : Component.type α (Component.val Component.Valued.stv)
ho₁ : rtr₁[Component.val Component.Valued.stv][i✝] = some o₁✝
ho₂ : rtr₂[Component.val Component.Valued.stv][i✝] = some o₂✝
⊢ o₁✝ = o₂✝
Tactic:
case stv => injection (rf₁.eq_state ▸ ho₁) ▸ rf₂.eq_state ▸ ho₂
State after:
no goals

State before:
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
i✝ : Component.idType (Component.val Component.Valued.act)
o₁✝ o₂✝ : Component.type α (Component.val Component.Valued.act)
ho₁ : rtr₁[Component.val Component.Valued.act][i✝] = some o₁✝
ho₂ : rtr₂[Component.val Component.Valued.act][i✝] = some o₂✝
⊢ o₁✝ = o₂✝
Tactic:
case act => injection (rf₁.acts     ▸ ho₁) ▸ rf₂.acts     ▸ ho₂
State after:
no goals

State before:
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
i✝ : Component.idType (Component.val Component.Valued.inp)
o₁✝ o₂✝ : Component.type α (Component.val Component.Valued.inp)
ho₁ : rtr₁[Component.val Component.Valued.inp][i✝] = some o₁✝
ho₂ : rtr₂[Component.val Component.Valued.inp][i✝] = some o₂✝
⊢ o₁✝ = o₂✝
Tactic:
case inp => injection (rf₁.inputs   ▸ ho₁) ▸ rf₂.inputs   ▸ ho₂
State after:
no goals

State before:
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
i✝ : Component.idType (Component.val Component.Valued.out)
o₁✝ o₂✝ : Component.type α (Component.val Component.Valued.out)
ho₁ : rtr₁[Component.val Component.Valued.out][i✝] = some o₁✝
ho₂ : rtr₂[Component.val Component.Valued.out][i✝] = some o₂✝
⊢ o₁✝ = o₂✝
Tactic:
case out => injection (rf₁.outputs  ▸ ho₁) ▸ rf₂.outputs  ▸ ho₂
State after:
no goals

State before:
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
i✝ : Component.idType (Component.val Component.Valued.stv)
o₁✝ o₂✝ : Component.type α (Component.val Component.Valued.stv)
ho₁ : rtr₁[Component.val Component.Valued.stv][i✝] = some o₁✝
ho₂ : rtr₂[Component.val Component.Valued.stv][i✝] = some o₂✝
⊢ o₁✝ = o₂✝
Tactic:
injection (rf₁.eq_state ▸ ho₁) ▸ rf₂.eq_state ▸ ho₂
State after:
no goals

State before:
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
i✝ : Component.idType (Component.val Component.Valued.act)
o₁✝ o₂✝ : Component.type α (Component.val Component.Valued.act)
ho₁ : rtr₁[Component.val Component.Valued.act][i✝] = some o₁✝
ho₂ : rtr₂[Component.val Component.Valued.act][i✝] = some o₂✝
⊢ o₁✝ = o₂✝
Tactic:
injection (rf₁.acts     ▸ ho₁) ▸ rf₂.acts     ▸ ho₂
State after:
no goals

State before:
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
i✝ : Component.idType (Component.val Component.Valued.inp)
o₁✝ o₂✝ : Component.type α (Component.val Component.Valued.inp)
ho₁ : rtr₁[Component.val Component.Valued.inp][i✝] = some o₁✝
ho₂ : rtr₂[Component.val Component.Valued.inp][i✝] = some o₂✝
⊢ o₁✝ = o₂✝
Tactic:
injection (rf₁.inputs   ▸ ho₁) ▸ rf₂.inputs   ▸ ho₂
State after:
no goals

State before:
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
i✝ : Component.idType (Component.val Component.Valued.out)
o₁✝ o₂✝ : Component.type α (Component.val Component.Valued.out)
ho₁ : rtr₁[Component.val Component.Valued.out][i✝] = some o₁✝
ho₂ : rtr₂[Component.val Component.Valued.out][i✝] = some o₂✝
⊢ o₁✝ = o₂✝
Tactic:
injection (rf₁.outputs  ▸ ho₁) ▸ rf₂.outputs  ▸ ho₂
State after:
no goals