---

Step * 1 of Lemma cs-ref-map-step


1. [V] : Type
2. {∃v1,v2:V. (¬(v1 = v2 ∈ V))}@i
3. A : Id List@i
4. W : {a:Id| (a ∈ A)}  List List@i
5. ||W|| ≥ 1 
6. f : ConsensusState ─→ (consensus-state3(V) List)@i
7. cs-ref-map-constraints(V;A;W;f)@i
8. x : ConsensusState@i
9. \\%5 : (λa.<-1, ⊗>) ((λx,y. CR[x,y])^*) x@i
10. y : ConsensusState@i
11. \\%7 : (λa.<-1, ⊗>) ((λx,y. CR[x,y])^*) y@i
12. CR[x,y]@i
⊢ ||f x|| ≤ ||f y||
BY
{ ((SupposeNot
    THEN (Assert ∃a:{a:Id| (a ∈ A)} . (||f y|| ≤ Inning(x;a)) BY
                (Unfold `cs-ref-map-constraints` 7
                 THEN (InstHyp [⌈x⌉;⌈||f y||⌉] 7⋅ THENA Auto)
                 THEN D -1
                 THEN D -2
                 THEN D -3
                 THEN Auto))
    )
   THEN D -1
   THEN (Assert ⌈Inning(x;a) ≤ Inning(y;a)⌉⋅
         THENL [((InstLemma `consensus-ts4-inning-rel` [⌈V⌉;⌈A⌉;⌈W⌉;⌈a⌉]⋅ THENA Auto)
                 THEN UnfoldTopAb (-1)
                 THEN (BHyp -1  THENM (BLemma `rel_rel_star` THEN Auto))
                 THEN RepUR ``ts-rel ts-type consensus-ts4`` 0
                 THEN Auto)
               ; (Unfold `cs-ref-map-constraints` 7
                  THEN (InstHyp [⌈y⌉;⌈||f y||⌉] 7⋅ THENA Auto)
                  THEN D -1
                  THEN RepeatFor 2 (D -2)
                  THEN Auto
                  THEN InstConcl [⌈a⌉]⋅
                  THEN Auto)]
   )) }

---

Latex:



1.  [V]  :  Type
2.  \{\mexists{}v1,v2:V.  (\mneg{}(v1  =  v2))\}@i
3.  A  :  Id  List@i
4.  W  :  \{a:Id|  (a  \mmember{}  A)\}    List  List@i
5.  ||W||  \mgeq{}  1 
6.  f  :  ConsensusState  {}\mrightarrow{}  (consensus-state3(V)  List)@i
7.  cs-ref-map-constraints(V;A;W;f)@i
8.  x  :  ConsensusState@i
9.  \mbackslash{}\mbackslash{}\%5  :  (\mlambda{}a.<-1,  \motimes{}>)  rel\_star(ConsensusState;  \mlambda{}x,y.  CR[x,y])  x@i
10.  y  :  ConsensusState@i
11.  \mbackslash{}\mbackslash{}\%7  :  (\mlambda{}a.<-1,  \motimes{}>)  rel\_star(ConsensusState;  \mlambda{}x,y.  CR[x,y])  y@i
12.  CR[x,y]@i
\mvdash{}  ||f  x||  \mleq{}  ||f  y||


By

((SupposeNot
    THEN  (Assert  \mexists{}a:\{a:Id|  (a  \mmember{}  A)\}  .  (||f  y||  \mleq{}  Inning(x;a))  BY
                            (Unfold  `cs-ref-map-constraints`  7
                              THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}||f  y||\mkleeneclose{}]  7\mcdot{}  THENA  Auto)
                              THEN  D  -1
                              THEN  D  -2
                              THEN  D  -3
                              THEN  Auto))
    )
  THEN  D  -1
  THEN  (Assert  \mkleeneopen{}Inning(x;a)  \mleq{}  Inning(y;a)\mkleeneclose{}\mcdot{}
              THENL  [((InstLemma  `consensus-ts4-inning-rel`  [\mkleeneopen{}V\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}W\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)
                              THEN  UnfoldTopAb  (-1)
                              THEN  (BHyp  -1    THENM  (BLemma  `rel\_rel\_star`  THEN  Auto))
                              THEN  RepUR  ``ts-rel  ts-type  consensus-ts4``  0
                              THEN  Auto)
                          ;  (Unfold  `cs-ref-map-constraints`  7
                                THEN  (InstHyp  [\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}||f  y||\mkleeneclose{}]  7\mcdot{}  THENA  Auto)
                                THEN  D  -1
                                THEN  RepeatFor  2  (D  -2)
                                THEN  Auto
                                THEN  InstConcl  [\mkleeneopen{}a\mkleeneclose{}]\mcdot{}
                                THEN  Auto)]
  ))

---

Home Index