// This proof script shows that all words of even length n are // sums of exactly 4 generalized palindromes of length exactly n-1 NestedWordAutomaton palindromeChecker = ( callAlphabet = { a b }, internalAlphabet = { c d }, returnAlphabet = { e f }, states = {f_0_ZERO f_0_ONE f_0_TWO f_0_THREE f_0_FOUR f_1_ZERO f_1_ONE f_1_TWO f_1_THREE f_1_FOUR f_2_ZERO f_2_ONE f_2_TWO f_2_THREE f_2_FOUR f_3_ZERO f_3_ONE f_3_TWO f_3_THREE f_3_FOUR s0 s1 s2 s3 acc}, initialStates = {f_0_ZERO f_0_ONE f_0_TWO f_0_THREE f_0_FOUR}, finalStates = {acc}, callTransitions = { (f_0_ZERO a f_0_ZERO) (f_0_ZERO a f_0_ONE) (f_0_ZERO a f_0_TWO) (f_0_ZERO a f_0_THREE) (f_0_ZERO a f_0_FOUR) (f_0_ONE b f_0_ZERO) (f_0_ONE b f_0_ONE) (f_0_ONE b f_0_TWO) (f_0_ONE b f_0_THREE) (f_0_ONE b f_0_FOUR) (f_0_TWO a f_1_ZERO) (f_0_TWO a f_1_ONE) (f_0_TWO a f_1_TWO) (f_0_TWO a f_1_THREE) (f_0_TWO a f_1_FOUR) (f_0_THREE b f_1_ZERO) (f_0_THREE b f_1_ONE) (f_0_THREE b f_1_TWO) (f_0_THREE b f_1_THREE) (f_0_THREE b f_1_FOUR) (f_0_FOUR a f_2_ZERO) (f_0_FOUR a f_2_ONE) (f_0_FOUR a f_2_TWO) (f_0_FOUR a f_2_THREE) (f_0_FOUR a f_2_FOUR) (f_1_ZERO b f_0_ZERO) (f_1_ZERO b f_0_ONE) (f_1_ZERO b f_0_TWO) (f_1_ZERO b f_0_THREE) (f_1_ZERO b f_0_FOUR) (f_1_ONE a f_1_ZERO) (f_1_ONE a f_1_ONE) (f_1_ONE a f_1_TWO) (f_1_ONE a f_1_THREE) (f_1_ONE a f_1_FOUR) (f_1_TWO b f_1_ZERO) (f_1_TWO b f_1_ONE) (f_1_TWO b f_1_TWO) (f_1_TWO b f_1_THREE) (f_1_TWO b f_1_FOUR) (f_1_THREE a f_2_ZERO) (f_1_THREE a f_2_ONE) (f_1_THREE a f_2_TWO) (f_1_THREE a f_2_THREE) (f_1_THREE a f_2_FOUR) (f_1_FOUR b f_2_ZERO) (f_1_FOUR b f_2_ONE) (f_1_FOUR b f_2_TWO) (f_1_FOUR b f_2_THREE) (f_1_FOUR b f_2_FOUR) (f_2_ZERO a f_1_ZERO) (f_2_ZERO a f_1_ONE) (f_2_ZERO a f_1_TWO) (f_2_ZERO a f_1_THREE) (f_2_ZERO a f_1_FOUR) (f_2_ONE b f_1_ZERO) (f_2_ONE b f_1_ONE) (f_2_ONE b f_1_TWO) (f_2_ONE b f_1_THREE) (f_2_ONE b f_1_FOUR) (f_2_TWO a f_2_ZERO) (f_2_TWO a f_2_ONE) (f_2_TWO a f_2_TWO) (f_2_TWO a f_2_THREE) (f_2_TWO a f_2_FOUR) (f_2_THREE b f_2_ZERO) (f_2_THREE b f_2_ONE) (f_2_THREE b f_2_TWO) (f_2_THREE b f_2_THREE) (f_2_THREE b f_2_FOUR) (f_2_FOUR a f_3_ZERO) (f_2_FOUR a f_3_ONE) (f_2_FOUR a f_3_TWO) (f_2_FOUR a f_3_THREE) (f_2_FOUR a f_3_FOUR) (f_3_ZERO b f_1_ZERO) (f_3_ZERO b f_1_ONE) (f_3_ZERO b f_1_TWO) (f_3_ZERO b f_1_THREE) (f_3_ZERO b f_1_FOUR) (f_3_ONE a f_2_ZERO) (f_3_ONE a f_2_ONE) (f_3_ONE a f_2_TWO) (f_3_ONE a f_2_THREE) (f_3_ONE a f_2_FOUR) (f_3_TWO b f_2_ZERO) (f_3_TWO b f_2_ONE) (f_3_TWO b f_2_TWO) (f_3_TWO b f_2_THREE) (f_3_TWO b f_2_FOUR) (f_3_THREE a f_3_ZERO) (f_3_THREE a f_3_ONE) (f_3_THREE a f_3_TWO) (f_3_THREE a f_3_THREE) (f_3_THREE a f_3_FOUR) (f_3_FOUR b f_3_ZERO) (f_3_FOUR b f_3_ONE) (f_3_FOUR b f_3_TWO) (f_3_FOUR b f_3_THREE) (f_3_FOUR b f_3_FOUR) }, internalTransitions = { (f_0_ZERO c s0) (f_0_ZERO c s1) (f_0_ZERO c s2) (f_0_ZERO d s0) (f_0_ZERO d s1) (f_0_ONE c s0) (f_0_ONE c s1) (f_0_ONE c s2) (f_0_ONE d s0) (f_0_ONE d s1) (f_0_TWO c s0) (f_0_TWO c s1) (f_0_TWO c s2) (f_0_TWO d s0) (f_0_TWO d s1) (f_0_THREE c s0) (f_0_THREE c s1) (f_0_THREE c s2) (f_0_THREE d s0) (f_0_THREE d s1) (f_0_FOUR c s0) (f_0_FOUR c s1) (f_0_FOUR c s2) (f_0_FOUR d s0) (f_0_FOUR d s1) (f_1_ZERO c s1) (f_1_ZERO c s2) (f_1_ZERO d s0) (f_1_ZERO d s1) (f_1_ZERO d s2) (f_1_ONE c s1) (f_1_ONE c s2) (f_1_ONE d s0) (f_1_ONE d s1) (f_1_ONE d s2) (f_1_TWO c s1) (f_1_TWO c s2) (f_1_TWO d s0) (f_1_TWO d s1) (f_1_TWO d s2) (f_1_THREE c s1) (f_1_THREE c s2) (f_1_THREE d s0) (f_1_THREE d s1) (f_1_THREE d s2) (f_1_FOUR c s1) (f_1_FOUR c s2) (f_1_FOUR d s0) (f_1_FOUR d s1) (f_1_FOUR d s2) (f_2_ZERO c s1) (f_2_ZERO c s2) (f_2_ZERO c s3) (f_2_ZERO d s1) (f_2_ZERO d s2) (f_2_ONE c s1) (f_2_ONE c s2) (f_2_ONE c s3) (f_2_ONE d s1) (f_2_ONE d s2) (f_2_TWO c s1) (f_2_TWO c s2) (f_2_TWO c s3) (f_2_TWO d s1) (f_2_TWO d s2) (f_2_THREE c s1) (f_2_THREE c s2) (f_2_THREE c s3) (f_2_THREE d s1) (f_2_THREE d s2) (f_2_FOUR c s1) (f_2_FOUR c s2) (f_2_FOUR c s3) (f_2_FOUR d s1) (f_2_FOUR d s2) (f_3_ZERO c s2) (f_3_ZERO c s3) (f_3_ZERO d s1) (f_3_ZERO d s2) (f_3_ZERO d s3) (f_3_ONE c s2) (f_3_ONE c s3) (f_3_ONE d s1) (f_3_ONE d s2) (f_3_ONE d s3) (f_3_TWO c s2) (f_3_TWO c s3) (f_3_TWO d s1) (f_3_TWO d s2) (f_3_TWO d s3) (f_3_THREE c s2) (f_3_THREE c s3) (f_3_THREE d s1) (f_3_THREE d s2) (f_3_THREE d s3) (f_3_FOUR c s2) (f_3_FOUR c s3) (f_3_FOUR d s1) (f_3_FOUR d s2) (f_3_FOUR d s3) (s1 d acc) }, returnTransitions = { (s0 f_0_ZERO e s0) (s0 f_1_ZERO e s0) (s0 f_2_ZERO e s0) (s0 f_3_ZERO e s0) (s0 f_0_ONE f s0) (s0 f_1_ONE f s0) (s0 f_2_ONE f s0) (s0 f_3_ONE f s0) (s0 f_0_TWO e s1) (s0 f_1_TWO e s1) (s0 f_2_TWO e s1) (s0 f_3_TWO e s1) (s0 f_0_THREE f s1) (s0 f_1_THREE f s1) (s0 f_2_THREE f s1) (s0 f_3_THREE f s1) (s0 f_0_FOUR e s2) (s0 f_1_FOUR e s2) (s0 f_2_FOUR e s2) (s0 f_3_FOUR e s2) (s1 f_0_ZERO f s0) (s1 f_1_ZERO f s0) (s1 f_2_ZERO f s0) (s1 f_3_ZERO f s0) (s1 f_0_ONE e s1) (s1 f_1_ONE e s1) (s1 f_2_ONE e s1) (s1 f_3_ONE e s1) (s1 f_0_TWO f s1) (s1 f_1_TWO f s1) (s1 f_2_TWO f s1) (s1 f_3_TWO f s1) (s1 f_0_THREE e s2) (s1 f_1_THREE e s2) (s1 f_2_THREE e s2) (s1 f_3_THREE e s2) (s1 f_0_FOUR f s2) (s1 f_1_FOUR f s2) (s1 f_2_FOUR f s2) (s1 f_3_FOUR f s2) (s2 f_0_ZERO e s1) (s2 f_1_ZERO e s1) (s2 f_2_ZERO e s1) (s2 f_3_ZERO e s1) (s2 f_0_ONE f s1) (s2 f_1_ONE f s1) (s2 f_2_ONE f s1) (s2 f_3_ONE f s1) (s2 f_0_TWO e s2) (s2 f_1_TWO e s2) (s2 f_2_TWO e s2) (s2 f_3_TWO e s2) (s2 f_0_THREE f s2) (s2 f_1_THREE f s2) (s2 f_2_THREE f s2) (s2 f_3_THREE f s2) (s2 f_0_FOUR e s3) (s2 f_1_FOUR e s3) (s2 f_2_FOUR e s3) (s2 f_3_FOUR e s3) (s3 f_0_ZERO f s1) (s3 f_1_ZERO f s1) (s3 f_2_ZERO f s1) (s3 f_3_ZERO f s1) (s3 f_0_ONE e s2) (s3 f_1_ONE e s2) (s3 f_2_ONE e s2) (s3 f_3_ONE e s2) (s3 f_0_TWO f s2) (s3 f_1_TWO f s2) (s3 f_2_TWO f s2) (s3 f_3_TWO f s2) (s3 f_0_THREE e s3) (s3 f_1_THREE e s3) (s3 f_2_THREE e s3) (s3 f_3_THREE e s3) (s3 f_0_FOUR f s3) (s3 f_1_FOUR f s3) (s3 f_2_FOUR f s3) (s3 f_3_FOUR f s3) } ); NestedWordAutomaton detPalCheck = determinize(palindromeChecker); print(numberOfStates(detPalCheck)); NestedWordAutomaton syntaxChecker = ( callAlphabet = { a b }, internalAlphabet = { c d }, returnAlphabet = { e f }, states = {q0 q1 q2}, initialStates = {q0}, finalStates = {q2}, callTransitions = { (q0 a q0) (q0 b q0) }, internalTransitions = { (q0 c q1) (q0 d q1) (q1 d q2) }, returnTransitions = { (q1 q0 e q1) (q1 q0 f q1) } ); assert(IsEquivalent(palindromeChecker, syntaxChecker));