1. Куча / Говнокод #29264

    0

    1. 01
    2. 02
    3. 03
    4. 04
    5. 05
    6. 06
    7. 07
    8. 08
    9. 09
    10. 10
    11. 11
    12. 12
    13. 13
    14. 14
    15. 15
    16. 16
    17. 17
    18. 18
    19. 19
    20. 20
    21. 21
    22. 22
    23. 23
    24. 24
    25. 25
    26. 26
    27. 27
    28. 28
    29. 29
    30. 30
    31. 31
    32. 32
    33. 33
    34. 34
    35. 35
    36. 36
    37. 37
    38. 38
    39. 39
    40. 40
    41. 41
    42. 42
    43. 43
    Lemma mfun_equiv_commut f g g1 g2 :
  mfun_equiv g (g2 ∘ g1) ->
  commute f g1 ->
  commute f g2 ->
  commute f g.
Proof.
  intros Hg Hcomm_g1 Hcomm_g2 a z.
  split; intros H; unfold mfun_equiv in Hg.
  - destruct H as [b [Hb Hz]].
    rewrite Hg in Hz.
    destruct Hz as [d [Hd Hz]].
    destruct (Hcomm_g1 a d) as [Hg1f Hfg1]. clear Hfg1.
    destruct Hg1f as [d' [Had' Hcd']]. { sauto. }
    morph_shift g2 d'.
    destruct Had' as [c' Hc'].
    destruct (Hcomm_g2 c' z') as [Hg2f Hfg2].
    destruct Hg2f as [z'' [Hz'' Hz'z'']]. { sauto. }
    destruct Hz'' as [e'' He''].
    exists z''.
    split.
    + exists e''.
      split.
      * rewrite Hg. sauto.
      * easy.
    + now rewrite Hequiv_z_z', Hz'z''.
  - destruct H as [c [Hc Hz]].
    rewrite Hg in Hc.
    destruct Hc as [b [Hb Hc]].
    destruct (Hcomm_g2 b z) as [Hg2f Hfg2]. clear Hg2f.
    destruct Hfg2 as [z' [Hbz' Hzz']]. { sauto. }
    destruct Hbz' as [d [Hdz' Hbd']].
    destruct (Hcomm_g1 a d) as [Hg1f Hfg1]. clear Hg1f.
    destruct Hfg1 as [d' [Had' Hdd']]. { sauto. }
    destruct Had' as [b' [Hab' Hb'd']].
    morph_shift g2 d'.
    exists z''.
    split.
    + exists b'.
      split.
      * easy.
      * rewrite Hg. exists d'. sauto.
    + now rewrite Hzz', Hequiv_z'_z''.
Qed.

    Why are we here, just to suffer?

    Запостил: CHayT, 30 Мая 2026

    Комментарии (2) RSS

    • ava CHayT 4 часа назад # 0

      seo-пост: говно эти ваши комплюктеры. Вот с такой питушнёй приходится иметь дело, просто чтобы доказать, что если разбить инструкции некой абстрактной машины на некий ``микрокод'', то отсутствие гонок и конфликтов между последовательностью микроинструкций гарантирует отсутствие гонок между самими инструкциями с точностью до сетоида.
      Ответить

    • ava guest6 2 часа назад # 0

      Переведи на «PHP».
      Ответить

    Добавить комментарий