---

Step * of Lemma rleq2_functionality

∀x1,y1,x2,y2:ℕ+ ⟶ ℤ.  (bdd-diff(x1;x2) ⇒ bdd-diff(y1;y2) ⇒ (rleq2(x1;y1) ⇐⇒ rleq2(x2;y2)))
BY
{ (Assert ⌜∀x1,y1,x2,y2:ℕ+ ⟶ ℤ.  (bdd-diff(x1;x2) ⇒ bdd-diff(y1;y2) ⇒ rleq2(x1;y1) ⇒ rleq2(x2;y2))⌝⋅ THEN Auto) }

1
1. x1 : ℕ+ ⟶ ℤ@i
2. y1 : ℕ+ ⟶ ℤ@i
3. x2 : ℕ+ ⟶ ℤ@i
4. y2 : ℕ+ ⟶ ℤ@i
5. bdd-diff(x1;x2)@i
6. bdd-diff(y1;y2)@i
7. rleq2(x1;y1)@i
⊢ rleq2(x2;y2)

2
1. ∀x1,y1,x2,y2:ℕ+ ⟶ ℤ.  (bdd-diff(x1;x2) ⇒ bdd-diff(y1;y2) ⇒ rleq2(x1;y1) ⇒ rleq2(x2;y2))
2. x1 : ℕ+ ⟶ ℤ@i
3. y1 : ℕ+ ⟶ ℤ@i
4. x2 : ℕ+ ⟶ ℤ@i
5. y2 : ℕ+ ⟶ ℤ@i
6. bdd-diff(x1;x2)@i
7. bdd-diff(y1;y2)@i
8. rleq2(x2;y2)@i
⊢ rleq2(x1;y1)

---

Latex:

---

Latex:
\mforall{}x1,y1,x2,y2:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}.    (bdd-diff(x1;x2)  {}\mRightarrow{}  bdd-diff(y1;y2)  {}\mRightarrow{}  (rleq2(x1;y1)  \mLeftarrow{}{}\mRightarrow{}  rleq2(x2;y2)))


By

---

Latex:
(Assert 
  \mkleeneopen{}\mforall{}x1,y1,x2,y2:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}.    (bdd-diff(x1;x2)  {}\mRightarrow{}  bdd-diff(y1;y2)  {}\mRightarrow{}  rleq2(x1;y1)  {}\mRightarrow{}  rleq2(x2;y2))\mkleeneclose{}\mcdot{}
  THEN  Auto
  )

---

Home Index