---

Step * of Lemma ppcc-test4

∀f:ℤ ⟶ ℤ
  ∀[Q,P:ℤ ⟶ ℤ ⟶ ℙ].
    ((∀a,b:ℤ.  (Q[f[a];b] ⇐⇒ P[a;f[b]]))
    ⇒ Trans(ℤ;a,b.P[a;b])
    ⇒ (∀z,w:𝔹.
          ∀a,b,c,d,e:ℤ. ∀x:{z:ℤ| f[(z + 1) - 1] = d ∈ ℤ} .
            ((f[(b + 2) - 2] = if (w ∨bz) ∧b (c =z x) then e + 1 else f[b] fi  ∈ ℤ) c∧ P[a;a + 1])
            ⇒ P[(a + a) - a;c]
            ⇒ (∀x:ℤ × ℤ. Q[fst(x);b] ⇒ P[snd(x);e + 1] supposing x = <d, a> ∈ (ℤ × ℤ)) 
            supposing <<c, a>, e> = <<x, a>, e> ∈ (ℤ × ℤ × ℤ) 
          supposing (↑z) ∧ (¬↑w)))
BY
{ TACTIC:(UnivCD THENA Auto) }

1
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]

---

Latex:

---

Latex:
\mforall{}f:\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}
    \mforall{}[Q,P:\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}  {}\mrightarrow{}  \mBbbP{}].
        ((\mforall{}a,b:\mBbbZ{}.    (Q[f[a];b]  \mLeftarrow{}{}\mRightarrow{}  P[a;f[b]]))
        {}\mRightarrow{}  Trans(\mBbbZ{};a,b.P[a;b])
        {}\mRightarrow{}  (\mforall{}z,w:\mBbbB{}.
                    \mforall{}a,b,c,d,e:\mBbbZ{}.  \mforall{}x:\{z:\mBbbZ{}|  f[(z  +  1)  -  1]  =  d\}  .
                        ((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])
                        {}\mRightarrow{}  P[(a  +  a)  -  a;c]
                        {}\mRightarrow{}  (\mforall{}x:\mBbbZ{}  \mtimes{}  \mBbbZ{}.  Q[fst(x);b]  {}\mRightarrow{}  P[snd(x);e  +  1]  supposing  x  =  <d,  a>) 
                        supposing  <<c,  a>,  e>  =  <<x,  a>,  e> 
                    supposing  (\muparrow{}z)  \mwedge{}  (\mneg{}\muparrow{}w)))


By

---

Latex:
TACTIC:(UnivCD  THENA  Auto)

---

Home Index