Theorem: endNodeOfChild_to_endNode (Pdl/Soundness.lean)

State before:
X Y : TNode
ltX : LocalTableau X
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
h : ltX = LocalTableau.byLocalRule lrA subTabs
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
⊢ Z ∈ endNodesOf ltX
Tactic:
cases h' : subTabs Y Y_in
State after:
case byLocalRule
X Y : TNode
ltX : LocalTableau X
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
h : ltX = LocalTableau.byLocalRule lrA subTabs
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
B✝ : List TNode
next✝ : (Y : TNode) → Y ∈ B✝ → LocalTableau Y
x✝ : LocalRuleApp Y B✝
h' : subTabs Y Y_in = LocalTableau.byLocalRule x✝ next✝
⊢ Z ∈ endNodesOf ltX

case sim
X Y : TNode
ltX : LocalTableau X
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
h : ltX = LocalTableau.byLocalRule lrA subTabs
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
a✝ : isBasic Y = true
h' : subTabs Y Y_in = LocalTableau.sim a✝
⊢ Z ∈ endNodesOf ltX

State before:
X Y : TNode
ltX : LocalTableau X
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
h : ltX = LocalTableau.byLocalRule lrA subTabs
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
Y_isSimp : isBasic Y = true
h' : subTabs Y Y_in = LocalTableau.sim Y_isSimp
⊢ Z ∈ endNodesOf ltX
Tactic:
subst h
State after:
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
Y_isSimp : isBasic Y = true
h' : subTabs Y Y_in = LocalTableau.sim Y_isSimp
⊢ Z ∈ endNodesOf (LocalTableau.byLocalRule lrA subTabs)

State before:
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
Y_isSimp : isBasic Y = true
h' : subTabs Y Y_in = LocalTableau.sim Y_isSimp
⊢ Z ∈ endNodesOf (LocalTableau.byLocalRule lrA subTabs)
Tactic:
simp
State after:
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
Y_isSimp : isBasic Y = true
h' : subTabs Y Y_in = LocalTableau.sim Y_isSimp
⊢ ∃ l, (∃ a, ∃ (h : a ∈ C), endNodesOf (subTabs a ⋯) = l) ∧ Z ∈ l

State before:
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
Y_isSimp : isBasic Y = true
h' : subTabs Y Y_in = LocalTableau.sim Y_isSimp
⊢ ∃ l, (∃ a, ∃ (h : a ∈ C), endNodesOf (subTabs a ⋯) = l) ∧ Z ∈ l
Tactic:
use endNodesOf (subTabs Y Y_in)
State after:
case h
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
Y_isSimp : isBasic Y = true
h' : subTabs Y Y_in = LocalTableau.sim Y_isSimp
⊢ (∃ a, ∃ (h : a ∈ C), endNodesOf (subTabs a ⋯) = endNodesOf (subTabs Y Y_in)) ∧ Z ∈ endNodesOf (subTabs Y Y_in)

State before:
case h
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
Y_isSimp : isBasic Y = true
h' : subTabs Y Y_in = LocalTableau.sim Y_isSimp
⊢ (∃ a, ∃ (h : a ∈ C), endNodesOf (subTabs a ⋯) = endNodesOf (subTabs Y Y_in)) ∧ Z ∈ endNodesOf (subTabs Y Y_in)
Tactic:
constructor
State after:
case h.left
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
Y_isSimp : isBasic Y = true
h' : subTabs Y Y_in = LocalTableau.sim Y_isSimp
⊢ ∃ a, ∃ (h : a ∈ C), endNodesOf (subTabs a ⋯) = endNodesOf (subTabs Y Y_in)

case h.right
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
Y_isSimp : isBasic Y = true
h' : subTabs Y Y_in = LocalTableau.sim Y_isSimp
⊢ Z ∈ endNodesOf (subTabs Y Y_in)

State before:
case h.left
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
Y_isSimp : isBasic Y = true
h' : subTabs Y Y_in = LocalTableau.sim Y_isSimp
⊢ ∃ a, ∃ (h : a ∈ C), endNodesOf (subTabs a ⋯) = endNodesOf (subTabs Y Y_in)
Tactic:
use Y, Y_in
State after:
no goals

State before:
case h.right
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
Y_isSimp : isBasic Y = true
h' : subTabs Y Y_in = LocalTableau.sim Y_isSimp
⊢ Z ∈ endNodesOf (subTabs Y Y_in)
Tactic:
exact Z_in
State after:
no goals

State before:
X Y : TNode
ltX : LocalTableau X
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
h : ltX = LocalTableau.byLocalRule lrA subTabs
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
C' : List TNode
subTabs' : (Y : TNode) → Y ∈ C' → LocalTableau Y
lrA' : LocalRuleApp Y C'
h' : subTabs Y Y_in = LocalTableau.byLocalRule lrA' subTabs'
⊢ Z ∈ endNodesOf ltX
Tactic:
subst h
State after:
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
C' : List TNode
subTabs' : (Y : TNode) → Y ∈ C' → LocalTableau Y
lrA' : LocalRuleApp Y C'
h' : subTabs Y Y_in = LocalTableau.byLocalRule lrA' subTabs'
⊢ Z ∈ endNodesOf (LocalTableau.byLocalRule lrA subTabs)

State before:
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
C' : List TNode
subTabs' : (Y : TNode) → Y ∈ C' → LocalTableau Y
lrA' : LocalRuleApp Y C'
h' : subTabs Y Y_in = LocalTableau.byLocalRule lrA' subTabs'
⊢ Z ∈ endNodesOf (LocalTableau.byLocalRule lrA subTabs)
Tactic:
rw [h'] at Z_in
State after:
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
C' : List TNode
subTabs' : (Y : TNode) → Y ∈ C' → LocalTableau Y
lrA' : LocalRuleApp Y C'
Z_in : Z ∈ endNodesOf (LocalTableau.byLocalRule lrA' subTabs')
h' : subTabs Y Y_in = LocalTableau.byLocalRule lrA' subTabs'
⊢ Z ∈ endNodesOf (LocalTableau.byLocalRule lrA subTabs)

State before:
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
C' : List TNode
subTabs' : (Y : TNode) → Y ∈ C' → LocalTableau Y
lrA' : LocalRuleApp Y C'
Z_in : Z ∈ endNodesOf (LocalTableau.byLocalRule lrA' subTabs')
h' : subTabs Y Y_in = LocalTableau.byLocalRule lrA' subTabs'
⊢ Z ∈ endNodesOf (LocalTableau.byLocalRule lrA subTabs)
Tactic:
simp
State after:
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
C' : List TNode
subTabs' : (Y : TNode) → Y ∈ C' → LocalTableau Y
lrA' : LocalRuleApp Y C'
Z_in : Z ∈ endNodesOf (LocalTableau.byLocalRule lrA' subTabs')
h' : subTabs Y Y_in = LocalTableau.byLocalRule lrA' subTabs'
⊢ ∃ l, (∃ a, ∃ (h : a ∈ C), endNodesOf (subTabs a ⋯) = l) ∧ Z ∈ l

State before:
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
C' : List TNode
subTabs' : (Y : TNode) → Y ∈ C' → LocalTableau Y
lrA' : LocalRuleApp Y C'
Z_in : Z ∈ endNodesOf (LocalTableau.byLocalRule lrA' subTabs')
h' : subTabs Y Y_in = LocalTableau.byLocalRule lrA' subTabs'
⊢ ∃ l, (∃ a, ∃ (h : a ∈ C), endNodesOf (subTabs a ⋯) = l) ∧ Z ∈ l
Tactic:
use endNodesOf (subTabs Y Y_in)
State after:
case h
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
C' : List TNode
subTabs' : (Y : TNode) → Y ∈ C' → LocalTableau Y
lrA' : LocalRuleApp Y C'
Z_in : Z ∈ endNodesOf (LocalTableau.byLocalRule lrA' subTabs')
h' : subTabs Y Y_in = LocalTableau.byLocalRule lrA' subTabs'
⊢ (∃ a, ∃ (h : a ∈ C), endNodesOf (subTabs a ⋯) = endNodesOf (subTabs Y Y_in)) ∧ Z ∈ endNodesOf (subTabs Y Y_in)

State before:
case h
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
C' : List TNode
subTabs' : (Y : TNode) → Y ∈ C' → LocalTableau Y
lrA' : LocalRuleApp Y C'
Z_in : Z ∈ endNodesOf (LocalTableau.byLocalRule lrA' subTabs')
h' : subTabs Y Y_in = LocalTableau.byLocalRule lrA' subTabs'
⊢ (∃ a, ∃ (h : a ∈ C), endNodesOf (subTabs a ⋯) = endNodesOf (subTabs Y Y_in)) ∧ Z ∈ endNodesOf (subTabs Y Y_in)
Tactic:
constructor
State after:
case h.left
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
C' : List TNode
subTabs' : (Y : TNode) → Y ∈ C' → LocalTableau Y
lrA' : LocalRuleApp Y C'
Z_in : Z ∈ endNodesOf (LocalTableau.byLocalRule lrA' subTabs')
h' : subTabs Y Y_in = LocalTableau.byLocalRule lrA' subTabs'
⊢ ∃ a, ∃ (h : a ∈ C), endNodesOf (subTabs a ⋯) = endNodesOf (subTabs Y Y_in)

case h.right
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
C' : List TNode
subTabs' : (Y : TNode) → Y ∈ C' → LocalTableau Y
lrA' : LocalRuleApp Y C'
Z_in : Z ∈ endNodesOf (LocalTableau.byLocalRule lrA' subTabs')
h' : subTabs Y Y_in = LocalTableau.byLocalRule lrA' subTabs'
⊢ Z ∈ endNodesOf (subTabs Y Y_in)

State before:
case h.left
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
C' : List TNode
subTabs' : (Y : TNode) → Y ∈ C' → LocalTableau Y
lrA' : LocalRuleApp Y C'
Z_in : Z ∈ endNodesOf (LocalTableau.byLocalRule lrA' subTabs')
h' : subTabs Y Y_in = LocalTableau.byLocalRule lrA' subTabs'
⊢ ∃ a, ∃ (h : a ∈ C), endNodesOf (subTabs a ⋯) = endNodesOf (subTabs Y Y_in)
Tactic:
use Y, Y_in
State after:
no goals

State before:
case h.right
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
C' : List TNode
subTabs' : (Y : TNode) → Y ∈ C' → LocalTableau Y
lrA' : LocalRuleApp Y C'
Z_in : Z ∈ endNodesOf (LocalTableau.byLocalRule lrA' subTabs')
h' : subTabs Y Y_in = LocalTableau.byLocalRule lrA' subTabs'
⊢ Z ∈ endNodesOf (subTabs Y Y_in)
Tactic:
rw [h']
State after:
case h.right
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
C' : List TNode
subTabs' : (Y : TNode) → Y ∈ C' → LocalTableau Y
lrA' : LocalRuleApp Y C'
Z_in : Z ∈ endNodesOf (LocalTableau.byLocalRule lrA' subTabs')
h' : subTabs Y Y_in = LocalTableau.byLocalRule lrA' subTabs'
⊢ Z ∈ endNodesOf (LocalTableau.byLocalRule lrA' subTabs')

State before:
case h.right
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
C' : List TNode
subTabs' : (Y : TNode) → Y ∈ C' → LocalTableau Y
lrA' : LocalRuleApp Y C'
Z_in : Z ∈ endNodesOf (LocalTableau.byLocalRule lrA' subTabs')
h' : subTabs Y Y_in = LocalTableau.byLocalRule lrA' subTabs'
⊢ Z ∈ endNodesOf (LocalTableau.byLocalRule lrA' subTabs')
Tactic:
exact Z_in
State after:
no goals