---

Step * 1 of Lemma ppcc-test4


1. f : ℤ ⟶ ℤ
2. [Q] : ℤ ⟶ ℤ ⟶ ℙ
3. [P] : ℤ ⟶ ℤ ⟶ ℙ
4. ∀a,b:ℤ.  (Q[f[a];b] ⇐⇒ P[a;f[b]])
5. Trans(ℤ;a,b.P[a;b])
6. z : 𝔹
7. w : 𝔹
8. (↑z) ∧ (¬↑w)
9. a : ℤ
10. b : ℤ
11. c : ℤ
12. d : ℤ
13. e : ℤ
14. x : {z:ℤ| f[(z + 1) - 1] = d ∈ ℤ} 
15. <<c, a>, e> = <<x, a>, e> ∈ (ℤ × ℤ × ℤ)
16. (f[(b + 2) - 2] = if (w ∨bz) ∧b (c =z x) then e + 1 else f[b] fi  ∈ ℤ) c∧ P[a;a + 1]
17. P[(a + a) - a;c]
18. x1 : ℤ × ℤ
19. x1 = <d, a> ∈ (ℤ × ℤ)
20. Q[fst(x1);b]
⊢ P[snd(x1);e + 1]
BY
{ Auto }

---

Latex:

---

Latex:

1.  f  :  \mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}
2.  [Q]  :  \mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}  {}\mrightarrow{}  \mBbbP{}
3.  [P]  :  \mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}  {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}a,b:\mBbbZ{}.    (Q[f[a];b]  \mLeftarrow{}{}\mRightarrow{}  P[a;f[b]])
5.  Trans(\mBbbZ{};a,b.P[a;b])
6.  z  :  \mBbbB{}
7.  w  :  \mBbbB{}
8.  (\muparrow{}z)  \mwedge{}  (\mneg{}\muparrow{}w)
9.  a  :  \mBbbZ{}
10.  b  :  \mBbbZ{}
11.  c  :  \mBbbZ{}
12.  d  :  \mBbbZ{}
13.  e  :  \mBbbZ{}
14.  x  :  \{z:\mBbbZ{}|  f[(z  +  1)  -  1]  =  d\} 
15.  <<c,  a>,  e>  =  <<x,  a>,  e>
16.  (f[(b  +  2)  -  2]  =  if  (w  \mvee{}\msubb{}z)  \mwedge{}\msubb{}  (c  =\msubz{}  x)  then  e  +  1  else  f[b]  fi  )  c\mwedge{}  P[a;a  +  1]
17.  P[(a  +  a)  -  a;c]
18.  x1  :  \mBbbZ{}  \mtimes{}  \mBbbZ{}
19.  x1  =  <d,  a>
20.  Q[fst(x1);b]
\mvdash{}  P[snd(x1);e  +  1]


By

---

Latex:
Auto

---

Home Index