include('Axioms/quotient_sum^2.ax').
thf(conj_thm_2EOmega__Automata_2EDET__OMEGA__EXISTS__FORALL__THEOREM,lemma,( ! [A_27input:del]: ( ! [A_27state:del]: ( ! [V0t0:tp__ty_2Enum_2Enum] : ( ! [V1InitVal:$i] : ((mem@V1InitVal@A_27state) => ( ! [V2TransRel:$i] : ((mem@V2TransRel@(arr@(ty_2Epair_2Eprod@A_27input@A_27state)@A_27state)) => ( ! [V3i:$i] : ((mem@V3i@(arr@ty_2Enum_2Enum@A_27input)) => ( ! [V4Accept:$i] : ((mem@V4Accept@(arr@(ty_2Epair_2Eprod@(arr@ty_2Enum_2Enum@A_27input)@(arr@ty_2Enum_2Enum@A_27state))@bool)) => ((? [V5q:$i] : ((mem@V5q@(arr@ty_2Enum_2Enum@A_27state)) & (((ap@V5q@(inj__ty_2Enum_2Enum @ V0t0)) = V1InitVal) & (( ! [V6t:tp__ty_2Enum_2Enum] : ((ap@V5q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V6t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) = (ap@V2TransRel@(ap@(ap@(c_2Epair_2E_2C@A_27input@A_27state)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V6t))@(inj__ty_2Enum_2Enum @ V0t0))))@(ap@V5q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V6t))@(inj__ty_2Enum_2Enum @ V0t0))))))) & (p@(ap@V4Accept@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@A_27input)@(arr@ty_2Enum_2Enum@A_27state))@V3i)@(lam@ty_2Enum_2Enum@(^ [V7t:$i] : (ap@V5q@(ap@(ap@c_2Earithmetic_2E_2B@V7t)@(inj__ty_2Enum_2Enum @ V0t0)))))))))))) <=> ( ! [V8q:$i] : ((mem@V8q@(arr@ty_2Enum_2Enum@A_27state)) => ((((ap@V8q@(inj__ty_2Enum_2Enum @ V0t0)) = V1InitVal) & ( ! [V9t:tp__ty_2Enum_2Enum] : ((ap@V8q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V9t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) = (ap@V2TransRel@(ap@(ap@(c_2Epair_2E_2C@A_27input@A_27state)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V9t))@(inj__ty_2Enum_2Enum @ V0t0))))@(ap@V8q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V9t))@(inj__ty_2Enum_2Enum @ V0t0)))))))) => (p@(ap@V4Accept@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@A_27input)@(arr@ty_2Enum_2Enum@A_27state))@V3i)@(lam@ty_2Enum_2Enum@(^ [V10t:$i] : (ap@V8q@(ap@(ap@c_2Earithmetic_2E_2B@V10t)@(inj__ty_2Enum_2Enum @ V0t0)))))))))))))))))))))))).
thf(conj_thm_2EOmega__Automata_2ENEG__DET__AUTOMATA,lemma,( ! [A_27input:del]: ( ! [A_27state:del]: ( ! [V0t0:tp__ty_2Enum_2Enum] : ( ! [V1InitVal:$i] : ((mem@V1InitVal@A_27state) => ( ! [V2TransRel:$i] : ((mem@V2TransRel@(arr@(ty_2Epair_2Eprod@A_27input@A_27state)@A_27state)) => ( ! [V3i:$i] : ((mem@V3i@(arr@ty_2Enum_2Enum@A_27input)) => ( ! [V4Accept:$i] : ((mem@V4Accept@(arr@(ty_2Epair_2Eprod@(arr@ty_2Enum_2Enum@A_27input)@(arr@ty_2Enum_2Enum@A_27state))@bool)) => ((~~ (? [V5q:$i] : ((mem@V5q@(arr@ty_2Enum_2Enum@A_27state)) & (((ap@V5q@(inj__ty_2Enum_2Enum @ V0t0)) = V1InitVal) & (( ! [V6t:tp__ty_2Enum_2Enum] : ((ap@V5q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V6t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) = (ap@V2TransRel@(ap@(ap@(c_2Epair_2E_2C@A_27input@A_27state)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V6t))@(inj__ty_2Enum_2Enum @ V0t0))))@(ap@V5q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V6t))@(inj__ty_2Enum_2Enum @ V0t0))))))) & (p@(ap@V4Accept@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@A_27input)@(arr@ty_2Enum_2Enum@A_27state))@V3i)@(lam@ty_2Enum_2Enum@(^ [V7t:$i] : (ap@V5q@(ap@(ap@c_2Earithmetic_2E_2B@V7t)@(inj__ty_2Enum_2Enum @ V0t0))))))))))))) <=> (? [V8q:$i] : ((mem@V8q@(arr@ty_2Enum_2Enum@A_27state)) & (((ap@V8q@(inj__ty_2Enum_2Enum @ V0t0)) = V1InitVal) & (( ! [V9t:tp__ty_2Enum_2Enum] : ((ap@V8q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V9t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) = (ap@V2TransRel@(ap@(ap@(c_2Epair_2E_2C@A_27input@A_27state)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V9t))@(inj__ty_2Enum_2Enum @ V0t0))))@(ap@V8q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V9t))@(inj__ty_2Enum_2Enum @ V0t0))))))) & (~~ (p@(ap@V4Accept@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@A_27input)@(arr@ty_2Enum_2Enum@A_27state))@V3i)@(lam@ty_2Enum_2Enum@(^ [V10t:$i] : (ap@V8q@(ap@(ap@c_2Earithmetic_2E_2B@V10t)@(inj__ty_2Enum_2Enum @ V0t0)))))))))))))))))))))))))).
thf(conj_thm_2EOmega__Automata_2EOMEGA__CONJ__CLOSURE,lemma,( ! [A_27a:del]: ( ! [A_27b1:del]: ( ! [A_27b2:del]: ( ! [V0Phi__I1:$i] : ((mem@V0Phi__I1@(arr@A_27b1@bool)) => ( ! [V1t0:tp__ty_2Enum_2Enum] : ( ! [V2Phi__R1:$i] : ((mem@V2Phi__R1@(arr@(ty_2Epair_2Eprod@A_27a@A_27b1)@bool)) => ( ! [V3i:$i] : ((mem@V3i@(arr@ty_2Enum_2Enum@A_27a)) => ( ! [V4Psi1:$i] : ((mem@V4Psi1@(arr@(ty_2Epair_2Eprod@(arr@ty_2Enum_2Enum@A_27a)@(arr@ty_2Enum_2Enum@A_27b1))@bool)) => ( ! [V5Phi__I2:$i] : ((mem@V5Phi__I2@(arr@A_27b2@bool)) => ( ! [V6Phi__R2:$i] : ((mem@V6Phi__R2@(arr@(ty_2Epair_2Eprod@A_27a@A_27b2)@bool)) => ( ! [V7Psi2:$i] : ((mem@V7Psi2@(arr@(ty_2Epair_2Eprod@(arr@ty_2Enum_2Enum@A_27a)@(arr@ty_2Enum_2Enum@A_27b2))@bool)) => (((? [V8q1:$i] : ((mem@V8q1@(arr@ty_2Enum_2Enum@A_27b1)) & ((p@(ap@V0Phi__I1@(ap@V8q1@(inj__ty_2Enum_2Enum @ V1t0)))) & (( ! [V9t:tp__ty_2Enum_2Enum] : (p@(ap@V2Phi__R1@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b1)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V9t))@(inj__ty_2Enum_2Enum @ V1t0))))@(ap@V8q1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V9t))@(inj__ty_2Enum_2Enum @ V1t0))))))) & (p@(ap@V4Psi1@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@A_27a)@(arr@ty_2Enum_2Enum@A_27b1))@V3i)@V8q1))))))) & (? [V10q2:$i] : ((mem@V10q2@(arr@ty_2Enum_2Enum@A_27b2)) & ((p@(ap@V5Phi__I2@(ap@V10q2@(inj__ty_2Enum_2Enum @ V1t0)))) & (( ! [V11t:tp__ty_2Enum_2Enum] : (p@(ap@V6Phi__R2@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b2)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11t))@(inj__ty_2Enum_2Enum @ V1t0))))@(ap@V10q2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11t))@(inj__ty_2Enum_2Enum @ V1t0))))))) & (p@(ap@V7Psi2@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@A_27a)@(arr@ty_2Enum_2Enum@A_27b2))@V3i)@V10q2)))))))) <=> (? [V12q1:$i] : ((mem@V12q1@(arr@ty_2Enum_2Enum@A_27b1)) & (? [V13q2:$i] : ((mem@V13q2@(arr@ty_2Enum_2Enum@A_27b2)) & (((p@(ap@V0Phi__I1@(ap@V12q1@(inj__ty_2Enum_2Enum @ V1t0)))) & (p@(ap@V5Phi__I2@(ap@V13q2@(inj__ty_2Enum_2Enum @ V1t0))))) & (( ! [V14t:tp__ty_2Enum_2Enum] : ((p@(ap@V2Phi__R1@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b1)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t))@(inj__ty_2Enum_2Enum @ V1t0))))@(ap@V12q1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t))@(inj__ty_2Enum_2Enum @ V1t0)))))) & (p@(ap@V6Phi__R2@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b2)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t))@(inj__ty_2Enum_2Enum @ V1t0))))@(ap@V13q2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t))@(inj__ty_2Enum_2Enum @ V1t0)))))))) & ((p@(ap@V4Psi1@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@A_27a)@(arr@ty_2Enum_2Enum@A_27b1))@V3i)@V12q1))) & (p@(ap@V7Psi2@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@A_27a)@(arr@ty_2Enum_2Enum@A_27b2))@V3i)@V13q2)))))))))))))))))))))))))))))).
thf(conj_thm_2EOmega__Automata_2EOMEGA__DISJ__CLOSURE,lemma,( ! [A_27a:del]: ( ! [A_27b1:del]: ( ! [A_27b2:del]: ( ! [V0Phi__I1:$i] : ((mem@V0Phi__I1@(arr@A_27b1@bool)) => ( ! [V1t0:tp__ty_2Enum_2Enum] : ( ! [V2Phi__R1:$i] : ((mem@V2Phi__R1@(arr@(ty_2Epair_2Eprod@A_27a@A_27b1)@bool)) => ( ! [V3i:$i] : ((mem@V3i@(arr@ty_2Enum_2Enum@A_27a)) => ( ! [V4Psi1:$i] : ((mem@V4Psi1@(arr@(ty_2Epair_2Eprod@(arr@ty_2Enum_2Enum@A_27a)@(arr@ty_2Enum_2Enum@A_27b1))@bool)) => ( ! [V5Phi__I2:$i] : ((mem@V5Phi__I2@(arr@A_27b2@bool)) => ( ! [V6Phi__R2:$i] : ((mem@V6Phi__R2@(arr@(ty_2Epair_2Eprod@A_27a@A_27b2)@bool)) => ( ! [V7Psi2:$i] : ((mem@V7Psi2@(arr@(ty_2Epair_2Eprod@(arr@ty_2Enum_2Enum@A_27a)@(arr@ty_2Enum_2Enum@A_27b2))@bool)) => (((? [V8q1:$i] : ((mem@V8q1@(arr@ty_2Enum_2Enum@A_27b1)) & ((p@(ap@V0Phi__I1@(ap@V8q1@(inj__ty_2Enum_2Enum @ V1t0)))) & (( ! [V9t:tp__ty_2Enum_2Enum] : (p@(ap@V2Phi__R1@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b1)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V9t))@(inj__ty_2Enum_2Enum @ V1t0))))@(ap@V8q1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V9t))@(inj__ty_2Enum_2Enum @ V1t0))))))) & (p@(ap@V4Psi1@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@A_27a)@(arr@ty_2Enum_2Enum@A_27b1))@V3i)@V8q1))))))) | (? [V10q2:$i] : ((mem@V10q2@(arr@ty_2Enum_2Enum@A_27b2)) & ((p@(ap@V5Phi__I2@(ap@V10q2@(inj__ty_2Enum_2Enum @ V1t0)))) & (( ! [V11t:tp__ty_2Enum_2Enum] : (p@(ap@V6Phi__R2@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b2)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11t))@(inj__ty_2Enum_2Enum @ V1t0))))@(ap@V10q2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11t))@(inj__ty_2Enum_2Enum @ V1t0))))))) & (p@(ap@V7Psi2@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@A_27a)@(arr@ty_2Enum_2Enum@A_27b2))@V3i)@V10q2)))))))) <=> (? [V12p:$i] : ((mem@V12p@(arr@ty_2Enum_2Enum@bool)) & (? [V13q1:$i] : ((mem@V13q1@(arr@ty_2Enum_2Enum@A_27b1)) & (? [V14q2:$i] : ((mem@V14q2@(arr@ty_2Enum_2Enum@A_27b2)) & ((((~~ (p@(ap@V12p@(inj__ty_2Enum_2Enum @ V1t0)))) & (p@(ap@V0Phi__I1@(ap@V13q1@(inj__ty_2Enum_2Enum @ V1t0))))) | ((p@(ap@V12p@(inj__ty_2Enum_2Enum @ V1t0))) & (p@(ap@V5Phi__I2@(ap@V14q2@(inj__ty_2Enum_2Enum @ V1t0)))))) & (( ! [V15t:tp__ty_2Enum_2Enum] : (((~~ (p@(ap@V12p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V1t0))))) & ((p@(ap@V2Phi__R1@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b1)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V1t0))))@(ap@V13q1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V1t0)))))) & (~~ (p@(ap@V12p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V1t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) | ((p@(ap@V12p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V1t0)))) & ((p@(ap@V6Phi__R2@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b2)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V1t0))))@(ap@V14q2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V1t0)))))) & (p@(ap@V12p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V1t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) & (((~~ (p@(ap@V12p@(inj__ty_2Enum_2Enum @ V1t0)))) & (p@(ap@V4Psi1@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@A_27a)@(arr@ty_2Enum_2Enum@A_27b1))@V3i)@V13q1)))) | ((p@(ap@V12p@(inj__ty_2Enum_2Enum @ V1t0))) & (p@(ap@V7Psi2@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@A_27a)@(arr@ty_2Enum_2Enum@A_27b2))@V3i)@V14q2))))))))))))))))))))))))))))))))).
thf(conj_thm_2EOmega__Automata_2EBOOLEAN__CLOSURE__G,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1t0:tp__ty_2Enum_2Enum] : ( ! [V2b:$i] : ((mem@V2b@(arr@ty_2Enum_2Enum@bool)) => (((~~ ( ! [V3t:tp__ty_2Enum_2Enum] : (p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V3t))@(inj__ty_2Enum_2Enum @ V1t0)))))) <=> (? [V4t:tp__ty_2Enum_2Enum] : (~~ (p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V1t0))))))) & (((( ! [V5t:tp__ty_2Enum_2Enum] : (p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t))@(inj__ty_2Enum_2Enum @ V1t0))))) & ( ! [V6t:tp__ty_2Enum_2Enum] : (p@(ap@V2b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V6t))@(inj__ty_2Enum_2Enum @ V1t0)))))) <=> ( ! [V7t:tp__ty_2Enum_2Enum] : ((p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V7t))@(inj__ty_2Enum_2Enum @ V1t0)))) & (p@(ap@V2b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V7t))@(inj__ty_2Enum_2Enum @ V1t0))))))) & ((( ! [V8t:tp__ty_2Enum_2Enum] : (p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V8t))@(inj__ty_2Enum_2Enum @ V1t0))))) | ( ! [V9t:tp__ty_2Enum_2Enum] : (p@(ap@V2b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V9t))@(inj__ty_2Enum_2Enum @ V1t0)))))) <=> (? [V10p:$i] : ((mem@V10p@(arr@ty_2Enum_2Enum@bool)) & (? [V11q:$i] : ((mem@V11q@(arr@ty_2Enum_2Enum@bool)) & (((~~ (p@(ap@V10p@(inj__ty_2Enum_2Enum @ V1t0)))) & (~~ (p@(ap@V11q@(inj__ty_2Enum_2Enum @ V1t0))))) & (( ! [V12t:tp__ty_2Enum_2Enum] : (((p@(ap@V10p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V12t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V1t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) <=> ((p@(ap@V10p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V12t))@(inj__ty_2Enum_2Enum @ V1t0)))) | (~~ (p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V12t))@(inj__ty_2Enum_2Enum @ V1t0))))))) & ((p@(ap@V11q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V12t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V1t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) <=> ((p@(ap@V11q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V12t))@(inj__ty_2Enum_2Enum @ V1t0)))) | (~~ (p@(ap@V2b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V12t))@(inj__ty_2Enum_2Enum @ V1t0))))))))) & ( ! [V13t:tp__ty_2Enum_2Enum] : ((~~ (p@(ap@V10p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V13t))@(inj__ty_2Enum_2Enum @ V1t0))))) | (~~ (p@(ap@V11q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V13t))@(inj__ty_2Enum_2Enum @ V1t0)))))))))))))))))))))).
thf(conj_thm_2EOmega__Automata_2EBOOLEAN__CLOSURE__F,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1t0:tp__ty_2Enum_2Enum] : ( ! [V2b:$i] : ((mem@V2b@(arr@ty_2Enum_2Enum@bool)) => (((~~ (? [V3t:tp__ty_2Enum_2Enum] : (p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V3t))@(inj__ty_2Enum_2Enum @ V1t0)))))) <=> ( ! [V4t:tp__ty_2Enum_2Enum] : (~~ (p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V1t0))))))) & ((((? [V5t:tp__ty_2Enum_2Enum] : (p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t))@(inj__ty_2Enum_2Enum @ V1t0))))) | (? [V6t:tp__ty_2Enum_2Enum] : (p@(ap@V2b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V6t))@(inj__ty_2Enum_2Enum @ V1t0)))))) <=> (? [V7t:tp__ty_2Enum_2Enum] : ((p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V7t))@(inj__ty_2Enum_2Enum @ V1t0)))) | (p@(ap@V2b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V7t))@(inj__ty_2Enum_2Enum @ V1t0))))))) & (((? [V8t:tp__ty_2Enum_2Enum] : (p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V8t))@(inj__ty_2Enum_2Enum @ V1t0))))) & (? [V9t:tp__ty_2Enum_2Enum] : (p@(ap@V2b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V9t))@(inj__ty_2Enum_2Enum @ V1t0)))))) <=> (? [V10p:$i] : ((mem@V10p@(arr@ty_2Enum_2Enum@bool)) & (? [V11q:$i] : ((mem@V11q@(arr@ty_2Enum_2Enum@bool)) & (((~~ (p@(ap@V10p@(inj__ty_2Enum_2Enum @ V1t0)))) & (~~ (p@(ap@V11q@(inj__ty_2Enum_2Enum @ V1t0))))) & (( ! [V12t:tp__ty_2Enum_2Enum] : (((p@(ap@V10p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V12t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V1t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) <=> ((p@(ap@V10p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V12t))@(inj__ty_2Enum_2Enum @ V1t0)))) | (p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V12t))@(inj__ty_2Enum_2Enum @ V1t0)))))) & ((p@(ap@V11q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V12t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V1t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) <=> ((p@(ap@V11q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V12t))@(inj__ty_2Enum_2Enum @ V1t0)))) | (p@(ap@V2b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V12t))@(inj__ty_2Enum_2Enum @ V1t0)))))))) & (? [V13t:tp__ty_2Enum_2Enum] : ((p@(ap@V10p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V13t))@(inj__ty_2Enum_2Enum @ V1t0)))) & (p@(ap@V11q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V13t))@(inj__ty_2Enum_2Enum @ V1t0))))))))))))))))))))).
thf(conj_thm_2EOmega__Automata_2EBOOLEAN__CLOSURE__FG,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1t0:tp__ty_2Enum_2Enum] : ( ! [V2b:$i] : ((mem@V2b@(arr@ty_2Enum_2Enum@bool)) => (((~~ (? [V3t1:tp__ty_2Enum_2Enum] : ( ! [V4t2:tp__ty_2Enum_2Enum] : (p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V3t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t2))@(inj__ty_2Enum_2Enum @ V1t0)))))))) <=> ( ! [V5t1:tp__ty_2Enum_2Enum] : (? [V6t2:tp__ty_2Enum_2Enum] : (~~ (p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V6t2))@(inj__ty_2Enum_2Enum @ V1t0))))))))) & ((((? [V7t1:tp__ty_2Enum_2Enum] : ( ! [V8t2:tp__ty_2Enum_2Enum] : (p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V7t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V8t2))@(inj__ty_2Enum_2Enum @ V1t0))))))) & (? [V9t1:tp__ty_2Enum_2Enum] : ( ! [V10t2:tp__ty_2Enum_2Enum] : (p@(ap@V2b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V9t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V10t2))@(inj__ty_2Enum_2Enum @ V1t0)))))))) <=> (? [V11t1:tp__ty_2Enum_2Enum] : ( ! [V12t2:tp__ty_2Enum_2Enum] : ((p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V12t2))@(inj__ty_2Enum_2Enum @ V1t0))))) & (p@(ap@V2b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V12t2))@(inj__ty_2Enum_2Enum @ V1t0))))))))) & (((? [V13t1:tp__ty_2Enum_2Enum] : ( ! [V14t2:tp__ty_2Enum_2Enum] : (p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V13t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t2))@(inj__ty_2Enum_2Enum @ V1t0))))))) | (? [V15t1:tp__ty_2Enum_2Enum] : ( ! [V16t2:tp__ty_2Enum_2Enum] : (p@(ap@V2b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V16t2))@(inj__ty_2Enum_2Enum @ V1t0)))))))) <=> (? [V17q:$i] : ((mem@V17q@(arr@ty_2Enum_2Enum@bool)) & ((~~ (p@(ap@V17q@(inj__ty_2Enum_2Enum @ V1t0)))) & (( ! [V18t:tp__ty_2Enum_2Enum] : ((p@(ap@V17q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V18t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V1t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) <=> (p@(ap@(ap@(ap@(c_2Ebool_2ECOND@bool)@(ap@V17q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V18t))@(inj__ty_2Enum_2Enum @ V1t0))))@(ap@V2b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V18t))@(inj__ty_2Enum_2Enum @ V1t0))))@(ap@c_2Ebool_2E_7E@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V18t))@(inj__ty_2Enum_2Enum @ V1t0)))))))) & (? [V19t1:tp__ty_2Enum_2Enum] : ( ! [V20t2:tp__ty_2Enum_2Enum] : ((~~ (p@(ap@V17q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V19t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V20t2))@(inj__ty_2Enum_2Enum @ V1t0)))))) | (p@(ap@V2b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V19t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V20t2))@(inj__ty_2Enum_2Enum @ V1t0))))))))))))))))))))).
thf(conj_thm_2EOmega__Automata_2EBOOLEAN__CLOSURE__GF,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1t0:tp__ty_2Enum_2Enum] : ( ! [V2b:$i] : ((mem@V2b@(arr@ty_2Enum_2Enum@bool)) => (((~~ ( ! [V3t1:tp__ty_2Enum_2Enum] : (? [V4t2:tp__ty_2Enum_2Enum] : (p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V3t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t2))@(inj__ty_2Enum_2Enum @ V1t0)))))))) <=> (? [V5t1:tp__ty_2Enum_2Enum] : ( ! [V6t2:tp__ty_2Enum_2Enum] : (~~ (p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V6t2))@(inj__ty_2Enum_2Enum @ V1t0))))))))) & (((( ! [V7t1:tp__ty_2Enum_2Enum] : (? [V8t2:tp__ty_2Enum_2Enum] : (p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V7t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V8t2))@(inj__ty_2Enum_2Enum @ V1t0))))))) | ( ! [V9t1:tp__ty_2Enum_2Enum] : (? [V10t2:tp__ty_2Enum_2Enum] : (p@(ap@V2b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V9t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V10t2))@(inj__ty_2Enum_2Enum @ V1t0)))))))) <=> ( ! [V11t1:tp__ty_2Enum_2Enum] : (? [V12t2:tp__ty_2Enum_2Enum] : ((p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V12t2))@(inj__ty_2Enum_2Enum @ V1t0))))) | (p@(ap@V2b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V12t2))@(inj__ty_2Enum_2Enum @ V1t0))))))))) & ((( ! [V13t1:tp__ty_2Enum_2Enum] : (? [V14t2:tp__ty_2Enum_2Enum] : (p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V13t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t2))@(inj__ty_2Enum_2Enum @ V1t0))))))) & ( ! [V15t1:tp__ty_2Enum_2Enum] : (? [V16t2:tp__ty_2Enum_2Enum] : (p@(ap@V2b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V16t2))@(inj__ty_2Enum_2Enum @ V1t0)))))))) <=> (? [V17q:$i] : ((mem@V17q@(arr@ty_2Enum_2Enum@bool)) & ((~~ (p@(ap@V17q@(inj__ty_2Enum_2Enum @ V1t0)))) & (( ! [V18t:tp__ty_2Enum_2Enum] : ((p@(ap@V17q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V18t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V1t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) <=> (p@(ap@(ap@(ap@(c_2Ebool_2ECOND@bool)@(ap@V17q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V18t))@(inj__ty_2Enum_2Enum @ V1t0))))@(ap@c_2Ebool_2E_7E@(ap@V2b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V18t))@(inj__ty_2Enum_2Enum @ V1t0)))))@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V18t))@(inj__ty_2Enum_2Enum @ V1t0))))))) & ( ! [V19t1:tp__ty_2Enum_2Enum] : (? [V20t2:tp__ty_2Enum_2Enum] : ((p@(ap@V17q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V19t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V20t2))@(inj__ty_2Enum_2Enum @ V1t0))))) & (p@(ap@V2b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V19t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V20t2))@(inj__ty_2Enum_2Enum @ V1t0))))))))))))))))))))).
thf(conj_thm_2EOmega__Automata_2EBOREL__HIERARCHY__G,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1t0:tp__ty_2Enum_2Enum] : ((( ! [V2t:tp__ty_2Enum_2Enum] : (p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V2t))@(inj__ty_2Enum_2Enum @ V1t0))))) <=> (? [V3q:$i] : ((mem@V3q@(arr@ty_2Enum_2Enum@bool)) & ((p@(ap@V3q@(inj__ty_2Enum_2Enum @ V1t0))) & (( ! [V4t:tp__ty_2Enum_2Enum] : ((p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V1t0)))) & ((p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V1t0)))) & (p@(ap@V3q@(ap@c_2Enum_2ESUC@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V1t0)))))))) & (? [V5t:tp__ty_2Enum_2Enum] : (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t))@(inj__ty_2Enum_2Enum @ V1t0)))))))))) & ((( ! [V6t:tp__ty_2Enum_2Enum] : (p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V6t))@(inj__ty_2Enum_2Enum @ V1t0))))) <=> (? [V7q:$i] : ((mem@V7q@(arr@ty_2Enum_2Enum@bool)) & ((p@(ap@V7q@(inj__ty_2Enum_2Enum @ V1t0))) & (( ! [V8t:tp__ty_2Enum_2Enum] : ((p@(ap@V7q@(ap@c_2Enum_2ESUC@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V8t))@(inj__ty_2Enum_2Enum @ V1t0))))) <=> ((p@(ap@V7q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V8t))@(inj__ty_2Enum_2Enum @ V1t0)))) & (p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V8t))@(inj__ty_2Enum_2Enum @ V1t0))))))) & (? [V9t1:tp__ty_2Enum_2Enum] : ( ! [V10t2:tp__ty_2Enum_2Enum] : (p@(ap@V7q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V9t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V10t2))@(inj__ty_2Enum_2Enum @ V1t0)))))))))))) & (( ! [V11t:tp__ty_2Enum_2Enum] : (p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11t))@(inj__ty_2Enum_2Enum @ V1t0))))) <=> (? [V12q:$i] : ((mem@V12q@(arr@ty_2Enum_2Enum@bool)) & ((p@(ap@V12q@(inj__ty_2Enum_2Enum @ V1t0))) & (( ! [V13t:tp__ty_2Enum_2Enum] : ((p@(ap@V12q@(ap@c_2Enum_2ESUC@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V13t))@(inj__ty_2Enum_2Enum @ V1t0))))) <=> ((p@(ap@V12q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V13t))@(inj__ty_2Enum_2Enum @ V1t0)))) & (p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V13t))@(inj__ty_2Enum_2Enum @ V1t0))))))) & ( ! [V14t1:tp__ty_2Enum_2Enum] : (? [V15t2:tp__ty_2Enum_2Enum] : (p@(ap@V12q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t2))@(inj__ty_2Enum_2Enum @ V1t0)))))))))))))))))).
thf(conj_thm_2EOmega__Automata_2EBOREL__HIERARCHY__F,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1t0:tp__ty_2Enum_2Enum] : (((? [V2t:tp__ty_2Enum_2Enum] : (p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V2t))@(inj__ty_2Enum_2Enum @ V1t0))))) <=> (? [V3q:$i] : ((mem@V3q@(arr@ty_2Enum_2Enum@bool)) & ((~~ (p@(ap@V3q@(inj__ty_2Enum_2Enum @ V1t0)))) & (( ! [V4t:tp__ty_2Enum_2Enum] : ((p@(ap@V3q@(ap@c_2Enum_2ESUC@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V1t0))))) <=> ((p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V1t0)))) | (p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V1t0))))))) & (? [V5t1:tp__ty_2Enum_2Enum] : ( ! [V6t2:tp__ty_2Enum_2Enum] : (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V6t2))@(inj__ty_2Enum_2Enum @ V1t0)))))))))))) & ((? [V7t:tp__ty_2Enum_2Enum] : (p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V7t))@(inj__ty_2Enum_2Enum @ V1t0))))) <=> (? [V8q:$i] : ((mem@V8q@(arr@ty_2Enum_2Enum@bool)) & ((~~ (p@(ap@V8q@(inj__ty_2Enum_2Enum @ V1t0)))) & (( ! [V9t:tp__ty_2Enum_2Enum] : ((p@(ap@V8q@(ap@c_2Enum_2ESUC@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V9t))@(inj__ty_2Enum_2Enum @ V1t0))))) <=> ((p@(ap@V8q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V9t))@(inj__ty_2Enum_2Enum @ V1t0)))) | (p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V9t))@(inj__ty_2Enum_2Enum @ V1t0))))))) & ( ! [V10t1:tp__ty_2Enum_2Enum] : (? [V11t2:tp__ty_2Enum_2Enum] : (p@(ap@V8q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V10t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11t2))@(inj__ty_2Enum_2Enum @ V1t0))))))))))))))))).
thf(conj_thm_2EOmega__Automata_2EBOREL__HIERARCHY__FG,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1t0:tp__ty_2Enum_2Enum] : (((? [V2t1:tp__ty_2Enum_2Enum] : ( ! [V3t2:tp__ty_2Enum_2Enum] : (p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V2t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V3t2))@(inj__ty_2Enum_2Enum @ V1t0))))))) <=> (? [V4q:$i] : ((mem@V4q@(arr@ty_2Enum_2Enum@bool)) & ((~~ (p@(ap@V4q@(inj__ty_2Enum_2Enum @ V1t0)))) & (( ! [V5t:tp__ty_2Enum_2Enum] : ((p@(ap@V4q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t))@(inj__ty_2Enum_2Enum @ V1t0)))) => ((p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t))@(inj__ty_2Enum_2Enum @ V1t0)))) & (p@(ap@V4q@(ap@c_2Enum_2ESUC@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t))@(inj__ty_2Enum_2Enum @ V1t0)))))))) & (? [V6t:tp__ty_2Enum_2Enum] : (p@(ap@V4q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V6t))@(inj__ty_2Enum_2Enum @ V1t0)))))))))) & ((? [V7t1:tp__ty_2Enum_2Enum] : ( ! [V8t2:tp__ty_2Enum_2Enum] : (p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V7t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V8t2))@(inj__ty_2Enum_2Enum @ V1t0))))))) <=> (? [V9p:$i] : ((mem@V9p@(arr@ty_2Enum_2Enum@bool)) & (? [V10q:$i] : ((mem@V10q@(arr@ty_2Enum_2Enum@bool)) & (((~~ (p@(ap@V9p@(inj__ty_2Enum_2Enum @ V1t0)))) & (~~ (p@(ap@V10q@(inj__ty_2Enum_2Enum @ V1t0))))) & (( ! [V11t:tp__ty_2Enum_2Enum] : (((p@(ap@V9p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11t))@(inj__ty_2Enum_2Enum @ V1t0)))) => (p@(ap@V9p@(ap@c_2Enum_2ESUC@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11t))@(inj__ty_2Enum_2Enum @ V1t0)))))) & (((p@(ap@V9p@(ap@c_2Enum_2ESUC@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11t))@(inj__ty_2Enum_2Enum @ V1t0))))) => ((p@(ap@V9p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11t))@(inj__ty_2Enum_2Enum @ V1t0)))) | (~~ (p@(ap@V10q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11t))@(inj__ty_2Enum_2Enum @ V1t0))))))) & ((p@(ap@V10q@(ap@c_2Enum_2ESUC@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11t))@(inj__ty_2Enum_2Enum @ V1t0))))) <=> (((p@(ap@V9p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11t))@(inj__ty_2Enum_2Enum @ V1t0)))) & ((~~ (p@(ap@V10q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11t))@(inj__ty_2Enum_2Enum @ V1t0))))) & (~~ (p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11t))@(inj__ty_2Enum_2Enum @ V1t0))))))) | ((p@(ap@V9p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11t))@(inj__ty_2Enum_2Enum @ V1t0)))) & (p@(ap@V10q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11t))@(inj__ty_2Enum_2Enum @ V1t0)))))))))) & ( ! [V12t1:tp__ty_2Enum_2Enum] : (? [V13t2:tp__ty_2Enum_2Enum] : ((p@(ap@V9p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V12t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V13t2))@(inj__ty_2Enum_2Enum @ V1t0))))) & (~~ (p@(ap@V10q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V12t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V13t2))@(inj__ty_2Enum_2Enum @ V1t0))))))))))))))))))))).
thf(conj_thm_2EOmega__Automata_2ETEMP__OPS__DEFS__TO__OMEGA,lemma,( ! [V0l:$i] : ((mem@V0l@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1a:$i] : ((mem@V1a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V2b:$i] : ((mem@V2b@(arr@ty_2Enum_2Enum@bool)) => (((V0l = (ap@c_2ETemporal__Logic_2ENEXT@V1a)) <=> ($true & (( ! [V3t:tp__ty_2Enum_2Enum] : ((p@(ap@V0l@(inj__ty_2Enum_2Enum @ V3t))) <=> (p@(ap@V1a@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V3t)))))) & $true))) & (((V0l = (ap@c_2ETemporal__Logic_2EALWAYS@V1a)) <=> ($true & (( ! [V4t:tp__ty_2Enum_2Enum] : ((p@(ap@V0l@(inj__ty_2Enum_2Enum @ V4t))) <=> ((p@(ap@V1a@(inj__ty_2Enum_2Enum @ V4t))) & (p@(ap@V0l@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V4t))))))) & ( ! [V5t1:tp__ty_2Enum_2Enum] : (? [V6t2:tp__ty_2Enum_2Enum] : ((p@(ap@V1a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t1))@(inj__ty_2Enum_2Enum @ V6t2)))) => (p@(ap@V0l@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t1))@(inj__ty_2Enum_2Enum @ V6t2)))))))))) & (((V0l = (ap@c_2ETemporal__Logic_2EEVENTUAL@V1a)) <=> ($true & (( ! [V7t:tp__ty_2Enum_2Enum] : ((p@(ap@V0l@(inj__ty_2Enum_2Enum @ V7t))) <=> ((p@(ap@V1a@(inj__ty_2Enum_2Enum @ V7t))) | (p@(ap@V0l@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V7t))))))) & ( ! [V8t1:tp__ty_2Enum_2Enum] : (? [V9t2:tp__ty_2Enum_2Enum] : ((p@(ap@V0l@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V8t1))@(inj__ty_2Enum_2Enum @ V9t2)))) => (p@(ap@V1a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V8t1))@(inj__ty_2Enum_2Enum @ V9t2)))))))))) & (((V0l = (ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V1a)@V2b)) <=> ($true & (( ! [V10t:tp__ty_2Enum_2Enum] : ((p@(ap@V0l@(inj__ty_2Enum_2Enum @ V10t))) <=> ((~~ (p@(ap@V2b@(inj__ty_2Enum_2Enum @ V10t)))) => ((p@(ap@V1a@(inj__ty_2Enum_2Enum @ V10t))) & (p@(ap@V0l@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V10t)))))))) & ( ! [V11t1:tp__ty_2Enum_2Enum] : (? [V12t2:tp__ty_2Enum_2Enum] : ((p@(ap@V0l@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11t1))@(inj__ty_2Enum_2Enum @ V12t2)))) => ((~~ (p@(ap@V1a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11t1))@(inj__ty_2Enum_2Enum @ V12t2))))) | (p@(ap@V2b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11t1))@(inj__ty_2Enum_2Enum @ V12t2))))))))))) & (((V0l = (ap@(ap@c_2ETemporal__Logic_2ESWHEN@V1a)@V2b)) <=> ($true & (( ! [V13t:tp__ty_2Enum_2Enum] : ((p@(ap@V0l@(inj__ty_2Enum_2Enum @ V13t))) <=> (p@(ap@(ap@(ap@(c_2Ebool_2ECOND@bool)@(ap@V2b@(inj__ty_2Enum_2Enum @ V13t)))@(ap@V1a@(inj__ty_2Enum_2Enum @ V13t)))@(ap@V0l@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V13t))))))) & ( ! [V14t1:tp__ty_2Enum_2Enum] : (? [V15t2:tp__ty_2Enum_2Enum] : ((p@(ap@V0l@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t1))@(inj__ty_2Enum_2Enum @ V15t2)))) => (p@(ap@V2b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t1))@(inj__ty_2Enum_2Enum @ V15t2)))))))))) & (((V0l = (ap@(ap@c_2ETemporal__Logic_2ESBEFORE@V1a)@V2b)) <=> ($true & (( ! [V16t:tp__ty_2Enum_2Enum] : ((p@(ap@V0l@(inj__ty_2Enum_2Enum @ V16t))) <=> ((~~ (p@(ap@V2b@(inj__ty_2Enum_2Enum @ V16t)))) & ((p@(ap@V1a@(inj__ty_2Enum_2Enum @ V16t))) | (p@(ap@V0l@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V16t)))))))) & ( ! [V17t1:tp__ty_2Enum_2Enum] : (? [V18t2:tp__ty_2Enum_2Enum] : ((p@(ap@V0l@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V17t1))@(inj__ty_2Enum_2Enum @ V18t2)))) => ((p@(ap@V1a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V17t1))@(inj__ty_2Enum_2Enum @ V18t2)))) | (p@(ap@V2b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V17t1))@(inj__ty_2Enum_2Enum @ V18t2))))))))))) & (((V0l = (ap@(ap@c_2ETemporal__Logic_2EUNTIL@V1a)@V2b)) <=> ($true & (( ! [V19t:tp__ty_2Enum_2Enum] : ((p@(ap@V0l@(inj__ty_2Enum_2Enum @ V19t))) <=> ((~~ (p@(ap@V2b@(inj__ty_2Enum_2Enum @ V19t)))) => ((p@(ap@V1a@(inj__ty_2Enum_2Enum @ V19t))) & (p@(ap@V0l@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V19t)))))))) & ( ! [V20t1:tp__ty_2Enum_2Enum] : (? [V21t2:tp__ty_2Enum_2Enum] : ((~~ (p@(ap@V0l@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V20t1))@(inj__ty_2Enum_2Enum @ V21t2))))) => ((~~ (p@(ap@V1a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V20t1))@(inj__ty_2Enum_2Enum @ V21t2))))) | (p@(ap@V2b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V20t1))@(inj__ty_2Enum_2Enum @ V21t2))))))))))) & (((V0l = (ap@(ap@c_2ETemporal__Logic_2EWHEN@V1a)@V2b)) <=> ($true & (( ! [V22t:tp__ty_2Enum_2Enum] : ((p@(ap@V0l@(inj__ty_2Enum_2Enum @ V22t))) <=> (p@(ap@(ap@(ap@(c_2Ebool_2ECOND@bool)@(ap@V2b@(inj__ty_2Enum_2Enum @ V22t)))@(ap@V1a@(inj__ty_2Enum_2Enum @ V22t)))@(ap@V0l@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V22t))))))) & ( ! [V23t1:tp__ty_2Enum_2Enum] : (? [V24t2:tp__ty_2Enum_2Enum] : ((p@(ap@V0l@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V23t1))@(inj__ty_2Enum_2Enum @ V24t2)))) | (p@(ap@V2b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V23t1))@(inj__ty_2Enum_2Enum @ V24t2)))))))))) & (((V0l = (ap@(ap@c_2ETemporal__Logic_2EBEFORE@V1a)@V2b)) <=> ($true & (( ! [V25t:tp__ty_2Enum_2Enum] : ((p@(ap@V0l@(inj__ty_2Enum_2Enum @ V25t))) <=> ((~~ (p@(ap@V2b@(inj__ty_2Enum_2Enum @ V25t)))) & ((p@(ap@V1a@(inj__ty_2Enum_2Enum @ V25t))) | (p@(ap@V0l@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V25t)))))))) & ( ! [V26t1:tp__ty_2Enum_2Enum] : (? [V27t2:tp__ty_2Enum_2Enum] : ((~~ (p@(ap@V0l@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V26t1))@(inj__ty_2Enum_2Enum @ V27t2))))) => ((p@(ap@V1a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V26t1))@(inj__ty_2Enum_2Enum @ V27t2)))) | (p@(ap@V2b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V26t1))@(inj__ty_2Enum_2Enum @ V27t2))))))))))) & (((V0l = (ap@c_2EPast__Temporal__Logic_2EPNEXT@V1a)) <=> (((p@(ap@V0l@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) <=> $true) & (( ! [V28t:tp__ty_2Enum_2Enum] : ((p@(ap@V0l@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V28t)))) <=> (p@(ap@V1a@(inj__ty_2Enum_2Enum @ V28t))))) & $true))) & (((V0l = (ap@c_2EPast__Temporal__Logic_2EPSNEXT@V1a)) <=> (((p@(ap@V0l@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) <=> $false) & (( ! [V29t:tp__ty_2Enum_2Enum] : ((p@(ap@V0l@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V29t)))) <=> (p@(ap@V1a@(inj__ty_2Enum_2Enum @ V29t))))) & $true))) & (((V0l = (ap@c_2EPast__Temporal__Logic_2EPNEXT@(ap@c_2EPast__Temporal__Logic_2EPALWAYS@V1a))) <=> (((p@(ap@V0l@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) <=> $true) & (( ! [V30t:tp__ty_2Enum_2Enum] : ((p@(ap@V0l@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V30t)))) <=> ((p@(ap@V1a@(inj__ty_2Enum_2Enum @ V30t))) & (p@(ap@V0l@(inj__ty_2Enum_2Enum @ V30t)))))) & $true))) & (((V0l = (ap@c_2EPast__Temporal__Logic_2EPSNEXT@(ap@c_2EPast__Temporal__Logic_2EPEVENTUAL@V1a))) <=> (((p@(ap@V0l@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) <=> $false) & (( ! [V31t:tp__ty_2Enum_2Enum] : ((p@(ap@V0l@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V31t)))) <=> ((p@(ap@V1a@(inj__ty_2Enum_2Enum @ V31t))) | (p@(ap@V0l@(inj__ty_2Enum_2Enum @ V31t)))))) & $true))) & (((V0l = (ap@c_2EPast__Temporal__Logic_2EPSNEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V1a)@V2b))) <=> (((p@(ap@V0l@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) <=> $false) & (( ! [V32t:tp__ty_2Enum_2Enum] : ((p@(ap@V0l@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V32t)))) <=> ((p@(ap@V2b@(inj__ty_2Enum_2Enum @ V32t))) | ((p@(ap@V1a@(inj__ty_2Enum_2Enum @ V32t))) & (p@(ap@V0l@(inj__ty_2Enum_2Enum @ V32t))))))) & $true))) & (((V0l = (ap@c_2EPast__Temporal__Logic_2EPSNEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@V1a)@V2b))) <=> (((p@(ap@V0l@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) <=> $false) & (( ! [V33t:tp__ty_2Enum_2Enum] : ((p@(ap@V0l@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V33t)))) <=> (((p@(ap@V1a@(inj__ty_2Enum_2Enum @ V33t))) & (p@(ap@V2b@(inj__ty_2Enum_2Enum @ V33t)))) | ((~~ (p@(ap@V2b@(inj__ty_2Enum_2Enum @ V33t)))) & (p@(ap@V0l@(inj__ty_2Enum_2Enum @ V33t))))))) & $true))) & (((V0l = (ap@c_2EPast__Temporal__Logic_2EPSNEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V1a)@V2b))) <=> (((p@(ap@V0l@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) <=> $false) & (( ! [V34t:tp__ty_2Enum_2Enum] : ((p@(ap@V0l@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V34t)))) <=> ((~~ (p@(ap@V2b@(inj__ty_2Enum_2Enum @ V34t)))) & ((p@(ap@V1a@(inj__ty_2Enum_2Enum @ V34t))) | (p@(ap@V0l@(inj__ty_2Enum_2Enum @ V34t))))))) & $true))) & (((V0l = (ap@c_2EPast__Temporal__Logic_2EPNEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@V1a)@V2b))) <=> (((p@(ap@V0l@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) <=> $true) & (( ! [V35t:tp__ty_2Enum_2Enum] : ((p@(ap@V0l@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V35t)))) <=> ((p@(ap@V2b@(inj__ty_2Enum_2Enum @ V35t))) | ((p@(ap@V1a@(inj__ty_2Enum_2Enum @ V35t))) & (p@(ap@V0l@(inj__ty_2Enum_2Enum @ V35t))))))) & $true))) & (((V0l = (ap@c_2EPast__Temporal__Logic_2EPNEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@V1a)@V2b))) <=> (((p@(ap@V0l@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) <=> $true) & (( ! [V36t:tp__ty_2Enum_2Enum] : ((p@(ap@V0l@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V36t)))) <=> (((p@(ap@V1a@(inj__ty_2Enum_2Enum @ V36t))) & (p@(ap@V2b@(inj__ty_2Enum_2Enum @ V36t)))) | ((~~ (p@(ap@V2b@(inj__ty_2Enum_2Enum @ V36t)))) & (p@(ap@V0l@(inj__ty_2Enum_2Enum @ V36t))))))) & $true))) & ((V0l = (ap@c_2EPast__Temporal__Logic_2EPNEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V1a)@V2b))) <=> (((p@(ap@V0l@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) <=> $true) & (( ! [V37t:tp__ty_2Enum_2Enum] : ((p@(ap@V0l@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V37t)))) <=> ((~~ (p@(ap@V2b@(inj__ty_2Enum_2Enum @ V37t)))) & ((p@(ap@V1a@(inj__ty_2Enum_2Enum @ V37t))) | (p@(ap@V0l@(inj__ty_2Enum_2Enum @ V37t))))))) & $true)))))))))))))))))))))))))))).
thf(conj_thm_2EOmega__Automata_2EAUTOMATON__TEMP__CLOSURE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0Phi__I1:$i] : ((mem@V0Phi__I1@(arr@(arr@ty_2Enum_2Enum@A_27a)@bool)) => ( ! [V1Phi__R1:$i] : ((mem@V1Phi__R1@(arr@(arr@ty_2Enum_2Enum@A_27a)@bool)) => ( ! [V2Phi__I2:$i] : ((mem@V2Phi__I2@(arr@(arr@ty_2Enum_2Enum@A_27b)@bool)) => ( ! [V3Phi__R2:$i] : ((mem@V3Phi__R2@(arr@(ty_2Epair_2Eprod@(arr@ty_2Enum_2Enum@A_27b)@(arr@ty_2Enum_2Enum@A_27a))@bool)) => ( ! [V4Phi__F:$i] : ((mem@V4Phi__F@(arr@(ty_2Epair_2Eprod@(arr@ty_2Enum_2Enum@A_27a)@(arr@ty_2Enum_2Enum@A_27b))@bool)) => ( ! [V5Phi:$i] : ((mem@V5Phi@(arr@(arr@ty_2Enum_2Enum@bool)@bool)) => ( ! [V6phi:$i] : ((mem@V6phi@(arr@ty_2Enum_2Enum@bool)) => ( ! [V7a:$i] : ((mem@V7a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V8b:$i] : ((mem@V8b@(arr@ty_2Enum_2Enum@bool)) => (((? [V9q1:$i] : ((mem@V9q1@(arr@ty_2Enum_2Enum@A_27a)) & ((p@(ap@V0Phi__I1@V9q1)) & ((p@(ap@V1Phi__R1@V9q1)) & (? [V10q2:$i] : ((mem@V10q2@(arr@ty_2Enum_2Enum@A_27b)) & ((p@(ap@V2Phi__I2@V10q2)) & ((p@(ap@V3Phi__R2@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@A_27b)@(arr@ty_2Enum_2Enum@A_27a))@V10q2)@V9q1))) & (p@(ap@V4Phi__F@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@A_27a)@(arr@ty_2Enum_2Enum@A_27b))@V9q1)@V10q2))))))))))) <=> (? [V11q1:$i] : ((mem@V11q1@(arr@ty_2Enum_2Enum@A_27a)) & (? [V12q2:$i] : ((mem@V12q2@(arr@ty_2Enum_2Enum@A_27b)) & (((p@(ap@V0Phi__I1@V11q1)) & (p@(ap@V2Phi__I2@V12q2))) & (((p@(ap@V1Phi__R1@V11q1)) & (p@(ap@V3Phi__R2@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@A_27b)@(arr@ty_2Enum_2Enum@A_27a))@V12q2)@V11q1)))) & (p@(ap@V4Phi__F@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@A_27a)@(arr@ty_2Enum_2Enum@A_27b))@V11q1)@V12q2)))))))))) & (((p@(ap@V5Phi@(ap@c_2ETemporal__Logic_2ENEXT@V6phi))) <=> (? [V13q0:$i] : ((mem@V13q0@(arr@ty_2Enum_2Enum@bool)) & (? [V14q1:$i] : ((mem@V14q1@(arr@ty_2Enum_2Enum@bool)) & ($true & (( ! [V15t:tp__ty_2Enum_2Enum] : (((p@(ap@V13q0@(inj__ty_2Enum_2Enum @ V15t))) <=> (p@(ap@V6phi@(inj__ty_2Enum_2Enum @ V15t)))) & ((p@(ap@V14q1@(inj__ty_2Enum_2Enum @ V15t))) <=> (p@(ap@V13q0@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))) & (p@(ap@V5Phi@V14q1))))))))) & (((p@(ap@V5Phi@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V6phi))) <=> (? [V16q:$i] : ((mem@V16q@(arr@ty_2Enum_2Enum@bool)) & ((p@(ap@V16q@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) & (( ! [V17t:tp__ty_2Enum_2Enum] : ((p@(ap@V16q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V17t))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) <=> (p@(ap@V6phi@(inj__ty_2Enum_2Enum @ V17t))))) & (p@(ap@V5Phi@V16q))))))) & (((p@(ap@V5Phi@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V6phi))) <=> (? [V18q:$i] : ((mem@V18q@(arr@ty_2Enum_2Enum@bool)) & ((~~ (p@(ap@V18q@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) & (( ! [V19t:tp__ty_2Enum_2Enum] : ((p@(ap@V18q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V19t))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) <=> (p@(ap@V6phi@(inj__ty_2Enum_2Enum @ V19t))))) & (p@(ap@V5Phi@V18q))))))) & (((p@(ap@V5Phi@(ap@c_2EPast__Temporal__Logic_2EPNEXT@(ap@c_2EPast__Temporal__Logic_2EPALWAYS@V7a)))) <=> (? [V20q:$i] : ((mem@V20q@(arr@ty_2Enum_2Enum@bool)) & ((p@(ap@V20q@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) & (( ! [V21t:tp__ty_2Enum_2Enum] : ((p@(ap@V20q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V21t))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) <=> ((p@(ap@V7a@(inj__ty_2Enum_2Enum @ V21t))) & (p@(ap@V20q@(inj__ty_2Enum_2Enum @ V21t)))))) & (p@(ap@V5Phi@V20q))))))) & (((p@(ap@V5Phi@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@(ap@c_2EPast__Temporal__Logic_2EPEVENTUAL@V7a)))) <=> (? [V22q:$i] : ((mem@V22q@(arr@ty_2Enum_2Enum@bool)) & ((~~ (p@(ap@V22q@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) & (( ! [V23t:tp__ty_2Enum_2Enum] : ((p@(ap@V22q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V23t))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) <=> ((p@(ap@V7a@(inj__ty_2Enum_2Enum @ V23t))) | (p@(ap@V22q@(inj__ty_2Enum_2Enum @ V23t)))))) & (p@(ap@V5Phi@V22q))))))) & (((p@(ap@V5Phi@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V7a)@V8b)))) <=> (? [V24q:$i] : ((mem@V24q@(arr@ty_2Enum_2Enum@bool)) & ((~~ (p@(ap@V24q@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) & (( ! [V25t:tp__ty_2Enum_2Enum] : ((p@(ap@V24q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V25t))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) <=> ((p@(ap@V8b@(inj__ty_2Enum_2Enum @ V25t))) | ((p@(ap@V7a@(inj__ty_2Enum_2Enum @ V25t))) & (p@(ap@V24q@(inj__ty_2Enum_2Enum @ V25t))))))) & (p@(ap@V5Phi@V24q))))))) & (((p@(ap@V5Phi@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@V7a)@V8b)))) <=> (? [V26q:$i] : ((mem@V26q@(arr@ty_2Enum_2Enum@bool)) & ((~~ (p@(ap@V26q@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) & (( ! [V27t:tp__ty_2Enum_2Enum] : ((p@(ap@V26q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V27t))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) <=> (((p@(ap@V7a@(inj__ty_2Enum_2Enum @ V27t))) & (p@(ap@V8b@(inj__ty_2Enum_2Enum @ V27t)))) | ((~~ (p@(ap@V8b@(inj__ty_2Enum_2Enum @ V27t)))) & (p@(ap@V26q@(inj__ty_2Enum_2Enum @ V27t))))))) & (p@(ap@V5Phi@V26q))))))) & (((p@(ap@V5Phi@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V7a)@V8b)))) <=> (? [V28q:$i] : ((mem@V28q@(arr@ty_2Enum_2Enum@bool)) & ((~~ (p@(ap@V28q@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) & (( ! [V29t:tp__ty_2Enum_2Enum] : ((p@(ap@V28q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V29t))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) <=> ((~~ (p@(ap@V8b@(inj__ty_2Enum_2Enum @ V29t)))) & ((p@(ap@V7a@(inj__ty_2Enum_2Enum @ V29t))) | (p@(ap@V28q@(inj__ty_2Enum_2Enum @ V29t))))))) & (p@(ap@V5Phi@V28q))))))) & (((p@(ap@V5Phi@(ap@c_2EPast__Temporal__Logic_2EPNEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@V7a)@V8b)))) <=> (? [V30q:$i] : ((mem@V30q@(arr@ty_2Enum_2Enum@bool)) & ((p@(ap@V30q@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) & (( ! [V31t:tp__ty_2Enum_2Enum] : ((p@(ap@V30q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V31t))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) <=> ((p@(ap@V8b@(inj__ty_2Enum_2Enum @ V31t))) | ((p@(ap@V7a@(inj__ty_2Enum_2Enum @ V31t))) & (p@(ap@V30q@(inj__ty_2Enum_2Enum @ V31t))))))) & (p@(ap@V5Phi@V30q))))))) & (((p@(ap@V5Phi@(ap@c_2EPast__Temporal__Logic_2EPNEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@V7a)@V8b)))) <=> (? [V32q:$i] : ((mem@V32q@(arr@ty_2Enum_2Enum@bool)) & ((p@(ap@V32q@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) & (( ! [V33t:tp__ty_2Enum_2Enum] : ((p@(ap@V32q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V33t))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) <=> (((p@(ap@V7a@(inj__ty_2Enum_2Enum @ V33t))) & (p@(ap@V8b@(inj__ty_2Enum_2Enum @ V33t)))) | ((~~ (p@(ap@V8b@(inj__ty_2Enum_2Enum @ V33t)))) & (p@(ap@V32q@(inj__ty_2Enum_2Enum @ V33t))))))) & (p@(ap@V5Phi@V32q))))))) & ((p@(ap@V5Phi@(ap@c_2EPast__Temporal__Logic_2EPNEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V7a)@V8b)))) <=> (? [V34q:$i] : ((mem@V34q@(arr@ty_2Enum_2Enum@bool)) & ((p@(ap@V34q@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) & (( ! [V35t:tp__ty_2Enum_2Enum] : ((p@(ap@V34q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V35t))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) <=> ((~~ (p@(ap@V8b@(inj__ty_2Enum_2Enum @ V35t)))) & ((p@(ap@V7a@(inj__ty_2Enum_2Enum @ V35t))) | (p@(ap@V34q@(inj__ty_2Enum_2Enum @ V35t))))))) & (p@(ap@V5Phi@V34q))))))))))))))))))))))))))))))))))))))).
thf(conj_thm_2EOmega__Automata_2EBUECHI__TRANSLATION,lemma,( ! [V0Phi:$i] : ((mem@V0Phi@(arr@(arr@ty_2Enum_2Enum@bool)@bool)) => ( ! [V1phi:$i] : ((mem@V1phi@(arr@ty_2Enum_2Enum@bool)) => ( ! [V2a:$i] : ((mem@V2a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V3b:$i] : ((mem@V3b@(arr@ty_2Enum_2Enum@bool)) => (((p@(ap@V0Phi@(ap@c_2ETemporal__Logic_2ENEXT@V1phi))) <=> (? [V4q0:$i] : ((mem@V4q0@(arr@ty_2Enum_2Enum@bool)) & (? [V5q1:$i] : ((mem@V5q1@(arr@ty_2Enum_2Enum@bool)) & ($true & (( ! [V6t:tp__ty_2Enum_2Enum] : (((p@(ap@V4q0@(inj__ty_2Enum_2Enum @ V6t))) <=> (p@(ap@V1phi@(inj__ty_2Enum_2Enum @ V6t)))) & ((p@(ap@V5q1@(inj__ty_2Enum_2Enum @ V6t))) <=> (p@(ap@V4q0@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V6t))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))) & (p@(ap@V0Phi@V5q1))))))))) & (((p@(ap@V0Phi@(ap@c_2ETemporal__Logic_2EALWAYS@V2a))) <=> (? [V7q:$i] : ((mem@V7q@(arr@ty_2Enum_2Enum@bool)) & ($true & (( ! [V8t:tp__ty_2Enum_2Enum] : ((p@(ap@V7q@(inj__ty_2Enum_2Enum @ V8t))) <=> ((p@(ap@V2a@(inj__ty_2Enum_2Enum @ V8t))) & (p@(ap@V7q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V8t))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))) & (( ! [V9t1:tp__ty_2Enum_2Enum] : (? [V10t2:tp__ty_2Enum_2Enum] : ((p@(ap@V2a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V9t1))@(inj__ty_2Enum_2Enum @ V10t2)))) => (p@(ap@V7q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V9t1))@(inj__ty_2Enum_2Enum @ V10t2))))))) & (p@(ap@V0Phi@V7q)))))))) & (((p@(ap@V0Phi@(ap@c_2ETemporal__Logic_2EEVENTUAL@V2a))) <=> (? [V11q:$i] : ((mem@V11q@(arr@ty_2Enum_2Enum@bool)) & ($true & (( ! [V12t:tp__ty_2Enum_2Enum] : ((p@(ap@V11q@(inj__ty_2Enum_2Enum @ V12t))) <=> ((p@(ap@V2a@(inj__ty_2Enum_2Enum @ V12t))) | (p@(ap@V11q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V12t))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))) & (( ! [V13t1:tp__ty_2Enum_2Enum] : (? [V14t2:tp__ty_2Enum_2Enum] : ((p@(ap@V11q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V13t1))@(inj__ty_2Enum_2Enum @ V14t2)))) => (p@(ap@V2a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V13t1))@(inj__ty_2Enum_2Enum @ V14t2))))))) & (p@(ap@V0Phi@V11q)))))))) & (((p@(ap@V0Phi@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V2a)@V3b))) <=> (? [V15q:$i] : ((mem@V15q@(arr@ty_2Enum_2Enum@bool)) & ($true & (( ! [V16t:tp__ty_2Enum_2Enum] : ((p@(ap@V15q@(inj__ty_2Enum_2Enum @ V16t))) <=> ((p@(ap@V3b@(inj__ty_2Enum_2Enum @ V16t))) | ((p@(ap@V2a@(inj__ty_2Enum_2Enum @ V16t))) & (p@(ap@V15q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V16t))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) & (( ! [V17t1:tp__ty_2Enum_2Enum] : (? [V18t2:tp__ty_2Enum_2Enum] : ((p@(ap@V15q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V17t1))@(inj__ty_2Enum_2Enum @ V18t2)))) => ((~~ (p@(ap@V2a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V17t1))@(inj__ty_2Enum_2Enum @ V18t2))))) | (p@(ap@V3b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V17t1))@(inj__ty_2Enum_2Enum @ V18t2)))))))) & (p@(ap@V0Phi@V15q)))))))) & (((p@(ap@V0Phi@(ap@(ap@c_2ETemporal__Logic_2EUNTIL@V2a)@V3b))) <=> (? [V19q:$i] : ((mem@V19q@(arr@ty_2Enum_2Enum@bool)) & ($true & (( ! [V20t:tp__ty_2Enum_2Enum] : ((p@(ap@V19q@(inj__ty_2Enum_2Enum @ V20t))) <=> ((p@(ap@V3b@(inj__ty_2Enum_2Enum @ V20t))) | ((p@(ap@V2a@(inj__ty_2Enum_2Enum @ V20t))) & (p@(ap@V19q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V20t))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) & (( ! [V21t1:tp__ty_2Enum_2Enum] : (? [V22t2:tp__ty_2Enum_2Enum] : ((~~ (p@(ap@V19q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V21t1))@(inj__ty_2Enum_2Enum @ V22t2))))) => ((~~ (p@(ap@V2a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V21t1))@(inj__ty_2Enum_2Enum @ V22t2))))) | (p@(ap@V3b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V21t1))@(inj__ty_2Enum_2Enum @ V22t2)))))))) & (p@(ap@V0Phi@V19q)))))))) & (((p@(ap@V0Phi@(ap@(ap@c_2ETemporal__Logic_2ESWHEN@V2a)@V3b))) <=> (? [V23q:$i] : ((mem@V23q@(arr@ty_2Enum_2Enum@bool)) & ($true & (( ! [V24t:tp__ty_2Enum_2Enum] : ((p@(ap@V23q@(inj__ty_2Enum_2Enum @ V24t))) <=> (p@(ap@(ap@(ap@(c_2Ebool_2ECOND@bool)@(ap@V3b@(inj__ty_2Enum_2Enum @ V24t)))@(ap@V2a@(inj__ty_2Enum_2Enum @ V24t)))@(ap@V23q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V24t))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))) & (( ! [V25t1:tp__ty_2Enum_2Enum] : (? [V26t2:tp__ty_2Enum_2Enum] : ((p@(ap@V23q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V25t1))@(inj__ty_2Enum_2Enum @ V26t2)))) => (p@(ap@V3b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V25t1))@(inj__ty_2Enum_2Enum @ V26t2))))))) & (p@(ap@V0Phi@V23q)))))))) & (((p@(ap@V0Phi@(ap@(ap@c_2ETemporal__Logic_2EWHEN@V2a)@V3b))) <=> (? [V27q:$i] : ((mem@V27q@(arr@ty_2Enum_2Enum@bool)) & ($true & (( ! [V28t:tp__ty_2Enum_2Enum] : ((p@(ap@V27q@(inj__ty_2Enum_2Enum @ V28t))) <=> (p@(ap@(ap@(ap@(c_2Ebool_2ECOND@bool)@(ap@V3b@(inj__ty_2Enum_2Enum @ V28t)))@(ap@V2a@(inj__ty_2Enum_2Enum @ V28t)))@(ap@V27q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V28t))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))) & (( ! [V29t1:tp__ty_2Enum_2Enum] : (? [V30t2:tp__ty_2Enum_2Enum] : ((p@(ap@V27q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V29t1))@(inj__ty_2Enum_2Enum @ V30t2)))) | (p@(ap@V3b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V29t1))@(inj__ty_2Enum_2Enum @ V30t2))))))) & (p@(ap@V0Phi@V27q)))))))) & (((p@(ap@V0Phi@(ap@(ap@c_2ETemporal__Logic_2ESBEFORE@V2a)@V3b))) <=> (? [V31q:$i] : ((mem@V31q@(arr@ty_2Enum_2Enum@bool)) & ($true & (( ! [V32t:tp__ty_2Enum_2Enum] : ((p@(ap@V31q@(inj__ty_2Enum_2Enum @ V32t))) <=> ((~~ (p@(ap@V3b@(inj__ty_2Enum_2Enum @ V32t)))) & ((p@(ap@V2a@(inj__ty_2Enum_2Enum @ V32t))) | (p@(ap@V31q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V32t))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) & (( ! [V33t1:tp__ty_2Enum_2Enum] : (? [V34t2:tp__ty_2Enum_2Enum] : ((p@(ap@V31q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V33t1))@(inj__ty_2Enum_2Enum @ V34t2)))) => ((p@(ap@V2a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V33t1))@(inj__ty_2Enum_2Enum @ V34t2)))) | (p@(ap@V3b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V33t1))@(inj__ty_2Enum_2Enum @ V34t2)))))))) & (p@(ap@V0Phi@V31q)))))))) & ((p@(ap@V0Phi@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@V2a)@V3b))) <=> (? [V35q:$i] : ((mem@V35q@(arr@ty_2Enum_2Enum@bool)) & ($true & (( ! [V36t:tp__ty_2Enum_2Enum] : ((p@(ap@V35q@(inj__ty_2Enum_2Enum @ V36t))) <=> ((~~ (p@(ap@V3b@(inj__ty_2Enum_2Enum @ V36t)))) & ((p@(ap@V2a@(inj__ty_2Enum_2Enum @ V36t))) | (p@(ap@V35q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V36t))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) & (( ! [V37t1:tp__ty_2Enum_2Enum] : (? [V38t2:tp__ty_2Enum_2Enum] : ((~~ (p@(ap@V35q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V37t1))@(inj__ty_2Enum_2Enum @ V38t2))))) => ((p@(ap@V2a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V37t1))@(inj__ty_2Enum_2Enum @ V38t2)))) | (p@(ap@V3b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V37t1))@(inj__ty_2Enum_2Enum @ V38t2)))))))) & (p@(ap@V0Phi@V35q))))))))))))))))))))))))).
thf(conj_thm_2EOmega__Automata_2ECO__BUECHI__CONJ__CLOSURE,lemma,( ! [A_27a:del]: ( ! [A_27b1:del]: ( ! [A_27b2:del]: ( ! [V0Phi__I1:$i] : ((mem@V0Phi__I1@(arr@A_27b1@bool)) => ( ! [V1t0:tp__ty_2Enum_2Enum] : ( ! [V2Phi__R1:$i] : ((mem@V2Phi__R1@(arr@(ty_2Epair_2Eprod@A_27a@A_27b1)@bool)) => ( ! [V3i:$i] : ((mem@V3i@(arr@ty_2Enum_2Enum@A_27a)) => ( ! [V4Psi1:$i] : ((mem@V4Psi1@(arr@(ty_2Epair_2Eprod@A_27a@A_27b1)@bool)) => ( ! [V5Phi__I2:$i] : ((mem@V5Phi__I2@(arr@A_27b2@bool)) => ( ! [V6Phi__R2:$i] : ((mem@V6Phi__R2@(arr@(ty_2Epair_2Eprod@A_27a@A_27b2)@bool)) => ( ! [V7Psi2:$i] : ((mem@V7Psi2@(arr@(ty_2Epair_2Eprod@A_27a@A_27b2)@bool)) => (((? [V8q1:$i] : ((mem@V8q1@(arr@ty_2Enum_2Enum@A_27b1)) & ((p@(ap@V0Phi__I1@(ap@V8q1@(inj__ty_2Enum_2Enum @ V1t0)))) & (( ! [V9t:tp__ty_2Enum_2Enum] : (p@(ap@V2Phi__R1@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b1)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V9t))@(inj__ty_2Enum_2Enum @ V1t0))))@(ap@V8q1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V9t))@(inj__ty_2Enum_2Enum @ V1t0))))))) & (? [V10t1:tp__ty_2Enum_2Enum] : ( ! [V11t2:tp__ty_2Enum_2Enum] : (p@(ap@V4Psi1@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b1)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V10t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11t2))@(inj__ty_2Enum_2Enum @ V1t0)))))@(ap@V8q1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V10t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11t2))@(inj__ty_2Enum_2Enum @ V1t0))))))))))))) & (? [V12q2:$i] : ((mem@V12q2@(arr@ty_2Enum_2Enum@A_27b2)) & ((p@(ap@V5Phi__I2@(ap@V12q2@(inj__ty_2Enum_2Enum @ V1t0)))) & (( ! [V13t:tp__ty_2Enum_2Enum] : (p@(ap@V6Phi__R2@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b2)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V13t))@(inj__ty_2Enum_2Enum @ V1t0))))@(ap@V12q2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V13t))@(inj__ty_2Enum_2Enum @ V1t0))))))) & (? [V14t1:tp__ty_2Enum_2Enum] : ( ! [V15t2:tp__ty_2Enum_2Enum] : (p@(ap@V7Psi2@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b2)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t2))@(inj__ty_2Enum_2Enum @ V1t0)))))@(ap@V12q2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t2))@(inj__ty_2Enum_2Enum @ V1t0)))))))))))))) <=> (? [V16q1:$i] : ((mem@V16q1@(arr@ty_2Enum_2Enum@A_27b1)) & (? [V17q2:$i] : ((mem@V17q2@(arr@ty_2Enum_2Enum@A_27b2)) & (((p@(ap@V0Phi__I1@(ap@V16q1@(inj__ty_2Enum_2Enum @ V1t0)))) & (p@(ap@V5Phi__I2@(ap@V17q2@(inj__ty_2Enum_2Enum @ V1t0))))) & (( ! [V18t:tp__ty_2Enum_2Enum] : ((p@(ap@V2Phi__R1@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b1)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V18t))@(inj__ty_2Enum_2Enum @ V1t0))))@(ap@V16q1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V18t))@(inj__ty_2Enum_2Enum @ V1t0)))))) & (p@(ap@V6Phi__R2@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b2)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V18t))@(inj__ty_2Enum_2Enum @ V1t0))))@(ap@V17q2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V18t))@(inj__ty_2Enum_2Enum @ V1t0)))))))) & (? [V19t1:tp__ty_2Enum_2Enum] : ( ! [V20t2:tp__ty_2Enum_2Enum] : ((p@(ap@V4Psi1@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b1)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V19t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V20t2))@(inj__ty_2Enum_2Enum @ V1t0)))))@(ap@V16q1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V19t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V20t2))@(inj__ty_2Enum_2Enum @ V1t0))))))) & (p@(ap@V7Psi2@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b2)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V19t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V20t2))@(inj__ty_2Enum_2Enum @ V1t0)))))@(ap@V17q2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V19t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V20t2))@(inj__ty_2Enum_2Enum @ V1t0)))))))))))))))))))))))))))))))))))).
thf(conj_thm_2EOmega__Automata_2ECO__BUECHI__DISJ__CLOSURE,lemma,( ! [A_27a:del]: ( ! [A_27b1:del]: ( ! [A_27b2:del]: ( ! [V0Phi__I1:$i] : ((mem@V0Phi__I1@(arr@A_27b1@bool)) => ( ! [V1t0:tp__ty_2Enum_2Enum] : ( ! [V2Phi__R1:$i] : ((mem@V2Phi__R1@(arr@(ty_2Epair_2Eprod@A_27a@A_27b1)@bool)) => ( ! [V3i:$i] : ((mem@V3i@(arr@ty_2Enum_2Enum@A_27a)) => ( ! [V4Psi1:$i] : ((mem@V4Psi1@(arr@(ty_2Epair_2Eprod@A_27a@A_27b1)@bool)) => ( ! [V5Phi__I2:$i] : ((mem@V5Phi__I2@(arr@A_27b2@bool)) => ( ! [V6Phi__R2:$i] : ((mem@V6Phi__R2@(arr@(ty_2Epair_2Eprod@A_27a@A_27b2)@bool)) => ( ! [V7Psi2:$i] : ((mem@V7Psi2@(arr@(ty_2Epair_2Eprod@A_27a@A_27b2)@bool)) => ( ! [V8t:tp__ty_2Enum_2Enum] : (((? [V9q1:$i] : ((mem@V9q1@(arr@ty_2Enum_2Enum@A_27b1)) & ((p@(ap@V0Phi__I1@(ap@V9q1@(inj__ty_2Enum_2Enum @ V1t0)))) & (( ! [V10t:tp__ty_2Enum_2Enum] : (p@(ap@V2Phi__R1@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b1)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V10t))@(inj__ty_2Enum_2Enum @ V1t0))))@(ap@V9q1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V10t))@(inj__ty_2Enum_2Enum @ V1t0))))))) & (? [V11t1:tp__ty_2Enum_2Enum] : ( ! [V12t2:tp__ty_2Enum_2Enum] : (p@(ap@V4Psi1@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b1)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V12t2))@(inj__ty_2Enum_2Enum @ V1t0)))))@(ap@V9q1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V12t2))@(inj__ty_2Enum_2Enum @ V1t0))))))))))))) | (? [V13q2:$i] : ((mem@V13q2@(arr@ty_2Enum_2Enum@A_27b2)) & ((p@(ap@V5Phi__I2@(ap@V13q2@(inj__ty_2Enum_2Enum @ V1t0)))) & (( ! [V14t:tp__ty_2Enum_2Enum] : (p@(ap@V6Phi__R2@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b2)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t))@(inj__ty_2Enum_2Enum @ V1t0))))@(ap@V13q2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t))@(inj__ty_2Enum_2Enum @ V1t0))))))) & (? [V15t1:tp__ty_2Enum_2Enum] : ( ! [V16t2:tp__ty_2Enum_2Enum] : (p@(ap@V7Psi2@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b2)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V16t2))@(inj__ty_2Enum_2Enum @ V1t0)))))@(ap@V13q2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V16t2))@(inj__ty_2Enum_2Enum @ V1t0)))))))))))))) <=> (? [V17p:$i] : ((mem@V17p@(arr@ty_2Enum_2Enum@bool)) & (? [V18q1:$i] : ((mem@V18q1@(arr@ty_2Enum_2Enum@A_27b1)) & (? [V19q2:$i] : ((mem@V19q2@(arr@ty_2Enum_2Enum@A_27b2)) & ((((~~ (p@(ap@V17p@(inj__ty_2Enum_2Enum @ V1t0)))) & (p@(ap@V0Phi__I1@(ap@V18q1@(inj__ty_2Enum_2Enum @ V1t0))))) | ((p@(ap@V17p@(inj__ty_2Enum_2Enum @ V1t0))) & (p@(ap@V5Phi__I2@(ap@V19q2@(inj__ty_2Enum_2Enum @ V1t0)))))) & (( ! [V20t:tp__ty_2Enum_2Enum] : (((~~ (p@(ap@V17p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V20t))@(inj__ty_2Enum_2Enum @ V1t0))))) & ((p@(ap@V2Phi__R1@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b1)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V20t))@(inj__ty_2Enum_2Enum @ V1t0))))@(ap@V18q1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V20t))@(inj__ty_2Enum_2Enum @ V1t0)))))) & (~~ (p@(ap@V17p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V20t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V1t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) | ((p@(ap@V17p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V20t))@(inj__ty_2Enum_2Enum @ V1t0)))) & ((p@(ap@V6Phi__R2@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b2)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V20t))@(inj__ty_2Enum_2Enum @ V1t0))))@(ap@V19q2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V20t))@(inj__ty_2Enum_2Enum @ V1t0)))))) & (p@(ap@V17p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V20t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V1t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) & (? [V21t1:tp__ty_2Enum_2Enum] : ( ! [V22t2:tp__ty_2Enum_2Enum] : (((~~ (p@(ap@V17p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V8t))@(inj__ty_2Enum_2Enum @ V1t0))))) & (p@(ap@V4Psi1@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b1)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V21t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V22t2))@(inj__ty_2Enum_2Enum @ V1t0)))))@(ap@V18q1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V21t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V22t2))@(inj__ty_2Enum_2Enum @ V1t0)))))))) | ((p@(ap@V17p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V8t))@(inj__ty_2Enum_2Enum @ V1t0)))) & (p@(ap@V7Psi2@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b2)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V21t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V22t2))@(inj__ty_2Enum_2Enum @ V1t0)))))@(ap@V19q2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V21t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V22t2))@(inj__ty_2Enum_2Enum @ V1t0)))))))))))))))))))))))))))))))))))))))).
thf(conj_thm_2EOmega__Automata_2ECO__BUECHI__NEXT__CLOSURE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0Phi__I:$i] : ((mem@V0Phi__I@(arr@A_27b@bool)) => ( ! [V1Phi__R:$i] : ((mem@V1Phi__R@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)) => ( ! [V2i:$i] : ((mem@V2i@(arr@ty_2Enum_2Enum@A_27a)) => ( ! [V3Psi:$i] : ((mem@V3Psi@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)) => ( ! [V4t0:tp__ty_2Enum_2Enum] : ( ! [V5c:$i] : ((mem@V5c@A_27b) => ((p@(ap@(ap@c_2ETemporal__Logic_2ENEXT@(lam@ty_2Enum_2Enum@(^ [V6t0:$i] : (ap@(c_2Ebool_2E_3F@(arr@ty_2Enum_2Enum@A_27b))@(lam@(arr@ty_2Enum_2Enum@A_27b)@(^ [V7q:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0Phi__I@(ap@V7q@V6t0)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(c_2Ebool_2E_21@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V8t:$i] : (ap@V1Phi__R@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@(ap@V2i@(ap@(ap@c_2Earithmetic_2E_2B@V8t)@V6t0)))@(ap@V7q@(ap@(ap@c_2Earithmetic_2E_2B@V8t)@V6t0))))))))@(ap@(c_2Ebool_2E_3F@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V9t1:$i] : (ap@(c_2Ebool_2E_21@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V10t2:$i] : (ap@V3Psi@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@(ap@V2i@(ap@(ap@c_2Earithmetic_2E_2B@V9t1)@(ap@(ap@c_2Earithmetic_2E_2B@V10t2)@V6t0))))@(ap@V7q@(ap@(ap@c_2Earithmetic_2E_2B@V9t1)@(ap@(ap@c_2Earithmetic_2E_2B@V10t2)@V6t0)))))))))))))))))))@(inj__ty_2Enum_2Enum @ V4t0))) <=> (? [V11p:$i] : ((mem@V11p@(arr@ty_2Enum_2Enum@bool)) & (? [V12q:$i] : ((mem@V12q@(arr@ty_2Enum_2Enum@A_27b)) & ((((p@(ap@V11p@(inj__ty_2Enum_2Enum @ V4t0))) <=> $false) & ((ap@V12q@(inj__ty_2Enum_2Enum @ V4t0)) = V5c)) & (( ! [V13t:tp__ty_2Enum_2Enum] : (((~~ (p@(ap@V11p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V13t))@(inj__ty_2Enum_2Enum @ V4t0))))) & (((ap@V12q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V13t))@(inj__ty_2Enum_2Enum @ V4t0))) = V5c) & ((p@(ap@V11p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V13t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & (p@(ap@V0Phi__I@(ap@V12q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V13t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) | ((p@(ap@V11p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V13t))@(inj__ty_2Enum_2Enum @ V4t0)))) & ((p@(ap@V1Phi__R@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@(ap@V2i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V13t))@(inj__ty_2Enum_2Enum @ V4t0))))@(ap@V12q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V13t))@(inj__ty_2Enum_2Enum @ V4t0)))))) & (p@(ap@V11p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V13t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) & (? [V14t1:tp__ty_2Enum_2Enum] : ( ! [V15t2:tp__ty_2Enum_2Enum] : (p@(ap@V3Psi@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@(ap@V2i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t2))@(inj__ty_2Enum_2Enum @ V4t0)))))@(ap@V12q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t2))@(inj__ty_2Enum_2Enum @ V4t0)))))))))))))))))))))))))))))).
thf(conj_thm_2EOmega__Automata_2ECO__BUECHI__SUNTIL__CLOSURE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0phi:$i] : ((mem@V0phi@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1Phi__I:$i] : ((mem@V1Phi__I@(arr@A_27b@bool)) => ( ! [V2Phi__R:$i] : ((mem@V2Phi__R@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)) => ( ! [V3i:$i] : ((mem@V3i@(arr@ty_2Enum_2Enum@A_27a)) => ( ! [V4Psi:$i] : ((mem@V4Psi@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)) => ( ! [V5t0:tp__ty_2Enum_2Enum] : ( ! [V6c:$i] : ((mem@V6c@A_27b) => ((p@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V0phi)@(lam@ty_2Enum_2Enum@(^ [V7t0:$i] : (ap@(c_2Ebool_2E_3F@(arr@ty_2Enum_2Enum@A_27b))@(lam@(arr@ty_2Enum_2Enum@A_27b)@(^ [V8q:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1Phi__I@(ap@V8q@V7t0)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(c_2Ebool_2E_21@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V9t:$i] : (ap@V2Phi__R@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@V9t)@V7t0)))@(ap@V8q@(ap@(ap@c_2Earithmetic_2E_2B@V9t)@V7t0))))))))@(ap@(c_2Ebool_2E_3F@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V10t1:$i] : (ap@(c_2Ebool_2E_21@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V11t2:$i] : (ap@V4Psi@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@V10t1)@(ap@(ap@c_2Earithmetic_2E_2B@V11t2)@V7t0))))@(ap@V8q@(ap@(ap@c_2Earithmetic_2E_2B@V10t1)@(ap@(ap@c_2Earithmetic_2E_2B@V11t2)@V7t0)))))))))))))))))))@(inj__ty_2Enum_2Enum @ V5t0))) <=> (? [V12p:$i] : ((mem@V12p@(arr@ty_2Enum_2Enum@bool)) & (? [V13q:$i] : ((mem@V13q@(arr@ty_2Enum_2Enum@A_27b)) & ((p@(ap@(ap@(ap@(c_2Ebool_2ECOND@bool)@(ap@V12p@(inj__ty_2Enum_2Enum @ V5t0)))@(ap@V1Phi__I@(ap@V13q@(inj__ty_2Enum_2Enum @ V5t0))))@(ap@(ap@(c_2Emin_2E_3D@A_27b)@(ap@V13q@(inj__ty_2Enum_2Enum @ V5t0)))@V6c))) & (( ! [V14t:tp__ty_2Enum_2Enum] : (((~~ (p@(ap@V12p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t))@(inj__ty_2Enum_2Enum @ V5t0))))) & (((ap@V13q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t))@(inj__ty_2Enum_2Enum @ V5t0))) = V6c) & ((p@(ap@V0phi@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t))@(inj__ty_2Enum_2Enum @ V5t0)))) & ((~~ (p@(ap@V12p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))) & ((ap@V13q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) = V6c))))) | (((~~ (p@(ap@V12p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t))@(inj__ty_2Enum_2Enum @ V5t0))))) & (((ap@V13q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t))@(inj__ty_2Enum_2Enum @ V5t0))) = V6c) & ((p@(ap@V0phi@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t))@(inj__ty_2Enum_2Enum @ V5t0)))) & ((p@(ap@V12p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & (p@(ap@V1Phi__I@(ap@V13q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))) | ((p@(ap@V12p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t))@(inj__ty_2Enum_2Enum @ V5t0)))) & ((p@(ap@V2Phi__R@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t))@(inj__ty_2Enum_2Enum @ V5t0))))@(ap@V13q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t))@(inj__ty_2Enum_2Enum @ V5t0)))))) & (p@(ap@V12p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))) & (? [V15t1:tp__ty_2Enum_2Enum] : ( ! [V16t2:tp__ty_2Enum_2Enum] : ((p@(ap@V12p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V16t2))@(inj__ty_2Enum_2Enum @ V5t0))))) & (p@(ap@V4Psi@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V16t2))@(inj__ty_2Enum_2Enum @ V5t0)))))@(ap@V13q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V16t2))@(inj__ty_2Enum_2Enum @ V5t0))))))))))))))))))))))))))))))))).
thf(conj_thm_2EOmega__Automata_2ECO__BUECHI__UNTIL__CLOSURE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0phi:$i] : ((mem@V0phi@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1Phi__I:$i] : ((mem@V1Phi__I@(arr@A_27b@bool)) => ( ! [V2Phi__R:$i] : ((mem@V2Phi__R@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)) => ( ! [V3i:$i] : ((mem@V3i@(arr@ty_2Enum_2Enum@A_27a)) => ( ! [V4Psi:$i] : ((mem@V4Psi@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)) => ( ! [V5t0:tp__ty_2Enum_2Enum] : ( ! [V6c:$i] : ((mem@V6c@A_27b) => ((p@(ap@(ap@(ap@c_2ETemporal__Logic_2EUNTIL@V0phi)@(lam@ty_2Enum_2Enum@(^ [V7t0:$i] : (ap@(c_2Ebool_2E_3F@(arr@ty_2Enum_2Enum@A_27b))@(lam@(arr@ty_2Enum_2Enum@A_27b)@(^ [V8q:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1Phi__I@(ap@V8q@V7t0)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(c_2Ebool_2E_21@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V9t:$i] : (ap@V2Phi__R@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@V9t)@V7t0)))@(ap@V8q@(ap@(ap@c_2Earithmetic_2E_2B@V9t)@V7t0))))))))@(ap@(c_2Ebool_2E_3F@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V10t1:$i] : (ap@(c_2Ebool_2E_21@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V11t2:$i] : (ap@V4Psi@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@V10t1)@(ap@(ap@c_2Earithmetic_2E_2B@V11t2)@V7t0))))@(ap@V8q@(ap@(ap@c_2Earithmetic_2E_2B@V10t1)@(ap@(ap@c_2Earithmetic_2E_2B@V11t2)@V7t0)))))))))))))))))))@(inj__ty_2Enum_2Enum @ V5t0))) <=> (? [V12p:$i] : ((mem@V12p@(arr@ty_2Enum_2Enum@bool)) & (? [V13q:$i] : ((mem@V13q@(arr@ty_2Enum_2Enum@A_27b)) & ((p@(ap@(ap@(ap@(c_2Ebool_2ECOND@bool)@(ap@V12p@(inj__ty_2Enum_2Enum @ V5t0)))@(ap@V1Phi__I@(ap@V13q@(inj__ty_2Enum_2Enum @ V5t0))))@(ap@(ap@(c_2Emin_2E_3D@A_27b)@(ap@V13q@(inj__ty_2Enum_2Enum @ V5t0)))@V6c))) & (( ! [V14t:tp__ty_2Enum_2Enum] : (((~~ (p@(ap@V12p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t))@(inj__ty_2Enum_2Enum @ V5t0))))) & (((ap@V13q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t))@(inj__ty_2Enum_2Enum @ V5t0))) = V6c) & ((p@(ap@V0phi@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t))@(inj__ty_2Enum_2Enum @ V5t0)))) & ((~~ (p@(ap@V12p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))) & ((ap@V13q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) = V6c))))) | (((~~ (p@(ap@V12p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t))@(inj__ty_2Enum_2Enum @ V5t0))))) & (((ap@V13q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t))@(inj__ty_2Enum_2Enum @ V5t0))) = V6c) & ((p@(ap@V0phi@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t))@(inj__ty_2Enum_2Enum @ V5t0)))) & ((p@(ap@V12p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & (p@(ap@V1Phi__I@(ap@V13q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))) | ((p@(ap@V12p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t))@(inj__ty_2Enum_2Enum @ V5t0)))) & ((p@(ap@V2Phi__R@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t))@(inj__ty_2Enum_2Enum @ V5t0))))@(ap@V13q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t))@(inj__ty_2Enum_2Enum @ V5t0)))))) & (p@(ap@V12p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V14t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))) & (? [V15t1:tp__ty_2Enum_2Enum] : ( ! [V16t2:tp__ty_2Enum_2Enum] : ((~~ (p@(ap@V12p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V16t2))@(inj__ty_2Enum_2Enum @ V5t0)))))) | (p@(ap@V4Psi@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@(ap@V3i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V16t2))@(inj__ty_2Enum_2Enum @ V5t0)))))@(ap@V13q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V16t2))@(inj__ty_2Enum_2Enum @ V5t0))))))))))))))))))))))))))))))))).
thf(conj_thm_2EOmega__Automata_2ECO__BUECHI__SBEFORE__CLOSURE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0Phi__I:$i] : ((mem@V0Phi__I@(arr@A_27b@bool)) => ( ! [V1Phi__R:$i] : ((mem@V1Phi__R@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)) => ( ! [V2i:$i] : ((mem@V2i@(arr@ty_2Enum_2Enum@A_27a)) => ( ! [V3Psi:$i] : ((mem@V3Psi@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)) => ( ! [V4phi:$i] : ((mem@V4phi@(arr@ty_2Enum_2Enum@bool)) => ( ! [V5t0:tp__ty_2Enum_2Enum] : ( ! [V6c:$i] : ((mem@V6c@A_27b) => ((p@(ap@(ap@(ap@c_2ETemporal__Logic_2ESBEFORE@(lam@ty_2Enum_2Enum@(^ [V7t0:$i] : (ap@(c_2Ebool_2E_3F@(arr@ty_2Enum_2Enum@A_27b))@(lam@(arr@ty_2Enum_2Enum@A_27b)@(^ [V8q:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0Phi__I@(ap@V8q@V7t0)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(c_2Ebool_2E_21@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V9t:$i] : (ap@V1Phi__R@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@(ap@V2i@(ap@(ap@c_2Earithmetic_2E_2B@V9t)@V7t0)))@(ap@V8q@(ap@(ap@c_2Earithmetic_2E_2B@V9t)@V7t0))))))))@(ap@(c_2Ebool_2E_3F@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V10t1:$i] : (ap@(c_2Ebool_2E_21@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V11t2:$i] : (ap@V3Psi@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@(ap@V2i@(ap@(ap@c_2Earithmetic_2E_2B@V10t1)@(ap@(ap@c_2Earithmetic_2E_2B@V11t2)@V7t0))))@(ap@V8q@(ap@(ap@c_2Earithmetic_2E_2B@V10t1)@(ap@(ap@c_2Earithmetic_2E_2B@V11t2)@V7t0)))))))))))))))))))@V4phi)@(inj__ty_2Enum_2Enum @ V5t0))) <=> (? [V12p1:$i] : ((mem@V12p1@(arr@ty_2Enum_2Enum@bool)) & (? [V13p2:$i] : ((mem@V13p2@(arr@ty_2Enum_2Enum@bool)) & (? [V14q:$i] : ((mem@V14q@(arr@ty_2Enum_2Enum@A_27b)) & ((((~~ (p@(ap@V12p1@(inj__ty_2Enum_2Enum @ V5t0)))) & ((~~ (p@(ap@V13p2@(inj__ty_2Enum_2Enum @ V5t0)))) & ((ap@V14q@(inj__ty_2Enum_2Enum @ V5t0)) = V6c))) | ((p@(ap@V12p1@(inj__ty_2Enum_2Enum @ V5t0))) & ((~~ (p@(ap@V13p2@(inj__ty_2Enum_2Enum @ V5t0)))) & (p@(ap@V0Phi__I@(ap@V14q@(inj__ty_2Enum_2Enum @ V5t0))))))) & (( ! [V15t:tp__ty_2Enum_2Enum] : (((~~ (p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))) & ((~~ (p@(ap@V13p2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))) & (((ap@V14q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))) = V6c) & ((~~ (p@(ap@V4phi@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))) & ((~~ (p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))) & ((~~ (p@(ap@V13p2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))) & ((ap@V14q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) = V6c))))))) | (((~~ (p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))) & ((~~ (p@(ap@V13p2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))) & (((ap@V14q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))) = V6c) & ((~~ (p@(ap@V4phi@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))) & ((p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & ((~~ (p@(ap@V13p2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))) & (p@(ap@V0Phi__I@(ap@V14q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))))) | (((p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0)))) & ((~~ (p@(ap@V13p2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))) & ((~~ (p@(ap@V4phi@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))) & ((p@(ap@V0Phi__I@(ap@V14q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))) & ((p@(ap@V1Phi__R@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@(ap@V2i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))@(ap@V14q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0)))))) & ((p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & (p@(ap@V13p2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))))) | ((p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0)))) & ((p@(ap@V13p2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0)))) & ((p@(ap@V1Phi__R@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@(ap@V2i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))@(ap@V14q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0)))))) & ((p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & (p@(ap@V13p2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))))))) & (? [V16t1:tp__ty_2Enum_2Enum] : ( ! [V17t2:tp__ty_2Enum_2Enum] : ((p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V16t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V17t2))@(inj__ty_2Enum_2Enum @ V5t0))))) & (p@(ap@V3Psi@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@(ap@V2i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V16t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V17t2))@(inj__ty_2Enum_2Enum @ V5t0)))))@(ap@V14q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V16t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V17t2))@(inj__ty_2Enum_2Enum @ V5t0))))))))))))))))))))))))))))))))))).
thf(conj_thm_2EOmega__Automata_2ECO__BUECHI__BEFORE__CLOSURE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0Phi__I:$i] : ((mem@V0Phi__I@(arr@A_27b@bool)) => ( ! [V1Phi__R:$i] : ((mem@V1Phi__R@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)) => ( ! [V2i:$i] : ((mem@V2i@(arr@ty_2Enum_2Enum@A_27a)) => ( ! [V3Psi:$i] : ((mem@V3Psi@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)) => ( ! [V4phi:$i] : ((mem@V4phi@(arr@ty_2Enum_2Enum@bool)) => ( ! [V5t0:tp__ty_2Enum_2Enum] : ( ! [V6c:$i] : ((mem@V6c@A_27b) => ((p@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@(lam@ty_2Enum_2Enum@(^ [V7t0:$i] : (ap@(c_2Ebool_2E_3F@(arr@ty_2Enum_2Enum@A_27b))@(lam@(arr@ty_2Enum_2Enum@A_27b)@(^ [V8q:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0Phi__I@(ap@V8q@V7t0)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(c_2Ebool_2E_21@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V9t:$i] : (ap@V1Phi__R@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@(ap@V2i@(ap@(ap@c_2Earithmetic_2E_2B@V9t)@V7t0)))@(ap@V8q@(ap@(ap@c_2Earithmetic_2E_2B@V9t)@V7t0))))))))@(ap@(c_2Ebool_2E_3F@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V10t1:$i] : (ap@(c_2Ebool_2E_21@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V11t2:$i] : (ap@V3Psi@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@(ap@V2i@(ap@(ap@c_2Earithmetic_2E_2B@V10t1)@(ap@(ap@c_2Earithmetic_2E_2B@V11t2)@V7t0))))@(ap@V8q@(ap@(ap@c_2Earithmetic_2E_2B@V10t1)@(ap@(ap@c_2Earithmetic_2E_2B@V11t2)@V7t0)))))))))))))))))))@V4phi)@(inj__ty_2Enum_2Enum @ V5t0))) <=> (? [V12p1:$i] : ((mem@V12p1@(arr@ty_2Enum_2Enum@bool)) & (? [V13p2:$i] : ((mem@V13p2@(arr@ty_2Enum_2Enum@bool)) & (? [V14q:$i] : ((mem@V14q@(arr@ty_2Enum_2Enum@A_27b)) & ((((~~ (p@(ap@V12p1@(inj__ty_2Enum_2Enum @ V5t0)))) & ((~~ (p@(ap@V13p2@(inj__ty_2Enum_2Enum @ V5t0)))) & ((ap@V14q@(inj__ty_2Enum_2Enum @ V5t0)) = V6c))) | ((p@(ap@V12p1@(inj__ty_2Enum_2Enum @ V5t0))) & ((~~ (p@(ap@V13p2@(inj__ty_2Enum_2Enum @ V5t0)))) & (p@(ap@V0Phi__I@(ap@V14q@(inj__ty_2Enum_2Enum @ V5t0))))))) & (( ! [V15t:tp__ty_2Enum_2Enum] : (((~~ (p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))) & ((~~ (p@(ap@V13p2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))) & (((ap@V14q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))) = V6c) & ((~~ (p@(ap@V4phi@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))) & ((~~ (p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))) & ((~~ (p@(ap@V13p2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))) & ((ap@V14q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) = V6c))))))) | (((~~ (p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))) & ((~~ (p@(ap@V13p2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))) & (((ap@V14q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))) = V6c) & ((~~ (p@(ap@V4phi@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))) & ((p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & ((~~ (p@(ap@V13p2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))) & (p@(ap@V0Phi__I@(ap@V14q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))))) | (((p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0)))) & ((~~ (p@(ap@V13p2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))) & ((~~ (p@(ap@V4phi@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))) & ((p@(ap@V0Phi__I@(ap@V14q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))) & ((p@(ap@V1Phi__R@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@(ap@V2i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))@(ap@V14q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0)))))) & ((p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & (p@(ap@V13p2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))))) | ((p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0)))) & ((p@(ap@V13p2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0)))) & ((p@(ap@V1Phi__R@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@(ap@V2i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))@(ap@V14q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0)))))) & ((p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & (p@(ap@V13p2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))))))) & (? [V16t1:tp__ty_2Enum_2Enum] : ( ! [V17t2:tp__ty_2Enum_2Enum] : ((~~ (p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V16t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V17t2))@(inj__ty_2Enum_2Enum @ V5t0)))))) | (p@(ap@V3Psi@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@(ap@V2i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V16t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V17t2))@(inj__ty_2Enum_2Enum @ V5t0)))))@(ap@V14q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V16t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V17t2))@(inj__ty_2Enum_2Enum @ V5t0))))))))))))))))))))))))))))))))))).
thf(conj_thm_2EOmega__Automata_2ECO__BUECHI__SWHEN__CLOSURE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0Phi__I:$i] : ((mem@V0Phi__I@(arr@A_27b@bool)) => ( ! [V1Phi__R:$i] : ((mem@V1Phi__R@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)) => ( ! [V2i:$i] : ((mem@V2i@(arr@ty_2Enum_2Enum@A_27a)) => ( ! [V3Psi:$i] : ((mem@V3Psi@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)) => ( ! [V4phi:$i] : ((mem@V4phi@(arr@ty_2Enum_2Enum@bool)) => ( ! [V5t0:tp__ty_2Enum_2Enum] : ( ! [V6c:$i] : ((mem@V6c@A_27b) => ((p@(ap@(ap@(ap@c_2ETemporal__Logic_2ESWHEN@(lam@ty_2Enum_2Enum@(^ [V7t0:$i] : (ap@(c_2Ebool_2E_3F@(arr@ty_2Enum_2Enum@A_27b))@(lam@(arr@ty_2Enum_2Enum@A_27b)@(^ [V8q:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0Phi__I@(ap@V8q@V7t0)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(c_2Ebool_2E_21@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V9t:$i] : (ap@V1Phi__R@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@(ap@V2i@(ap@(ap@c_2Earithmetic_2E_2B@V9t)@V7t0)))@(ap@V8q@(ap@(ap@c_2Earithmetic_2E_2B@V9t)@V7t0))))))))@(ap@(c_2Ebool_2E_3F@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V10t1:$i] : (ap@(c_2Ebool_2E_21@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V11t2:$i] : (ap@V3Psi@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@(ap@V2i@(ap@(ap@c_2Earithmetic_2E_2B@V10t1)@(ap@(ap@c_2Earithmetic_2E_2B@V11t2)@V7t0))))@(ap@V8q@(ap@(ap@c_2Earithmetic_2E_2B@V10t1)@(ap@(ap@c_2Earithmetic_2E_2B@V11t2)@V7t0)))))))))))))))))))@V4phi)@(inj__ty_2Enum_2Enum @ V5t0))) <=> (? [V12p1:$i] : ((mem@V12p1@(arr@ty_2Enum_2Enum@bool)) & (? [V13p2:$i] : ((mem@V13p2@(arr@ty_2Enum_2Enum@bool)) & (? [V14q:$i] : ((mem@V14q@(arr@ty_2Enum_2Enum@A_27b)) & ((((~~ (p@(ap@V12p1@(inj__ty_2Enum_2Enum @ V5t0)))) & ((~~ (p@(ap@V13p2@(inj__ty_2Enum_2Enum @ V5t0)))) & ((ap@V14q@(inj__ty_2Enum_2Enum @ V5t0)) = V6c))) | ((p@(ap@V12p1@(inj__ty_2Enum_2Enum @ V5t0))) & ((~~ (p@(ap@V13p2@(inj__ty_2Enum_2Enum @ V5t0)))) & (p@(ap@V0Phi__I@(ap@V14q@(inj__ty_2Enum_2Enum @ V5t0))))))) & (( ! [V15t:tp__ty_2Enum_2Enum] : (((~~ (p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))) & ((~~ (p@(ap@V13p2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))) & (((ap@V14q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))) = V6c) & ((~~ (p@(ap@V4phi@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))) & ((~~ (p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))) & ((~~ (p@(ap@V13p2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))) & ((ap@V14q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) = V6c))))))) | (((~~ (p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))) & ((~~ (p@(ap@V13p2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))) & (((ap@V14q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))) = V6c) & ((~~ (p@(ap@V4phi@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))) & ((p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & ((~~ (p@(ap@V13p2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))) & (p@(ap@V0Phi__I@(ap@V14q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))))) | (((p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0)))) & ((~~ (p@(ap@V13p2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))) & ((p@(ap@V4phi@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0)))) & ((p@(ap@V0Phi__I@(ap@V14q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))) & ((p@(ap@V1Phi__R@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@(ap@V2i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))@(ap@V14q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0)))))) & ((p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & (p@(ap@V13p2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))))) | ((p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0)))) & ((p@(ap@V13p2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0)))) & ((p@(ap@V1Phi__R@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@(ap@V2i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))@(ap@V14q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0)))))) & ((p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & (p@(ap@V13p2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))))))) & (? [V16t1:tp__ty_2Enum_2Enum] : ( ! [V17t2:tp__ty_2Enum_2Enum] : ((p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V16t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V17t2))@(inj__ty_2Enum_2Enum @ V5t0))))) & (p@(ap@V3Psi@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@(ap@V2i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V16t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V17t2))@(inj__ty_2Enum_2Enum @ V5t0)))))@(ap@V14q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V16t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V17t2))@(inj__ty_2Enum_2Enum @ V5t0))))))))))))))))))))))))))))))))))).
thf(conj_thm_2EOmega__Automata_2ECO__BUECHI__WHEN__CLOSURE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0Phi__I:$i] : ((mem@V0Phi__I@(arr@A_27b@bool)) => ( ! [V1Phi__R:$i] : ((mem@V1Phi__R@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)) => ( ! [V2i:$i] : ((mem@V2i@(arr@ty_2Enum_2Enum@A_27a)) => ( ! [V3Psi:$i] : ((mem@V3Psi@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)) => ( ! [V4phi:$i] : ((mem@V4phi@(arr@ty_2Enum_2Enum@bool)) => ( ! [V5t0:tp__ty_2Enum_2Enum] : ( ! [V6c:$i] : ((mem@V6c@A_27b) => ((p@(ap@(ap@(ap@c_2ETemporal__Logic_2EWHEN@(lam@ty_2Enum_2Enum@(^ [V7t0:$i] : (ap@(c_2Ebool_2E_3F@(arr@ty_2Enum_2Enum@A_27b))@(lam@(arr@ty_2Enum_2Enum@A_27b)@(^ [V8q:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0Phi__I@(ap@V8q@V7t0)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(c_2Ebool_2E_21@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V9t:$i] : (ap@V1Phi__R@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@(ap@V2i@(ap@(ap@c_2Earithmetic_2E_2B@V9t)@V7t0)))@(ap@V8q@(ap@(ap@c_2Earithmetic_2E_2B@V9t)@V7t0))))))))@(ap@(c_2Ebool_2E_3F@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V10t1:$i] : (ap@(c_2Ebool_2E_21@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V11t2:$i] : (ap@V3Psi@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@(ap@V2i@(ap@(ap@c_2Earithmetic_2E_2B@V10t1)@(ap@(ap@c_2Earithmetic_2E_2B@V11t2)@V7t0))))@(ap@V8q@(ap@(ap@c_2Earithmetic_2E_2B@V10t1)@(ap@(ap@c_2Earithmetic_2E_2B@V11t2)@V7t0)))))))))))))))))))@V4phi)@(inj__ty_2Enum_2Enum @ V5t0))) <=> (? [V12p1:$i] : ((mem@V12p1@(arr@ty_2Enum_2Enum@bool)) & (? [V13p2:$i] : ((mem@V13p2@(arr@ty_2Enum_2Enum@bool)) & (? [V14q:$i] : ((mem@V14q@(arr@ty_2Enum_2Enum@A_27b)) & ((((~~ (p@(ap@V12p1@(inj__ty_2Enum_2Enum @ V5t0)))) & ((~~ (p@(ap@V13p2@(inj__ty_2Enum_2Enum @ V5t0)))) & ((ap@V14q@(inj__ty_2Enum_2Enum @ V5t0)) = V6c))) | ((p@(ap@V12p1@(inj__ty_2Enum_2Enum @ V5t0))) & ((~~ (p@(ap@V13p2@(inj__ty_2Enum_2Enum @ V5t0)))) & (p@(ap@V0Phi__I@(ap@V14q@(inj__ty_2Enum_2Enum @ V5t0))))))) & (( ! [V15t:tp__ty_2Enum_2Enum] : (((~~ (p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))) & ((~~ (p@(ap@V13p2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))) & (((ap@V14q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))) = V6c) & ((~~ (p@(ap@V4phi@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))) & ((~~ (p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))) & ((~~ (p@(ap@V13p2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))) & ((ap@V14q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) = V6c))))))) | (((~~ (p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))) & ((~~ (p@(ap@V13p2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))) & (((ap@V14q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))) = V6c) & ((~~ (p@(ap@V4phi@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))) & ((p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & ((~~ (p@(ap@V13p2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))) & (p@(ap@V0Phi__I@(ap@V14q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))))) | (((p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0)))) & ((~~ (p@(ap@V13p2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))) & ((p@(ap@V4phi@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0)))) & ((p@(ap@V0Phi__I@(ap@V14q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))) & ((p@(ap@V1Phi__R@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@(ap@V2i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))@(ap@V14q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0)))))) & ((p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & (p@(ap@V13p2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))))) | ((p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0)))) & ((p@(ap@V13p2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0)))) & ((p@(ap@V1Phi__R@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@(ap@V2i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0))))@(ap@V14q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(inj__ty_2Enum_2Enum @ V5t0)))))) & ((p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & (p@(ap@V13p2@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))))))) & (? [V16t1:tp__ty_2Enum_2Enum] : ( ! [V17t2:tp__ty_2Enum_2Enum] : ((~~ (p@(ap@V12p1@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V16t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V17t2))@(inj__ty_2Enum_2Enum @ V5t0)))))) | (p@(ap@V3Psi@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@(ap@V2i@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V16t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V17t2))@(inj__ty_2Enum_2Enum @ V5t0)))))@(ap@V14q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V16t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V17t2))@(inj__ty_2Enum_2Enum @ V5t0))))))))))))))))))))))))))))))))))).
thf(conj_thm_2EOmega__Automata_2ENEXT__AS__CO__BUECHI,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1t0:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V0a)@(inj__ty_2Enum_2Enum @ V1t0))) <=> (? [V2p:$i] : ((mem@V2p@(arr@ty_2Enum_2Enum@bool)) & (? [V3q:$i] : ((mem@V3q@(arr@ty_2Enum_2Enum@bool)) & (((~~ (p@(ap@V2p@(inj__ty_2Enum_2Enum @ V1t0)))) & (~~ (p@(ap@V3q@(inj__ty_2Enum_2Enum @ V1t0))))) & (( ! [V4t:tp__ty_2Enum_2Enum] : (((~~ (p@(ap@V2p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V1t0))))) & ((~~ (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V1t0))))) & ((p@(ap@V2p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V1t0))))) & (~~ (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V1t0))))))))) | (((p@(ap@V2p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V1t0)))) & ((~~ (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V1t0))))) & ((p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V1t0)))) & ((p@(ap@V2p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V1t0))))) & (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V1t0))))))))) | ((p@(ap@V2p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V1t0)))) & ((p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V1t0)))) & ((p@(ap@V2p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V1t0))))) & (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V1t0))))))))))) & (? [V5t1:tp__ty_2Enum_2Enum] : ( ! [V6t2:tp__ty_2Enum_2Enum] : (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V6t2))@(inj__ty_2Enum_2Enum @ V1t0)))))))))))))))))).
thf(conj_thm_2EOmega__Automata_2ESUNTIL__AS__CO__BUECHI,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@ty_2Enum_2Enum@bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V0a)@V1b)@(inj__ty_2Enum_2Enum @ V2t0))) <=> (? [V3q:$i] : ((mem@V3q@(arr@ty_2Enum_2Enum@bool)) & ((~~ (p@(ap@V3q@(inj__ty_2Enum_2Enum @ V2t0)))) & (( ! [V4t:tp__ty_2Enum_2Enum] : (((~~ (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0))))) & ((p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0)))) & ((~~ (p@(ap@V1b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0))))) & (~~ (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V2t0))))))))) | (((~~ (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0))))) & ((p@(ap@V1b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0)))) & (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V2t0))))))) | ((p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0)))) & (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V2t0))))))))) & (? [V5t1:tp__ty_2Enum_2Enum] : ( ! [V6t2:tp__ty_2Enum_2Enum] : (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V6t2))@(inj__ty_2Enum_2Enum @ V2t0)))))))))))))))))).
thf(conj_thm_2EOmega__Automata_2EUNTIL__AS__CO__BUECHI,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@ty_2Enum_2Enum@bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@(ap@c_2ETemporal__Logic_2EUNTIL@V0a)@V1b)@(inj__ty_2Enum_2Enum @ V2t0))) <=> (? [V3q:$i] : ((mem@V3q@(arr@ty_2Enum_2Enum@bool)) & ((~~ (p@(ap@V3q@(inj__ty_2Enum_2Enum @ V2t0)))) & (( ! [V4t:tp__ty_2Enum_2Enum] : (((~~ (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0))))) & ((p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0)))) & ((~~ (p@(ap@V1b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0))))) & (~~ (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V2t0))))))))) | (((~~ (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0))))) & ((p@(ap@V1b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0)))) & (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V2t0))))))) | ((p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0)))) & (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V2t0))))))))) & (? [V5t1:tp__ty_2Enum_2Enum] : ( ! [V6t2:tp__ty_2Enum_2Enum] : ((~~ (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V6t2))@(inj__ty_2Enum_2Enum @ V2t0)))))) | (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V6t2))@(inj__ty_2Enum_2Enum @ V2t0))))))))))))))))))).
thf(conj_thm_2EOmega__Automata_2ESBEFORE__AS__CO__BUECHI,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@ty_2Enum_2Enum@bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@(ap@c_2ETemporal__Logic_2ESBEFORE@V0a)@V1b)@(inj__ty_2Enum_2Enum @ V2t0))) <=> (? [V3q:$i] : ((mem@V3q@(arr@ty_2Enum_2Enum@bool)) & ((~~ (p@(ap@V3q@(inj__ty_2Enum_2Enum @ V2t0)))) & (( ! [V4t:tp__ty_2Enum_2Enum] : (((~~ (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0))))) & ((~~ (p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0))))) & ((~~ (p@(ap@V1b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0))))) & (~~ (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V2t0))))))))) | (((~~ (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0))))) & ((p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0)))) & ((~~ (p@(ap@V1b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0))))) & (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V2t0)))))))) | ((p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0)))) & (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V2t0))))))))) & (? [V5t1:tp__ty_2Enum_2Enum] : ( ! [V6t2:tp__ty_2Enum_2Enum] : (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V6t2))@(inj__ty_2Enum_2Enum @ V2t0)))))))))))))))))).
thf(conj_thm_2EOmega__Automata_2EBEFORE__AS__CO__BUECHI,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@ty_2Enum_2Enum@bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@V0a)@V1b)@(inj__ty_2Enum_2Enum @ V2t0))) <=> (? [V3q:$i] : ((mem@V3q@(arr@ty_2Enum_2Enum@bool)) & ((~~ (p@(ap@V3q@(inj__ty_2Enum_2Enum @ V2t0)))) & (( ! [V4t:tp__ty_2Enum_2Enum] : (((~~ (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0))))) & ((~~ (p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0))))) & ((~~ (p@(ap@V1b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0))))) & (~~ (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V2t0))))))))) | (((~~ (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0))))) & ((p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0)))) & ((~~ (p@(ap@V1b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0))))) & (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V2t0)))))))) | ((p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0)))) & (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V2t0))))))))) & (? [V5t1:tp__ty_2Enum_2Enum] : ( ! [V6t2:tp__ty_2Enum_2Enum] : ((~~ (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V6t2))@(inj__ty_2Enum_2Enum @ V2t0)))))) | (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V6t2))@(inj__ty_2Enum_2Enum @ V2t0))))))))))))))))))).
thf(conj_thm_2EOmega__Automata_2ESWHEN__AS__CO__BUECHI,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@ty_2Enum_2Enum@bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@(ap@c_2ETemporal__Logic_2ESWHEN@V0a)@V1b)@(inj__ty_2Enum_2Enum @ V2t0))) <=> (? [V3q:$i] : ((mem@V3q@(arr@ty_2Enum_2Enum@bool)) & ((~~ (p@(ap@V3q@(inj__ty_2Enum_2Enum @ V2t0)))) & (( ! [V4t:tp__ty_2Enum_2Enum] : (((~~ (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0))))) & ((~~ (p@(ap@V1b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0))))) & (~~ (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V2t0)))))))) | (((~~ (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0))))) & ((p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0)))) & ((p@(ap@V1b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0)))) & (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V2t0)))))))) | ((p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0)))) & (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V2t0))))))))) & (? [V5t1:tp__ty_2Enum_2Enum] : ( ! [V6t2:tp__ty_2Enum_2Enum] : (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V6t2))@(inj__ty_2Enum_2Enum @ V2t0)))))))))))))))))).
thf(conj_thm_2EOmega__Automata_2EWHEN__AS__CO__BUECHI,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@ty_2Enum_2Enum@bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@(ap@c_2ETemporal__Logic_2EWHEN@V0a)@V1b)@(inj__ty_2Enum_2Enum @ V2t0))) <=> (? [V3q:$i] : ((mem@V3q@(arr@ty_2Enum_2Enum@bool)) & ((~~ (p@(ap@V3q@(inj__ty_2Enum_2Enum @ V2t0)))) & (( ! [V4t:tp__ty_2Enum_2Enum] : (((~~ (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0))))) & ((~~ (p@(ap@V1b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0))))) & (~~ (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V2t0)))))))) | (((~~ (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0))))) & ((p@(ap@V0a@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0)))) & ((p@(ap@V1b@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0)))) & (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V2t0)))))))) | ((p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0)))) & (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4t))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V2t0))))))))) & (? [V5t1:tp__ty_2Enum_2Enum] : ( ! [V6t2:tp__ty_2Enum_2Enum] : ((~~ (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V6t2))@(inj__ty_2Enum_2Enum @ V2t0)))))) | (p@(ap@V3q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5t1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V6t2))@(inj__ty_2Enum_2Enum @ V2t0))))))))))))))))))).
thf(conj_thm_2EOmega__Automata_2EBUECHI__PERIODIC__MODEL,lemma,( ! [A_27a:del]: ( ! [A_27state:del]: ( ! [V0InitState:$i] : ((mem@V0InitState@(arr@A_27state@bool)) => ( ! [V1TransRel:$i] : ((mem@V1TransRel@(arr@(ty_2Epair_2Eprod@A_27a@(ty_2Epair_2Eprod@A_27state@A_27state))@bool)) => ( ! [V2Accept:$i] : ((mem@V2Accept@(arr@A_27state@bool)) => (( ! [V3s:$i] : ((mem@V3s@(arr@ty_2Enum_2Enum@A_27state)) => (? [V4x0:tp__ty_2Enum_2Enum] : (? [V5l:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V5l))) & ((ap@V3s@(inj__ty_2Enum_2Enum @ V4x0)) = (ap@V3s@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4x0))@(inj__ty_2Enum_2Enum @ V5l))))))))) => ((? [V6i:$i] : ((mem@V6i@(arr@ty_2Enum_2Enum@A_27a)) & (? [V7q:$i] : ((mem@V7q@(arr@ty_2Enum_2Enum@A_27state)) & ((p@(ap@V0InitState@(ap@V7q@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) & (( ! [V8t:tp__ty_2Enum_2Enum] : (p@(ap@V1TransRel@(ap@(ap@(c_2Epair_2E_2C@A_27a@(ty_2Epair_2Eprod@A_27state@A_27state))@(ap@V6i@(inj__ty_2Enum_2Enum @ V8t)))@(ap@(ap@(c_2Epair_2E_2C@A_27state@A_27state)@(ap@V7q@(inj__ty_2Enum_2Enum @ V8t)))@(ap@V7q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V8t))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) & ( ! [V9t1:tp__ty_2Enum_2Enum] : (? [V10t2:tp__ty_2Enum_2Enum] : (p@(ap@V2Accept@(ap@V7q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V9t1))@(inj__ty_2Enum_2Enum @ V10t2))))))))))))) <=> (? [V11x0:tp__ty_2Enum_2Enum] : (? [V12l:tp__ty_2Enum_2Enum] : (? [V13j:$i] : ((mem@V13j@(arr@ty_2Enum_2Enum@A_27a)) & (? [V14p:$i] : ((mem@V14p@(arr@ty_2Enum_2Enum@A_27state)) & ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V12l))) & (( ! [V15t2:tp__ty_2Enum_2Enum] : ((ap@V13j@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11x0))@(inj__ty_2Enum_2Enum @ V15t2))) = (ap@V13j@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11x0))@(ap@(ap@c_2Earithmetic_2EMOD@(inj__ty_2Enum_2Enum @ V15t2))@(inj__ty_2Enum_2Enum @ V12l)))))) & (( ! [V16t2:tp__ty_2Enum_2Enum] : ((ap@V14p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11x0))@(inj__ty_2Enum_2Enum @ V16t2))) = (ap@V14p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11x0))@(ap@(ap@c_2Earithmetic_2EMOD@(inj__ty_2Enum_2Enum @ V16t2))@(inj__ty_2Enum_2Enum @ V12l)))))) & ((p@(ap@V0InitState@(ap@V14p@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) & (( ! [V17t:tp__ty_2Enum_2Enum] : (p@(ap@V1TransRel@(ap@(ap@(c_2Epair_2E_2C@A_27a@(ty_2Epair_2Eprod@A_27state@A_27state))@(ap@V13j@(inj__ty_2Enum_2Enum @ V17t)))@(ap@(ap@(c_2Epair_2E_2C@A_27state@A_27state)@(ap@V14p@(inj__ty_2Enum_2Enum @ V17t)))@(ap@V14p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V17t))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) & ( ! [V18t1:tp__ty_2Enum_2Enum] : (? [V19t2:tp__ty_2Enum_2Enum] : (p@(ap@V2Accept@(ap@V14p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V18t1))@(inj__ty_2Enum_2Enum @ V19t2))))))))))))))))))))))))))))).
thf(conj_thm_2EOmega__Automata_2EBUECHI__PERIODIC__REDUCTION__THM,lemma,( ! [A_27a:del]: ( ! [A_27state:del]: ( ! [V0InitState:$i] : ((mem@V0InitState@(arr@A_27state@bool)) => ( ! [V1TransRel:$i] : ((mem@V1TransRel@(arr@(ty_2Epair_2Eprod@A_27a@(ty_2Epair_2Eprod@A_27state@A_27state))@bool)) => ( ! [V2Accept:$i] : ((mem@V2Accept@(arr@A_27state@bool)) => (( ! [V3s:$i] : ((mem@V3s@(arr@ty_2Enum_2Enum@A_27state)) => (? [V4x0:tp__ty_2Enum_2Enum] : (? [V5l:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V5l))) & ((ap@V3s@(inj__ty_2Enum_2Enum @ V4x0)) = (ap@V3s@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4x0))@(inj__ty_2Enum_2Enum @ V5l))))))))) => ((? [V6i:$i] : ((mem@V6i@(arr@ty_2Enum_2Enum@A_27a)) & (? [V7q:$i] : ((mem@V7q@(arr@ty_2Enum_2Enum@A_27state)) & ((p@(ap@V0InitState@(ap@V7q@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) & (( ! [V8t:tp__ty_2Enum_2Enum] : (p@(ap@V1TransRel@(ap@(ap@(c_2Epair_2E_2C@A_27a@(ty_2Epair_2Eprod@A_27state@A_27state))@(ap@V6i@(inj__ty_2Enum_2Enum @ V8t)))@(ap@(ap@(c_2Epair_2E_2C@A_27state@A_27state)@(ap@V7q@(inj__ty_2Enum_2Enum @ V8t)))@(ap@V7q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V8t))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) & ( ! [V9t1:tp__ty_2Enum_2Enum] : (? [V10t2:tp__ty_2Enum_2Enum] : (p@(ap@V2Accept@(ap@V7q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V9t1))@(inj__ty_2Enum_2Enum @ V10t2))))))))))))) <=> (? [V11x0:tp__ty_2Enum_2Enum] : (? [V12l:tp__ty_2Enum_2Enum] : (? [V13j:$i] : ((mem@V13j@(arr@ty_2Enum_2Enum@A_27a)) & (? [V14p:$i] : ((mem@V14p@(arr@ty_2Enum_2Enum@A_27state)) & ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V12l))) & (( ! [V15t2:tp__ty_2Enum_2Enum] : ((ap@V13j@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11x0))@(inj__ty_2Enum_2Enum @ V15t2))) = (ap@V13j@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11x0))@(ap@(ap@c_2Earithmetic_2EMOD@(inj__ty_2Enum_2Enum @ V15t2))@(inj__ty_2Enum_2Enum @ V12l)))))) & (( ! [V16t2:tp__ty_2Enum_2Enum] : ((ap@V14p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11x0))@(inj__ty_2Enum_2Enum @ V16t2))) = (ap@V14p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11x0))@(ap@(ap@c_2Earithmetic_2EMOD@(inj__ty_2Enum_2Enum @ V16t2))@(inj__ty_2Enum_2Enum @ V12l)))))) & ((p@(ap@V0InitState@(ap@V14p@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) & (( ! [V17t:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V17t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11x0))@(inj__ty_2Enum_2Enum @ V12l)))) => (p@(ap@V1TransRel@(ap@(ap@(c_2Epair_2E_2C@A_27a@(ty_2Epair_2Eprod@A_27state@A_27state))@(ap@V13j@(inj__ty_2Enum_2Enum @ V17t)))@(ap@(ap@(c_2Epair_2E_2C@A_27state@A_27state)@(ap@V14p@(inj__ty_2Enum_2Enum @ V17t)))@(ap@V14p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V17t))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) & (? [V18t:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V18t))@(inj__ty_2Enum_2Enum @ V12l))) & (p@(ap@V2Accept@(ap@V14p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11x0))@(inj__ty_2Enum_2Enum @ V18t))))))))))))))))))))))))))))).
thf(conj_thm_2EOmega__Automata_2EBUECHI__PROP__REDUCTION,lemma,( ! [A_27a:del]: ( ! [A_27state:del]: ( ! [V0InitState:$i] : ((mem@V0InitState@(arr@A_27state@bool)) => ( ! [V1TransRel:$i] : ((mem@V1TransRel@(arr@(ty_2Epair_2Eprod@A_27a@(ty_2Epair_2Eprod@A_27state@A_27state))@bool)) => ( ! [V2Accept:$i] : ((mem@V2Accept@(arr@A_27state@bool)) => (( ! [V3s:$i] : ((mem@V3s@(arr@ty_2Enum_2Enum@A_27state)) => (? [V4x0:tp__ty_2Enum_2Enum] : (? [V5l:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V5l))) & ((ap@V3s@(inj__ty_2Enum_2Enum @ V4x0)) = (ap@V3s@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4x0))@(inj__ty_2Enum_2Enum @ V5l))))))))) => ((? [V6i:$i] : ((mem@V6i@(arr@ty_2Enum_2Enum@A_27a)) & (? [V7q:$i] : ((mem@V7q@(arr@ty_2Enum_2Enum@A_27state)) & ((p@(ap@V0InitState@(ap@V7q@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) & (( ! [V8t:tp__ty_2Enum_2Enum] : (p@(ap@V1TransRel@(ap@(ap@(c_2Epair_2E_2C@A_27a@(ty_2Epair_2Eprod@A_27state@A_27state))@(ap@V6i@(inj__ty_2Enum_2Enum @ V8t)))@(ap@(ap@(c_2Epair_2E_2C@A_27state@A_27state)@(ap@V7q@(inj__ty_2Enum_2Enum @ V8t)))@(ap@V7q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V8t))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) & ( ! [V9t1:tp__ty_2Enum_2Enum] : (? [V10t2:tp__ty_2Enum_2Enum] : (p@(ap@V2Accept@(ap@V7q@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V9t1))@(inj__ty_2Enum_2Enum @ V10t2))))))))))))) <=> (? [V11x0:tp__ty_2Enum_2Enum] : (? [V12l:tp__ty_2Enum_2Enum] : (? [V13j:$i] : ((mem@V13j@(arr@ty_2Enum_2Enum@A_27a)) & (? [V14p:$i] : ((mem@V14p@(arr@ty_2Enum_2Enum@A_27state)) & ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V12l))) & ((p@(ap@V0InitState@(ap@V14p@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) & (( ! [V15t:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V15t))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11x0))@(inj__ty_2Enum_2Enum @ V12l)))) => (p@(ap@V1TransRel@(ap@(ap@(c_2Epair_2E_2C@A_27a@(ty_2Epair_2Eprod@A_27state@A_27state))@(ap@V13j@(inj__ty_2Enum_2Enum @ V15t)))@(ap@(ap@(c_2Epair_2E_2C@A_27state@A_27state)@(ap@V14p@(inj__ty_2Enum_2Enum @ V15t)))@(ap@V14p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V15t))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) & ((? [V16t:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V16t))@(inj__ty_2Enum_2Enum @ V12l))) & (p@(ap@V2Accept@(ap@V14p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11x0))@(inj__ty_2Enum_2Enum @ V16t))))))) & ((ap@V14p@(inj__ty_2Enum_2Enum @ V11x0)) = (ap@V14p@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V11x0))@(inj__ty_2Enum_2Enum @ V12l))))))))))))))))))))))))).
thf(conj_thm_2EOmega__Automata_2EEQUALITY__THM,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => ((V0x = V1y) <=> ( ! [V2P:$i] : ((mem@V2P@(arr@A_27a@bool)) => ((p@(ap@V2P@V0x)) <=> (p@(ap@V2P@V1y)))))))))))).
thf(conj_thm_2EOmega__Automata_2ELESS__THM,lemma,( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1y:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0x))@(inj__ty_2Enum_2Enum @ V1y))) <=> (? [V2P:$i] : ((mem@V2P@(arr@ty_2Enum_2Enum@bool)) & ((p@(ap@V2P@(inj__ty_2Enum_2Enum @ V0x))) & ((~~ (p@(ap@V2P@(inj__ty_2Enum_2Enum @ V1y)))) & ( ! [V3z:tp__ty_2Enum_2Enum] : ((p@(ap@V2P@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V3z)))) => (p@(ap@V2P@(inj__ty_2Enum_2Enum @ V3z))))))))))))).
thf(conj_thm_2EOmega__Automata_2EFORALL__EXISTS__THM,lemma,( ! [V0P:$i] : ((mem@V0P@(arr@ty_2Enum_2Enum@bool)) => (( ! [V1t1:tp__ty_2Enum_2Enum] : (? [V2t2:tp__ty_2Enum_2Enum] : (p@(ap@V0P@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V1t1))@(inj__ty_2Enum_2Enum @ V2t2)))))) <=> ( ! [V3t1:tp__ty_2Enum_2Enum] : (? [V4t2:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V3t1))@(inj__ty_2Enum_2Enum @ V4t2))) & (p@(ap@V0P@(inj__ty_2Enum_2Enum @ V4t2)))))))))).
thf(conj_thm_2EOmega__Automata_2EEXISTS__FORALL__THM,lemma,( ! [V0P:$i] : ((mem@V0P@(arr@ty_2Enum_2Enum@bool)) => ((? [V1t1:tp__ty_2Enum_2Enum] : ( ! [V2t2:tp__ty_2Enum_2Enum] : (p@(ap@V0P@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V1t1))@(inj__ty_2Enum_2Enum @ V2t2)))))) <=> (? [V3t1:tp__ty_2Enum_2Enum] : ( ! [V4t2:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V3t1))@(inj__ty_2Enum_2Enum @ V4t2))) => (p@(ap@V0P@(inj__ty_2Enum_2Enum @ V4t2)))))))))).
thf(conj_thm_2EOmega__Automata_2EELGOT__LEMMA,conjecture,( ! [A_27a:del]: ( ! [V0PHI:$i] : ((mem@V0PHI@(arr@(arr@A_27a@bool)@(arr@A_27a@bool))) => ((? [V1x:$i] : ((mem@V1x@A_27a) & ( ! [V2p:$i] : ((mem@V2p@(arr@A_27a@bool)) => (p@(ap@(ap@V0PHI@V2p)@V1x)))))) <=> (? [V3q:$i] : ((mem@V3q@(arr@A_27a@bool)) & (( ! [V4x:$i] : ((mem@V4x@A_27a) => ((p@(ap@V3q@V4x)) => ( ! [V5p:$i] : ((mem@V5p@(arr@A_27a@bool)) => (p@(ap@(ap@V0PHI@V5p)@V4x))))))) & (? [V6z:$i] : ((mem@V6z@A_27a) & (p@(ap@V3q@V6z)))))))))))).
