---

Step * 1 1 1 1 1 of Lemma tl_perm_wf


1. n : ℕ+
2. p : Perm(ℕn)
3. x : ℕ+n
4. x ≠ 0
⊢ p.f if (x =z p.b 0) then 0 else x fi  ∈ ℕ+n
BY
{ (BoolCase ⌜(x =z p.b 0)⌝⋅ THENA Auto) }

1
1. n : ℕ+
2. p : Perm(ℕn)
3. x : ℕ+n
4. x ≠ 0
5. x = (p.b 0) ∈ ℤ
⊢ p.f 0 ∈ ℕ+n

2
1. n : ℕ+
2. p : Perm(ℕn)
3. x : ℕ+n
4. x ≠ p.b 0
5. x ≠ 0
⊢ p.f x ∈ ℕ+n

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  p  :  Perm(\mBbbN{}n)
3.  x  :  \mBbbN{}\msupplus{}n
4.  x  \mneq{}  0
\mvdash{}  p.f  if  (x  =\msubz{}  p.b  0)  then  0  else  x  fi    \mmember{}  \mBbbN{}\msupplus{}n


By

---

Latex:
(BoolCase  \mkleeneopen{}(x  =\msubz{}  p.b  0)\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index