Step
*
1
1
1
1
of Lemma
pv11_p1_pmax_desc
1. ldrs_uid : Id ─→ ℤ@i
2. x2 : ℤ
3. x3 : Id
4. x4 : ℤ@i
5. x5 : Id@i
⊢ (¬↑(x4 <z x2 ∨b((x4 =z x2) ∧b ldrs_uid x5 ≤z ldrs_uid x3)))
⇒ (↑(x2 <z x4 ∨b((x2 =z x4) ∧b ldrs_uid x3 <z ldrs_uid x5)))
BY
{ (AutoBoolCase ⌈x4 <z x2⌉⋅
THEN AutoBoolCase ⌈x2 <z x4⌉⋅
THEN AutoBoolCase ⌈(x4 =z x2)⌉⋅
THEN AutoBoolCase ⌈(x2 =z x4)⌉⋅
THEN AutoBoolCase ⌈ldrs_uid x5 ≤z ldrs_uid x3⌉⋅) }
Latex:
Latex:
1. ldrs$_{uid}$ : Id {}\mrightarrow{} \mBbbZ{}@i
2. x2 : \mBbbZ{}
3. x3 : Id
4. x4 : \mBbbZ{}@i
5. x5 : Id@i
\mvdash{} (\mneg{}\muparrow{}(x4 <z x2 \mvee{}\msubb{}((x4 =\msubz{} x2) \mwedge{}\msubb{} ldrs$_{uid}$ x5 \mleq{}z ldrs$_{uid}\mbackslash{}f\000Cf24 x3)))
{}\mRightarrow{} (\muparrow{}(x2 <z x4 \mvee{}\msubb{}((x2 =\msubz{} x4) \mwedge{}\msubb{} ldrs$_{uid}$ x3 <z ldrs$_{uid}\mbackslash{}f\000Cf24 x5)))
By
Latex:
(AutoBoolCase \mkleeneopen{}x4 <z x2\mkleeneclose{}\mcdot{}
THEN AutoBoolCase \mkleeneopen{}x2 <z x4\mkleeneclose{}\mcdot{}
THEN AutoBoolCase \mkleeneopen{}(x4 =\msubz{} x2)\mkleeneclose{}\mcdot{}
THEN AutoBoolCase \mkleeneopen{}(x2 =\msubz{} x4)\mkleeneclose{}\mcdot{}
THEN AutoBoolCase \mkleeneopen{}ldrs$_{uid}$ x5 \mleq{}z ldrs$_{uid}$ x3\mkleeneclose{}\mcdot{})
Home
Index