let E be non empty set ; :: thesis: for A being non empty automaton over (Lex E) \/ {(<%> E)} holds Lang A = Lang ()
let A be non empty automaton over (Lex E) \/ {(<%> E)}; :: thesis: Lang A = Lang ()
set DA = _bool A;
A1: for w being Element of E ^omega st w in Lang A holds
w in Lang ()
proof
let w be Element of E ^omega ; :: thesis: ( w in Lang A implies w in Lang () )
assume w in Lang A ; :: thesis: w in Lang ()
then w -succ_of ( the InitS of A,A) meets the FinalS of A by Th19;
then ex x being object st
( x in w -succ_of ( the InitS of A,A) & x in the FinalS of A ) by XBOOLE_0:3;
then A2: w -succ_of ( the InitS of A,A) in the FinalS of () by Th33;
w -succ_of ( the InitS of (),()) = {(w -succ_of ( the InitS of A,A))} by Th37;
then w -succ_of ( the InitS of A,A) in w -succ_of ( the InitS of (),()) by TARSKI:def 1;
then w -succ_of ( the InitS of (),()) meets the FinalS of () by ;
hence w in Lang () by Th19; :: thesis: verum
end;
for w being Element of E ^omega st w in Lang () holds
w in Lang A
proof
let w be Element of E ^omega ; :: thesis: ( w in Lang () implies w in Lang A )
assume w in Lang () ; :: thesis: w in Lang A
then w -succ_of ( the InitS of (),()) meets the FinalS of () by Th19;
then consider x being object such that
A3: x in w -succ_of ( the InitS of (),()) and
A4: x in the FinalS of () by XBOOLE_0:3;
w -succ_of ( the InitS of (),()) = {(w -succ_of ( the InitS of A,A))} by Th37;
then x = w -succ_of ( the InitS of A,A) by ;
then w -succ_of ( the InitS of A,A) meets the FinalS of A by ;
hence w in Lang A by Th19; :: thesis: verum
end;
hence Lang A = Lang () by ; :: thesis: verum