let E be non empty set ; :: thesis: for A being non empty automaton over (Lex E) \/ {(<%> E)} holds Lang A = Lang (_bool A)

let A be non empty automaton over (Lex E) \/ {(<%> E)}; :: thesis: Lang A = Lang (_bool A)

set DA = _bool A;

A1: for w being Element of E ^omega st w in Lang A holds

w in Lang (_bool A)

w in Lang A

let A be non empty automaton over (Lex E) \/ {(<%> E)}; :: thesis: Lang A = Lang (_bool A)

set DA = _bool A;

A1: for w being Element of E ^omega st w in Lang A holds

w in Lang (_bool A)

proof

for w being Element of E ^omega st w in Lang (_bool A) holds
let w be Element of E ^omega ; :: thesis: ( w in Lang A implies w in Lang (_bool A) )

assume w in Lang A ; :: thesis: w in Lang (_bool A)

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 (_bool A) by Th33;

w -succ_of ( the InitS of (_bool A),(_bool A)) = {(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 (_bool A),(_bool A)) by TARSKI:def 1;

then w -succ_of ( the InitS of (_bool A),(_bool A)) meets the FinalS of (_bool A) by A2, XBOOLE_0:3;

hence w in Lang (_bool A) by Th19; :: thesis: verum

end;assume w in Lang A ; :: thesis: w in Lang (_bool A)

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 (_bool A) by Th33;

w -succ_of ( the InitS of (_bool A),(_bool A)) = {(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 (_bool A),(_bool A)) by TARSKI:def 1;

then w -succ_of ( the InitS of (_bool A),(_bool A)) meets the FinalS of (_bool A) by A2, XBOOLE_0:3;

hence w in Lang (_bool A) by Th19; :: thesis: verum

w in Lang A

proof

hence
Lang A = Lang (_bool A)
by A1, SUBSET_1:3; :: thesis: verum
let w be Element of E ^omega ; :: thesis: ( w in Lang (_bool A) implies w in Lang A )

assume w in Lang (_bool A) ; :: thesis: w in Lang A

then w -succ_of ( the InitS of (_bool A),(_bool A)) meets the FinalS of (_bool A) by Th19;

then consider x being object such that

A3: x in w -succ_of ( the InitS of (_bool A),(_bool A)) and

A4: x in the FinalS of (_bool A) by XBOOLE_0:3;

w -succ_of ( the InitS of (_bool A),(_bool A)) = {(w -succ_of ( the InitS of A,A))} by Th37;

then x = w -succ_of ( the InitS of A,A) by A3, TARSKI:def 1;

then w -succ_of ( the InitS of A,A) meets the FinalS of A by A4, Th34;

hence w in Lang A by Th19; :: thesis: verum

end;assume w in Lang (_bool A) ; :: thesis: w in Lang A

then w -succ_of ( the InitS of (_bool A),(_bool A)) meets the FinalS of (_bool A) by Th19;

then consider x being object such that

A3: x in w -succ_of ( the InitS of (_bool A),(_bool A)) and

A4: x in the FinalS of (_bool A) by XBOOLE_0:3;

w -succ_of ( the InitS of (_bool A),(_bool A)) = {(w -succ_of ( the InitS of A,A))} by Th37;

then x = w -succ_of ( the InitS of A,A) by A3, TARSKI:def 1;

then w -succ_of ( the InitS of A,A) meets the FinalS of A by A4, Th34;

hence w in Lang A by Th19; :: thesis: verum