after applying start

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

after applying RemoveIds1

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

after applying RemoveIds1

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

after applying RemoveIds1

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

after applying RemoveIds1

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

after applying MapIntoComp

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

after applying MapIntoAlltup

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

after applying MapIntoComp

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

after applying MapIntoAlltup

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

after applying MapIntoComp

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

after applying MapIntoComp

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

after applying MapIntoComp

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

after applying MapIntoAlltup

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

after applying MapIntoComp

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

after applying MapIntoComp

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

after applying MapIntoComp

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

after applying MapIntoAlltup

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

after applying MapIntoComp

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

after applying MapIntoAlltup

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

after applying MapIntoComp

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

after applying MapIntoComp

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

after applying MapIntoComp

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

after applying MapIntoComp

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

after applying LeftAssociate

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

after applying LeftAssociate

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

after applying LeftAssociate

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

after applying LeftAssociate

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

after applying LeftAssociate

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

after applying CompIntoMap

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

after applying CompIntoMap

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

after applying CompIntoMap

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

after applying CompIntoMap

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

after applying CompIntoMap

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

after applying CompIntoMap

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

after applying CompIntoMap

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

after applying CompIntoMap

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

after applying MapIntoComp

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

after applying MapIntoComp

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

after applying MapIntoComp

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

after applying MapIntoComp

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

after applying MapIntoComp

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

after applying MapIntoComp

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

after applying MapIntoComp

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

after applying MapIntoComp

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

after applying DistlElim

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

after applying LeftAssociate

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

after applying CompIntoMap

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

after applying CompIntoMap

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

after applying CompIntoMap

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

after applying CompIntoMap

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

after applying CompIntoMap

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

after applying CompIntoMap

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

after applying CompIntoMap

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

after applying CompIntoMap

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

after applying RightAssoc2

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

after applying CompIntoAlltup1

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

after applying RightAssoc2

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

after applying CompIntoAlltup1

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

after applying RightAssoc2

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

after applying CompIntoAlltup1

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

after applying RightAssoc2

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

after applying CompIntoAlltup1

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

after applying RightAssoc2

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

after applying CompIntoAlltup1

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

after applying RightAssoc2

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

after applying CompIntoAlltup1

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

after applying RightAssoc2

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

after applying CompIntoAlltup1

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

after applying RightAssoc2

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

after applying CompIntoAlltup1

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

after applying RightAssoc2

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

after applying CompIntoAlltup1

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

after applying RightAssoc2

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

after applying CompIntoAlltup1

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

after applying AddrIntoZip

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

after applying AddrIntoAlltup

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

after applying AddrIntoZip

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

after applying AddrIntoAlltup

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

after applying MapIntoComp

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

after applying MapIntoComp

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

after applying MapIntoComp

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

after applying MapIntoComp

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

after applying MapIntoComp

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

after applying MapIntoComp

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

after applying MapIntoComp

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

after applying MapIntoComp

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

after applying RightAssoc2

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

after applying AddrIntoZip

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

after applying RightAssoc2

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

after applying AddrIntoAlltup

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

after applying LeftAssociate

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

after applying RightAssoc2

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

after applying RepeatFusion

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

after applying LeftAssociate

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

after applying RepeatFusion

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