---

Step * 1 1 of Lemma extend_permf_over_comp


1. n : ℕ
2. f : ℕn ⟶ ℕn
3. g : ℕn ⟶ ℕn
4. m : ℕn + 1
⊢ if (m =z n) then m else g (f m) fi 
= if (if (m =z n) then m else f m fi  =z n)
  then if (m =z n) then m else f m fi 
  else g if (m =z n) then m else f m fi 
  fi 
∈ ℕn + 1
BY
{ (BoolCase ⌜(m =z n)⌝⋅ THENA Auto) }

1
1. n : ℕ
2. f : ℕn ⟶ ℕn
3. g : ℕn ⟶ ℕn
4. m : ℕn + 1
5. m = n ∈ ℤ
⊢ m = m ∈ ℕn + 1

2
1. n : ℕ
2. f : ℕn ⟶ ℕn
3. g : ℕn ⟶ ℕn
4. m : ℕn + 1
5. m ≠ n
⊢ (g (f m)) = if (f m =z n) then f m else g (f m) fi  ∈ ℕn + 1

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  f  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n
3.  g  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n
4.  m  :  \mBbbN{}n  +  1
\mvdash{}  if  (m  =\msubz{}  n)  then  m  else  g  (f  m)  fi 
=  if  (if  (m  =\msubz{}  n)  then  m  else  f  m  fi    =\msubz{}  n)
    then  if  (m  =\msubz{}  n)  then  m  else  f  m  fi 
    else  g  if  (m  =\msubz{}  n)  then  m  else  f  m  fi 
    fi 


By

---

Latex:
(BoolCase  \mkleeneopen{}(m  =\msubz{}  n)\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index