// Date: 16.01.2012
// Author: heizmann@informatik.uni-freiburg.de
//
// bluegreen-i was the i-th intermediate result of 
// terminationTraceAbstractionBlueGreen.fat in revision 4679.
// 
// After buchiIntersect and buchiComplementFKV removeNon-Live and minimizeDFA
// was used.


assert(!buchiAccepts(buchiReduce(bluegreen_RemovedNonLiveMinimizeDfa5), [,]));
//assert(!buchiAccepts(minimizeDfaTable(bluegreen_RemovedNonLiveMinimizeDfa5"), [,]));


NestedWordAutomaton bluegreen_RemovedNonLiveMinimizeDfa1 = (
	callAlphabet = {},
	internalAlphabet = {a0 a1 },
	returnAlphabet = {},
	states = {s2 s3 s0 s1 s6 s4 s5 },
	initialStates = {s1 },
	finalStates = {s1 s2 s6 },
	callTransitions = {
	},
	internalTransitions = {
		 (s0 a0 s0)
		 (s0 a0 s3)
		 (s0 a1 s4)
		 (s1 a0 s0)
		 (s1 a0 s3)
		 (s1 a1 s4)
		 (s2 a0 s4)
		 (s2 a1 s4)
		 (s3 a0 s6)
		 (s3 a1 s2)
		 (s4 a0 s2)
		 (s4 a1 s2)
		 (s5 a0 s5)
		 (s5 a1 s4)
		 (s6 a0 s5)
		 (s6 a1 s4)
	},
	returnTransitions = {
	}
);

NestedWordAutomaton bluegreen_RemovedNonLiveMinimizeDfa2 = (
	callAlphabet = {},
	internalAlphabet = {a0 a1 },
	returnAlphabet = {},
	states = {s2 s3 s0 s1 s6 s7 s4 s5 s10 s11 s8 s9 s14 s15 s12 s13 s19 s18 s17 s16 s21 s20 },
	initialStates = {s16 },
	finalStates = {s1 s10 s16 s18 s20 },
	callTransitions = {
	},
	internalTransitions = {
		 (s0 a1 s8)
		 (s1 a0 s8)
		 (s1 a1 s8)
		 (s2 a1 s1)
		 (s3 a0 s0)
		 (s3 a0 s19)
		 (s3 a1 s12)
		 (s3 a1 s13)
		 (s4 a0 s0)
		 (s4 a0 s19)
		 (s4 a1 s15)
		 (s5 a0 s5)
		 (s5 a1 s8)
		 (s6 a1 s12)
		 (s7 a0 s10)
		 (s7 a1 s1)
		 (s8 a0 s1)
		 (s8 a1 s1)
		 (s9 a1 s20)
		 (s10 a0 s5)
		 (s10 a1 s8)
		 (s11 a0 s7)
		 (s11 a0 s11)
		 (s11 a1 s8)
		 (s12 a1 s17)
		 (s13 a0 s2)
		 (s13 a0 s14)
		 (s13 a1 s3)
		 (s13 a1 s9)
		 (s14 a0 s21)
		 (s14 a1 s15)
		 (s15 a0 s8)
		 (s15 a1 s8)
		 (s16 a0 s7)
		 (s16 a0 s11)
		 (s16 a1 s3)
		 (s16 a1 s9)
		 (s17 a1 s18)
		 (s18 a1 s6)
		 (s19 a0 s4)
		 (s19 a1 s8)
		 (s20 a1 s9)
		 (s21 a0 s2)
		 (s21 a0 s14)
		 (s21 a1 s8)
	},
	returnTransitions = {
	}
);

NestedWordAutomaton bluegreen_RemovedNonLiveMinimizeDfa3 = (
	callAlphabet = {},
	internalAlphabet = {a0 a1 },
	returnAlphabet = {},
	states = {s2 s3 s0 s1 s6 s7 s4 s5 s10 s11 s8 s9 s14 s15 s12 s13 },
	initialStates = {s13 },
	finalStates = {s1 s5 s13 },
	callTransitions = {
	},
	internalTransitions = {
		 (s0 a0 s3)
		 (s0 a0 s9)
		 (s0 a1 s2)
		 (s1 a0 s2)
		 (s1 a1 s2)
		 (s2 a0 s1)
		 (s2 a1 s1)
		 (s3 a1 s1)
		 (s4 a0 s8)
		 (s4 a0 s11)
		 (s4 a1 s6)
		 (s5 a0 s7)
		 (s5 a1 s2)
		 (s6 a0 s3)
		 (s6 a0 s9)
		 (s6 a1 s4)
		 (s7 a0 s7)
		 (s7 a1 s2)
		 (s8 a0 s14)
		 (s8 a1 s2)
		 (s9 a0 s0)
		 (s9 a1 s15)
		 (s10 a0 s5)
		 (s10 a1 s1)
		 (s11 a1 s2)
		 (s12 a0 s10)
		 (s12 a0 s12)
		 (s12 a1 s2)
		 (s13 a0 s10)
		 (s13 a0 s12)
		 (s13 a1 s4)
		 (s14 a0 s8)
		 (s14 a0 s11)
		 (s14 a1 s15)
		 (s15 a0 s2)
		 (s15 a1 s2)
	},
	returnTransitions = {
	}
);

NestedWordAutomaton bluegreen_RemovedNonLiveMinimizeDfa4 = (
	callAlphabet = {},
	internalAlphabet = {a0 a1 },
	returnAlphabet = {},
	states = {s36 s37 s38 s39 s32 s33 s34 s35 s2 s3 s0 s1 s6 s7 s4 s5 s10 s11 s8 s9 s14 s15 s12 s13 s19 s18 s17 s16 s23 s22 s21 s20 s27 s26 s25 s24 s31 s30 s29 s28 },
	initialStates = {s28 },
	finalStates = {s2 s26 s28 s34 },
	callTransitions = {
	},
	internalTransitions = {
		 (s0 a0 s15)
		 (s0 a1 s21)
		 (s1 a0 s16)
		 (s1 a0 s38)
		 (s1 a1 s12)
		 (s2 a0 s10)
		 (s2 a1 s13)
		 (s3 a1 s5)
		 (s3 a1 s7)
		 (s4 a0 s2)
		 (s4 a1 s26)
		 (s5 a0 s37)
		 (s5 a1 s37)
		 (s6 a0 s16)
		 (s6 a0 s38)
		 (s6 a1 s37)
		 (s7 a0 s17)
		 (s7 a0 s30)
		 (s7 a1 s17)
		 (s7 a1 s30)
		 (s8 a0 s36)
		 (s8 a1 s37)
		 (s9 a1 s37)
		 (s10 a0 s10)
		 (s10 a1 s37)
		 (s11 a0 s10)
		 (s11 a0 s11)
		 (s11 a1 s17)
		 (s11 a1 s30)
		 (s12 a0 s31)
		 (s12 a0 s33)
		 (s12 a1 s1)
		 (s13 a0 s32)
		 (s13 a1 s5)
		 (s14 a0 s4)
		 (s14 a0 s14)
		 (s14 a1 s37)
		 (s15 a0 s16)
		 (s15 a0 s38)
		 (s15 a1 s17)
		 (s16 a1 s34)
		 (s17 a0 s26)
		 (s17 a1 s26)
		 (s18 a1 s17)
		 (s18 a1 s30)
		 (s19 a0 s8)
		 (s19 a0 s9)
		 (s19 a0 s18)
		 (s19 a0 s23)
		 (s19 a1 s1)
		 (s19 a1 s20)
		 (s20 a0 s0)
		 (s20 a0 s3)
		 (s20 a0 s35)
		 (s20 a0 s39)
		 (s20 a1 s12)
		 (s20 a1 s19)
		 (s21 a0 s37)
		 (s21 a1 s17)
		 (s22 a0 s0)
		 (s22 a0 s3)
		 (s22 a0 s35)
		 (s22 a0 s39)
		 (s22 a1 s17)
		 (s22 a1 s30)
		 (s23 a0 s24)
		 (s23 a0 s25)
		 (s23 a1 s17)
		 (s23 a1 s30)
		 (s24 a0 s31)
		 (s24 a0 s33)
		 (s24 a1 s21)
		 (s25 a0 s8)
		 (s25 a0 s9)
		 (s25 a0 s18)
		 (s25 a0 s23)
		 (s25 a1 s5)
		 (s25 a1 s7)
		 (s26 a0 s13)
		 (s26 a1 s17)
		 (s27 a0 s4)
		 (s27 a0 s14)
		 (s27 a0 s27)
		 (s27 a0 s29)
		 (s27 a1 s17)
		 (s27 a1 s30)
		 (s28 a0 s4)
		 (s28 a0 s14)
		 (s28 a0 s27)
		 (s28 a0 s29)
		 (s28 a1 s12)
		 (s28 a1 s19)
		 (s29 a0 s10)
		 (s29 a0 s11)
		 (s29 a1 s5)
		 (s29 a1 s7)
		 (s30 a0 s5)
		 (s30 a0 s7)
		 (s30 a1 s5)
		 (s30 a1 s7)
		 (s31 a0 s36)
		 (s31 a1 s17)
		 (s32 a0 s13)
		 (s32 a1 s17)
		 (s33 a1 s17)
		 (s34 a0 s13)
		 (s34 a1 s13)
		 (s35 a1 s26)
		 (s36 a0 s31)
		 (s36 a0 s33)
		 (s36 a1 s5)
		 (s37 a0 s26)
		 (s37 a1 s34)
		 (s38 a0 s15)
		 (s38 a1 s5)
		 (s39 a0 s6)
		 (s39 a0 s22)
		 (s39 a1 s5)
		 (s39 a1 s7)
	},
	returnTransitions = {
	}
);

NestedWordAutomaton bluegreen_RemovedNonLiveMinimizeDfa5 = (
	callAlphabet = {},
	internalAlphabet = {a0 a1 },
	returnAlphabet = {},
	states = {s2 s3 s0 s1 s6 s7 s4 s5 s10 s11 s8 s9 s14 s15 s12 s13 s19 s18 s17 s16 s23 s22 s21 s20 s27 s26 s25 s24 s31 s30 s29 s28 s36 s37 s38 s39 s32 s33 s34 s35 s44 s45 s46 s47 s40 s41 s42 s43 s53 s52 s55 s54 s49 s48 s51 s50 s61 s60 s63 s62 s57 s56 s59 s58 s70 s71 s68 s69 s66 s67 s64 s65 s78 s79 s76 s77 s74 s75 s72 s73 s87 s86 s85 s84 s83 s82 s81 s80 s95 s94 s93 s92 s91 s90 s89 s88 s105 s104 s107 s106 s108 s97 s96 s99 s98 s101 s100 s103 s102 },
	initialStates = {s106 },
	finalStates = {s21 s44 s76 s106 },
	callTransitions = {
	},
	internalTransitions = {
		 (s0 a0 s7)
		 (s0 a0 s55)
		 (s0 a0 s59)
		 (s0 a0 s97)
		 (s0 a1 s4)
		 (s0 a1 s20)
		 (s0 a1 s78)
		 (s0 a1 s108)
		 (s1 a0 s28)
		 (s1 a0 s104)
		 (s1 a1 s4)
		 (s1 a1 s20)
		 (s2 a1 s4)
		 (s2 a1 s78)
		 (s3 a0 s28)
		 (s3 a0 s101)
		 (s3 a1 s4)
		 (s3 a1 s7)
		 (s3 a1 s93)
		 (s4 a0 s21)
		 (s5 a0 s5)
		 (s5 a0 s45)
		 (s5 a1 s4)
		 (s6 a0 s27)
		 (s7 a0 s21)
		 (s7 a1 s76)
		 (s8 a0 s26)
		 (s8 a0 s62)
		 (s8 a0 s65)
		 (s8 a0 s95)
		 (s8 a1 s4)
		 (s8 a1 s7)
		 (s8 a1 s37)
		 (s9 a0 s7)
		 (s9 a0 s92)
		 (s9 a1 s4)
		 (s9 a1 s7)
		 (s9 a1 s93)
		 (s10 a1 s4)
		 (s10 a1 s20)
		 (s10 a1 s78)
		 (s10 a1 s108)
		 (s11 a0 s19)
		 (s11 a0 s51)
		 (s11 a1 s42)
		 (s11 a1 s91)
		 (s12 a0 s12)
		 (s12 a1 s4)
		 (s13 a0 s3)
		 (s13 a0 s15)
		 (s13 a0 s24)
		 (s13 a0 s32)
		 (s13 a1 s41)
		 (s13 a1 s42)
		 (s13 a1 s83)
		 (s14 a0 s2)
		 (s14 a0 s24)
		 (s14 a0 s32)
		 (s14 a0 s98)
		 (s14 a1 s42)
		 (s14 a1 s91)
		 (s15 a1 s4)
		 (s15 a1 s7)
		 (s15 a1 s93)
		 (s16 a0 s22)
		 (s16 a0 s27)
		 (s16 a1 s41)
		 (s16 a1 s42)
		 (s16 a1 s94)
		 (s17 a0 s5)
		 (s17 a0 s17)
		 (s17 a0 s29)
		 (s17 a0 s45)
		 (s17 a1 s4)
		 (s17 a1 s78)
		 (s18 a0 s24)
		 (s18 a0 s32)
		 (s18 a1 s40)
		 (s19 a0 s11)
		 (s19 a0 s62)
		 (s19 a0 s65)
		 (s19 a0 s77)
		 (s19 a1 s4)
		 (s19 a1 s78)
		 (s20 a0 s25)
		 (s20 a0 s27)
		 (s20 a1 s22)
		 (s20 a1 s27)
		 (s20 a1 s66)
		 (s21 a0 s85)
		 (s21 a1 s6)
		 (s22 a0 s16)
		 (s22 a0 s85)
		 (s22 a1 s4)
		 (s22 a1 s7)
		 (s22 a1 s93)
		 (s23 a0 s12)
		 (s23 a0 s43)
		 (s23 a0 s50)
		 (s23 a0 s56)
		 (s23 a1 s39)
		 (s23 a1 s42)
		 (s23 a1 s48)
		 (s23 a1 s91)
		 (s24 a1 s4)
		 (s25 a0 s64)
		 (s25 a0 s85)
		 (s25 a1 s4)
		 (s25 a1 s20)
		 (s26 a0 s51)
		 (s26 a0 s72)
		 (s26 a1 s41)
		 (s26 a1 s42)
		 (s26 a1 s94)
		 (s27 a0 s85)
		 (s27 a1 s4)
		 (s28 a0 s24)
		 (s28 a0 s32)
		 (s28 a1 s42)
		 (s29 a0 s12)
		 (s29 a0 s50)
		 (s29 a1 s42)
		 (s29 a1 s91)
		 (s30 a0 s5)
		 (s30 a0 s17)
		 (s30 a0 s23)
		 (s30 a0 s29)
		 (s30 a0 s30)
		 (s30 a0 s45)
		 (s30 a0 s79)
		 (s30 a0 s88)
		 (s30 a1 s4)
		 (s30 a1 s20)
		 (s30 a1 s78)
		 (s30 a1 s108)
		 (s31 a0 s2)
		 (s31 a0 s10)
		 (s31 a0 s24)
		 (s31 a0 s32)
		 (s31 a0 s38)
		 (s31 a0 s98)
		 (s31 a0 s102)
		 (s31 a0 s107)
		 (s31 a1 s39)
		 (s31 a1 s42)
		 (s31 a1 s48)
		 (s31 a1 s91)
		 (s32 a0 s28)
		 (s32 a1 s4)
		 (s33 a0 s24)
		 (s33 a0 s32)
		 (s34 a0 s11)
		 (s34 a0 s62)
		 (s34 a0 s65)
		 (s34 a0 s77)
		 (s35 a0 s64)
		 (s35 a0 s85)
		 (s35 a1 s4)
		 (s35 a1 s7)
		 (s35 a1 s93)
		 (s36 a0 s85)
		 (s36 a1 s6)
		 (s37 a0 s22)
		 (s37 a0 s27)
		 (s37 a1 s36)
		 (s37 a1 s61)
		 (s37 a1 s66)
		 (s38 a0 s14)
		 (s38 a0 s28)
		 (s38 a0 s31)
		 (s38 a0 s82)
		 (s38 a1 s4)
		 (s38 a1 s20)
		 (s38 a1 s78)
		 (s38 a1 s108)
		 (s39 a0 s7)
		 (s39 a0 s55)
		 (s39 a0 s59)
		 (s39 a0 s97)
		 (s39 a1 s4)
		 (s39 a1 s7)
		 (s39 a1 s53)
		 (s39 a1 s55)
		 (s39 a1 s78)
		 (s39 a1 s93)
		 (s40 a0 s62)
		 (s40 a0 s65)
		 (s41 a0 s7)
		 (s41 a1 s4)
		 (s42 a0 s7)
		 (s43 a0 s12)
		 (s43 a0 s43)
		 (s43 a0 s50)
		 (s43 a0 s56)
		 (s43 a1 s4)
		 (s43 a1 s20)
		 (s43 a1 s78)
		 (s43 a1 s108)
		 (s44 a0 s12)
		 (s44 a1 s6)
		 (s45 a0 s44)
		 (s45 a1 s76)
		 (s46 a0 s28)
		 (s46 a0 s101)
		 (s46 a1 s4)
		 (s46 a1 s7)
		 (s46 a1 s37)
		 (s47 a0 s51)
		 (s47 a0 s72)
		 (s47 a1 s41)
		 (s47 a1 s42)
		 (s47 a1 s83)
		 (s48 a0 s7)
		 (s48 a0 s92)
		 (s48 a1 s4)
		 (s48 a1 s7)
		 (s48 a1 s37)
		 (s49 a0 s2)
		 (s49 a0 s24)
		 (s49 a0 s32)
		 (s49 a0 s98)
		 (s50 a0 s12)
		 (s50 a0 s50)
		 (s50 a1 s4)
		 (s50 a1 s78)
		 (s51 a0 s62)
		 (s51 a0 s65)
		 (s51 a1 s4)
		 (s52 a0 s8)
		 (s52 a0 s19)
		 (s52 a0 s51)
		 (s52 a0 s81)
		 (s52 a1 s41)
		 (s52 a1 s42)
		 (s52 a1 s75)
		 (s52 a1 s80)
		 (s52 a1 s91)
		 (s52 a1 s94)
		 (s53 a0 s41)
		 (s53 a0 s75)
		 (s53 a0 s80)
		 (s53 a0 s94)
		 (s53 a1 s41)
		 (s53 a1 s42)
		 (s53 a1 s75)
		 (s53 a1 s80)
		 (s53 a1 s91)
		 (s53 a1 s94)
		 (s54 a0 s3)
		 (s54 a0 s15)
		 (s54 a0 s24)
		 (s54 a0 s32)
		 (s54 a1 s40)
		 (s54 a1 s73)
		 (s54 a1 s105)
		 (s55 a0 s41)
		 (s55 a0 s80)
		 (s55 a1 s42)
		 (s55 a1 s91)
		 (s56 a0 s12)
		 (s56 a0 s56)
		 (s56 a1 s4)
		 (s56 a1 s84)
		 (s57 a0 s7)
		 (s57 a0 s92)
		 (s57 a1 s4)
		 (s57 a1 s84)
		 (s58 a0 s1)
		 (s58 a0 s24)
		 (s58 a0 s32)
		 (s58 a0 s60)
		 (s58 a1 s40)
		 (s58 a1 s73)
		 (s58 a1 s105)
		 (s59 a0 s0)
		 (s59 a0 s41)
		 (s59 a0 s57)
		 (s59 a0 s80)
		 (s59 a1 s39)
		 (s59 a1 s42)
		 (s59 a1 s48)
		 (s59 a1 s91)
		 (s60 a1 s4)
		 (s60 a1 s20)
		 (s61 a0 s16)
		 (s61 a0 s85)
		 (s61 a1 s6)
		 (s61 a1 s16)
		 (s61 a1 s85)
		 (s62 a1 s76)
		 (s63 a1 s22)
		 (s63 a1 s27)
		 (s63 a1 s66)
		 (s64 a0 s25)
		 (s64 a0 s27)
		 (s64 a1 s42)
		 (s64 a1 s48)
		 (s65 a0 s51)
		 (s65 a1 s42)
		 (s66 a0 s85)
		 (s67 a0 s2)
		 (s67 a0 s24)
		 (s67 a0 s32)
		 (s67 a0 s46)
		 (s67 a0 s68)
		 (s67 a0 s90)
		 (s67 a0 s96)
		 (s67 a0 s98)
		 (s67 a1 s34)
		 (s67 a1 s40)
		 (s67 a1 s71)
		 (s67 a1 s73)
		 (s67 a1 s74)
		 (s67 a1 s105)
		 (s68 a1 s4)
		 (s68 a1 s7)
		 (s68 a1 s37)
		 (s69 a1 s41)
		 (s69 a1 s42)
		 (s69 a1 s75)
		 (s69 a1 s80)
		 (s69 a1 s91)
		 (s69 a1 s94)
		 (s70 a0 s25)
		 (s70 a0 s27)
		 (s70 a1 s41)
		 (s70 a1 s42)
		 (s70 a1 s94)
		 (s71 a0 s11)
		 (s71 a0 s62)
		 (s71 a0 s65)
		 (s71 a0 s77)
		 (s71 a1 s33)
		 (s71 a1 s49)
		 (s72 a0 s26)
		 (s72 a0 s62)
		 (s72 a0 s65)
		 (s72 a0 s95)
		 (s72 a1 s4)
		 (s72 a1 s7)
		 (s72 a1 s93)
		 (s73 a0 s26)
		 (s73 a0 s62)
		 (s73 a0 s65)
		 (s73 a0 s95)
		 (s73 a1 s18)
		 (s73 a1 s33)
		 (s73 a1 s54)
		 (s74 a0 s11)
		 (s74 a0 s47)
		 (s74 a0 s52)
		 (s74 a0 s62)
		 (s74 a0 s63)
		 (s74 a0 s65)
		 (s74 a0 s69)
		 (s74 a0 s77)
		 (s74 a1 s18)
		 (s74 a1 s33)
		 (s74 a1 s49)
		 (s74 a1 s54)
		 (s74 a1 s67)
		 (s74 a1 s87)
		 (s75 a0 s7)
		 (s75 a0 s53)
		 (s75 a0 s55)
		 (s75 a0 s93)
		 (s75 a1 s4)
		 (s75 a1 s7)
		 (s75 a1 s53)
		 (s75 a1 s55)
		 (s75 a1 s78)
		 (s75 a1 s93)
		 (s76 a0 s85)
		 (s77 a1 s42)
		 (s77 a1 s91)
		 (s78 a0 s41)
		 (s78 a0 s80)
		 (s79 a0 s5)
		 (s79 a0 s45)
		 (s79 a0 s79)
		 (s79 a0 s88)
		 (s79 a1 s4)
		 (s79 a1 s84)
		 (s80 a0 s7)
		 (s80 a0 s55)
		 (s80 a1 s4)
		 (s80 a1 s78)
		 (s81 a0 s11)
		 (s81 a0 s47)
		 (s81 a0 s52)
		 (s81 a0 s62)
		 (s81 a0 s63)
		 (s81 a0 s65)
		 (s81 a0 s69)
		 (s81 a0 s77)
		 (s81 a1 s4)
		 (s81 a1 s7)
		 (s81 a1 s53)
		 (s81 a1 s55)
		 (s81 a1 s78)
		 (s81 a1 s93)
		 (s82 a0 s1)
		 (s82 a0 s24)
		 (s82 a0 s32)
		 (s82 a0 s60)
		 (s82 a1 s9)
		 (s82 a1 s42)
		 (s83 a0 s7)
		 (s83 a0 s37)
		 (s83 a1 s4)
		 (s83 a1 s7)
		 (s83 a1 s93)
		 (s84 a0 s25)
		 (s84 a0 s27)
		 (s84 a1 s36)
		 (s84 a1 s61)
		 (s84 a1 s66)
		 (s85 a0 s27)
		 (s85 a1 s42)
		 (s86 a0 s2)
		 (s86 a0 s10)
		 (s86 a0 s24)
		 (s86 a0 s32)
		 (s86 a0 s38)
		 (s86 a0 s98)
		 (s86 a0 s102)
		 (s86 a0 s107)
		 (s86 a1 s34)
		 (s86 a1 s40)
		 (s86 a1 s71)
		 (s86 a1 s73)
		 (s86 a1 s74)
		 (s86 a1 s105)
		 (s87 a0 s2)
		 (s87 a0 s24)
		 (s87 a0 s32)
		 (s87 a0 s98)
		 (s87 a1 s34)
		 (s87 a1 s40)
		 (s88 a0 s100)
		 (s88 a0 s103)
		 (s88 a1 s35)
		 (s88 a1 s66)
		 (s89 a0 s64)
		 (s89 a0 s85)
		 (s89 a1 s6)
		 (s89 a1 s16)
		 (s89 a1 s85)
		 (s90 a1 s4)
		 (s90 a1 s7)
		 (s90 a1 s53)
		 (s90 a1 s55)
		 (s90 a1 s78)
		 (s90 a1 s93)
		 (s91 a0 s7)
		 (s91 a0 s55)
		 (s92 a0 s25)
		 (s92 a0 s27)
		 (s92 a1 s66)
		 (s92 a1 s89)
		 (s93 a0 s22)
		 (s93 a0 s27)
		 (s93 a1 s22)
		 (s93 a1 s27)
		 (s93 a1 s66)
		 (s94 a0 s7)
		 (s94 a0 s37)
		 (s94 a1 s4)
		 (s94 a1 s7)
		 (s94 a1 s37)
		 (s95 a1 s36)
		 (s95 a1 s61)
		 (s95 a1 s66)
		 (s96 a0 s13)
		 (s96 a0 s14)
		 (s96 a0 s28)
		 (s96 a0 s99)
		 (s96 a1 s4)
		 (s96 a1 s7)
		 (s96 a1 s53)
		 (s96 a1 s55)
		 (s96 a1 s78)
		 (s96 a1 s93)
		 (s97 a0 s25)
		 (s97 a0 s27)
		 (s97 a1 s35)
		 (s97 a1 s66)
		 (s98 a0 s14)
		 (s98 a0 s28)
		 (s98 a1 s4)
		 (s98 a1 s78)
		 (s99 a0 s2)
		 (s99 a0 s24)
		 (s99 a0 s32)
		 (s99 a0 s46)
		 (s99 a0 s68)
		 (s99 a0 s90)
		 (s99 a0 s96)
		 (s99 a0 s98)
		 (s99 a1 s41)
		 (s99 a1 s42)
		 (s99 a1 s75)
		 (s99 a1 s80)
		 (s99 a1 s91)
		 (s99 a1 s94)
		 (s100 a0 s12)
		 (s100 a1 s6)
		 (s101 a0 s3)
		 (s101 a0 s15)
		 (s101 a0 s24)
		 (s101 a0 s32)
		 (s101 a1 s41)
		 (s101 a1 s42)
		 (s101 a1 s94)
		 (s102 a0 s28)
		 (s102 a0 s104)
		 (s102 a1 s4)
		 (s102 a1 s84)
		 (s103 a0 s12)
		 (s103 a0 s56)
		 (s103 a1 s6)
		 (s103 a1 s70)
		 (s104 a0 s1)
		 (s104 a0 s24)
		 (s104 a0 s32)
		 (s104 a0 s60)
		 (s104 a1 s42)
		 (s104 a1 s48)
		 (s105 a0 s62)
		 (s105 a0 s65)
		 (s105 a1 s33)
		 (s106 a0 s5)
		 (s106 a0 s17)
		 (s106 a0 s23)
		 (s106 a0 s29)
		 (s106 a0 s30)
		 (s106 a0 s45)
		 (s106 a0 s79)
		 (s106 a0 s88)
		 (s106 a1 s33)
		 (s106 a1 s49)
		 (s106 a1 s58)
		 (s106 a1 s86)
		 (s107 a1 s4)
		 (s107 a1 s84)
		 (s108 a0 s0)
		 (s108 a0 s41)
		 (s108 a0 s57)
		 (s108 a0 s80)
		 (s108 a1 s41)
		 (s108 a1 s42)
		 (s108 a1 s75)
		 (s108 a1 s80)
		 (s108 a1 s91)
		 (s108 a1 s94)
	},
	returnTransitions = {
	}
);

NestedWordAutomaton bluegreen_RemovedNonLiveMinimizeDfa6 = (
	callAlphabet = {},
	internalAlphabet = {a0 a1 },
	returnAlphabet = {},
	states = {s0 },
	initialStates = {s0 },
	finalStates = {},
	callTransitions = {
	},
	internalTransitions = {
		 (s0 a0 s0)
		 (s0 a1 s0)
	},
	returnTransitions = {
	}
);