include('Axioms/quotient_sum_2.ax').
tff(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),f2023(A_27state,V0t0,V5q)))))))) <=> ( ! [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),f2024(A_27state,V0t0,V8q))))))))))))))))))))).
tff(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),f2023(A_27state,V0t0,V5q))))))))) <=> (? [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),f2024(A_27state,V0t0,V8q))))))))))))))))))))))).
tff(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))))))))))))))))))))))))))))))).
tff(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)))))))))))))))))))))))))))))))))).
tff(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))))))))))))))))))))))).
tff(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)))))))))))))))))))))).
tff(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)))))))))))))))))))))).
tff(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)))))))))))))))))))))).
tff(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))))))))))))))))))).
tff(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)))))))))))))))))).
tff(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)))))))))))))))))))))).
tff(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))))))))))))))))))))))))))))).
tff(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)))))))))))))))))))))))))))))))))))))))).
tff(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)))))))))))))))))))))))))).
tff(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))))))))))))))))))))))))))))))))))))).
tff(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))))))))))))))))))))))))))))))))))))))))).
tff(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,f2029(A_27a,A_27b,V0Phi__I,V1Phi__R,V2i,V3Psi)),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))))))))))))))))))))))))))))))).
tff(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),f2034(A_27a,A_27b,V1Phi__I,V2Phi__R,V3i,V4Psi)),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)))))))))))))))))))))))))))))))))).
tff(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),f2034(A_27a,A_27b,V1Phi__I,V2Phi__R,V3i,V4Psi)),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)))))))))))))))))))))))))))))))))).
tff(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,f2039(A_27a,A_27b,V0Phi__I,V1Phi__R,V2i,V3Psi)),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)))))))))))))))))))))))))))))))))))).
tff(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,f2039(A_27a,A_27b,V0Phi__I,V1Phi__R,V2i,V3Psi)),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)))))))))))))))))))))))))))))))))))).
tff(conj_thm_2EOmega__Automata_2ECO__BUECHI__SWHEN__CLOSURE,conjecture,(( ! [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,f2039(A_27a,A_27b,V0Phi__I,V1Phi__R,V2i,V3Psi)),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)))))))))))))))))))))))))))))))))))).
