Step
*
1
of Lemma
set_lt_transitivity_2
1. s : QOSet
2. a : |s|
3. b : |s|
4. c : |s|
5. strict_part(x,y.x ≤ y;a;b)
6. b ≤ c
⊢ strict_part(x,y.x ≤ y;a;c)
BY
{ ((InstLemma `utrans_imp_sp_utrans_b` [⌜|s|⌝;⌜λ2x y.x ≤ y⌝]⋅ THENA Auto)
THEN Try ((FHyp (-1) [-2;-3]⋅ THEN Auto))
THEN BLemma `set_leq_trans`
THEN Auto) }
Latex:
Latex:
1. s : QOSet
2. a : |s|
3. b : |s|
4. c : |s|
5. strict\_part(x,y.x \mleq{} y;a;b)
6. b \mleq{} c
\mvdash{} strict\_part(x,y.x \mleq{} y;a;c)
By
Latex:
((InstLemma `utrans\_imp\_sp\_utrans\_b` [\mkleeneopen{}|s|\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x y.x \mleq{} y\mkleeneclose{}]\mcdot{} THENA Auto)
THEN Try ((FHyp (-1) [-2;-3]\mcdot{} THEN Auto))
THEN BLemma `set\_leq\_trans`
THEN Auto)
Home
Index