begin
begin
begin
definition
let M be ( (
Function-like quasi_total ) ( non
empty Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) )
-defined bool props : ( ( ) (
functional )
Subset of ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
LTLModel) ;
func SAT M -> ( (
Function-like quasi_total ) ( non
empty Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set )
-defined BOOLEAN : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total boolean-valued )
Function of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
means
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) holds
(
it : ( (
V41()
V100()
V101()
V102()
V149()
V150()
V151()
V152()
V163() ) (
V41()
V100()
V101()
V102()
V149()
V150()
V151()
V152()
V163() )
L6())
. [n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,TFALSUM : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( )
Element of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) )
= 0 : ( ( ) (
empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11()
V12()
Function-like functional ext-real non
positive non
negative V104() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) & ( for
k being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) holds
(
it : ( (
V41()
V100()
V101()
V102()
V149()
V150()
V151()
V152()
V163() ) (
V41()
V100()
V101()
V102()
V149()
V150()
V151()
V152()
V163() )
L6())
. [n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,(prop k : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ) : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( )
Element of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) )
= 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) iff
prop k : ( ( ) (
Relation-like Function-like FinSequence-like )
Element of
LTLB_WFF : ( ( ) ( non
empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed )
set ) ) : ( ( ) (
Relation-like Function-like FinSequence-like )
Element of
LTLB_WFF : ( ( ) ( non
empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed )
set ) )
in M : ( ( non
empty V106() ) ( non
empty V106() )
set )
. n : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
functional )
Element of
bool props : ( ( ) (
functional )
Subset of ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) ) ) & ( for
p,
q being ( ( ) (
Relation-like Function-like FinSequence-like )
Element of
LTLB_WFF : ( ( ) ( non
empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed )
set ) ) holds
(
it : ( (
V41()
V100()
V101()
V102()
V149()
V150()
V151()
V152()
V163() ) (
V41()
V100()
V101()
V102()
V149()
V150()
V151()
V152()
V163() )
L6())
. [n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,(p : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) => q : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ) : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( )
Element of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) )
= (it : ( ( V41() V100() V101() V102() V149() V150() V151() V152() V163() ) ( V41() V100() V101() V102() V149() V150() V151() V152() V163() ) L6()) . [n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,p : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( ) Element of [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non empty ) set ) ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) )
=> (it : ( ( V41() V100() V101() V102() V149() V150() V151() V152() V163() ) ( V41() V100() V101() V102() V149() V150() V151() V152() V163() ) L6()) . [n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,q : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( ) Element of [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non empty ) set ) ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
set ) & (
it : ( (
V41()
V100()
V101()
V102()
V149()
V150()
V151()
V152()
V163() ) (
V41()
V100()
V101()
V102()
V149()
V150()
V151()
V152()
V163() )
L6())
. [n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,(p : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) 'Us' q : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ) : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( )
Element of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) )
= 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) implies ex
i being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) st
(
0 : ( ( ) (
empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11()
V12()
Function-like functional ext-real non
positive non
negative V104() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) )
< i : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) &
it : ( (
V41()
V100()
V101()
V102()
V149()
V150()
V151()
V152()
V163() ) (
V41()
V100()
V101()
V102()
V149()
V150()
V151()
V152()
V163() )
L6())
. [(n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) + i : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,q : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( )
Element of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) )
= 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) & ( for
j being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) st 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) )
<= j : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) &
j : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) )
< i : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) holds
it : ( (
V41()
V100()
V101()
V102()
V149()
V150()
V151()
V152()
V163() ) (
V41()
V100()
V101()
V102()
V149()
V150()
V151()
V152()
V163() )
L6())
. [(n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) + j : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,p : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( )
Element of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) )
= 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) ) ) ) & ( ex
i being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) st
(
0 : ( ( ) (
empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11()
V12()
Function-like functional ext-real non
positive non
negative V104() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) )
< i : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) &
it : ( (
V41()
V100()
V101()
V102()
V149()
V150()
V151()
V152()
V163() ) (
V41()
V100()
V101()
V102()
V149()
V150()
V151()
V152()
V163() )
L6())
. [(n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) + i : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,q : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( )
Element of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) )
= 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) & ( for
j being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) st 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) )
<= j : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) &
j : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) )
< i : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) holds
it : ( (
V41()
V100()
V101()
V102()
V149()
V150()
V151()
V152()
V163() ) (
V41()
V100()
V101()
V102()
V149()
V150()
V151()
V152()
V163() )
L6())
. [(n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) + j : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,p : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( )
Element of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) )
= 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) ) ) implies
it : ( (
V41()
V100()
V101()
V102()
V149()
V150()
V151()
V152()
V163() ) (
V41()
V100()
V101()
V102()
V149()
V150()
V151()
V152()
V163() )
L6())
. [n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,(p : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) 'Us' q : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ) : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( )
Element of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) )
= 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) ) ) ) );
end;
theorem
for
A being ( ( ) (
Relation-like Function-like FinSequence-like )
Element of
LTLB_WFF : ( ( ) ( non
empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed )
set ) )
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) )
for
M being ( (
Function-like quasi_total ) ( non
empty Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) )
-defined bool props : ( ( ) (
functional )
Subset of ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
LTLModel) holds
(
(SAT M : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool props : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) LTLModel) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set )
-defined BOOLEAN : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total boolean-valued )
Function of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
. [n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,('not' A : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ) : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( )
Element of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) )
= 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) iff
(SAT M : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool props : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) LTLModel) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set )
-defined BOOLEAN : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total boolean-valued )
Function of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
. [n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,A : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( )
Element of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) )
= 0 : ( ( ) (
empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11()
V12()
Function-like functional ext-real non
positive non
negative V104() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) ) ;
theorem
for
A,
B being ( ( ) (
Relation-like Function-like FinSequence-like )
Element of
LTLB_WFF : ( ( ) ( non
empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed )
set ) )
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) )
for
M being ( (
Function-like quasi_total ) ( non
empty Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) )
-defined bool props : ( ( ) (
functional )
Subset of ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
LTLModel) holds
(
(SAT M : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool props : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) LTLModel) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set )
-defined BOOLEAN : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total boolean-valued )
Function of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
. [n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,(A : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) '&&' B : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ) : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( )
Element of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) )
= 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) iff (
(SAT M : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool props : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) LTLModel) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set )
-defined BOOLEAN : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total boolean-valued )
Function of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
. [n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,A : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( )
Element of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) )
= 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) &
(SAT M : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool props : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) LTLModel) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set )
-defined BOOLEAN : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total boolean-valued )
Function of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
. [n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,B : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( )
Element of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) )
= 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) ) ) ;
theorem
for
A,
B being ( ( ) (
Relation-like Function-like FinSequence-like )
Element of
LTLB_WFF : ( ( ) ( non
empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed )
set ) )
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) )
for
M being ( (
Function-like quasi_total ) ( non
empty Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) )
-defined bool props : ( ( ) (
functional )
Subset of ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
LTLModel) holds
(
(SAT M : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool props : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) LTLModel) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set )
-defined BOOLEAN : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total boolean-valued )
Function of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
. [n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,(A : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) 'or' B : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ) : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( )
Element of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) )
= 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) iff (
(SAT M : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool props : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) LTLModel) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set )
-defined BOOLEAN : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total boolean-valued )
Function of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
. [n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,A : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( )
Element of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) )
= 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) or
(SAT M : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool props : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) LTLModel) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set )
-defined BOOLEAN : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total boolean-valued )
Function of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
. [n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,B : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( )
Element of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) )
= 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) ) ) ;
theorem
for
A being ( ( ) (
Relation-like Function-like FinSequence-like )
Element of
LTLB_WFF : ( ( ) ( non
empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed )
set ) )
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) )
for
M being ( (
Function-like quasi_total ) ( non
empty Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) )
-defined bool props : ( ( ) (
functional )
Subset of ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
LTLModel) holds
(SAT M : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool props : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) LTLModel) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set )
-defined BOOLEAN : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total boolean-valued )
Function of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
. [n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,('X' A : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ) : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( )
Element of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) )
= (SAT M : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool props : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) LTLModel) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set )
-defined BOOLEAN : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total boolean-valued )
Function of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
. [(n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,A : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( )
Element of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) ) ;
theorem
for
A being ( ( ) (
Relation-like Function-like FinSequence-like )
Element of
LTLB_WFF : ( ( ) ( non
empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed )
set ) )
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) )
for
M being ( (
Function-like quasi_total ) ( non
empty Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) )
-defined bool props : ( ( ) (
functional )
Subset of ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
LTLModel) holds
(
(SAT M : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool props : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) LTLModel) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set )
-defined BOOLEAN : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total boolean-valued )
Function of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
. [n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,('G' A : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ) : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( )
Element of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) )
= 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) iff for
i being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) holds
(SAT M : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool props : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) LTLModel) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set )
-defined BOOLEAN : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total boolean-valued )
Function of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
. [(n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) + i : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,A : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( )
Element of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) )
= 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) ) ;
theorem
for
A being ( ( ) (
Relation-like Function-like FinSequence-like )
Element of
LTLB_WFF : ( ( ) ( non
empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed )
set ) )
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) )
for
M being ( (
Function-like quasi_total ) ( non
empty Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) )
-defined bool props : ( ( ) (
functional )
Subset of ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
LTLModel) holds
(
(SAT M : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool props : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) LTLModel) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set )
-defined BOOLEAN : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total boolean-valued )
Function of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
. [n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,('F' A : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ) : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( )
Element of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) )
= 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) iff ex
i being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) st
(SAT M : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool props : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) LTLModel) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set )
-defined BOOLEAN : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total boolean-valued )
Function of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
. [(n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) + i : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,A : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( )
Element of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) )
= 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) ) ;
theorem
for
p,
q being ( ( ) (
Relation-like Function-like FinSequence-like )
Element of
LTLB_WFF : ( ( ) ( non
empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed )
set ) )
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) )
for
M being ( (
Function-like quasi_total ) ( non
empty Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) )
-defined bool props : ( ( ) (
functional )
Subset of ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
LTLModel) holds
(
(SAT M : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool props : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) LTLModel) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set )
-defined BOOLEAN : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total boolean-valued )
Function of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
. [n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,(p : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) 'U' q : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ) : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( )
Element of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) )
= 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) iff ex
i being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) st
(
(SAT M : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool props : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) LTLModel) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set )
-defined BOOLEAN : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total boolean-valued )
Function of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
. [(n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) + i : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,q : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( )
Element of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) )
= 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) & ( for
j being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) st
j : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) )
< i : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) holds
(SAT M : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool props : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) LTLModel) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set )
-defined BOOLEAN : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total boolean-valued )
Function of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
. [(n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) + j : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,p : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( )
Element of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) )
= 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) ) ) ) ;
theorem
for
p,
q being ( ( ) (
Relation-like Function-like FinSequence-like )
Element of
LTLB_WFF : ( ( ) ( non
empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed )
set ) )
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) )
for
M being ( (
Function-like quasi_total ) ( non
empty Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) )
-defined bool props : ( ( ) (
functional )
Subset of ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
LTLModel) holds
(
(SAT M : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool props : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) LTLModel) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set )
-defined BOOLEAN : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total boolean-valued )
Function of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
. [n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,(p : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) 'R' q : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ) : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( )
Element of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) )
= 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) iff ( ex
i being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) st
(
(SAT M : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool props : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) LTLModel) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set )
-defined BOOLEAN : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total boolean-valued )
Function of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
. [(n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) + i : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,p : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( )
Element of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) )
= 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) & ( for
j being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) st
j : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) )
<= i : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) holds
(SAT M : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool props : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) LTLModel) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set )
-defined BOOLEAN : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total boolean-valued )
Function of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
. [(n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) + j : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,q : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( )
Element of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) )
= 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) ) ) or for
i being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) holds
(SAT M : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool props : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) LTLModel) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set )
-defined BOOLEAN : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total boolean-valued )
Function of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
. [(n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) + i : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,q : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( )
Element of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) )
= 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) ) ) ;
theorem
for
B being ( ( ) (
Relation-like Function-like FinSequence-like )
Element of
LTLB_WFF : ( ( ) ( non
empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed )
set ) )
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) )
for
M being ( (
Function-like quasi_total ) ( non
empty Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) )
-defined bool props : ( ( ) (
functional )
Subset of ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
LTLModel) holds
(SAT M : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool props : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) LTLModel) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set )
-defined BOOLEAN : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total boolean-valued )
Function of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
. [n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,('not' ('X' B : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ) : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ) : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( )
Element of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) )
= (SAT M : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool props : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) LTLModel) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set )
-defined BOOLEAN : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total boolean-valued )
Function of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
. [n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,('X' ('not' B : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ) : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ) : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( )
Element of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) ) ;
begin
theorem
for
A being ( ( ) (
Relation-like Function-like FinSequence-like )
Element of
LTLB_WFF : ( ( ) ( non
empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed )
set ) )
for
i,
j being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) )
for
M being ( (
Function-like quasi_total ) ( non
empty Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) )
-defined bool props : ( ( ) (
functional )
Subset of ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
LTLModel) holds
(SAT (M : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool props : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) LTLModel) ^\ i : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool props : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(bool props : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set )
-defined BOOLEAN : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total boolean-valued )
Function of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
. [j : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,A : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( )
Element of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) )
= (SAT M : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool props : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) LTLModel) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set )
-defined BOOLEAN : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total boolean-valued )
Function of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
. [(i : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) + j : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,A : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( )
Element of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) ) ;
theorem
for
A being ( ( ) (
Relation-like Function-like FinSequence-like )
Element of
LTLB_WFF : ( ( ) ( non
empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed )
set ) )
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) )
for
M being ( (
Function-like quasi_total ) ( non
empty Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
bool REAL : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) )
-defined bool props : ( ( ) (
functional )
Subset of ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
LTLModel)
for
f being ( (
Function-like quasi_total ) ( non
empty Relation-like LTLB_WFF : ( ( ) ( non
empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed )
set )
-defined BOOLEAN : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total boolean-valued )
Function of
LTLB_WFF : ( ( ) ( non
empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) ) st ( for
B being ( ( ) ( )
set ) st
B : ( ( ) ( )
set )
in LTLB_WFF : ( ( ) ( non
empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed )
set ) holds
f : ( (
Function-like quasi_total ) ( non
empty Relation-like LTLB_WFF : ( ( ) ( non
empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed )
set )
-defined BOOLEAN : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total boolean-valued )
Function of
LTLB_WFF : ( ( ) ( non
empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
. B : ( ( ) ( )
set ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
set )
= (SAT M : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool props : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) LTLModel) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set )
-defined BOOLEAN : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total boolean-valued )
Function of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
. [n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,B : ( ( ) ( ) set ) ] : ( ( ) ( )
set ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
set ) ) holds
(VAL f : ( ( Function-like quasi_total ) ( non empty Relation-like LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total boolean-valued ) Function of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like LTLB_WFF : ( ( ) ( non
empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed )
set )
-defined BOOLEAN : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total boolean-valued )
Function of
LTLB_WFF : ( ( ) ( non
empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
. A : ( ( ) (
Relation-like Function-like FinSequence-like )
Element of
LTLB_WFF : ( ( ) ( non
empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) )
= (SAT M : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool props : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) LTLModel) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set )
-defined BOOLEAN : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total boolean-valued )
Function of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
. [n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,A : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) ) ] : ( ( ) ( )
Element of
[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,LTLB_WFF : ( ( ) ( non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
V12()
ext-real non
negative boolean )
Element of
BOOLEAN : ( ( ) ( non
empty )
set ) ) ;
begin
definition
let D be ( ( ) ( )
set ) ;
end;
begin