take CatStr(# {0},{1},(1 :-> 0),(1 :-> 0),((1,1) :-> 1),(0 :-> 1) #) ; :: thesis: ( not CatStr(# {0},{1},(1 :-> 0),(1 :-> 0),((1,1) :-> 1),(0 :-> 1) #) is void & not CatStr(# {0},{1},(1 :-> 0),(1 :-> 0),((1,1) :-> 1),(0 :-> 1) #) is empty )
thus ( not CatStr(# {0},{1},(1 :-> 0),(1 :-> 0),((1,1) :-> 1),(0 :-> 1) #) is void & not CatStr(# {0},{1},(1 :-> 0),(1 :-> 0),((1,1) :-> 1),(0 :-> 1) #) is empty ) ; :: thesis: verum