Theorem: not_mem_imp_no_direct_succ (FOL/Parsing/DFT.lean)

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
h1 : x ∉ g.nodes_of
⊢ direct_succ_list g x = []
Tactic:
induction g
State after:
case nil
Node : Type
inst✝ : DecidableEq Node
x : Node
h1 : x ∉ Graph.nodes_of []
⊢ direct_succ_list [] x = []

case cons
Node : Type
inst✝ : DecidableEq Node
x : Node
head✝ : Node × List Node
tail✝ : List (Node × List Node)
tail_ih✝ : x ∉ Graph.nodes_of tail✝ → direct_succ_list tail✝ x = []
h1 : x ∉ Graph.nodes_of (head✝ :: tail✝)
⊢ direct_succ_list (head✝ :: tail✝) x = []

State before:
Node : Type
inst✝ : DecidableEq Node
x : Node
h1 : x ∉ Graph.nodes_of []
⊢ direct_succ_list [] x = []
Tactic:
case nil =>
  simp only [direct_succ_list]
State after:
no goals

State before:
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
ih : x ∉ Graph.nodes_of tl → direct_succ_list tl x = []
h1 : x ∉ Graph.nodes_of (hd :: tl)
⊢ direct_succ_list (hd :: tl) x = []
Tactic:
case cons hd tl ih =>
  simp only [Graph.nodes_of] at ih
  simp at ih
  simp only [Graph.nodes_of] at h1
  simp at h1
  simp only [direct_succ_list]
  split_ifs
  case pos c1 =>
    subst c1
    simp at h1
  case neg c1 =>
    tauto
State after:
no goals

State before:
Node : Type
inst✝ : DecidableEq Node
x : Node
h1 : x ∉ Graph.nodes_of []
⊢ direct_succ_list [] x = []
Tactic:
simp only [direct_succ_list]
State after:
no goals

State before:
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
ih : x ∉ Graph.nodes_of tl → direct_succ_list tl x = []
h1 : x ∉ Graph.nodes_of (hd :: tl)
⊢ direct_succ_list (hd :: tl) x = []
Tactic:
simp only [Graph.nodes_of] at ih
State after:
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
ih : x ∉ List.map Prod.fst tl ∪ (List.map Prod.snd tl).join → direct_succ_list tl x = []
h1 : x ∉ Graph.nodes_of (hd :: tl)
⊢ direct_succ_list (hd :: tl) x = []

State before:
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
ih : x ∉ List.map Prod.fst tl ∪ (List.map Prod.snd tl).join → direct_succ_list tl x = []
h1 : x ∉ Graph.nodes_of (hd :: tl)
⊢ direct_succ_list (hd :: tl) x = []
Tactic:
simp at ih
State after:
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
h1 : x ∉ Graph.nodes_of (hd :: tl)
ih :
  (∀ (x_1 : List Node), (x, x_1) ∉ tl) →
    (∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1) → direct_succ_list tl x = []
⊢ direct_succ_list (hd :: tl) x = []

State before:
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
h1 : x ∉ Graph.nodes_of (hd :: tl)
ih :
  (∀ (x_1 : List Node), (x, x_1) ∉ tl) →
    (∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1) → direct_succ_list tl x = []
⊢ direct_succ_list (hd :: tl) x = []
Tactic:
simp only [Graph.nodes_of] at h1
State after:
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
h1 : x ∉ List.map Prod.fst (hd :: tl) ∪ (List.map Prod.snd (hd :: tl)).join
ih :
  (∀ (x_1 : List Node), (x, x_1) ∉ tl) →
    (∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1) → direct_succ_list tl x = []
⊢ direct_succ_list (hd :: tl) x = []

State before:
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
h1 : x ∉ List.map Prod.fst (hd :: tl) ∪ (List.map Prod.snd (hd :: tl)).join
ih :
  (∀ (x_1 : List Node), (x, x_1) ∉ tl) →
    (∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1) → direct_succ_list tl x = []
⊢ direct_succ_list (hd :: tl) x = []
Tactic:
simp at h1
State after:
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
ih :
  (∀ (x_1 : List Node), (x, x_1) ∉ tl) →
    (∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1) → direct_succ_list tl x = []
h1 :
  ¬x = hd.1 ∧
    (∀ (x_1 : List Node), (x, x_1) ∉ tl) ∧ x ∉ hd.2 ∧ ∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1
⊢ direct_succ_list (hd :: tl) x = []

State before:
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
ih :
  (∀ (x_1 : List Node), (x, x_1) ∉ tl) →
    (∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1) → direct_succ_list tl x = []
h1 :
  ¬x = hd.1 ∧
    (∀ (x_1 : List Node), (x, x_1) ∉ tl) ∧ x ∉ hd.2 ∧ ∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1
⊢ direct_succ_list (hd :: tl) x = []
Tactic:
simp only [direct_succ_list]
State after:
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
ih :
  (∀ (x_1 : List Node), (x, x_1) ∉ tl) →
    (∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1) → direct_succ_list tl x = []
h1 :
  ¬x = hd.1 ∧
    (∀ (x_1 : List Node), (x, x_1) ∉ tl) ∧ x ∉ hd.2 ∧ ∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1
⊢ (if hd.1 = x then hd.2 ++ direct_succ_list tl x else direct_succ_list tl x) = []

State before:
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
ih :
  (∀ (x_1 : List Node), (x, x_1) ∉ tl) →
    (∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1) → direct_succ_list tl x = []
h1 :
  ¬x = hd.1 ∧
    (∀ (x_1 : List Node), (x, x_1) ∉ tl) ∧ x ∉ hd.2 ∧ ∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1
⊢ (if hd.1 = x then hd.2 ++ direct_succ_list tl x else direct_succ_list tl x) = []
Tactic:
split_ifs
State after:
case pos
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
ih :
  (∀ (x_1 : List Node), (x, x_1) ∉ tl) →
    (∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1) → direct_succ_list tl x = []
h1 :
  ¬x = hd.1 ∧
    (∀ (x_1 : List Node), (x, x_1) ∉ tl) ∧ x ∉ hd.2 ∧ ∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1
h✝ : hd.1 = x
⊢ hd.2 ++ direct_succ_list tl x = []

case neg
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
ih :
  (∀ (x_1 : List Node), (x, x_1) ∉ tl) →
    (∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1) → direct_succ_list tl x = []
h1 :
  ¬x = hd.1 ∧
    (∀ (x_1 : List Node), (x, x_1) ∉ tl) ∧ x ∉ hd.2 ∧ ∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1
h✝ : ¬hd.1 = x
⊢ direct_succ_list tl x = []

State before:
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
ih :
  (∀ (x_1 : List Node), (x, x_1) ∉ tl) →
    (∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1) → direct_succ_list tl x = []
h1 :
  ¬x = hd.1 ∧
    (∀ (x_1 : List Node), (x, x_1) ∉ tl) ∧ x ∉ hd.2 ∧ ∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1
c1 : hd.1 = x
⊢ hd.2 ++ direct_succ_list tl x = []
Tactic:
case pos c1 =>
  subst c1
  simp at h1
State after:
no goals

State before:
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
ih :
  (∀ (x_1 : List Node), (x, x_1) ∉ tl) →
    (∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1) → direct_succ_list tl x = []
h1 :
  ¬x = hd.1 ∧
    (∀ (x_1 : List Node), (x, x_1) ∉ tl) ∧ x ∉ hd.2 ∧ ∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1
c1 : ¬hd.1 = x
⊢ direct_succ_list tl x = []
Tactic:
case neg c1 =>
  tauto
State after:
no goals

State before:
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
ih :
  (∀ (x_1 : List Node), (x, x_1) ∉ tl) →
    (∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1) → direct_succ_list tl x = []
h1 :
  ¬x = hd.1 ∧
    (∀ (x_1 : List Node), (x, x_1) ∉ tl) ∧ x ∉ hd.2 ∧ ∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1
c1 : hd.1 = x
⊢ hd.2 ++ direct_succ_list tl x = []
Tactic:
subst c1
State after:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih :
  (∀ (x : List Node), (hd.1, x) ∉ tl) →
    (∀ (x : List Node) (x_1 : Node), (x_1, x) ∈ tl → hd.1 ∉ x) → direct_succ_list tl hd.1 = []
h1 :
  ¬hd.1 = hd.1 ∧
    (∀ (x : List Node), (hd.1, x) ∉ tl) ∧ hd.1 ∉ hd.2 ∧ ∀ (x : List Node) (x_1 : Node), (x_1, x) ∈ tl → hd.1 ∉ x
⊢ hd.2 ++ direct_succ_list tl hd.1 = []

State before:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih :
  (∀ (x : List Node), (hd.1, x) ∉ tl) →
    (∀ (x : List Node) (x_1 : Node), (x_1, x) ∈ tl → hd.1 ∉ x) → direct_succ_list tl hd.1 = []
h1 :
  ¬hd.1 = hd.1 ∧
    (∀ (x : List Node), (hd.1, x) ∉ tl) ∧ hd.1 ∉ hd.2 ∧ ∀ (x : List Node) (x_1 : Node), (x_1, x) ∈ tl → hd.1 ∉ x
⊢ hd.2 ++ direct_succ_list tl hd.1 = []
Tactic:
simp at h1
State after:
no goals

State before:
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
ih :
  (∀ (x_1 : List Node), (x, x_1) ∉ tl) →
    (∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1) → direct_succ_list tl x = []
h1 :
  ¬x = hd.1 ∧
    (∀ (x_1 : List Node), (x, x_1) ∉ tl) ∧ x ∉ hd.2 ∧ ∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1
c1 : ¬hd.1 = x
⊢ direct_succ_list tl x = []
Tactic:
tauto
State after:
no goals