---

Step * 1 1 2 4 of Lemma inj_into_ocmon


1. g : GrpSig
2. h : OCMon
3. Assoc(|h|;*)
4. Ident(|h|;*;e)
5. Comm(|h|;*)
6. UniformlyRefl(|h|;x,y.↑(x ≤b y))
7. UniformlyTrans(|h|;x,y.↑(x ≤b y))
8. UniformlyAntiSym(|h|;x,y.↑(x ≤b y))
9. Connex(|h|;x,y.↑(x ≤b y))
10. Cancel(|h|;|h|;*)
11. ∀[z:|h|]. monot(|h|;x,y.↑(x ≤b y);λw.(z * w))
12. f : |g| ⟶ |h|
13. FunThru2op(|g|;|h|;*;*;f)
14. (f e) = e ∈ |h|
15. Inj(|g|;|h|;f)
16. RelsIso(|g|;|h|;x,y.↑(x =b y);x,y.↑(x =b y);f)
17. RelsIso(|g|;|h|;x,y.↑(x ≤b y);x,y.↑(x ≤b y);f)
18. UniformLinorder(|g|;x,y.↑(x ≤b y))
19. =b = (λx,y. ((x ≤b y) ∧b (y ≤b x))) ∈ (|g| ⟶ |g| ⟶ 𝔹)
20. Cancel(|g|;|g|;*)
21. z : |g|
⊢ monot(|g|;x,y.↑(x ≤b y);λw.(z * w))
BY
{ % should extend chaining lemmas to cope with hyps and concls % 
% also bug here: FLemma couldn't even get some bindings when  
chaining with hyp 16 % 
 
((Using [`B',|h|;`S',λ2x y.↑(x ≤b y) 
      ;`opb',λw.((f z) * w);`f',f] 
 (BLemma `monot_shift`) ) THEN Auto) }

1
1. g : GrpSig
2. h : OCMon
3. Assoc(|h|;*)
4. Ident(|h|;*;e)
5. Comm(|h|;*)
6. UniformlyRefl(|h|;x,y.↑(x ≤b y))
7. UniformlyTrans(|h|;x,y.↑(x ≤b y))
8. UniformlyAntiSym(|h|;x,y.↑(x ≤b y))
9. Connex(|h|;x,y.↑(x ≤b y))
10. Cancel(|h|;|h|;*)
11. ∀[z:|h|]. monot(|h|;x,y.↑(x ≤b y);λw.(z * w))
12. f : |g| ⟶ |h|
13. FunThru2op(|g|;|h|;*;*;f)
14. (f e) = e ∈ |h|
15. Inj(|g|;|h|;f)
16. RelsIso(|g|;|h|;x,y.↑(x =b y);x,y.↑(x =b y);f)
17. RelsIso(|g|;|h|;x,y.↑(x ≤b y);x,y.↑(x ≤b y);f)
18. UniformLinorder(|g|;x,y.↑(x ≤b y))
19. =b = (λx,y. ((x ≤b y) ∧b (y ≤b x))) ∈ (|g| ⟶ |g| ⟶ 𝔹)
20. Cancel(|g|;|g|;*)
21. z : |g|
⊢ fun_thru_1op(|g|;|h|;λw.(z * w);λw.((f z) * w);f)

---

Latex:

---

Latex:

1.  g  :  GrpSig
2.  h  :  OCMon
3.  Assoc(|h|;*)
4.  Ident(|h|;*;e)
5.  Comm(|h|;*)
6.  UniformlyRefl(|h|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))
7.  UniformlyTrans(|h|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))
8.  UniformlyAntiSym(|h|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))
9.  Connex(|h|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))
10.  Cancel(|h|;|h|;*)
11.  \mforall{}[z:|h|].  monot(|h|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y);\mlambda{}w.(z  *  w))
12.  f  :  |g|  {}\mrightarrow{}  |h|
13.  FunThru2op(|g|;|h|;*;*;f)
14.  (f  e)  =  e
15.  Inj(|g|;|h|;f)
16.  RelsIso(|g|;|h|;x,y.\muparrow{}(x  =\msubb{}  y);x,y.\muparrow{}(x  =\msubb{}  y);f)
17.  RelsIso(|g|;|h|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y);x,y.\muparrow{}(x  \mleq{}\msubb{}  y);f)
18.  UniformLinorder(|g|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))
19.  =\msubb{}  =  (\mlambda{}x,y.  ((x  \mleq{}\msubb{}  y)  \mwedge{}\msubb{}  (y  \mleq{}\msubb{}  x)))
20.  Cancel(|g|;|g|;*)
21.  z  :  |g|
\mvdash{}  monot(|g|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y);\mlambda{}w.(z  *  w))


By

---

Latex:
\%  should  extend  chaining  lemmas  to  cope  with  hyps  and  concls  \% 
\%  also  bug  here:  FLemma  couldn't  even  get  some  bindings  when   
chaining  with  hyp  16  \% 
 
((Using  [`B',|h|;`S',\mlambda{}\msubtwo{}x  y.\muparrow{}(x  \mleq{}\msubb{}  y) 
            ;`opb',\mlambda{}w.((f  z)  *  w);`f',f] 
  (BLemma  `monot\_shift`)  )  THEN  Auto)

---

Home Index