---

Step * 2 of Lemma rleq2_functionality


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)
BY
{ ((InstHyp [⌜x2⌝;⌜y2⌝;⌜x1⌝;⌜y1⌝] 1⋅ THEN Auto) THEN RelRST THEN Auto) }

---

Latex:

---

Latex:

1.  \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))
2.  x1  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}@i
3.  y1  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}@i
4.  x2  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}@i
5.  y2  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}@i
6.  bdd-diff(x1;x2)@i
7.  bdd-diff(y1;y2)@i
8.  rleq2(x2;y2)@i
\mvdash{}  rleq2(x1;y1)


By

---

Latex:
((InstHyp  [\mkleeneopen{}x2\mkleeneclose{};\mkleeneopen{}y2\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}y1\mkleeneclose{}]  1\mcdot{}  THEN  Auto)  THEN  RelRST  THEN  Auto)

---

Home Index