// 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));