after applying start

( + . (!.(id.²π₁.²π₁,²π₂)^o,!.(id.²π₂.²π₁,²π₂)^o)^o )* . distl . (id,iota.#.id.²π₁)^o . id . id . id

after applying RemoveIds1

( + . (!.(²π₁.²π₁,²π₂)^o,!.(id.²π₂.²π₁,²π₂)^o)^o )* . distl . (id,iota.#.id.²π₁)^o . id . id . id

after applying RemoveIds1

( + . (!.(²π₁.²π₁,²π₂)^o,!.(²π₂.²π₁,²π₂)^o)^o )* . distl . (id,iota.#.id.²π₁)^o . id . id . id

after applying MapIntoComp

( + )* . ( (!.(²π₁.²π₁,²π₂)^o,!.(²π₂.²π₁,²π₂)^o)^o )* . distl . (id,iota.#.id.²π₁)^o . id . id . id

after applying MapIntoAlltup

( + )* . zip₂ . ((!.(²π₁.²π₁,²π₂)^o)*,(!.(²π₂.²π₁,²π₂)^o)*)^o . distl . (id,iota.#.id.²π₁)^o . id . id . id

after applying MapIntoComp

( + )* . zip₂ . ((!)*.((²π₁.²π₁,²π₂)^o)*,(!.(²π₂.²π₁,²π₂)^o)*)^o . distl . (id,iota.#.id.²π₁)^o . id . id . id

after applying MapIntoAlltup

( + )* . zip₂ . ((!)*.zip₂.((²π₁.²π₁)*,(²π₂)*)^o,(!.(²π₂.²π₁,²π₂)^o)*)^o . distl . (id,iota.#.id.²π₁)^o . id . id . id

after applying MapIntoComp

( + )* . zip₂ . ((!)*.zip₂.((²π₁)*.(²π₁)*,(²π₂)*)^o,(!.(²π₂.²π₁,²π₂)^o)*)^o . distl . (id,iota.#.id.²π₁)^o . id . id . id

after applying MapIntoComp

( + )* . zip₂ . ((!)*.zip₂.((²π₁)*.(²π₁)*,(²π₂)*)^o,(!)*.((²π₂.²π₁,²π₂)^o)*)^o . distl . (id,iota.#.id.²π₁)^o . id . id . id

after applying MapIntoAlltup

( + )* . zip₂ . ((!)*.zip₂.((²π₁)*.(²π₁)*,(²π₂)*)^o,(!)*.zip₂.((²π₂.²π₁)*,(²π₂)*)^o)^o . distl . (id,iota.#.id.²π₁)^o . id . id . id

after applying MapIntoComp

( + )* . zip₂ . ((!)*.zip₂.((²π₁)*.(²π₁)*,(²π₂)*)^o,(!)*.zip₂.((²π₂)*.(²π₁)*,(²π₂)*)^o)^o . distl . (id,iota.#.id.²π₁)^o . id . id . id

after applying LeftAssociate

( + )* . zip₂ . ((!)*.zip₂.((²π₁)*.(²π₁)*,(²π₂)*)^o,(!)*.zip₂.((²π₂)*.(²π₁)*,(²π₂)*)^o)^o . distl . (id,iota.#.id.²π₁)^o . id . id . id

after applying LeftAssociate

( + )* . zip₂ . ((!)*.zip₂.((²π₁)*.(²π₁)*,(²π₂)*)^o,(!)*.zip₂.((²π₂)*.(²π₁)*,(²π₂)*)^o)^o . distl . (id,iota.#.id.²π₁)^o . id . id . id

after applying LeftAssociate

( + )* . zip₂ . ((!)*.zip₂.((²π₁)*.(²π₁)*,(²π₂)*)^o,(!)*.zip₂.((²π₂)*.(²π₁)*,(²π₂)*)^o)^o . distl . (id,iota.#.id.²π₁)^o . id . id . id

after applying CompIntoMap

( + )* . zip₂ . ((!)*.zip₂.((²π₁.²π₁)*,(²π₂)*)^o,(!)*.zip₂.((²π₂)*.(²π₁)*,(²π₂)*)^o)^o . distl . (id,iota.#.id.²π₁)^o . id . id . id

after applying CompIntoMap

( + )* . zip₂ . ((!)*.zip₂.((²π₁.²π₁)*,(²π₂)*)^o,(!)*.zip₂.((²π₂.²π₁)*,(²π₂)*)^o)^o . distl . (id,iota.#.id.²π₁)^o . id . id . id

after applying MapIntoComp

( + )* . zip₂ . ((!)*.zip₂.((²π₁)*.(²π₁)*,(²π₂)*)^o,(!)*.zip₂.((²π₂.²π₁)*,(²π₂)*)^o)^o . distl . (id,iota.#.id.²π₁)^o . id . id . id

after applying MapIntoComp

( + )* . zip₂ . ((!)*.zip₂.((²π₁)*.(²π₁)*,(²π₂)*)^o,(!)*.zip₂.((²π₂)*.(²π₁)*,(²π₂)*)^o)^o . distl . (id,iota.#.id.²π₁)^o . id . id . id

after applying DistlElim

( + )* . zip₂ . ((!)*.zip₂.((²π₁)*.(²π₁)*,(²π₂)*)^o,(!)*.zip₂.((²π₂)*.(²π₁)*,(²π₂)*)^o)^o . zip₂ . (repeat.(²π₁,#.²π₂)^o,²π₂)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying LeftAssociate

( + )* . zip₂ . ((!)*.zip₂.((²π₁)*.(²π₁)*,(²π₂)*)^o,(!)*.zip₂.((²π₂)*.(²π₁)*,(²π₂)*)^o)^o . zip₂ . (repeat.(²π₁,#.²π₂)^o,²π₂)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying CompIntoMap

( + )* . zip₂ . ((!)*.zip₂.((²π₁.²π₁)*,(²π₂)*)^o,(!)*.zip₂.((²π₂)*.(²π₁)*,(²π₂)*)^o)^o . zip₂ . (repeat.(²π₁,#.²π₂)^o,²π₂)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying CompIntoMap

( + )* . zip₂ . ((!)*.zip₂.((²π₁.²π₁)*,(²π₂)*)^o,(!)*.zip₂.((²π₂.²π₁)*,(²π₂)*)^o)^o . zip₂ . (repeat.(²π₁,#.²π₂)^o,²π₂)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying RightAssoc2

( + )* . zip₂ . ((!)*.zip₂.((²π₁.²π₁)*,(²π₂)*)^o,(!)*.zip₂.((²π₂.²π₁)*,(²π₂)*)^o)^o . zip₂ . (repeat.(²π₁,#.²π₂)^o,²π₂)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying CompIntoAlltup1

( + )* . zip₂ . ((!)*.zip₂.((²π₁.²π₁)*,(²π₂)*)^o.zip₂,(!)*.zip₂.((²π₂.²π₁)*,(²π₂)*)^o.zip₂)^o . (repeat.(²π₁,#.²π₂)^o,²π₂)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying RightAssoc2

( + )* . zip₂ . ((!)*.zip₂.((²π₁.²π₁)*,(²π₂)*)^o.zip₂,(!)*.zip₂.((²π₂.²π₁)*,(²π₂)*)^o.zip₂)^o . (repeat.(²π₁,#.²π₂)^o,²π₂)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying CompIntoAlltup1

( + )* . zip₂ . ((!)*.zip₂.((²π₁.²π₁)*.zip₂,(²π₂)*.zip₂)^o,(!)*.zip₂.((²π₂.²π₁)*,(²π₂)*)^o.zip₂)^o . (repeat.(²π₁,#.²π₂)^o,²π₂)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying RightAssoc2

( + )* . zip₂ . ((!)*.zip₂.((²π₁.²π₁)*.zip₂,(²π₂)*.zip₂)^o,(!)*.zip₂.((²π₂.²π₁)*,(²π₂)*)^o.zip₂)^o . (repeat.(²π₁,#.²π₂)^o,²π₂)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying CompIntoAlltup1

( + )* . zip₂ . ((!)*.zip₂.((²π₁.²π₁)*.zip₂,(²π₂)*.zip₂)^o,(!)*.zip₂.((²π₂.²π₁)*.zip₂,(²π₂)*.zip₂)^o)^o . (repeat.(²π₁,#.²π₂)^o,²π₂)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying RightAssoc2

( + )* . zip₂ . ((!)*.zip₂.((²π₁.²π₁)*.zip₂,(²π₂)*.zip₂)^o,(!)*.zip₂.((²π₂.²π₁)*.zip₂,(²π₂)*.zip₂)^o)^o . (repeat.(²π₁,#.²π₂)^o,²π₂)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying CompIntoAlltup1

( + )* . zip₂ . ((!)*.zip₂.((²π₁.²π₁)*.zip₂,(²π₂)*.zip₂)^o.(repeat.(²π₁,#.²π₂)^o,²π₂)^o,(!)*.zip₂.((²π₂.²π₁)*.zip₂,(²π₂)*.zip₂)^o.(repeat.(²π₁,#.²π₂)^o,²π₂)^o)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying RightAssoc2

( + )* . zip₂ . ((!)*.zip₂.((²π₁.²π₁)*.zip₂,(²π₂)*.zip₂)^o.(repeat.(²π₁,#.²π₂)^o,²π₂)^o,(!)*.zip₂.((²π₂.²π₁)*.zip₂,(²π₂)*.zip₂)^o.(repeat.(²π₁,#.²π₂)^o,²π₂)^o)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying CompIntoAlltup1

( + )* . zip₂ . ((!)*.zip₂.((²π₁.²π₁)*.zip₂.(repeat.(²π₁,#.²π₂)^o,²π₂)^o,(²π₂)*.zip₂.(repeat.(²π₁,#.²π₂)^o,²π₂)^o)^o,(!)*.zip₂.((²π₂.²π₁)*.zip₂,(²π₂)*.zip₂)^o.(repeat.(²π₁,#.²π₂)^o,²π₂)^o)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying RightAssoc2

( + )* . zip₂ . ((!)*.zip₂.((²π₁.²π₁)*.zip₂.(repeat.(²π₁,#.²π₂)^o,²π₂)^o,(²π₂)*.zip₂.(repeat.(²π₁,#.²π₂)^o,²π₂)^o)^o,(!)*.zip₂.((²π₂.²π₁)*.zip₂,(²π₂)*.zip₂)^o.(repeat.(²π₁,#.²π₂)^o,²π₂)^o)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying CompIntoAlltup1

( + )* . zip₂ . ((!)*.zip₂.((²π₁.²π₁)*.zip₂.(repeat.(²π₁,#.²π₂)^o,²π₂)^o,(²π₂)*.zip₂.(repeat.(²π₁,#.²π₂)^o,²π₂)^o)^o,(!)*.zip₂.((²π₂.²π₁)*.zip₂.(repeat.(²π₁,#.²π₂)^o,²π₂)^o,(²π₂)*.zip₂.(repeat.(²π₁,#.²π₂)^o,²π₂)^o)^o)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying AddrIntoZip

( + )* . zip₂ . ((!)*.zip₂.((²π₁.²π₁)*.zip₂.(repeat.(²π₁,#.²π₂)^o,²π₂)^o,²π₂.(repeat.(²π₁,#.²π₂)^o,²π₂)^o)^o,(!)*.zip₂.((²π₂.²π₁)*.zip₂.(repeat.(²π₁,#.²π₂)^o,²π₂)^o,(²π₂)*.zip₂.(repeat.(²π₁,#.²π₂)^o,²π₂)^o)^o)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying AddrIntoAlltup

( + )* . zip₂ . ((!)*.zip₂.((²π₁.²π₁)*.zip₂.(repeat.(²π₁,#.²π₂)^o,²π₂)^o,²π₂)^o,(!)*.zip₂.((²π₂.²π₁)*.zip₂.(repeat.(²π₁,#.²π₂)^o,²π₂)^o,(²π₂)*.zip₂.(repeat.(²π₁,#.²π₂)^o,²π₂)^o)^o)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying AddrIntoZip

( + )* . zip₂ . ((!)*.zip₂.((²π₁.²π₁)*.zip₂.(repeat.(²π₁,#.²π₂)^o,²π₂)^o,²π₂)^o,(!)*.zip₂.((²π₂.²π₁)*.zip₂.(repeat.(²π₁,#.²π₂)^o,²π₂)^o,²π₂.(repeat.(²π₁,#.²π₂)^o,²π₂)^o)^o)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying AddrIntoAlltup

( + )* . zip₂ . ((!)*.zip₂.((²π₁.²π₁)*.zip₂.(repeat.(²π₁,#.²π₂)^o,²π₂)^o,²π₂)^o,(!)*.zip₂.((²π₂.²π₁)*.zip₂.(repeat.(²π₁,#.²π₂)^o,²π₂)^o,²π₂)^o)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying MapIntoComp

( + )* . zip₂ . ((!)*.zip₂.((²π₁)*.(²π₁)*.zip₂.(repeat.(²π₁,#.²π₂)^o,²π₂)^o,²π₂)^o,(!)*.zip₂.((²π₂.²π₁)*.zip₂.(repeat.(²π₁,#.²π₂)^o,²π₂)^o,²π₂)^o)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying MapIntoComp

( + )* . zip₂ . ((!)*.zip₂.((²π₁)*.(²π₁)*.zip₂.(repeat.(²π₁,#.²π₂)^o,²π₂)^o,²π₂)^o,(!)*.zip₂.((²π₂)*.(²π₁)*.zip₂.(repeat.(²π₁,#.²π₂)^o,²π₂)^o,²π₂)^o)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying RightAssoc2

( + )* . zip₂ . ((!)*.zip₂.((²π₁)*.(²π₁)*.zip₂.(repeat.(²π₁,#.²π₂)^o,²π₂)^o,²π₂)^o,(!)*.zip₂.((²π₂)*.(²π₁)*.zip₂.(repeat.(²π₁,#.²π₂)^o,²π₂)^o,²π₂)^o)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying AddrIntoZip

( + )* . zip₂ . ((!)*.zip₂.((²π₁)*.²π₁.(repeat.(²π₁,#.²π₂)^o,²π₂)^o,²π₂)^o,(!)*.zip₂.((²π₂)*.(²π₁)*.zip₂.(repeat.(²π₁,#.²π₂)^o,²π₂)^o,²π₂)^o)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying RightAssoc2

( + )* . zip₂ . ((!)*.zip₂.((²π₁)*.²π₁.(repeat.(²π₁,#.²π₂)^o,²π₂)^o,²π₂)^o,(!)*.zip₂.((²π₂)*.(²π₁)*.zip₂.(repeat.(²π₁,#.²π₂)^o,²π₂)^o,²π₂)^o)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying AddrIntoAlltup

( + )* . zip₂ . ((!)*.zip₂.((²π₁)*.repeat.(²π₁,#.²π₂)^o,²π₂)^o,(!)*.zip₂.((²π₂)*.(²π₁)*.zip₂.(repeat.(²π₁,#.²π₂)^o,²π₂)^o,²π₂)^o)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying LeftAssociate

( + )* . zip₂ . ((!)*.zip₂.((²π₁)*.repeat.(²π₁,#.²π₂)^o,²π₂)^o,(!)*.zip₂.((²π₂)*.(²π₁)*.zip₂.(repeat.(²π₁,#.²π₂)^o,²π₂)^o,²π₂)^o)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying RepeatFusion

( + )* . zip₂ . ((!)*.zip₂.(repeat.(²π₁.²π₁,²π₂)^o.(²π₁,#.²π₂)^o,²π₂)^o,(!)*.zip₂.((²π₂)*.(²π₁)*.zip₂.(repeat.(²π₁,#.²π₂)^o,²π₂)^o,²π₂)^o)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying RightAssoc2

( + )* . zip₂ . ((!)*.zip₂.(repeat.(²π₁.²π₁,²π₂)^o.(²π₁,#.²π₂)^o,²π₂)^o,(!)*.zip₂.((²π₂)*.(²π₁)*.zip₂.(repeat.(²π₁,#.²π₂)^o,²π₂)^o,²π₂)^o)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying AddrIntoZip

( + )* . zip₂ . ((!)*.zip₂.(repeat.(²π₁.²π₁,²π₂)^o.(²π₁,#.²π₂)^o,²π₂)^o,(!)*.zip₂.((²π₂)*.²π₁.(repeat.(²π₁,#.²π₂)^o,²π₂)^o,²π₂)^o)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying RightAssoc2

( + )* . zip₂ . ((!)*.zip₂.(repeat.(²π₁.²π₁,²π₂)^o.(²π₁,#.²π₂)^o,²π₂)^o,(!)*.zip₂.((²π₂)*.²π₁.(repeat.(²π₁,#.²π₂)^o,²π₂)^o,²π₂)^o)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying AddrIntoAlltup

( + )* . zip₂ . ((!)*.zip₂.(repeat.(²π₁.²π₁,²π₂)^o.(²π₁,#.²π₂)^o,²π₂)^o,(!)*.zip₂.((²π₂)*.repeat.(²π₁,#.²π₂)^o,²π₂)^o)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying LeftAssociate

( + )* . zip₂ . ((!)*.zip₂.(repeat.(²π₁.²π₁,²π₂)^o.(²π₁,#.²π₂)^o,²π₂)^o,(!)*.zip₂.((²π₂)*.repeat.(²π₁,#.²π₂)^o,²π₂)^o)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying RepeatFusion

( + )* . zip₂ . ((!)*.zip₂.(repeat.(²π₁.²π₁,²π₂)^o.(²π₁,#.²π₂)^o,²π₂)^o,(!)*.zip₂.(repeat.(²π₂.²π₁,²π₂)^o.(²π₁,#.²π₂)^o,²π₂)^o)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying RightAssoc2

( + )* . zip₂ . ((!)*.zip₂.(repeat.(²π₁.²π₁,²π₂)^o.(²π₁,#.²π₂)^o,²π₂)^o,(!)*.zip₂.(repeat.(²π₂.²π₁,²π₂)^o.(²π₁,#.²π₂)^o,²π₂)^o)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying CompIntoAlltup1

( + )* . zip₂ . ((!)*.zip₂.(repeat.(²π₁.²π₁.(²π₁,#.²π₂)^o,²π₂.(²π₁,#.²π₂)^o)^o,²π₂)^o,(!)*.zip₂.(repeat.(²π₂.²π₁,²π₂)^o.(²π₁,#.²π₂)^o,²π₂)^o)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying RightAssoc2

( + )* . zip₂ . ((!)*.zip₂.(repeat.(²π₁.²π₁.(²π₁,#.²π₂)^o,²π₂.(²π₁,#.²π₂)^o)^o,²π₂)^o,(!)*.zip₂.(repeat.(²π₂.²π₁,²π₂)^o.(²π₁,#.²π₂)^o,²π₂)^o)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying CompIntoAlltup1

( + )* . zip₂ . ((!)*.zip₂.(repeat.(²π₁.²π₁.(²π₁,#.²π₂)^o,²π₂.(²π₁,#.²π₂)^o)^o,²π₂)^o,(!)*.zip₂.(repeat.(²π₂.²π₁.(²π₁,#.²π₂)^o,²π₂.(²π₁,#.²π₂)^o)^o,²π₂)^o)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying RightAssoc2

( + )* . zip₂ . ((!)*.zip₂.(repeat.(²π₁.²π₁.(²π₁,#.²π₂)^o,²π₂.(²π₁,#.²π₂)^o)^o,²π₂)^o,(!)*.zip₂.(repeat.(²π₂.²π₁.(²π₁,#.²π₂)^o,²π₂.(²π₁,#.²π₂)^o)^o,²π₂)^o)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying AddrIntoAlltup

( + )* . zip₂ . ((!)*.zip₂.(repeat.(²π₁.²π₁,²π₂.(²π₁,#.²π₂)^o)^o,²π₂)^o,(!)*.zip₂.(repeat.(²π₂.²π₁.(²π₁,#.²π₂)^o,²π₂.(²π₁,#.²π₂)^o)^o,²π₂)^o)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying AddrIntoAlltup

( + )* . zip₂ . ((!)*.zip₂.(repeat.(²π₁.²π₁,#.²π₂)^o,²π₂)^o,(!)*.zip₂.(repeat.(²π₂.²π₁.(²π₁,#.²π₂)^o,²π₂.(²π₁,#.²π₂)^o)^o,²π₂)^o)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying SelectIntro

( + )* . zip₂ . (select.(²π₁.²π₁,²π₂)^o,(!)*.zip₂.(repeat.(²π₂.²π₁.(²π₁,#.²π₂)^o,²π₂.(²π₁,#.²π₂)^o)^o,²π₂)^o)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying RightAssoc2

( + )* . zip₂ . (select.(²π₁.²π₁,²π₂)^o,(!)*.zip₂.(repeat.(²π₂.²π₁.(²π₁,#.²π₂)^o,²π₂.(²π₁,#.²π₂)^o)^o,²π₂)^o)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying AddrIntoAlltup

( + )* . zip₂ . (select.(²π₁.²π₁,²π₂)^o,(!)*.zip₂.(repeat.(²π₂.²π₁,²π₂.(²π₁,#.²π₂)^o)^o,²π₂)^o)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying AddrIntoAlltup

( + )* . zip₂ . (select.(²π₁.²π₁,²π₂)^o,(!)*.zip₂.(repeat.(²π₂.²π₁,#.²π₂)^o,²π₂)^o)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying SelectIntro

( + )* . zip₂ . (select.(²π₁.²π₁,²π₂)^o,select.(²π₂.²π₁,²π₂)^o)^o . (id,iota.#.id.²π₁)^o . id . id . id

after applying RemoveIds1

( + )* . zip₂ . (select.(²π₁.²π₁,²π₂)^o,select.(²π₂.²π₁,²π₂)^o)^o . (id,iota.#.²π₁)^o . id . id . id

after applying LeftAssociate

( + )* . zip₂ . (select.(²π₁.²π₁,²π₂)^o,select.(²π₂.²π₁,²π₂)^o)^o . (id,iota.#.²π₁)^o . id . id . id

after applying RightAssoc2

( + )* . zip₂ . (select.(²π₁.²π₁,²π₂)^o,select.(²π₂.²π₁,²π₂)^o)^o . (id,iota.#.²π₁)^o . id . id . id

after applying CompIntoAlltup1

( + )* . zip₂ . (select.(²π₁.²π₁,²π₂)^o.(id,iota.#.²π₁)^o,select.(²π₂.²π₁,²π₂)^o.(id,iota.#.²π₁)^o)^o . id . id . id

after applying RightAssoc2

( + )* . zip₂ . (select.(²π₁.²π₁,²π₂)^o.(id,iota.#.²π₁)^o,select.(²π₂.²π₁,²π₂)^o.(id,iota.#.²π₁)^o)^o . id . id . id

after applying CompIntoAlltup1

( + )* . zip₂ . (select.(²π₁.²π₁.(id,iota.#.²π₁)^o,²π₂.(id,iota.#.²π₁)^o)^o,select.(²π₂.²π₁,²π₂)^o.(id,iota.#.²π₁)^o)^o . id . id . id

after applying RightAssoc2

( + )* . zip₂ . (select.(²π₁.²π₁.(id,iota.#.²π₁)^o,²π₂.(id,iota.#.²π₁)^o)^o,select.(²π₂.²π₁,²π₂)^o.(id,iota.#.²π₁)^o)^o . id . id . id

after applying CompIntoAlltup1

( + )* . zip₂ . (select.(²π₁.²π₁.(id,iota.#.²π₁)^o,²π₂.(id,iota.#.²π₁)^o)^o,select.(²π₂.²π₁.(id,iota.#.²π₁)^o,²π₂.(id,iota.#.²π₁)^o)^o)^o . id . id . id

after applying RightAssoc2

( + )* . zip₂ . (select.(²π₁.²π₁.(id,iota.#.²π₁)^o,²π₂.(id,iota.#.²π₁)^o)^o,select.(²π₂.²π₁.(id,iota.#.²π₁)^o,²π₂.(id,iota.#.²π₁)^o)^o)^o . id . id . id

after applying AddrIntoAlltup

( + )* . zip₂ . (select.(²π₁.id,²π₂.(id,iota.#.²π₁)^o)^o,select.(²π₂.²π₁.(id,iota.#.²π₁)^o,²π₂.(id,iota.#.²π₁)^o)^o)^o . id . id . id

after applying RemoveIds2

( + )* . zip₂ . (select.(²π₁,²π₂.(id,iota.#.²π₁)^o)^o,select.(²π₂.²π₁.(id,iota.#.²π₁)^o,²π₂.(id,iota.#.²π₁)^o)^o)^o . id . id . id

after applying AddrIntoAlltup

( + )* . zip₂ . (select.(²π₁,iota.#.²π₁)^o,select.(²π₂.²π₁.(id,iota.#.²π₁)^o,²π₂.(id,iota.#.²π₁)^o)^o)^o . id . id . id

after applying SelectElim3

( + )* . zip₂ . (²π₁,select.(²π₂.²π₁.(id,iota.#.²π₁)^o,²π₂.(id,iota.#.²π₁)^o)^o)^o . id . id . id

after applying RightAssoc2

( + )* . zip₂ . (²π₁,select.(²π₂.²π₁.(id,iota.#.²π₁)^o,²π₂.(id,iota.#.²π₁)^o)^o)^o . id . id . id

after applying AddrIntoAlltup

( + )* . zip₂ . (²π₁,select.(²π₂.id,²π₂.(id,iota.#.²π₁)^o)^o)^o . id . id . id

after applying RemoveIds2

( + )* . zip₂ . (²π₁,select.(²π₂,²π₂.(id,iota.#.²π₁)^o)^o)^o . id . id . id

after applying AddrIntoAlltup

( + )* . zip₂ . (²π₁,select.(²π₂,iota.#.²π₁)^o)^o . id . id . id

after applying RemoveIds1

( + )* . zip₂ . (²π₁,select.(²π₂,iota.#.²π₁)^o)^o . id . id

after applying RightAssoc2

( + )* . zip₂ . (²π₁,select.(²π₂,iota.#.²π₁)^o)^o . id . id

after applying CompIntoAlltup1

( + )* . zip₂ . (²π₁.id,select.(²π₂,iota.#.²π₁)^o.id)^o . id

after applying RightAssoc2

( + )* . zip₂ . (²π₁.id,select.(²π₂,iota.#.²π₁)^o.id)^o . id

after applying CompIntoAlltup1

( + )* . zip₂ . (²π₁.id,select.(²π₂.id,iota.#.²π₁.id)^o)^o . id

after applying RemoveIds2

( + )* . zip₂ . (²π₁,select.(²π₂.id,iota.#.²π₁.id)^o)^o . id

after applying RemoveIds2

( + )* . zip₂ . (²π₁,select.(²π₂,iota.#.²π₁.id)^o)^o . id

after applying RightAssoc3

( + )* . zip₂ . (²π₁,select.(²π₂,iota.#.²π₁.id)^o)^o . id

after applying RemoveIds2

( + )* . zip₂ . (²π₁,select.(²π₂,iota.#.²π₁)^o)^o . id

after applying LeftAssociate

( + )* . zip₂ . (²π₁,select.(²π₂,iota.#.²π₁)^o)^o . id

after applying RightAssoc2

( + )* . zip₂ . (²π₁,select.(²π₂,iota.#.²π₁)^o)^o . id

after applying CompIntoAlltup1

( + )* . zip₂ . (²π₁.id,select.(²π₂,iota.#.²π₁)^o.id)^o

after applying RightAssoc2

( + )* . zip₂ . (²π₁.id,select.(²π₂,iota.#.²π₁)^o.id)^o

after applying CompIntoAlltup1

( + )* . zip₂ . (²π₁.id,select.(²π₂.id,iota.#.²π₁.id)^o)^o

after applying RemoveIds2

( + )* . zip₂ . (²π₁,select.(²π₂.id,iota.#.²π₁.id)^o)^o

after applying RemoveIds2

( + )* . zip₂ . (²π₁,select.(²π₂,iota.#.²π₁.id)^o)^o

after applying RightAssoc3

( + )* . zip₂ . (²π₁,select.(²π₂,iota.#.²π₁.id)^o)^o

after applying RemoveIds2

( + )* . zip₂ . (²π₁,select.(²π₂,iota.#.²π₁)^o)^o

after applying LeftAssociate

( + )* . zip₂ . (²π₁,select.(²π₂,iota.#.²π₁)^o)^o

end trace