theorem :: FUZIMPL2:1
#R 1 = (AffineMap (1,0)) | (right_open_halfline 0)