no goals
n : ℕ
f : Vector ℕ n → ℕ
this : ∀ (f : ℕ → ℕ), Nat.Primrec f → Primrec' fun v => f (Vector.head v)
hf : Primrec f
i : Vector ℕ n
⊢ Nat.pred ((fun m => encode (Option.map f (decode m))) (encode i)) = f i
simp [encodek]
case zero
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun x => 0) (Vector.head v)

case succ
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => Nat.succ (Vector.head v)

case left
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun n => (unpair n).fst) (Vector.head v)

case right
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun n => (unpair n).snd) (Vector.head v)

case pair
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => (fun n => pair (f✝ n) (g✝ n)) (Vector.head v)

case comp
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => (fun n => f✝ (g✝ n)) (Vector.head v)

case prec
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => unpaired (fun z n => Nat.rec (f✝ z) (fun y IH => g✝ (pair z (pair y IH))) n) (Vector.head v)
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
hf : Nat.Primrec f
⊢ Primrec' fun v => f (Vector.head v)
induction hf
case succ
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => Nat.succ (Vector.head v)

case left
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun n => (unpair n).fst) (Vector.head v)

case right
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun n => (unpair n).snd) (Vector.head v)

case pair
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => (fun n => pair (f✝ n) (g✝ n)) (Vector.head v)

case comp
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => (fun n => f✝ (g✝ n)) (Vector.head v)

case prec
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => unpaired (fun z n => Nat.rec (f✝ z) (fun y IH => g✝ (pair z (pair y IH))) n) (Vector.head v)
case zero
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun x => 0) (Vector.head v)

case succ
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => Nat.succ (Vector.head v)

case left
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun n => (unpair n).fst) (Vector.head v)

case right
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun n => (unpair n).snd) (Vector.head v)

case pair
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => (fun n => pair (f✝ n) (g✝ n)) (Vector.head v)

case comp
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => (fun n => f✝ (g✝ n)) (Vector.head v)

case prec
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => unpaired (fun z n => Nat.rec (f✝ z) (fun y IH => g✝ (pair z (pair y IH))) n) (Vector.head v)
case zero => exact const 0
case left
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun n => (unpair n).fst) (Vector.head v)

case right
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun n => (unpair n).snd) (Vector.head v)

case pair
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => (fun n => pair (f✝ n) (g✝ n)) (Vector.head v)

case comp
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => (fun n => f✝ (g✝ n)) (Vector.head v)

case prec
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => unpaired (fun z n => Nat.rec (f✝ z) (fun y IH => g✝ (pair z (pair y IH))) n) (Vector.head v)
case succ
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => Nat.succ (Vector.head v)

case left
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun n => (unpair n).fst) (Vector.head v)

case right
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun n => (unpair n).snd) (Vector.head v)

case pair
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => (fun n => pair (f✝ n) (g✝ n)) (Vector.head v)

case comp
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => (fun n => f✝ (g✝ n)) (Vector.head v)

case prec
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => unpaired (fun z n => Nat.rec (f✝ z) (fun y IH => g✝ (pair z (pair y IH))) n) (Vector.head v)
case succ => exact succ
case right
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun n => (unpair n).snd) (Vector.head v)

case pair
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => (fun n => pair (f✝ n) (g✝ n)) (Vector.head v)

case comp
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => (fun n => f✝ (g✝ n)) (Vector.head v)

case prec
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => unpaired (fun z n => Nat.rec (f✝ z) (fun y IH => g✝ (pair z (pair y IH))) n) (Vector.head v)
case left
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun n => (unpair n).fst) (Vector.head v)

case right
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun n => (unpair n).snd) (Vector.head v)

case pair
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => (fun n => pair (f✝ n) (g✝ n)) (Vector.head v)

case comp
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => (fun n => f✝ (g✝ n)) (Vector.head v)

case prec
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => unpaired (fun z n => Nat.rec (f✝ z) (fun y IH => g✝ (pair z (pair y IH))) n) (Vector.head v)
case left => exact unpair₁ head
case pair
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => (fun n => pair (f✝ n) (g✝ n)) (Vector.head v)

case comp
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => (fun n => f✝ (g✝ n)) (Vector.head v)

case prec
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => unpaired (fun z n => Nat.rec (f✝ z) (fun y IH => g✝ (pair z (pair y IH))) n) (Vector.head v)
case right
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun n => (unpair n).snd) (Vector.head v)

case pair
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => (fun n => pair (f✝ n) (g✝ n)) (Vector.head v)

case comp
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => (fun n => f✝ (g✝ n)) (Vector.head v)

case prec
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => unpaired (fun z n => Nat.rec (f✝ z) (fun y IH => g✝ (pair z (pair y IH))) n) (Vector.head v)
case right => exact unpair₂ head
case comp
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => (fun n => f✝ (g✝ n)) (Vector.head v)

case prec
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => unpaired (fun z n => Nat.rec (f✝ z) (fun y IH => g✝ (pair z (pair y IH))) n) (Vector.head v)
case pair
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => (fun n => pair (f✝ n) (g✝ n)) (Vector.head v)

case comp
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => (fun n => f✝ (g✝ n)) (Vector.head v)

case prec
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => unpaired (fun z n => Nat.rec (f✝ z) (fun y IH => g✝ (pair z (pair y IH))) n) (Vector.head v)
case pair f g _ _ hf hg => exact natPair.comp₂ _ hf hg
case prec
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => unpaired (fun z n => Nat.rec (f✝ z) (fun y IH => g✝ (pair z (pair y IH))) n) (Vector.head v)
case comp
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => (fun n => f✝ (g✝ n)) (Vector.head v)

case prec
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => unpaired (fun z n => Nat.rec (f✝ z) (fun y IH => g✝ (pair z (pair y IH))) n) (Vector.head v)
case comp f g _ _ hf hg => exact hf.comp₁ _ hg
no goals
case prec
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => unpaired (fun z n => Nat.rec (f✝ z) (fun y IH => g✝ (pair z (pair y IH))) n) (Vector.head v)
case prec f g _ _ hf hg =>
  simpa using
    prec' (unpair₂ head) (hf.comp₁ _ (unpair₁ head))
      (hg.comp₁ _ <|
        natPair.comp₂ _ (unpair₁ <| tail <| tail head) (natPair.comp₂ _ head (tail head)))
no goals
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun x => 0) (Vector.head v)
exact const 0
no goals
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => Nat.succ (Vector.head v)
exact succ
no goals
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun n => (unpair n).fst) (Vector.head v)
exact unpair₁ head
no goals
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun n => (unpair n).snd) (Vector.head v)
exact unpair₂ head
no goals
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f✝ f g : ℕ → ℕ
a✝¹ : Nat.Primrec f
a✝ : Nat.Primrec g
hf : Primrec' fun v => f (Vector.head v)
hg : Primrec' fun v => g (Vector.head v)
⊢ Primrec' fun v => (fun n => pair (f n) (g n)) (Vector.head v)
exact natPair.comp₂ _ hf hg
no goals
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f✝ f g : ℕ → ℕ
a✝¹ : Nat.Primrec f
a✝ : Nat.Primrec g
hf : Primrec' fun v => f (Vector.head v)
hg : Primrec' fun v => g (Vector.head v)
⊢ Primrec' fun v => (fun n => f (g n)) (Vector.head v)
exact hf.comp₁ _ hg
no goals
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f✝ f g : ℕ → ℕ
a✝¹ : Nat.Primrec f
a✝ : Nat.Primrec g
hf : Primrec' fun v => f (Vector.head v)
hg : Primrec' fun v => g (Vector.head v)
⊢ Primrec' fun v => unpaired (fun z n => Nat.rec (f z) (fun y IH => g (pair z (pair y IH))) n) (Vector.head v)
simpa using
  prec' (unpair₂ head) (hf.comp₁ _ (unpair₁ head))
    (hg.comp₁ _ <|
      natPair.comp₂ _ (unpair₁ <| tail <| tail head) (natPair.comp₂ _ head (tail head)))