Theorem: mord_wf_2 (Pdl/MultisetOrder.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
⊢ ∀ (M : Multiset α), AccM_1 M → AccM_1 (a ::ₘ M)
Tactic:
unfold AccM_1
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
⊢ ∀ (M : Multiset α), Acc MultisetRedLt M → Acc MultisetRedLt (a ::ₘ M)

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
⊢ ∀ (M : Multiset α), Acc MultisetRedLt M → Acc MultisetRedLt (a ::ₘ M)
Tactic:
intros M H0
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M : Multiset α
H0 : Acc MultisetRedLt M
⊢ Acc MultisetRedLt (a ::ₘ M)

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M : Multiset α
H0 : Acc MultisetRedLt M
⊢ Acc MultisetRedLt (a ::ₘ M)
Tactic:
induction H0 with
| intro x wfH wfH2 =>
  apply mord_wf_1
  . simpa
  . intros b x a
    unfold AccM_1
    apply H
    assumption
  . constructor
    simpa
  . simpa
State after:
no goals

State before:
case intro
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ Acc MultisetRedLt (a ::ₘ x)
Tactic:
apply mord_wf_1
State after:
case intro.x
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ Multiset α

case intro.H1
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)

case intro.H2
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ AccM_1 x

case intro.H3
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ ∀ (M : Multiset α), MultisetRedLt M x → AccM_1 (a ::ₘ M)

State before:
case intro.x
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ Multiset α

case intro.H1
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)

case intro.H2
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ AccM_1 x

case intro.H3
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ ∀ (M : Multiset α), MultisetRedLt M x → AccM_1 (a ::ₘ M)
Tactic:
. simpa
State after:
case intro.H1
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)

case intro.H2
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ AccM_1 x

case intro.H3
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ ∀ (M : Multiset α), MultisetRedLt M x → AccM_1 (a ::ₘ M)

State before:
case intro.H1
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)

case intro.H2
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ AccM_1 x

case intro.H3
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ ∀ (M : Multiset α), MultisetRedLt M x → AccM_1 (a ::ₘ M)
Tactic:
. intros b x a
  unfold AccM_1
  apply H
  assumption
State after:
case intro.H2
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ AccM_1 x

case intro.H3
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ ∀ (M : Multiset α), MultisetRedLt M x → AccM_1 (a ::ₘ M)

State before:
case intro.H2
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ AccM_1 x

case intro.H3
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ ∀ (M : Multiset α), MultisetRedLt M x → AccM_1 (a ::ₘ M)
Tactic:
. constructor
  simpa
State after:
case intro.H3
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ ∀ (M : Multiset α), MultisetRedLt M x → AccM_1 (a ::ₘ M)

State before:
case intro.H3
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ ∀ (M : Multiset α), MultisetRedLt M x → AccM_1 (a ::ₘ M)
Tactic:
. simpa
State after:
no goals

State before:
case intro.x
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ Multiset α
Tactic:
simpa
State after:
no goals

State before:
case intro.H1
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
Tactic:
intros b x a
State after:
case intro.H1
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
H : ∀ (b : α) (M : Multiset α), b < a✝ → AccM_1 M → AccM_1 (b ::ₘ M)
M x✝ : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x✝ → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x✝ → Acc MultisetRedLt (a✝ ::ₘ y)
b : α
x : Multiset α
a : b < a✝
⊢ AccM_1 x → AccM_1 (b ::ₘ x)

State before:
case intro.H1
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
H : ∀ (b : α) (M : Multiset α), b < a✝ → AccM_1 M → AccM_1 (b ::ₘ M)
M x✝ : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x✝ → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x✝ → Acc MultisetRedLt (a✝ ::ₘ y)
b : α
x : Multiset α
a : b < a✝
⊢ AccM_1 x → AccM_1 (b ::ₘ x)
Tactic:
unfold AccM_1
State after:
case intro.H1
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
H : ∀ (b : α) (M : Multiset α), b < a✝ → AccM_1 M → AccM_1 (b ::ₘ M)
M x✝ : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x✝ → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x✝ → Acc MultisetRedLt (a✝ ::ₘ y)
b : α
x : Multiset α
a : b < a✝
⊢ Acc MultisetRedLt x → Acc MultisetRedLt (b ::ₘ x)

State before:
case intro.H1
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
H : ∀ (b : α) (M : Multiset α), b < a✝ → AccM_1 M → AccM_1 (b ::ₘ M)
M x✝ : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x✝ → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x✝ → Acc MultisetRedLt (a✝ ::ₘ y)
b : α
x : Multiset α
a : b < a✝
⊢ Acc MultisetRedLt x → Acc MultisetRedLt (b ::ₘ x)
Tactic:
apply H
State after:
case intro.H1.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
H : ∀ (b : α) (M : Multiset α), b < a✝ → AccM_1 M → AccM_1 (b ::ₘ M)
M x✝ : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x✝ → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x✝ → Acc MultisetRedLt (a✝ ::ₘ y)
b : α
x : Multiset α
a : b < a✝
⊢ b < a✝

State before:
case intro.H1.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
H : ∀ (b : α) (M : Multiset α), b < a✝ → AccM_1 M → AccM_1 (b ::ₘ M)
M x✝ : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x✝ → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x✝ → Acc MultisetRedLt (a✝ ::ₘ y)
b : α
x : Multiset α
a : b < a✝
⊢ b < a✝
Tactic:
assumption
State after:
no goals

State before:
case intro.H2
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ AccM_1 x
Tactic:
constructor
State after:
case intro.H2.h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y

State before:
case intro.H2.h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
Tactic:
simpa
State after:
no goals

State before:
case intro.H3
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ ∀ (M : Multiset α), MultisetRedLt M x → AccM_1 (a ::ₘ M)
Tactic:
simpa
State after:
no goals