Theorem: LoopProgram.ofLen_contains_extendLenOne_image (FormalSystems/Computability/Loop.lean)

State before:
p : LoopProgram
n : ℕ
p' : LoopProgram
h₁ : p ∈ ofLen n
h₂ : p' ∈ extendLenOne p
⊢ p' ∈ ofLen (n + 1)
Tactic:
apply Finset.mem_union_left
State after:
case h
p : LoopProgram
n : ℕ
p' : LoopProgram
h₁ : p ∈ ofLen n
h₂ : p' ∈ extendLenOne p
⊢ p' ∈
    Finset.fold (fun a b => a ∪ b) ∅ extendLenOne
        ((fun y a =>
            Acc.rec
              (fun x₁ h ih =>
                (fun a a_1 =>
                    (match (motive :=
                        (x : ℕ) →
                          ((y : ℕ) →
                              (invImage (fun a => sizeOf a) instWellFoundedRelation).1 y x → Finset LoopProgram) →
                            Finset LoopProgram)
                        a with
                      | 0 => fun x => ∅
                      | Nat.succ n => fun x =>
                        Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (x n ⋯) ∪
                            Finset.fold (fun x x_1 => x ∪ x_1) ∅
                              (fun x_1 =>
                                match x_1 with
                                | { val := l, property := h } =>
                                  let_fun this := ⋯;
                                  Finset.image
                                    (fun x =>
                                      match x with
                                      | (a, b) => concat a b)
                                    (Finset.product (x l ⋯) (x (n - l) ⋯)))
                              (Finset.attach (Finset.range n)) ∪
                          baseProgram (n + 1))
                      a_1)
                  x₁ ih)
              ⋯)
          (Nat.add n 0) ⋯) ∪
      Finset.fold (fun x x_1 => x ∪ x_1) ∅
        (fun x =>
          match x with
          | { val := l, property := h } =>
            let_fun this := ⋯;
            Finset.image
              (fun x =>
                match x with
                | (a, b) => concat a b)
              (Finset.product
                ((fun y a =>
                    Acc.rec
                      (fun x₁ h ih =>
                        (fun a a_1 =>
                            (match (motive :=
                                (x : ℕ) →
                                  ((y : ℕ) →
                                      (invImage (fun a => sizeOf a) instWellFoundedRelation).1 y x →
                                        Finset LoopProgram) →
                                    Finset LoopProgram)
                                a with
                              | 0 => fun x => ∅
                              | Nat.succ n => fun x =>
                                Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (x n ⋯) ∪
                                    Finset.fold (fun x x_1 => x ∪ x_1) ∅
                                      (fun x_1 =>
                                        match x_1 with
                                        | { val := l, property := h } =>
                                          let_fun this := ⋯;
                                          Finset.image
                                            (fun x =>
                                              match x with
                                              | (a, b) => concat a b)
                                            (Finset.product (x l ⋯) (x (n - l) ⋯)))
                                      (Finset.attach (Finset.range n)) ∪
                                  baseProgram (n + 1))
                              a_1)
                          x₁ ih)
                      ⋯)
                  l ⋯)
                ((fun y a =>
                    Acc.rec
                      (fun x₁ h ih =>
                        (fun a a_1 =>
                            (match (motive :=
                                (x : ℕ) →
                                  ((y : ℕ) →
                                      (invImage (fun a => sizeOf a) instWellFoundedRelation).1 y x →
                                        Finset LoopProgram) →
                                    Finset LoopProgram)
                                a with
                              | 0 => fun x => ∅
                              | Nat.succ n => fun x =>
                                Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (x n ⋯) ∪
                                    Finset.fold (fun x x_1 => x ∪ x_1) ∅
                                      (fun x_1 =>
                                        match x_1 with
                                        | { val := l, property := h } =>
                                          let_fun this := ⋯;
                                          Finset.image
                                            (fun x =>
                                              match x with
                                              | (a, b) => concat a b)
                                            (Finset.product (x l ⋯) (x (n - l) ⋯)))
                                      (Finset.attach (Finset.range n)) ∪
                                  baseProgram (n + 1))
                              a_1)
                          x₁ ih)
                      ⋯)
                  (Nat.add n 0 - l) ⋯)))
        (Finset.attach (Finset.range (Nat.add n 0)))

State before:
case h
p : LoopProgram
n : ℕ
p' : LoopProgram
h₁ : p ∈ ofLen n
h₂ : p' ∈ extendLenOne p
⊢ p' ∈
    Finset.fold (fun a b => a ∪ b) ∅ extendLenOne
        ((fun y a =>
            Acc.rec
              (fun x₁ h ih =>
                (fun a a_1 =>
                    (match (motive :=
                        (x : ℕ) →
                          ((y : ℕ) →
                              (invImage (fun a => sizeOf a) instWellFoundedRelation).1 y x → Finset LoopProgram) →
                            Finset LoopProgram)
                        a with
                      | 0 => fun x => ∅
                      | Nat.succ n => fun x =>
                        Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (x n ⋯) ∪
                            Finset.fold (fun x x_1 => x ∪ x_1) ∅
                              (fun x_1 =>
                                match x_1 with
                                | { val := l, property := h } =>
                                  let_fun this := ⋯;
                                  Finset.image
                                    (fun x =>
                                      match x with
                                      | (a, b) => concat a b)
                                    (Finset.product (x l ⋯) (x (n - l) ⋯)))
                              (Finset.attach (Finset.range n)) ∪
                          baseProgram (n + 1))
                      a_1)
                  x₁ ih)
              ⋯)
          (Nat.add n 0) ⋯) ∪
      Finset.fold (fun x x_1 => x ∪ x_1) ∅
        (fun x =>
          match x with
          | { val := l, property := h } =>
            let_fun this := ⋯;
            Finset.image
              (fun x =>
                match x with
                | (a, b) => concat a b)
              (Finset.product
                ((fun y a =>
                    Acc.rec
                      (fun x₁ h ih =>
                        (fun a a_1 =>
                            (match (motive :=
                                (x : ℕ) →
                                  ((y : ℕ) →
                                      (invImage (fun a => sizeOf a) instWellFoundedRelation).1 y x →
                                        Finset LoopProgram) →
                                    Finset LoopProgram)
                                a with
                              | 0 => fun x => ∅
                              | Nat.succ n => fun x =>
                                Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (x n ⋯) ∪
                                    Finset.fold (fun x x_1 => x ∪ x_1) ∅
                                      (fun x_1 =>
                                        match x_1 with
                                        | { val := l, property := h } =>
                                          let_fun this := ⋯;
                                          Finset.image
                                            (fun x =>
                                              match x with
                                              | (a, b) => concat a b)
                                            (Finset.product (x l ⋯) (x (n - l) ⋯)))
                                      (Finset.attach (Finset.range n)) ∪
                                  baseProgram (n + 1))
                              a_1)
                          x₁ ih)
                      ⋯)
                  l ⋯)
                ((fun y a =>
                    Acc.rec
                      (fun x₁ h ih =>
                        (fun a a_1 =>
                            (match (motive :=
                                (x : ℕ) →
                                  ((y : ℕ) →
                                      (invImage (fun a => sizeOf a) instWellFoundedRelation).1 y x →
                                        Finset LoopProgram) →
                                    Finset LoopProgram)
                                a with
                              | 0 => fun x => ∅
                              | Nat.succ n => fun x =>
                                Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (x n ⋯) ∪
                                    Finset.fold (fun x x_1 => x ∪ x_1) ∅
                                      (fun x_1 =>
                                        match x_1 with
                                        | { val := l, property := h } =>
                                          let_fun this := ⋯;
                                          Finset.image
                                            (fun x =>
                                              match x with
                                              | (a, b) => concat a b)
                                            (Finset.product (x l ⋯) (x (n - l) ⋯)))
                                      (Finset.attach (Finset.range n)) ∪
                                  baseProgram (n + 1))
                              a_1)
                          x₁ ih)
                      ⋯)
                  (Nat.add n 0 - l) ⋯)))
        (Finset.attach (Finset.range (Nat.add n 0)))
Tactic:
apply Finset.mem_union_left
State after:
case h.h
p : LoopProgram
n : ℕ
p' : LoopProgram
h₁ : p ∈ ofLen n
h₂ : p' ∈ extendLenOne p
⊢ p' ∈
    Finset.fold (fun a b => a ∪ b) ∅ extendLenOne
      ((fun y a =>
          Acc.rec
            (fun x₁ h ih =>
              (fun a a_1 =>
                  (match (motive :=
                      (x : ℕ) →
                        ((y : ℕ) → (invImage (fun a => sizeOf a) instWellFoundedRelation).1 y x → Finset LoopProgram) →
                          Finset LoopProgram)
                      a with
                    | 0 => fun x => ∅
                    | Nat.succ n => fun x =>
                      Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (x n ⋯) ∪
                          Finset.fold (fun x x_1 => x ∪ x_1) ∅
                            (fun x_1 =>
                              match x_1 with
                              | { val := l, property := h } =>
                                let_fun this := ⋯;
                                Finset.image
                                  (fun x =>
                                    match x with
                                    | (a, b) => concat a b)
                                  (Finset.product (x l ⋯) (x (n - l) ⋯)))
                            (Finset.attach (Finset.range n)) ∪
                        baseProgram (n + 1))
                    a_1)
                x₁ ih)
            ⋯)
        (Nat.add n 0) ⋯)

State before:
case h.h
p : LoopProgram
n : ℕ
p' : LoopProgram
h₁ : p ∈ ofLen n
h₂ : p' ∈ extendLenOne p
⊢ p' ∈
    Finset.fold (fun a b => a ∪ b) ∅ extendLenOne
      ((fun y a =>
          Acc.rec
            (fun x₁ h ih =>
              (fun a a_1 =>
                  (match (motive :=
                      (x : ℕ) →
                        ((y : ℕ) → (invImage (fun a => sizeOf a) instWellFoundedRelation).1 y x → Finset LoopProgram) →
                          Finset LoopProgram)
                      a with
                    | 0 => fun x => ∅
                    | Nat.succ n => fun x =>
                      Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (x n ⋯) ∪
                          Finset.fold (fun x x_1 => x ∪ x_1) ∅
                            (fun x_1 =>
                              match x_1 with
                              | { val := l, property := h } =>
                                let_fun this := ⋯;
                                Finset.image
                                  (fun x =>
                                    match x with
                                    | (a, b) => concat a b)
                                  (Finset.product (x l ⋯) (x (n - l) ⋯)))
                            (Finset.attach (Finset.range n)) ∪
                        baseProgram (n + 1))
                    a_1)
                x₁ ih)
            ⋯)
        (Nat.add n 0) ⋯)
Tactic:
apply Finset.mem_fold_union_iff.mpr
State after:
case h.h
p : LoopProgram
n : ℕ
p' : LoopProgram
h₁ : p ∈ ofLen n
h₂ : p' ∈ extendLenOne p
⊢ ∃
    x ∈
      (fun y a =>
          Acc.rec
            (fun x₁ h ih =>
              (fun a a_1 =>
                  (match (motive :=
                      (x : ℕ) →
                        ((y : ℕ) → (invImage (fun a => sizeOf a) instWellFoundedRelation).1 y x → Finset LoopProgram) →
                          Finset LoopProgram)
                      a with
                    | 0 => fun x => ∅
                    | Nat.succ n => fun x =>
                      Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (x n ⋯) ∪
                          Finset.fold (fun x x_1 => x ∪ x_1) ∅
                            (fun x_1 =>
                              match x_1 with
                              | { val := l, property := h } =>
                                let_fun this := ⋯;
                                Finset.image
                                  (fun x =>
                                    match x with
                                    | (a, b) => concat a b)
                                  (Finset.product (x l ⋯) (x (n - l) ⋯)))
                            (Finset.attach (Finset.range n)) ∪
                        baseProgram (n + 1))
                    a_1)
                x₁ ih)
            ⋯)
        (Nat.add n 0) ⋯,
    p' ∈ extendLenOne x

State before:
case h.h
p : LoopProgram
n : ℕ
p' : LoopProgram
h₁ : p ∈ ofLen n
h₂ : p' ∈ extendLenOne p
⊢ ∃
    x ∈
      (fun y a =>
          Acc.rec
            (fun x₁ h ih =>
              (fun a a_1 =>
                  (match (motive :=
                      (x : ℕ) →
                        ((y : ℕ) → (invImage (fun a => sizeOf a) instWellFoundedRelation).1 y x → Finset LoopProgram) →
                          Finset LoopProgram)
                      a with
                    | 0 => fun x => ∅
                    | Nat.succ n => fun x =>
                      Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (x n ⋯) ∪
                          Finset.fold (fun x x_1 => x ∪ x_1) ∅
                            (fun x_1 =>
                              match x_1 with
                              | { val := l, property := h } =>
                                let_fun this := ⋯;
                                Finset.image
                                  (fun x =>
                                    match x with
                                    | (a, b) => concat a b)
                                  (Finset.product (x l ⋯) (x (n - l) ⋯)))
                            (Finset.attach (Finset.range n)) ∪
                        baseProgram (n + 1))
                    a_1)
                x₁ ih)
            ⋯)
        (Nat.add n 0) ⋯,
    p' ∈ extendLenOne x
Tactic:
exists p
State after:
no goals