// This proof script verifies that for n odd, n >= 5,
// all length-n numbers are the sum
// of at most 5 generalized binary palindromes of length n-2

NestedWordAutomaton palCheckerFIVE = (
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_0_FIVE 
f_1_ZERO f_1_ONE f_1_TWO f_1_THREE f_1_FOUR f_1_FIVE 
f_2_ZERO f_2_ONE f_2_TWO f_2_THREE f_2_FOUR f_2_FIVE 
f_3_ZERO f_3_ONE f_3_TWO f_3_THREE f_3_FOUR f_3_FIVE 
f_4_ZERO f_4_ONE f_4_TWO f_4_THREE f_4_FOUR f_4_FIVE 
s0 s1 s2 s3 s4 q acc},
initialStates = {f_0_ZERO f_0_ONE f_0_TWO f_0_THREE f_0_FOUR f_0_FIVE },
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_ZERO a f_0_FIVE)

(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_ONE b f_0_FIVE)

(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_TWO a f_1_FIVE)

(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_THREE b f_1_FIVE)

(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_0_FOUR a f_2_FIVE)

(f_0_FIVE b f_2_ZERO)
(f_0_FIVE b f_2_ONE)
(f_0_FIVE b f_2_TWO)
(f_0_FIVE b f_2_THREE)
(f_0_FIVE b f_2_FOUR)
(f_0_FIVE b f_2_FIVE)

(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_ZERO b f_0_FIVE)

(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_ONE a f_1_FIVE)

(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_TWO b f_1_FIVE)

(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_THREE a f_2_FIVE)

(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_1_FOUR b f_2_FIVE)

(f_1_FIVE a f_3_ZERO)
(f_1_FIVE a f_3_ONE)
(f_1_FIVE a f_3_TWO)
(f_1_FIVE a f_3_THREE)
(f_1_FIVE a f_3_FOUR)
(f_1_FIVE a f_3_FIVE)

(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_ZERO a f_1_FIVE)

(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_ONE b f_1_FIVE)

(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_TWO a f_2_FIVE)

(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_THREE b f_2_FIVE)

(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_2_FOUR a f_3_FIVE)

(f_2_FIVE b f_3_ZERO)
(f_2_FIVE b f_3_ONE)
(f_2_FIVE b f_3_TWO)
(f_2_FIVE b f_3_THREE)
(f_2_FIVE b f_3_FOUR)
(f_2_FIVE b f_3_FIVE)

(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_ZERO b f_1_FIVE)

(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_ONE a f_2_FIVE)

(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_TWO b f_2_FIVE)

(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_THREE a f_3_FIVE)

(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)
(f_3_FOUR b f_3_FIVE)

(f_3_FIVE a f_4_ZERO)
(f_3_FIVE a f_4_ONE)
(f_3_FIVE a f_4_TWO)
(f_3_FIVE a f_4_THREE)
(f_3_FIVE a f_4_FOUR)
(f_3_FIVE a f_4_FIVE)

(f_4_ZERO a f_2_ZERO)
(f_4_ZERO a f_2_ONE)
(f_4_ZERO a f_2_TWO)
(f_4_ZERO a f_2_THREE)
(f_4_ZERO a f_2_FOUR)
(f_4_ZERO a f_2_FIVE)

(f_4_ONE b f_2_ZERO)
(f_4_ONE b f_2_ONE)
(f_4_ONE b f_2_TWO)
(f_4_ONE b f_2_THREE)
(f_4_ONE b f_2_FOUR)
(f_4_ONE b f_2_FIVE)

(f_4_TWO a f_3_ZERO)
(f_4_TWO a f_3_ONE)
(f_4_TWO a f_3_TWO)
(f_4_TWO a f_3_THREE)
(f_4_TWO a f_3_FOUR)
(f_4_TWO a f_3_FIVE)

(f_4_THREE b f_3_ZERO)
(f_4_THREE b f_3_ONE)
(f_4_THREE b f_3_TWO)
(f_4_THREE b f_3_THREE)
(f_4_THREE b f_3_FOUR)
(f_4_THREE b f_3_FIVE)

(f_4_FOUR a f_4_ZERO)
(f_4_FOUR a f_4_ONE)
(f_4_FOUR a f_4_TWO)
(f_4_FOUR a f_4_THREE)
(f_4_FOUR a f_4_FOUR)
(f_4_FOUR a f_4_FIVE)

(f_4_FIVE b f_4_ZERO)
(f_4_FIVE b f_4_ONE)
(f_4_FIVE b f_4_TWO)
(f_4_FIVE b f_4_THREE)
(f_4_FIVE b f_4_FOUR)
(f_4_FIVE b f_4_FIVE)

},
internalTransitions = {
(f_0_ZERO c s0)
(f_0_ONE c s0)
(f_0_TWO c s0)
(f_0_THREE c s0)
(f_0_FOUR c s0)
(f_0_FIVE c s0)

(f_0_ZERO d s0)
(f_0_ONE d s0)
(f_0_TWO d s0)
(f_0_THREE d s0)
(f_0_FOUR d s0)
(f_0_FIVE d s0)

(f_0_ZERO c s1)
(f_0_ONE c s1)
(f_0_TWO c s1)
(f_0_THREE c s1)
(f_0_FOUR c s1)
(f_0_FIVE c s1)

(f_0_ZERO d s1)
(f_0_ONE d s1)
(f_0_TWO d s1)
(f_0_THREE d s1)
(f_0_FOUR d s1)
(f_0_FIVE d s1)

(f_0_ZERO c s2)
(f_0_ONE c s2)
(f_0_TWO c s2)
(f_0_THREE c s2)
(f_0_FOUR c s2)
(f_0_FIVE c s2)

(f_0_ZERO d s2)
(f_0_ONE d s2)
(f_0_TWO d s2)
(f_0_THREE d s2)
(f_0_FOUR d s2)
(f_0_FIVE d s2)

(f_1_ZERO d s0)
(f_1_ONE d s0)
(f_1_TWO d s0)
(f_1_THREE d s0)
(f_1_FOUR d s0)
(f_1_FIVE d s0)

(f_1_ZERO c s1)
(f_1_ONE c s1)
(f_1_TWO c s1)
(f_1_THREE c s1)
(f_1_FOUR c s1)
(f_1_FIVE c s1)

(f_1_ZERO d s1)
(f_1_ONE d s1)
(f_1_TWO d s1)
(f_1_THREE d s1)
(f_1_FOUR d s1)
(f_1_FIVE d s1)

(f_1_ZERO c s2)
(f_1_ONE c s2)
(f_1_TWO c s2)
(f_1_THREE c s2)
(f_1_FOUR c s2)
(f_1_FIVE c s2)

(f_1_ZERO d s2)
(f_1_ONE d s2)
(f_1_TWO d s2)
(f_1_THREE d s2)
(f_1_FOUR d s2)
(f_1_FIVE d s2)

(f_1_ZERO c s3)
(f_1_ONE c s3)
(f_1_TWO c s3)
(f_1_THREE c s3)
(f_1_FOUR c s3)
(f_1_FIVE c s3)

(f_2_ZERO c s1)
(f_2_ONE c s1)
(f_2_TWO c s1)
(f_2_THREE c s1)
(f_2_FOUR c s1)
(f_2_FIVE c s1)

(f_2_ZERO d s1)
(f_2_ONE d s1)
(f_2_TWO d s1)
(f_2_THREE d s1)
(f_2_FOUR d s1)
(f_2_FIVE d s1)

(f_2_ZERO c s2)
(f_2_ONE c s2)
(f_2_TWO c s2)
(f_2_THREE c s2)
(f_2_FOUR c s2)
(f_2_FIVE c s2)

(f_2_ZERO d s2)
(f_2_ONE d s2)
(f_2_TWO d s2)
(f_2_THREE d s2)
(f_2_FOUR d s2)
(f_2_FIVE d s2)

(f_2_ZERO c s3)
(f_2_ONE c s3)
(f_2_TWO c s3)
(f_2_THREE c s3)
(f_2_FOUR c s3)
(f_2_FIVE c s3)

(f_2_ZERO d s3)
(f_2_ONE d s3)
(f_2_TWO d s3)
(f_2_THREE d s3)
(f_2_FOUR d s3)
(f_2_FIVE d s3)

(f_3_ZERO d s1)
(f_3_ONE d s1)
(f_3_TWO d s1)
(f_3_THREE d s1)
(f_3_FOUR d s1)
(f_3_FIVE d s1)

(f_3_ZERO c s2)
(f_3_ONE c s2)
(f_3_TWO c s2)
(f_3_THREE c s2)
(f_3_FOUR c s2)
(f_3_FIVE c s2)

(f_3_ZERO d s2)
(f_3_ONE d s2)
(f_3_TWO d s2)
(f_3_THREE d s2)
(f_3_FOUR d s2)
(f_3_FIVE d s2)

(f_3_ZERO c s3)
(f_3_ONE c s3)
(f_3_TWO c s3)
(f_3_THREE c s3)
(f_3_FOUR c s3)
(f_3_FIVE c s3)

(f_3_ZERO d s3)
(f_3_ONE d s3)
(f_3_TWO d s3)
(f_3_THREE d s3)
(f_3_FOUR d s3)
(f_3_FIVE d s3)

(f_3_ZERO c s4)
(f_3_ONE c s4)
(f_3_TWO c s4)
(f_3_THREE c s4)
(f_3_FOUR c s4)
(f_3_FIVE c s4)

(f_4_ZERO c s2)
(f_4_ONE c s2)
(f_4_TWO c s2)
(f_4_THREE c s2)
(f_4_FOUR c s2)
(f_4_FIVE c s2)

(f_4_ZERO d s2)
(f_4_ONE d s2)
(f_4_TWO d s2)
(f_4_THREE d s2)
(f_4_FOUR d s2)
(f_4_FIVE d s2)

(f_4_ZERO c s3)
(f_4_ONE c s3)
(f_4_TWO c s3)
(f_4_THREE c s3)
(f_4_FOUR c s3)
(f_4_FIVE c s3)

(f_4_ZERO d s3)
(f_4_ONE d s3)
(f_4_TWO d s3)
(f_4_THREE d s3)
(f_4_FOUR d s3)
(f_4_FIVE d s3)

(f_4_ZERO c s4)
(f_4_ONE c s4)
(f_4_TWO c s4)
(f_4_THREE c s4)
(f_4_FOUR c s4)
(f_4_FIVE c s4)

(f_4_ZERO d s4)
(f_4_ONE d s4)
(f_4_TWO d s4)
(f_4_THREE d s4)
(f_4_FOUR d s4)
(f_4_FIVE d s4)

(s2 c q)
(s3 d q)
(q 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_4_ZERO e 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_4_TWO e 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)
(s0 f_4_FOUR e s2)

(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_4_ONE f s0)

(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_4_THREE f s1)

(s0 f_0_FIVE f s2)
(s0 f_1_FIVE f s2)
(s0 f_2_FIVE f s2)
(s0 f_3_FIVE f s2)
(s0 f_4_FIVE f 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_4_ZERO f s0)

(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_4_TWO f s1)

(s1 f_0_FOUR f s2)
(s1 f_1_FOUR f s2)
(s1 f_2_FOUR f s2)
(s1 f_3_FOUR f s2)
(s1 f_4_FOUR f s2)

(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_4_ONE e 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_4_THREE e s2)

(s1 f_0_FIVE e s3)
(s1 f_1_FIVE e s3)
(s1 f_2_FIVE e s3)
(s1 f_3_FIVE e s3)
(s1 f_4_FIVE e s3)


(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_4_ZERO e 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_4_TWO e 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)
(s2 f_4_FOUR e s3)

(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_4_ONE f s1)

(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_4_THREE f s2)

(s2 f_0_FIVE f s3)
(s2 f_1_FIVE f s3)
(s2 f_2_FIVE f s3)
(s2 f_3_FIVE f s3)
(s2 f_4_FIVE f 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_4_ZERO f s1)

(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_4_TWO f s2)

(s3 f_0_FOUR f s3)
(s3 f_1_FOUR f s3)
(s3 f_2_FOUR f s3)
(s3 f_3_FOUR f s3)
(s3 f_4_FOUR f s3)

(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_4_ONE e 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_4_THREE e s3)

(s3 f_0_FIVE e s4)
(s3 f_1_FIVE e s4)
(s3 f_2_FIVE e s4)
(s3 f_3_FIVE e s4)
(s3 f_4_FIVE e s4)


(s4 f_0_ZERO e s2)
(s4 f_1_ZERO e s2)
(s4 f_2_ZERO e s2)
(s4 f_3_ZERO e s2)
(s4 f_4_ZERO e s2)

(s4 f_0_TWO e s3)
(s4 f_1_TWO e s3)
(s4 f_2_TWO e s3)
(s4 f_3_TWO e s3)
(s4 f_4_TWO e s3)

(s4 f_0_FOUR e s4)
(s4 f_1_FOUR e s4)
(s4 f_2_FOUR e s4)
(s4 f_3_FOUR e s4)
(s4 f_4_FOUR e s4)

(s4 f_0_ONE f s2)
(s4 f_1_ONE f s2)
(s4 f_2_ONE f s2)
(s4 f_3_ONE f s2)
(s4 f_4_ONE f s2)

(s4 f_0_THREE f s3)
(s4 f_1_THREE f s3)
(s4 f_2_THREE f s3)
(s4 f_3_THREE f s3)
(s4 f_4_THREE f s3)

(s4 f_0_FIVE f s4)
(s4 f_1_FIVE f s4)
(s4 f_2_FIVE f s4)
(s4 f_3_FIVE f s4)
(s4 f_4_FIVE f s4)


}
);

print(numberOfStates(determinize(palCheckerFIVE)));

NestedWordAutomaton syntaxChecker = (
	callAlphabet = { a b },
	internalAlphabet = { c d },
	returnAlphabet = { e f },
	states = {q0 q1 q2 q3 q4 q5 },
	initialStates = {q0},
	finalStates = {q5},
	callTransitions = {
		(q0 a q1)
		(q0 b q1)

		(q1 a q1)
		(q1 b q1)
	},
	internalTransitions = {
		(q1 c q2)
		(q1 d q2)

		(q3 c q4)
		(q3 d q4)
		(q4 d q5)
	},
	returnTransitions = {
		(q2 q0 e q3)
		(q2 q0 f q3)

		(q2 q1 e q3)
		(q2 q1 f q3)

		(q3 q0 e q3)
		(q3 q0 f q3)

		(q3 q1 e q3)
		(q3 q1 f q3)
	}
);

assert(IsIncluded(syntaxChecker, palCheckerFIVE));