---

Step * 1 1 2 of Lemma permutation_inversion


1. [A] : Type
2. as : A List
3. bs : A List
4. f : ℕ||as|| ⟶ ℕ||as||
5. Inj(ℕ||as||;ℕ||as||;f)
6. bs = (as o f) ∈ (A List)
7. ||as|| = ||bs|| ∈ ℤ
8. Surj(ℕ||as||;ℕ||as||;f)
⊢ ∃g:ℕ||as|| ⟶ ℕ||as||. ∀x:ℕ||as||. ((f (g x)) = x ∈ ℤ)
BY
{ (Unfold `surject` -1 THEN Skolemize (-1) `g' THEN Auto THEN InstConcl [⌜g⌝]⋅ THEN Auto THEN BackThruSomeHyp) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  as  :  A  List
3.  bs  :  A  List
4.  f  :  \mBbbN{}||as||  {}\mrightarrow{}  \mBbbN{}||as||
5.  Inj(\mBbbN{}||as||;\mBbbN{}||as||;f)
6.  bs  =  (as  o  f)
7.  ||as||  =  ||bs||
8.  Surj(\mBbbN{}||as||;\mBbbN{}||as||;f)
\mvdash{}  \mexists{}g:\mBbbN{}||as||  {}\mrightarrow{}  \mBbbN{}||as||.  \mforall{}x:\mBbbN{}||as||.  ((f  (g  x))  =  x)


By

---

Latex:
(Unfold  `surject`  -1
  THEN  Skolemize  (-1)  `g'
  THEN  Auto
  THEN  InstConcl  [\mkleeneopen{}g\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  BackThruSomeHyp)

---

Home Index