:: MODELC_3 semantic presentation begin definitionlet "F" be ($#m2_finseq_1 :::"LTL-formula":::); :: original: :::"Subformulae"::: redefine func :::"Subformulae"::: "F" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) ); end; definitionlet "H" be ($#m2_finseq_1 :::"LTL-formula":::); func :::"LTLNew1"::: "H" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) "H" ")" ) equals :: MODELC_3:def 1 (Set ($#k2_tarski :::"{"::: ) (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) "H" ")" ) "," (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) "H" ")" ) ($#k2_tarski :::"}"::: ) ) if (Bool "H" "is" ($#v4_modelc_2 :::"conjunctive"::: ) ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) "H" ")" ) ($#k1_tarski :::"}"::: ) ) if (Bool "H" "is" ($#v5_modelc_2 :::"disjunctive"::: ) ) (Set ($#k1_xboole_0 :::"{}"::: ) ) if (Bool "H" "is" ($#v6_modelc_2 :::"next"::: ) ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) "H" ")" ) ($#k1_tarski :::"}"::: ) ) if (Bool "H" "is" ($#v7_modelc_2 :::"Until"::: ) ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) "H" ")" ) ($#k1_tarski :::"}"::: ) ) if (Bool "H" "is" ($#v8_modelc_2 :::"Release"::: ) ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); func :::"LTLNew2"::: "H" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) "H" ")" ) equals :: MODELC_3:def 2 (Set ($#k1_xboole_0 :::"{}"::: ) ) if (Bool "H" "is" ($#v4_modelc_2 :::"conjunctive"::: ) ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) "H" ")" ) ($#k1_tarski :::"}"::: ) ) if (Bool "H" "is" ($#v5_modelc_2 :::"disjunctive"::: ) ) (Set ($#k1_xboole_0 :::"{}"::: ) ) if (Bool "H" "is" ($#v6_modelc_2 :::"next"::: ) ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) "H" ")" ) ($#k1_tarski :::"}"::: ) ) if (Bool "H" "is" ($#v7_modelc_2 :::"Until"::: ) ) (Set ($#k2_tarski :::"{"::: ) (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) "H" ")" ) "," (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) "H" ")" ) ($#k2_tarski :::"}"::: ) ) if (Bool "H" "is" ($#v8_modelc_2 :::"Release"::: ) ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); func :::"LTLNext"::: "H" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) "H" ")" ) equals :: MODELC_3:def 3 (Set ($#k1_xboole_0 :::"{}"::: ) ) if (Bool "H" "is" ($#v4_modelc_2 :::"conjunctive"::: ) ) (Set ($#k1_xboole_0 :::"{}"::: ) ) if (Bool "H" "is" ($#v5_modelc_2 :::"disjunctive"::: ) ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k10_modelc_2 :::"the_argument_of"::: ) "H" ")" ) ($#k1_tarski :::"}"::: ) ) if (Bool "H" "is" ($#v6_modelc_2 :::"next"::: ) ) (Set ($#k1_tarski :::"{"::: ) "H" ($#k1_tarski :::"}"::: ) ) if (Bool "H" "is" ($#v7_modelc_2 :::"Until"::: ) ) (Set ($#k1_tarski :::"{"::: ) "H" ($#k1_tarski :::"}"::: ) ) if (Bool "H" "is" ($#v8_modelc_2 :::"Release"::: ) ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); end; :: deftheorem defines :::"LTLNew1"::: MODELC_3:def 1 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "H")) "is" ($#v4_modelc_2 :::"conjunctive"::: ) )) "implies" (Bool (Set ($#k2_modelc_3 :::"LTLNew1"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) "," (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")) ")" ) ($#k2_tarski :::"}"::: ) )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v5_modelc_2 :::"disjunctive"::: ) )) "implies" (Bool (Set ($#k2_modelc_3 :::"LTLNew1"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) ($#k1_tarski :::"}"::: ) )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v6_modelc_2 :::"next"::: ) )) "implies" (Bool (Set ($#k2_modelc_3 :::"LTLNew1"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v7_modelc_2 :::"Until"::: ) )) "implies" (Bool (Set ($#k2_modelc_3 :::"LTLNew1"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) ($#k1_tarski :::"}"::: ) )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v8_modelc_2 :::"Release"::: ) )) "implies" (Bool (Set ($#k2_modelc_3 :::"LTLNew1"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")) ")" ) ($#k1_tarski :::"}"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "H")) "is" ($#v4_modelc_2 :::"conjunctive"::: ) )) & (Bool (Bool "not" (Set (Var "H")) "is" ($#v5_modelc_2 :::"disjunctive"::: ) )) & (Bool (Bool "not" (Set (Var "H")) "is" ($#v6_modelc_2 :::"next"::: ) )) & (Bool (Bool "not" (Set (Var "H")) "is" ($#v7_modelc_2 :::"Until"::: ) )) & (Bool (Bool "not" (Set (Var "H")) "is" ($#v8_modelc_2 :::"Release"::: ) ))) "implies" (Bool (Set ($#k2_modelc_3 :::"LTLNew1"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" )); :: deftheorem defines :::"LTLNew2"::: MODELC_3:def 2 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "H")) "is" ($#v4_modelc_2 :::"conjunctive"::: ) )) "implies" (Bool (Set ($#k3_modelc_3 :::"LTLNew2"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v5_modelc_2 :::"disjunctive"::: ) )) "implies" (Bool (Set ($#k3_modelc_3 :::"LTLNew2"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")) ")" ) ($#k1_tarski :::"}"::: ) )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v6_modelc_2 :::"next"::: ) )) "implies" (Bool (Set ($#k3_modelc_3 :::"LTLNew2"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v7_modelc_2 :::"Until"::: ) )) "implies" (Bool (Set ($#k3_modelc_3 :::"LTLNew2"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")) ")" ) ($#k1_tarski :::"}"::: ) )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v8_modelc_2 :::"Release"::: ) )) "implies" (Bool (Set ($#k3_modelc_3 :::"LTLNew2"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) "," (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")) ")" ) ($#k2_tarski :::"}"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "H")) "is" ($#v4_modelc_2 :::"conjunctive"::: ) )) & (Bool (Bool "not" (Set (Var "H")) "is" ($#v5_modelc_2 :::"disjunctive"::: ) )) & (Bool (Bool "not" (Set (Var "H")) "is" ($#v6_modelc_2 :::"next"::: ) )) & (Bool (Bool "not" (Set (Var "H")) "is" ($#v7_modelc_2 :::"Until"::: ) )) & (Bool (Bool "not" (Set (Var "H")) "is" ($#v8_modelc_2 :::"Release"::: ) ))) "implies" (Bool (Set ($#k3_modelc_3 :::"LTLNew2"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" )); :: deftheorem defines :::"LTLNext"::: MODELC_3:def 3 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "H")) "is" ($#v4_modelc_2 :::"conjunctive"::: ) )) "implies" (Bool (Set ($#k4_modelc_3 :::"LTLNext"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v5_modelc_2 :::"disjunctive"::: ) )) "implies" (Bool (Set ($#k4_modelc_3 :::"LTLNext"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v6_modelc_2 :::"next"::: ) )) "implies" (Bool (Set ($#k4_modelc_3 :::"LTLNext"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k10_modelc_2 :::"the_argument_of"::: ) (Set (Var "H")) ")" ) ($#k1_tarski :::"}"::: ) )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v7_modelc_2 :::"Until"::: ) )) "implies" (Bool (Set ($#k4_modelc_3 :::"LTLNext"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "H")) ($#k1_tarski :::"}"::: ) )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v8_modelc_2 :::"Release"::: ) )) "implies" (Bool (Set ($#k4_modelc_3 :::"LTLNext"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "H")) ($#k1_tarski :::"}"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "H")) "is" ($#v4_modelc_2 :::"conjunctive"::: ) )) & (Bool (Bool "not" (Set (Var "H")) "is" ($#v5_modelc_2 :::"disjunctive"::: ) )) & (Bool (Bool "not" (Set (Var "H")) "is" ($#v6_modelc_2 :::"next"::: ) )) & (Bool (Bool "not" (Set (Var "H")) "is" ($#v7_modelc_2 :::"Until"::: ) )) & (Bool (Bool "not" (Set (Var "H")) "is" ($#v8_modelc_2 :::"Release"::: ) ))) "implies" (Bool (Set ($#k4_modelc_3 :::"LTLNext"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" )); definitionlet "v" be ($#m2_finseq_1 :::"LTL-formula":::); attr "c2" is :::"strict"::: ; struct :::"LTLnode"::: "over" "v" -> ; aggr :::"LTLnode":::(# :::"LTLold":::, :::"LTLnew":::, :::"LTLnext"::: #) -> ($#l1_modelc_3 :::"LTLnode"::: ) "over" "v"; sel :::"LTLold"::: "c2" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) "v" ")" ); sel :::"LTLnew"::: "c2" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) "v" ")" ); sel :::"LTLnext"::: "c2" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) "v" ")" ); end; definitionlet "v" be ($#m2_finseq_1 :::"LTL-formula":::); let "N" be ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Const "v")); let "H" be ($#m2_finseq_1 :::"LTL-formula":::); assume (Bool (Set (Const "H")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set (Const "N")))) ; func :::"SuccNode1"::: "(" "H" "," "N" ")" -> ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" "v" means :: MODELC_3:def 4 (Bool "(" (Bool (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" "N") ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) "H" ($#k1_tarski :::"}"::: ) ))) & (Bool (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" "N") ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) "H" ($#k1_tarski :::"}"::: ) ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" ($#k2_modelc_3 :::"LTLNew1"::: ) "H" ")" ) ($#k7_subset_1 :::"\"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" "N") ")" ))) & (Bool (Set "the" ($#u3_modelc_3 :::"LTLnext"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_modelc_3 :::"LTLnext"::: ) "of" "N") ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_modelc_3 :::"LTLNext"::: ) "H" ")" ))) ")" ); end; :: deftheorem defines :::"SuccNode1"::: MODELC_3:def 4 : (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "N")) "being" ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set (Var "N"))))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k5_modelc_3 :::"SuccNode1"::: ) "(" (Set (Var "H")) "," (Set (Var "N")) ")" )) "iff" (Bool "(" (Bool (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set (Var "N"))) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "H")) ($#k1_tarski :::"}"::: ) ))) & (Bool (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set (Var "N"))) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "H")) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" ($#k2_modelc_3 :::"LTLNew1"::: ) (Set (Var "H")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set (Var "N"))) ")" ))) & (Bool (Set "the" ($#u3_modelc_3 :::"LTLnext"::: ) "of" (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_modelc_3 :::"LTLnext"::: ) "of" (Set (Var "N"))) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_modelc_3 :::"LTLNext"::: ) (Set (Var "H")) ")" ))) ")" ) ")" ))))); definitionlet "v" be ($#m2_finseq_1 :::"LTL-formula":::); let "N" be ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Const "v")); let "H" be ($#m2_finseq_1 :::"LTL-formula":::); assume (Bool (Set (Const "H")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set (Const "N")))) ; func :::"SuccNode2"::: "(" "H" "," "N" ")" -> ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" "v" means :: MODELC_3:def 5 (Bool "(" (Bool (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" "N") ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) "H" ($#k1_tarski :::"}"::: ) ))) & (Bool (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" "N") ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) "H" ($#k1_tarski :::"}"::: ) ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" ($#k3_modelc_3 :::"LTLNew2"::: ) "H" ")" ) ($#k7_subset_1 :::"\"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" "N") ")" ))) & (Bool (Set "the" ($#u3_modelc_3 :::"LTLnext"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set "the" ($#u3_modelc_3 :::"LTLnext"::: ) "of" "N")) ")" ); end; :: deftheorem defines :::"SuccNode2"::: MODELC_3:def 5 : (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "N")) "being" ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set (Var "N"))))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k6_modelc_3 :::"SuccNode2"::: ) "(" (Set (Var "H")) "," (Set (Var "N")) ")" )) "iff" (Bool "(" (Bool (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set (Var "N"))) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "H")) ($#k1_tarski :::"}"::: ) ))) & (Bool (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set (Var "N"))) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "H")) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" ($#k3_modelc_3 :::"LTLNew2"::: ) (Set (Var "H")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set (Var "N"))) ")" ))) & (Bool (Set "the" ($#u3_modelc_3 :::"LTLnext"::: ) "of" (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u3_modelc_3 :::"LTLnext"::: ) "of" (Set (Var "N")))) ")" ) ")" ))))); definitionlet "v" be ($#m2_finseq_1 :::"LTL-formula":::); let "N1", "N2" be ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Const "v")); let "H" be ($#m2_finseq_1 :::"LTL-formula":::); pred "N2" :::"is_succ_of"::: "N1" "," "H" means :: MODELC_3:def 6 (Bool "(" (Bool "H" ($#r2_hidden :::"in"::: ) (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" "N1")) & (Bool "(" (Bool "N2" ($#r1_hidden :::"="::: ) (Set ($#k5_modelc_3 :::"SuccNode1"::: ) "(" "H" "," "N1" ")" )) "or" (Bool "(" (Bool "(" (Bool "H" "is" ($#v5_modelc_2 :::"disjunctive"::: ) ) "or" (Bool "H" "is" ($#v7_modelc_2 :::"Until"::: ) ) "or" (Bool "H" "is" ($#v8_modelc_2 :::"Release"::: ) ) ")" ) & (Bool "N2" ($#r1_hidden :::"="::: ) (Set ($#k6_modelc_3 :::"SuccNode2"::: ) "(" "H" "," "N1" ")" )) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"is_succ_of"::: MODELC_3:def 6 : (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" (Bool (Set (Var "N2")) ($#r1_modelc_3 :::"is_succ_of"::: ) (Set (Var "N1")) "," (Set (Var "H"))) "iff" (Bool "(" (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set (Var "N1")))) & (Bool "(" (Bool (Set (Var "N2")) ($#r1_hidden :::"="::: ) (Set ($#k5_modelc_3 :::"SuccNode1"::: ) "(" (Set (Var "H")) "," (Set (Var "N1")) ")" )) "or" (Bool "(" (Bool "(" (Bool (Set (Var "H")) "is" ($#v5_modelc_2 :::"disjunctive"::: ) ) "or" (Bool (Set (Var "H")) "is" ($#v7_modelc_2 :::"Until"::: ) ) "or" (Bool (Set (Var "H")) "is" ($#v8_modelc_2 :::"Release"::: ) ) ")" ) & (Bool (Set (Var "N2")) ($#r1_hidden :::"="::: ) (Set ($#k6_modelc_3 :::"SuccNode2"::: ) "(" (Set (Var "H")) "," (Set (Var "N1")) ")" )) ")" ) ")" ) ")" ) ")" )))); definitionlet "v" be ($#m2_finseq_1 :::"LTL-formula":::); let "N1", "N2" be ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Const "v")); pred "N2" :::"is_succ1_of"::: "N1" means :: MODELC_3:def 7 (Bool "ex" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool "(" (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" "N1")) & (Bool "N2" ($#r1_hidden :::"="::: ) (Set ($#k5_modelc_3 :::"SuccNode1"::: ) "(" (Set (Var "H")) "," "N1" ")" )) ")" )); pred "N2" :::"is_succ2_of"::: "N1" means :: MODELC_3:def 8 (Bool "ex" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool "(" (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" "N1")) & (Bool "(" (Bool (Set (Var "H")) "is" ($#v5_modelc_2 :::"disjunctive"::: ) ) "or" (Bool (Set (Var "H")) "is" ($#v7_modelc_2 :::"Until"::: ) ) "or" (Bool (Set (Var "H")) "is" ($#v8_modelc_2 :::"Release"::: ) ) ")" ) & (Bool "N2" ($#r1_hidden :::"="::: ) (Set ($#k6_modelc_3 :::"SuccNode2"::: ) "(" (Set (Var "H")) "," "N1" ")" )) ")" )); end; :: deftheorem defines :::"is_succ1_of"::: MODELC_3:def 7 : (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "holds" (Bool "(" (Bool (Set (Var "N2")) ($#r2_modelc_3 :::"is_succ1_of"::: ) (Set (Var "N1"))) "iff" (Bool "ex" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool "(" (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set (Var "N1")))) & (Bool (Set (Var "N2")) ($#r1_hidden :::"="::: ) (Set ($#k5_modelc_3 :::"SuccNode1"::: ) "(" (Set (Var "H")) "," (Set (Var "N1")) ")" )) ")" )) ")" ))); :: deftheorem defines :::"is_succ2_of"::: MODELC_3:def 8 : (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "holds" (Bool "(" (Bool (Set (Var "N2")) ($#r3_modelc_3 :::"is_succ2_of"::: ) (Set (Var "N1"))) "iff" (Bool "ex" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool "(" (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set (Var "N1")))) & (Bool "(" (Bool (Set (Var "H")) "is" ($#v5_modelc_2 :::"disjunctive"::: ) ) "or" (Bool (Set (Var "H")) "is" ($#v7_modelc_2 :::"Until"::: ) ) "or" (Bool (Set (Var "H")) "is" ($#v8_modelc_2 :::"Release"::: ) ) ")" ) & (Bool (Set (Var "N2")) ($#r1_hidden :::"="::: ) (Set ($#k6_modelc_3 :::"SuccNode2"::: ) "(" (Set (Var "H")) "," (Set (Var "N1")) ")" )) ")" )) ")" ))); definitionlet "v" be ($#m2_finseq_1 :::"LTL-formula":::); let "N1", "N2" be ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Const "v")); pred "N2" :::"is_succ_of"::: "N1" means :: MODELC_3:def 9 (Bool "(" (Bool "N2" ($#r2_modelc_3 :::"is_succ1_of"::: ) "N1") "or" (Bool "N2" ($#r3_modelc_3 :::"is_succ2_of"::: ) "N1") ")" ); end; :: deftheorem defines :::"is_succ_of"::: MODELC_3:def 9 : (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "holds" (Bool "(" (Bool (Set (Var "N2")) ($#r4_modelc_3 :::"is_succ_of"::: ) (Set (Var "N1"))) "iff" (Bool "(" (Bool (Set (Var "N2")) ($#r2_modelc_3 :::"is_succ1_of"::: ) (Set (Var "N1"))) "or" (Bool (Set (Var "N2")) ($#r3_modelc_3 :::"is_succ2_of"::: ) (Set (Var "N1"))) ")" ) ")" ))); definitionlet "v" be ($#m2_finseq_1 :::"LTL-formula":::); let "N" be ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Const "v")); attr "N" is :::"failure"::: means :: MODELC_3:def 10 (Bool "ex" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool "(" (Bool (Set (Var "H")) "is" ($#v2_modelc_2 :::"atomic"::: ) ) & (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k3_modelc_2 :::"'not'"::: ) (Set (Var "H")))) & (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" "N")) & (Bool (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" "N")) ")" )); end; :: deftheorem defines :::"failure"::: MODELC_3:def 10 : (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "N")) "being" ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "holds" (Bool "(" (Bool (Set (Var "N")) "is" ($#v2_modelc_3 :::"failure"::: ) ) "iff" (Bool "ex" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool "(" (Bool (Set (Var "H")) "is" ($#v2_modelc_2 :::"atomic"::: ) ) & (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k3_modelc_2 :::"'not'"::: ) (Set (Var "H")))) & (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set (Var "N")))) & (Bool (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set (Var "N")))) ")" )) ")" ))); definitionlet "v" be ($#m2_finseq_1 :::"LTL-formula":::); let "N" be ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Const "v")); attr "N" is :::"elementary"::: means :: MODELC_3:def 11 (Bool (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" "N") ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )); end; :: deftheorem defines :::"elementary"::: MODELC_3:def 11 : (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "N")) "being" ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "holds" (Bool "(" (Bool (Set (Var "N")) "is" ($#v3_modelc_3 :::"elementary"::: ) ) "iff" (Bool (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))); definitionlet "v" be ($#m2_finseq_1 :::"LTL-formula":::); let "N" be ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Const "v")); attr "N" is :::"final"::: means :: MODELC_3:def 12 (Bool "(" (Bool "N" "is" ($#v3_modelc_3 :::"elementary"::: ) ) & (Bool (Set "the" ($#u3_modelc_3 :::"LTLnext"::: ) "of" "N") ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ); end; :: deftheorem defines :::"final"::: MODELC_3:def 12 : (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "N")) "being" ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "holds" (Bool "(" (Bool (Set (Var "N")) "is" ($#v4_modelc_3 :::"final"::: ) ) "iff" (Bool "(" (Bool (Set (Var "N")) "is" ($#v3_modelc_3 :::"elementary"::: ) ) & (Bool (Set "the" ($#u3_modelc_3 :::"LTLnext"::: ) "of" (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" ))); definitionlet "v" be ($#m2_finseq_1 :::"LTL-formula":::); func :::"{}"::: "v" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) "v" ")" ) equals :: MODELC_3:def 13 (Set ($#k1_xboole_0 :::"{}"::: ) ); end; :: deftheorem defines :::"{}"::: MODELC_3:def 13 : (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool (Set ($#k7_modelc_3 :::"{}"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))); definitionlet "v" be ($#m2_finseq_1 :::"LTL-formula":::); func :::"Seed"::: "v" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) "v" ")" ) equals :: MODELC_3:def 14 (Set ($#k1_tarski :::"{"::: ) "v" ($#k1_tarski :::"}"::: ) ); end; :: deftheorem defines :::"Seed"::: MODELC_3:def 14 : (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool (Set ($#k8_modelc_3 :::"Seed"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "v")) ($#k1_tarski :::"}"::: ) ))); registrationlet "v" be ($#m2_finseq_1 :::"LTL-formula":::); cluster ($#v1_modelc_3 :::"strict"::: ) ($#v3_modelc_3 :::"elementary"::: ) for ($#l1_modelc_3 :::"LTLnode"::: ) "over" "v"; end; definitionlet "v" be ($#m2_finseq_1 :::"LTL-formula":::); func :::"FinalNode"::: "v" -> ($#v1_modelc_3 :::"strict"::: ) ($#v3_modelc_3 :::"elementary"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" "v" equals :: MODELC_3:def 15 (Set ($#g1_modelc_3 :::"LTLnode"::: ) "(#" (Set "(" ($#k7_modelc_3 :::"{}"::: ) "v" ")" ) "," (Set "(" ($#k7_modelc_3 :::"{}"::: ) "v" ")" ) "," (Set "(" ($#k7_modelc_3 :::"{}"::: ) "v" ")" ) "#)" ); end; :: deftheorem defines :::"FinalNode"::: MODELC_3:def 15 : (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool (Set ($#k9_modelc_3 :::"FinalNode"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#g1_modelc_3 :::"LTLnode"::: ) "(#" (Set "(" ($#k7_modelc_3 :::"{}"::: ) (Set (Var "v")) ")" ) "," (Set "(" ($#k7_modelc_3 :::"{}"::: ) (Set (Var "v")) ")" ) "," (Set "(" ($#k7_modelc_3 :::"{}"::: ) (Set (Var "v")) ")" ) "#)" ))); definitionlet "x" be ($#m1_hidden :::"set"::: ) ; let "v" be ($#m2_finseq_1 :::"LTL-formula":::); func :::"CastNode"::: "(" "x" "," "v" ")" -> ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" "v" equals :: MODELC_3:def 16 "x" if (Bool "x" "is" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" "v") otherwise (Set ($#g1_modelc_3 :::"LTLnode"::: ) "(#" (Set "(" ($#k7_modelc_3 :::"{}"::: ) "v" ")" ) "," (Set "(" ($#k7_modelc_3 :::"{}"::: ) "v" ")" ) "," (Set "(" ($#k7_modelc_3 :::"{}"::: ) "v" ")" ) "#)" ); end; :: deftheorem defines :::"CastNode"::: MODELC_3:def 16 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) "is" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")))) "implies" (Bool (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set (Var "x")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" & "(" (Bool (Bool (Set (Var "x")) "is" (Bool "not" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v"))))) "implies" (Bool (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set (Var "x")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g1_modelc_3 :::"LTLnode"::: ) "(#" (Set "(" ($#k7_modelc_3 :::"{}"::: ) (Set (Var "v")) ")" ) "," (Set "(" ($#k7_modelc_3 :::"{}"::: ) (Set (Var "v")) ")" ) "," (Set "(" ($#k7_modelc_3 :::"{}"::: ) (Set (Var "v")) ")" ) "#)" )) ")" ")" ))); definitionlet "v" be ($#m2_finseq_1 :::"LTL-formula":::); func :::"init"::: "v" -> ($#v1_modelc_3 :::"strict"::: ) ($#v3_modelc_3 :::"elementary"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" "v" equals :: MODELC_3:def 17 (Set ($#g1_modelc_3 :::"LTLnode"::: ) "(#" (Set "(" ($#k7_modelc_3 :::"{}"::: ) "v" ")" ) "," (Set "(" ($#k7_modelc_3 :::"{}"::: ) "v" ")" ) "," (Set "(" ($#k8_modelc_3 :::"Seed"::: ) "v" ")" ) "#)" ); end; :: deftheorem defines :::"init"::: MODELC_3:def 17 : (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool (Set ($#k11_modelc_3 :::"init"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#g1_modelc_3 :::"LTLnode"::: ) "(#" (Set "(" ($#k7_modelc_3 :::"{}"::: ) (Set (Var "v")) ")" ) "," (Set "(" ($#k7_modelc_3 :::"{}"::: ) (Set (Var "v")) ")" ) "," (Set "(" ($#k8_modelc_3 :::"Seed"::: ) (Set (Var "v")) ")" ) "#)" ))); definitionlet "v" be ($#m2_finseq_1 :::"LTL-formula":::); let "N" be ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Const "v")); func :::"'X'"::: "N" -> ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" "v" equals :: MODELC_3:def 18 (Set ($#g1_modelc_3 :::"LTLnode"::: ) "(#" (Set "(" ($#k7_modelc_3 :::"{}"::: ) "v" ")" ) "," (Set "the" ($#u3_modelc_3 :::"LTLnext"::: ) "of" "N") "," (Set "(" ($#k7_modelc_3 :::"{}"::: ) "v" ")" ) "#)" ); end; :: deftheorem defines :::"'X'"::: MODELC_3:def 18 : (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "N")) "being" ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "holds" (Bool (Set ($#k12_modelc_3 :::"'X'"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set ($#g1_modelc_3 :::"LTLnode"::: ) "(#" (Set "(" ($#k7_modelc_3 :::"{}"::: ) (Set (Var "v")) ")" ) "," (Set "the" ($#u3_modelc_3 :::"LTLnext"::: ) "of" (Set (Var "N"))) "," (Set "(" ($#k7_modelc_3 :::"{}"::: ) (Set (Var "v")) ")" ) "#)" )))); definitionlet "v" be ($#m2_finseq_1 :::"LTL-formula":::); let "L" be ($#m1_hidden :::"FinSequence":::); pred "L" :::"is_Finseq_for"::: "v" means :: MODELC_3:def 19 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) "L"))) "holds" (Bool "ex" (Set (Var "N")) "," (Set (Var "M")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" "v" "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_hidden :::"="::: ) (Set "L" ($#k1_funct_1 :::"."::: ) (Set (Var "k")))) & (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set "L" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set (Var "M")) ($#r4_modelc_3 :::"is_succ_of"::: ) (Set (Var "N"))) ")" ))); end; :: deftheorem defines :::"is_Finseq_for"::: MODELC_3:def 19 : (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "L")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "L")) ($#r5_modelc_3 :::"is_Finseq_for"::: ) (Set (Var "v"))) "iff" (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "L"))))) "holds" (Bool "ex" (Set (Var "N")) "," (Set (Var "M")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_hidden :::"="::: ) (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")))) & (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set (Var "M")) ($#r4_modelc_3 :::"is_succ_of"::: ) (Set (Var "N"))) ")" ))) ")" ))); definitionlet "v" be ($#m2_finseq_1 :::"LTL-formula":::); let "N1", "N2" be ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Const "v")); pred "N2" :::"is_next_of"::: "N1" means :: MODELC_3:def 20 (Bool "(" (Bool "N1" "is" ($#v3_modelc_3 :::"elementary"::: ) ) & (Bool "N2" "is" ($#v3_modelc_3 :::"elementary"::: ) ) & (Bool "ex" (Set (Var "L")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "L")))) & (Bool (Set (Var "L")) ($#r5_modelc_3 :::"is_Finseq_for"::: ) "v") & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k12_modelc_3 :::"'X'"::: ) "N1")) & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) "N2") ")" )) ")" ); end; :: deftheorem defines :::"is_next_of"::: MODELC_3:def 20 : (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "holds" (Bool "(" (Bool (Set (Var "N2")) ($#r6_modelc_3 :::"is_next_of"::: ) (Set (Var "N1"))) "iff" (Bool "(" (Bool (Set (Var "N1")) "is" ($#v3_modelc_3 :::"elementary"::: ) ) & (Bool (Set (Var "N2")) "is" ($#v3_modelc_3 :::"elementary"::: ) ) & (Bool "ex" (Set (Var "L")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "L")))) & (Bool (Set (Var "L")) ($#r5_modelc_3 :::"is_Finseq_for"::: ) (Set (Var "v"))) & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k12_modelc_3 :::"'X'"::: ) (Set (Var "N1")))) & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "N2"))) ")" )) ")" ) ")" ))); definitionlet "v" be ($#m2_finseq_1 :::"LTL-formula":::); let "W" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) (Set (Const "v")) ")" ); func :::"CastLTL"::: "W" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) ) equals :: MODELC_3:def 21 "W"; end; :: deftheorem defines :::"CastLTL"::: MODELC_3:def 21 : (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) (Set (Var "v")) ")" ) "holds" (Bool (Set ($#k13_modelc_3 :::"CastLTL"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Var "W"))))); definitionlet "v" be ($#m2_finseq_1 :::"LTL-formula":::); let "N" be ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Const "v")); func :::"*"::: "N" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) ) equals :: MODELC_3:def 22 (Set (Set "(" (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" "N") ($#k4_subset_1 :::"\/"::: ) (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" "N") ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k48_modelc_2 :::"'X'"::: ) (Set "(" ($#k13_modelc_3 :::"CastLTL"::: ) (Set "the" ($#u3_modelc_3 :::"LTLnext"::: ) "of" "N") ")" ) ")" )); end; :: deftheorem defines :::"*"::: MODELC_3:def 22 : (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "N")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "holds" (Bool (Set ($#k14_modelc_3 :::"*"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set (Var "N"))) ($#k4_subset_1 :::"\/"::: ) (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set (Var "N"))) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k48_modelc_2 :::"'X'"::: ) (Set "(" ($#k13_modelc_3 :::"CastLTL"::: ) (Set "the" ($#u3_modelc_3 :::"LTLnext"::: ) "of" (Set (Var "N"))) ")" ) ")" ))))); theorem :: MODELC_3:1 (Bool "for" (Set (Var "H")) "," (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "N")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) "st" (Bool (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set (Var "N")))) & (Bool "(" (Bool (Set (Var "H")) "is" ($#v2_modelc_2 :::"atomic"::: ) ) "or" (Bool (Set (Var "H")) "is" ($#v3_modelc_2 :::"negative"::: ) ) "or" (Bool (Set (Var "H")) "is" ($#v4_modelc_2 :::"conjunctive"::: ) ) "or" (Bool (Set (Var "H")) "is" ($#v6_modelc_2 :::"next"::: ) ) ")" )) "holds" (Bool "(" (Bool (Set (Var "w")) ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set (Var "N")))) "iff" (Bool (Set (Var "w")) ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set "(" ($#k5_modelc_3 :::"SuccNode1"::: ) "(" (Set (Var "H")) "," (Set (Var "N")) ")" ")" ))) ")" )))) ; theorem :: MODELC_3:2 (Bool "for" (Set (Var "H")) "," (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "N")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) "st" (Bool (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set (Var "N")))) & (Bool "(" (Bool (Set (Var "H")) "is" ($#v5_modelc_2 :::"disjunctive"::: ) ) "or" (Bool (Set (Var "H")) "is" ($#v7_modelc_2 :::"Until"::: ) ) "or" (Bool (Set (Var "H")) "is" ($#v8_modelc_2 :::"Release"::: ) ) ")" )) "holds" (Bool "(" (Bool (Set (Var "w")) ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set (Var "N")))) "iff" (Bool "(" (Bool (Set (Var "w")) ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set "(" ($#k5_modelc_3 :::"SuccNode1"::: ) "(" (Set (Var "H")) "," (Set (Var "N")) ")" ")" ))) "or" (Bool (Set (Var "w")) ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set "(" ($#k6_modelc_3 :::"SuccNode2"::: ) "(" (Set (Var "H")) "," (Set (Var "N")) ")" ")" ))) ")" ) ")" )))) ; theorem :: MODELC_3:3 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "ex" (Set (Var "L")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Set ($#k1_modelc_3 :::"Subformulae"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "L")))))) ; registrationlet "H" be ($#m2_finseq_1 :::"LTL-formula":::); cluster (Set ($#k13_modelc_2 :::"Subformulae"::: ) "H") -> ($#v1_finset_1 :::"finite"::: ) ; end; definitionlet "H" be ($#m2_finseq_1 :::"LTL-formula":::); let "W" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k13_modelc_2 :::"Subformulae"::: ) (Set (Const "H")) ")" ); let "L" be ($#m1_hidden :::"FinSequence":::); let "x" be ($#m1_hidden :::"set"::: ) ; func :::"Length_fun"::: "(" "L" "," "W" "," "x" ")" -> ($#m1_hidden :::"Nat":::) equals :: MODELC_3:def 23 (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k14_modelc_2 :::"CastLTL"::: ) (Set "(" "L" ($#k1_funct_1 :::"."::: ) "x" ")" ) ")" )) if (Bool (Set "L" ($#k1_funct_1 :::"."::: ) "x") ($#r2_hidden :::"in"::: ) "W") otherwise (Set ($#k6_numbers :::"0"::: ) ); end; :: deftheorem defines :::"Length_fun"::: MODELC_3:def 23 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k13_modelc_2 :::"Subformulae"::: ) (Set (Var "H")) ")" ) (Bool "for" (Set (Var "L")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Var "W")))) "implies" (Bool (Set ($#k15_modelc_3 :::"Length_fun"::: ) "(" (Set (Var "L")) "," (Set (Var "W")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k14_modelc_2 :::"CastLTL"::: ) (Set "(" (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Var "W"))))) "implies" (Bool (Set ($#k15_modelc_3 :::"Length_fun"::: ) "(" (Set (Var "L")) "," (Set (Var "W")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" ))))); definitionlet "H" be ($#m2_finseq_1 :::"LTL-formula":::); let "W" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k13_modelc_2 :::"Subformulae"::: ) (Set (Const "H")) ")" ); let "L" be ($#m1_hidden :::"FinSequence":::); func :::"Partial_seq"::: "(" "L" "," "W" ")" -> ($#m1_subset_1 :::"Real_Sequence":::) means :: MODELC_3:def 24 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" "(" (Bool (Bool (Set "L" ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) "W")) "implies" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k14_modelc_2 :::"CastLTL"::: ) (Set "(" "L" ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set "L" ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) "W"))) "implies" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" )); end; :: deftheorem defines :::"Partial_seq"::: MODELC_3:def 24 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k13_modelc_2 :::"Subformulae"::: ) (Set (Var "H")) ")" ) (Bool "for" (Set (Var "L")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k16_modelc_3 :::"Partial_seq"::: ) "(" (Set (Var "L")) "," (Set (Var "W")) ")" )) "iff" (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) (Set (Var "W")))) "implies" (Bool (Set (Set (Var "b4")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k14_modelc_2 :::"CastLTL"::: ) (Set "(" (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) (Set (Var "W"))))) "implies" (Bool (Set (Set (Var "b4")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" )) ")" ))))); definitionlet "H" be ($#m2_finseq_1 :::"LTL-formula":::); let "W" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k13_modelc_2 :::"Subformulae"::: ) (Set (Const "H")) ")" ); let "L" be ($#m1_hidden :::"FinSequence":::); func :::"len"::: "(" "L" "," "W" ")" -> ($#m1_subset_1 :::"Real":::) equals :: MODELC_3:def 25 (Set ($#k6_series_1 :::"Sum"::: ) "(" (Set "(" ($#k16_modelc_3 :::"Partial_seq"::: ) "(" "L" "," "W" ")" ")" ) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) "L" ")" ) ")" ); end; :: deftheorem defines :::"len"::: MODELC_3:def 25 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k13_modelc_2 :::"Subformulae"::: ) (Set (Var "H")) ")" ) (Bool "for" (Set (Var "L")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k17_modelc_3 :::"len"::: ) "(" (Set (Var "L")) "," (Set (Var "W")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_series_1 :::"Sum"::: ) "(" (Set "(" ($#k16_modelc_3 :::"Partial_seq"::: ) "(" (Set (Var "L")) "," (Set (Var "W")) ")" ")" ) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "L")) ")" ) ")" ))))); theorem :: MODELC_3:4 (Bool "for" (Set (Var "L")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool (Set ($#k17_modelc_3 :::"len"::: ) "(" (Set (Var "L")) "," (Set "(" ($#k7_modelc_3 :::"{}"::: ) (Set (Var "H")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: MODELC_3:5 (Bool "for" (Set (Var "L")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k13_modelc_2 :::"Subformulae"::: ) (Set (Var "H")) ")" ) "st" (Bool (Bool (Bool "not" (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set (Var "W"))))) "holds" (Bool (Set ($#k17_modelc_3 :::"len"::: ) "(" (Set (Var "L")) "," (Set "(" (Set (Var "W")) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "F")) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k17_modelc_3 :::"len"::: ) "(" (Set (Var "L")) "," (Set (Var "W")) ")" ))))) ; theorem :: MODELC_3:6 (Bool "for" (Set (Var "L")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k13_modelc_2 :::"Subformulae"::: ) (Set (Var "H")) ")" ) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k1_modelc_3 :::"Subformulae"::: ) (Set (Var "H")))) & (Bool (Set (Var "L")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set (Var "W")))) "holds" (Bool (Set ($#k17_modelc_3 :::"len"::: ) "(" (Set (Var "L")) "," (Set "(" (Set (Var "W")) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "F")) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k17_modelc_3 :::"len"::: ) "(" (Set (Var "L")) "," (Set (Var "W")) ")" ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")) ")" )))))) ; theorem :: MODELC_3:7 (Bool "for" (Set (Var "L")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "W")) "," (Set (Var "W1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k13_modelc_2 :::"Subformulae"::: ) (Set (Var "H")) ")" ) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k1_modelc_3 :::"Subformulae"::: ) (Set (Var "H")))) & (Bool (Set (Var "L")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Bool "not" (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set (Var "W")))) & (Bool (Set (Var "W1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "F")) ($#k1_tarski :::"}"::: ) )))) "holds" (Bool (Set ($#k17_modelc_3 :::"len"::: ) "(" (Set (Var "L")) "," (Set (Var "W1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k17_modelc_3 :::"len"::: ) "(" (Set (Var "L")) "," (Set (Var "W")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")) ")" )))))) ; theorem :: MODELC_3:8 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k13_modelc_2 :::"Subformulae"::: ) (Set (Var "H")) ")" ) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "L1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_modelc_3 :::"Subformulae"::: ) (Set (Var "H")))) & (Bool (Set (Var "L1")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "L2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_modelc_3 :::"Subformulae"::: ) (Set (Var "H")))) & (Bool (Set (Var "L2")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set ($#k17_modelc_3 :::"len"::: ) "(" (Set (Var "L1")) "," (Set (Var "W")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k17_modelc_3 :::"len"::: ) "(" (Set (Var "L2")) "," (Set (Var "W")) ")" ))))) ; definitionlet "H" be ($#m2_finseq_1 :::"LTL-formula":::); let "W" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k13_modelc_2 :::"Subformulae"::: ) (Set (Const "H")) ")" ); func :::"len"::: "W" -> ($#m1_subset_1 :::"Real":::) means :: MODELC_3:def 26 (Bool "ex" (Set (Var "L")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k1_modelc_3 :::"Subformulae"::: ) "H")) & (Bool (Set (Var "L")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k17_modelc_3 :::"len"::: ) "(" (Set (Var "L")) "," "W" ")" )) ")" )); end; :: deftheorem defines :::"len"::: MODELC_3:def 26 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k13_modelc_2 :::"Subformulae"::: ) (Set (Var "H")) ")" ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k18_modelc_3 :::"len"::: ) (Set (Var "W")))) "iff" (Bool "ex" (Set (Var "L")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k1_modelc_3 :::"Subformulae"::: ) (Set (Var "H")))) & (Bool (Set (Var "L")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k17_modelc_3 :::"len"::: ) "(" (Set (Var "L")) "," (Set (Var "W")) ")" )) ")" )) ")" )))); theorem :: MODELC_3:9 (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k13_modelc_2 :::"Subformulae"::: ) (Set (Var "H")) ")" ) "st" (Bool (Bool (Bool "not" (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set (Var "W"))))) "holds" (Bool (Set ($#k18_modelc_3 :::"len"::: ) (Set "(" (Set (Var "W")) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "F")) ($#k1_tarski :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k18_modelc_3 :::"len"::: ) (Set (Var "W")))))) ; theorem :: MODELC_3:10 (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k13_modelc_2 :::"Subformulae"::: ) (Set (Var "H")) ")" ) "st" (Bool (Bool (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set (Var "W")))) "holds" (Bool (Set ($#k18_modelc_3 :::"len"::: ) (Set "(" (Set (Var "W")) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "F")) ($#k1_tarski :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_modelc_3 :::"len"::: ) (Set (Var "W")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")) ")" ))))) ; theorem :: MODELC_3:11 (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "W")) "," (Set (Var "W1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k13_modelc_2 :::"Subformulae"::: ) (Set (Var "H")) ")" ) "st" (Bool (Bool (Bool "not" (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set (Var "W")))) & (Bool (Set (Var "W1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "F")) ($#k1_tarski :::"}"::: ) )))) "holds" (Bool (Set ($#k18_modelc_3 :::"len"::: ) (Set (Var "W1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_modelc_3 :::"len"::: ) (Set (Var "W")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")) ")" ))))) ; theorem :: MODELC_3:12 (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k13_modelc_2 :::"Subformulae"::: ) (Set (Var "H")) ")" ) "st" (Bool (Bool (Set (Var "W1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "F")) ($#k1_tarski :::"}"::: ) )))) "holds" (Bool (Set ($#k18_modelc_3 :::"len"::: ) (Set (Var "W1"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k18_modelc_3 :::"len"::: ) (Set (Var "W")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")) ")" ))))) ; theorem :: MODELC_3:13 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool (Set ($#k18_modelc_3 :::"len"::: ) (Set "(" ($#k7_modelc_3 :::"{}"::: ) (Set (Var "H")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: MODELC_3:14 (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k13_modelc_2 :::"Subformulae"::: ) (Set (Var "H")) ")" ) "st" (Bool (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "F")) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set ($#k18_modelc_3 :::"len"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")))))) ; theorem :: MODELC_3:15 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "W")) "," (Set (Var "W1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k13_modelc_2 :::"Subformulae"::: ) (Set (Var "H")) ")" ) "st" (Bool (Bool (Set (Var "W")) ($#r1_tarski :::"c="::: ) (Set (Var "W1")))) "holds" (Bool (Set ($#k18_modelc_3 :::"len"::: ) (Set (Var "W"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k18_modelc_3 :::"len"::: ) (Set (Var "W1")))))) ; theorem :: MODELC_3:16 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k13_modelc_2 :::"Subformulae"::: ) (Set (Var "H")) ")" ) "st" (Bool (Bool (Set ($#k18_modelc_3 :::"len"::: ) (Set (Var "W"))) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) (Set ($#k7_modelc_3 :::"{}"::: ) (Set (Var "H")))))) ; theorem :: MODELC_3:17 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k13_modelc_2 :::"Subformulae"::: ) (Set (Var "H")) ")" ) "holds" (Bool (Set ($#k18_modelc_3 :::"len"::: ) (Set (Var "W"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: MODELC_3:18 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "W")) "," (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k13_modelc_2 :::"Subformulae"::: ) (Set (Var "H")) ")" ) "st" (Bool (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "W2"))))) "holds" (Bool (Set ($#k18_modelc_3 :::"len"::: ) (Set (Var "W"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k18_modelc_3 :::"len"::: ) (Set (Var "W1")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k18_modelc_3 :::"len"::: ) (Set (Var "W2")) ")" ))))) ; definitionlet "v", "H" be ($#m2_finseq_1 :::"LTL-formula":::); assume (Bool (Set (Const "H")) ($#r2_hidden :::"in"::: ) (Set ($#k1_modelc_3 :::"Subformulae"::: ) (Set (Const "v")))) ; func :::"LTLNew1"::: "(" "H" "," "v" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) "v" ")" ) equals :: MODELC_3:def 27 (Set ($#k2_modelc_3 :::"LTLNew1"::: ) "H"); func :::"LTLNew2"::: "(" "H" "," "v" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) "v" ")" ) equals :: MODELC_3:def 28 (Set ($#k3_modelc_3 :::"LTLNew2"::: ) "H"); end; :: deftheorem defines :::"LTLNew1"::: MODELC_3:def 27 : (Bool "for" (Set (Var "v")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set ($#k1_modelc_3 :::"Subformulae"::: ) (Set (Var "v"))))) "holds" (Bool (Set ($#k19_modelc_3 :::"LTLNew1"::: ) "(" (Set (Var "H")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_modelc_3 :::"LTLNew1"::: ) (Set (Var "H"))))); :: deftheorem defines :::"LTLNew2"::: MODELC_3:def 28 : (Bool "for" (Set (Var "v")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set ($#k1_modelc_3 :::"Subformulae"::: ) (Set (Var "v"))))) "holds" (Bool (Set ($#k20_modelc_3 :::"LTLNew2"::: ) "(" (Set (Var "H")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_modelc_3 :::"LTLNew2"::: ) (Set (Var "H"))))); theorem :: MODELC_3:19 (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "N2")) "," (Set (Var "N1")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "st" (Bool (Bool (Set (Var "N2")) ($#r2_modelc_3 :::"is_succ1_of"::: ) (Set (Var "N1")))) "holds" (Bool (Set ($#k18_modelc_3 :::"len"::: ) (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set (Var "N2")))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k18_modelc_3 :::"len"::: ) (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set (Var "N1"))) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1))))) ; theorem :: MODELC_3:20 (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "N2")) "," (Set (Var "N1")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "st" (Bool (Bool (Set (Var "N2")) ($#r3_modelc_3 :::"is_succ2_of"::: ) (Set (Var "N1")))) "holds" (Bool (Set ($#k18_modelc_3 :::"len"::: ) (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set (Var "N2")))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k18_modelc_3 :::"len"::: ) (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set (Var "N1"))) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1))))) ; definitionlet "v" be ($#m2_finseq_1 :::"LTL-formula":::); let "N" be ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Const "v")); func :::"len"::: "N" -> ($#m1_hidden :::"Nat":::) equals :: MODELC_3:def 29 (Set ($#k1_int_1 :::"[\"::: ) (Set "(" ($#k18_modelc_3 :::"len"::: ) (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" "N") ")" ) ($#k1_int_1 :::"/]"::: ) ); end; :: deftheorem defines :::"len"::: MODELC_3:def 29 : (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "N")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "holds" (Bool (Set ($#k21_modelc_3 :::"len"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set ($#k1_int_1 :::"[\"::: ) (Set "(" ($#k18_modelc_3 :::"len"::: ) (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set (Var "N"))) ")" ) ($#k1_int_1 :::"/]"::: ) )))); theorem :: MODELC_3:21 (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "N2")) "," (Set (Var "N1")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "st" (Bool (Bool (Set (Var "N2")) ($#r4_modelc_3 :::"is_succ_of"::: ) (Set (Var "N1")))) "holds" (Bool (Set ($#k21_modelc_3 :::"len"::: ) (Set (Var "N2"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k21_modelc_3 :::"len"::: ) (Set (Var "N1")) ")" ) ($#k5_real_1 :::"-"::: ) (Num 1))))) ; theorem :: MODELC_3:22 (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "N")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "st" (Bool (Bool (Set ($#k21_modelc_3 :::"len"::: ) (Set (Var "N"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set ($#k7_modelc_3 :::"{}"::: ) (Set (Var "v")))))) ; theorem :: MODELC_3:23 (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "N")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "st" (Bool (Bool (Set ($#k21_modelc_3 :::"len"::: ) (Set (Var "N"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set (Var "N"))) ($#r1_hidden :::"<>"::: ) (Set ($#k7_modelc_3 :::"{}"::: ) (Set (Var "v")))))) ; theorem :: MODELC_3:24 (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "N")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::)(Bool "ex" (Set (Var "L")) "being" ($#m1_hidden :::"FinSequence":::)(Bool "ex" (Set (Var "M")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "st" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "N"))) & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "M"))) & (Bool (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k7_modelc_3 :::"{}"::: ) (Set (Var "v")))) & (Bool (Set (Var "L")) ($#r5_modelc_3 :::"is_Finseq_for"::: ) (Set (Var "v"))) ")" )))))) ; theorem :: MODELC_3:25 (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "N2")) "," (Set (Var "N1")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "st" (Bool (Bool (Set (Var "N2")) ($#r4_modelc_3 :::"is_succ_of"::: ) (Set (Var "N1")))) "holds" (Bool "(" (Bool (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set (Var "N1"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set (Var "N2")))) & (Bool (Set "the" ($#u3_modelc_3 :::"LTLnext"::: ) "of" (Set (Var "N1"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u3_modelc_3 :::"LTLnext"::: ) "of" (Set (Var "N2")))) ")" ))) ; theorem :: MODELC_3:26 (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "L")) "," (Set (Var "L1")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "L")) ($#r5_modelc_3 :::"is_Finseq_for"::: ) (Set (Var "v"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "L")))) & (Bool (Set (Var "L1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "L")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "m")) ")" )))) "holds" (Bool (Set (Var "L1")) ($#r5_modelc_3 :::"is_Finseq_for"::: ) (Set (Var "v")))))) ; theorem :: MODELC_3:27 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "L")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "F")) "," (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "L")) ($#r5_modelc_3 :::"is_Finseq_for"::: ) (Set (Var "v"))) & (Bool (Bool "not" (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) "," (Set (Var "v")) ")" ")" )))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "L")))) & (Bool (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set (Var "v")) ")" ")" )))) "holds" (Bool "ex" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) & (Bool (Bool "not" (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "m")) ")" ) "," (Set (Var "v")) ")" ")" )))) & (Bool (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "m")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "v")) ")" ")" ))) ")" ))))) ; theorem :: MODELC_3:28 (Bool "for" (Set (Var "F")) "," (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "N2")) "," (Set (Var "N1")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "st" (Bool (Bool (Set (Var "N2")) ($#r4_modelc_3 :::"is_succ_of"::: ) (Set (Var "N1"))) & (Bool (Bool "not" (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set (Var "N1"))))) & (Bool (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set (Var "N2"))))) "holds" (Bool (Set (Var "N2")) ($#r1_modelc_3 :::"is_succ_of"::: ) (Set (Var "N1")) "," (Set (Var "F"))))) ; theorem :: MODELC_3:29 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "L")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "F")) "," (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "L")) ($#r5_modelc_3 :::"is_Finseq_for"::: ) (Set (Var "v"))) & (Bool (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) "," (Set (Var "v")) ")" ")" ))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "L")))) & (Bool (Bool "not" (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set (Var "v")) ")" ")" ))))) "holds" (Bool "ex" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) & (Bool (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "m")) ")" ) "," (Set (Var "v")) ")" ")" ))) & (Bool (Bool "not" (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "m")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "v")) ")" ")" )))) ")" ))))) ; theorem :: MODELC_3:30 (Bool "for" (Set (Var "F")) "," (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "N2")) "," (Set (Var "N1")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "st" (Bool (Bool (Set (Var "N2")) ($#r4_modelc_3 :::"is_succ_of"::: ) (Set (Var "N1"))) & (Bool (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set (Var "N1")))) & (Bool (Bool "not" (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set (Var "N2")))))) "holds" (Bool (Set (Var "N2")) ($#r1_modelc_3 :::"is_succ_of"::: ) (Set (Var "N1")) "," (Set (Var "F"))))) ; theorem :: MODELC_3:31 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "L")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "L")) ($#r5_modelc_3 :::"is_Finseq_for"::: ) (Set (Var "v"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "L"))))) "holds" (Bool "(" (Bool (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "m")) ")" ) "," (Set (Var "v")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set (Var "v")) ")" ")" ))) & (Bool (Set "the" ($#u3_modelc_3 :::"LTLnext"::: ) "of" (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "m")) ")" ) "," (Set (Var "v")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set "the" ($#u3_modelc_3 :::"LTLnext"::: ) "of" (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set (Var "v")) ")" ")" ))) ")" )))) ; theorem :: MODELC_3:32 (Bool "for" (Set (Var "F")) "," (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "N2")) "," (Set (Var "N1")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "st" (Bool (Bool (Set (Var "N2")) ($#r1_modelc_3 :::"is_succ_of"::: ) (Set (Var "N1")) "," (Set (Var "F")))) "holds" (Bool (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set (Var "N2")))))) ; theorem :: MODELC_3:33 (Bool "for" (Set (Var "L")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "L")) ($#r5_modelc_3 :::"is_Finseq_for"::: ) (Set (Var "v"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "L")))) & (Bool (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "L")) ")" ) ")" ) "," (Set (Var "v")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_modelc_3 :::"{}"::: ) (Set (Var "v"))))) "holds" (Bool (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) "," (Set (Var "v")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "L")) ")" ) ")" ) "," (Set (Var "v")) ")" ")" ))))) ; theorem :: MODELC_3:34 (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "L")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "L")) ($#r5_modelc_3 :::"is_Finseq_for"::: ) (Set (Var "v"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "L")))) & (Bool (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "L")) ")" ) ")" ) "," (Set (Var "v")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_modelc_3 :::"{}"::: ) (Set (Var "v"))))) "holds" (Bool (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "m")) ")" ) "," (Set (Var "v")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "L")) ")" ) ")" ) "," (Set (Var "v")) ")" ")" )))))) ; theorem :: MODELC_3:35 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "L")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "L")) ($#r5_modelc_3 :::"is_Finseq_for"::: ) (Set (Var "v"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "L"))))) "holds" (Bool (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "v")) ")" ) ($#r4_modelc_3 :::"is_succ_of"::: ) (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) "," (Set (Var "v")) ")" ))))) ; theorem :: MODELC_3:36 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "L")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "L")) ($#r5_modelc_3 :::"is_Finseq_for"::: ) (Set (Var "v"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "L"))))) "holds" (Bool (Set ($#k21_modelc_3 :::"len"::: ) (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) "," (Set (Var "v")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" ($#k21_modelc_3 :::"len"::: ) (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) "," (Set (Var "v")) ")" ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "k")) ")" ) ($#k3_real_1 :::"+"::: ) (Num 1)))))) ; theorem :: MODELC_3:37 (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "s2")) "," (Set (Var "s1")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#v3_modelc_3 :::"elementary"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "st" (Bool (Bool (Set (Var "s2")) ($#r6_modelc_3 :::"is_next_of"::: ) (Set (Var "s1")))) "holds" (Bool (Set "the" ($#u3_modelc_3 :::"LTLnext"::: ) "of" (Set (Var "s1"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set (Var "s2")))))) ; theorem :: MODELC_3:38 (Bool "for" (Set (Var "F")) "," (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "s2")) "," (Set (Var "s1")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#v3_modelc_3 :::"elementary"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "st" (Bool (Bool (Set (Var "s2")) ($#r6_modelc_3 :::"is_next_of"::: ) (Set (Var "s1"))) & (Bool (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set (Var "s2"))))) "holds" (Bool "ex" (Set (Var "L")) "being" ($#m1_hidden :::"FinSequence":::)(Bool "ex" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "L")))) & (Bool (Set (Var "L")) ($#r5_modelc_3 :::"is_Finseq_for"::: ) (Set (Var "v"))) & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k12_modelc_3 :::"'X'"::: ) (Set (Var "s1")))) & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "s2"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "L")))) & (Bool (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "m")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "v")) ")" ) ($#r1_modelc_3 :::"is_succ_of"::: ) (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "m")) ")" ) "," (Set (Var "v")) ")" ) "," (Set (Var "F"))) ")" ))))) ; theorem :: MODELC_3:39 (Bool "for" (Set (Var "H")) "," (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "s2")) "," (Set (Var "s1")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#v3_modelc_3 :::"elementary"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "st" (Bool (Bool (Set (Var "s2")) ($#r6_modelc_3 :::"is_next_of"::: ) (Set (Var "s1"))) & (Bool (Set (Var "H")) "is" ($#v8_modelc_2 :::"Release"::: ) ) & (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set (Var "s2")))) & (Bool (Bool "not" (Set ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set (Var "s2")))))) "holds" (Bool "(" (Bool (Set ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set (Var "s2")))) & (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u3_modelc_3 :::"LTLnext"::: ) "of" (Set (Var "s2")))) ")" ))) ; theorem :: MODELC_3:40 (Bool "for" (Set (Var "H")) "," (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "s2")) "," (Set (Var "s1")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#v3_modelc_3 :::"elementary"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "st" (Bool (Bool (Set (Var "s2")) ($#r6_modelc_3 :::"is_next_of"::: ) (Set (Var "s1"))) & (Bool (Set (Var "H")) "is" ($#v8_modelc_2 :::"Release"::: ) ) & (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u3_modelc_3 :::"LTLnext"::: ) "of" (Set (Var "s1"))))) "holds" (Bool "(" (Bool (Set ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set (Var "s2")))) & (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set (Var "s2")))) ")" ))) ; theorem :: MODELC_3:41 (Bool "for" (Set (Var "H")) "," (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s0")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#v3_modelc_3 :::"elementary"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "st" (Bool (Bool (Set (Var "s1")) ($#r6_modelc_3 :::"is_next_of"::: ) (Set (Var "s0"))) & (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set (Var "s1"))))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "H")) "is" ($#v4_modelc_2 :::"conjunctive"::: ) )) "implies" (Bool "(" (Bool (Set ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set (Var "s1")))) & (Bool (Set ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set (Var "s1")))) ")" ) ")" & (Bool "(" (Bool "(" (Bool (Bool "not" (Set (Var "H")) "is" ($#v5_modelc_2 :::"disjunctive"::: ) )) & (Bool (Bool "not" (Set (Var "H")) "is" ($#v7_modelc_2 :::"Until"::: ) )) ")" ) "or" (Bool (Set ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set (Var "s1")))) "or" (Bool (Set ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set (Var "s1")))) ")" ) & "(" (Bool (Bool (Set (Var "H")) "is" ($#v6_modelc_2 :::"next"::: ) )) "implies" (Bool (Set ($#k10_modelc_2 :::"the_argument_of"::: ) (Set (Var "H"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u3_modelc_3 :::"LTLnext"::: ) "of" (Set (Var "s1")))) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v8_modelc_2 :::"Release"::: ) )) "implies" (Bool (Set ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set (Var "s1")))) ")" ")" ))) ; theorem :: MODELC_3:42 (Bool "for" (Set (Var "H")) "," (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s0")) "," (Set (Var "s2")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#v3_modelc_3 :::"elementary"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "st" (Bool (Bool (Set (Var "s1")) ($#r6_modelc_3 :::"is_next_of"::: ) (Set (Var "s0"))) & (Bool (Set (Var "s2")) ($#r6_modelc_3 :::"is_next_of"::: ) (Set (Var "s1"))) & (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set (Var "s1")))) & (Bool (Set (Var "H")) "is" ($#v7_modelc_2 :::"Until"::: ) ) & (Bool (Bool "not" (Set ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set (Var "s1")))))) "holds" (Bool "(" (Bool (Set ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set (Var "s1")))) & (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set (Var "s2")))) ")" ))) ; definitionlet "v" be ($#m2_finseq_1 :::"LTL-formula":::); func :::"LTLNodes"::: "v" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) means :: MODELC_3:def 30 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "N")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" "v" "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "N")))) ")" )); end; :: deftheorem defines :::"LTLNodes"::: MODELC_3:def 30 : (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "b2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k22_modelc_3 :::"LTLNodes"::: ) (Set (Var "v")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "ex" (Set (Var "N")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "N")))) ")" )) ")" ))); registrationlet "v" be ($#m2_finseq_1 :::"LTL-formula":::); cluster (Set ($#k22_modelc_3 :::"LTLNodes"::: ) "v") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ; end; definitionlet "v" be ($#m2_finseq_1 :::"LTL-formula":::); func :::"LTLStates"::: "v" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) equals :: MODELC_3:def 31 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k22_modelc_3 :::"LTLNodes"::: ) "v") : (Bool (Set (Var "x")) "is" ($#v1_modelc_3 :::"strict"::: ) ($#v3_modelc_3 :::"elementary"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" "v") "}" ; end; :: deftheorem defines :::"LTLStates"::: MODELC_3:def 31 : (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool (Set ($#k23_modelc_3 :::"LTLStates"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k22_modelc_3 :::"LTLNodes"::: ) (Set (Var "v"))) : (Bool (Set (Var "x")) "is" ($#v1_modelc_3 :::"strict"::: ) ($#v3_modelc_3 :::"elementary"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v"))) "}" )); registrationlet "v" be ($#m2_finseq_1 :::"LTL-formula":::); cluster (Set ($#k23_modelc_3 :::"LTLStates"::: ) "v") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: MODELC_3:43 (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool (Set ($#k11_modelc_3 :::"init"::: ) (Set (Var "v"))) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k23_modelc_3 :::"LTLStates"::: ) (Set (Var "v"))))) ; theorem :: MODELC_3:44 (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "s")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#v3_modelc_3 :::"elementary"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "holds" (Bool (Set (Var "s")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k23_modelc_3 :::"LTLStates"::: ) (Set (Var "v")))))) ; theorem :: MODELC_3:45 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k23_modelc_3 :::"LTLStates"::: ) (Set (Var "v")))) "iff" (Bool "ex" (Set (Var "s")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#v3_modelc_3 :::"elementary"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "st" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ")" ))) ; definitionlet "v" be ($#m2_finseq_1 :::"LTL-formula":::); let "w" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )); let "f" be ($#m1_hidden :::"Function":::); pred "f" :::"is_succ_homomorphism"::: "v" "," "w" means :: MODELC_3:def 32 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k22_modelc_3 :::"LTLNodes"::: ) "v")) & (Bool (Bool "not" (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set (Var "x")) "," "v" ")" ) "is" ($#v3_modelc_3 :::"elementary"::: ) )) & (Bool "w" ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set (Var "x")) "," "v" ")" ")" )))) "holds" (Bool "(" (Bool (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," "v" ")" ) ($#r4_modelc_3 :::"is_succ_of"::: ) (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set (Var "x")) "," "v" ")" )) & (Bool "w" ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," "v" ")" ")" ))) ")" )); pred "f" :::"is_homomorphism"::: "v" "," "w" means :: MODELC_3:def 33 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k22_modelc_3 :::"LTLNodes"::: ) "v")) & (Bool (Bool "not" (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set (Var "x")) "," "v" ")" ) "is" ($#v3_modelc_3 :::"elementary"::: ) )) & (Bool "w" ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set (Var "x")) "," "v" ")" ")" )))) "holds" (Bool "w" ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," "v" ")" ")" )))); end; :: deftheorem defines :::"is_succ_homomorphism"::: MODELC_3:def 32 : (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r7_modelc_3 :::"is_succ_homomorphism"::: ) (Set (Var "v")) "," (Set (Var "w"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k22_modelc_3 :::"LTLNodes"::: ) (Set (Var "v")))) & (Bool (Bool "not" (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set (Var "x")) "," (Set (Var "v")) ")" ) "is" ($#v3_modelc_3 :::"elementary"::: ) )) & (Bool (Set (Var "w")) ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set (Var "x")) "," (Set (Var "v")) ")" ")" )))) "holds" (Bool "(" (Bool (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "v")) ")" ) ($#r4_modelc_3 :::"is_succ_of"::: ) (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set (Var "x")) "," (Set (Var "v")) ")" )) & (Bool (Set (Var "w")) ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "v")) ")" ")" ))) ")" )) ")" )))); :: deftheorem defines :::"is_homomorphism"::: MODELC_3:def 33 : (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r8_modelc_3 :::"is_homomorphism"::: ) (Set (Var "v")) "," (Set (Var "w"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k22_modelc_3 :::"LTLNodes"::: ) (Set (Var "v")))) & (Bool (Bool "not" (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set (Var "x")) "," (Set (Var "v")) ")" ) "is" ($#v3_modelc_3 :::"elementary"::: ) )) & (Bool (Set (Var "w")) ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set (Var "x")) "," (Set (Var "v")) ")" ")" )))) "holds" (Bool (Set (Var "w")) ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "v")) ")" ")" )))) ")" )))); theorem :: MODELC_3:46 (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k22_modelc_3 :::"LTLNodes"::: ) (Set (Var "v")) ")" ) "," (Set "(" ($#k22_modelc_3 :::"LTLNodes"::: ) (Set (Var "v")) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r7_modelc_3 :::"is_succ_homomorphism"::: ) (Set (Var "v")) "," (Set (Var "w")))) "holds" (Bool (Set (Var "f")) ($#r8_modelc_3 :::"is_homomorphism"::: ) (Set (Var "v")) "," (Set (Var "w")))))) ; theorem :: MODELC_3:47 (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k22_modelc_3 :::"LTLNodes"::: ) (Set (Var "v")) ")" ) "," (Set "(" ($#k22_modelc_3 :::"LTLNodes"::: ) (Set (Var "v")) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r8_modelc_3 :::"is_homomorphism"::: ) (Set (Var "v")) "," (Set (Var "w")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k22_modelc_3 :::"LTLNodes"::: ) (Set (Var "v")))) & (Bool (Bool "not" (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set (Var "x")) "," (Set (Var "v")) ")" ) "is" ($#v3_modelc_3 :::"elementary"::: ) )) & (Bool (Set (Var "w")) ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set (Var "x")) "," (Set (Var "v")) ")" ")" )))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool "not" (Bool (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set "(" (Set (Var "f")) ($#k29_modelc_1 :::"|**"::: ) (Set (Var "i")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "v")) ")" ) "is" ($#v3_modelc_3 :::"elementary"::: ) )) ")" )) "holds" (Bool (Set (Var "w")) ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set "(" (Set (Var "f")) ($#k29_modelc_1 :::"|**"::: ) (Set (Var "k")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "v")) ")" ")" )))))))) ; theorem :: MODELC_3:48 (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k22_modelc_3 :::"LTLNodes"::: ) (Set (Var "v")) ")" ) "," (Set "(" ($#k22_modelc_3 :::"LTLNodes"::: ) (Set (Var "v")) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r7_modelc_3 :::"is_succ_homomorphism"::: ) (Set (Var "v")) "," (Set (Var "w")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k22_modelc_3 :::"LTLNodes"::: ) (Set (Var "v")))) & (Bool (Bool "not" (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set (Var "x")) "," (Set (Var "v")) ")" ) "is" ($#v3_modelc_3 :::"elementary"::: ) )) & (Bool (Set (Var "w")) ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set (Var "x")) "," (Set (Var "v")) ")" ")" )))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool "not" (Bool (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set "(" (Set (Var "f")) ($#k29_modelc_1 :::"|**"::: ) (Set (Var "i")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "v")) ")" ) "is" ($#v3_modelc_3 :::"elementary"::: ) )) ")" )) "holds" (Bool "(" (Bool (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set "(" (Set (Var "f")) ($#k29_modelc_1 :::"|**"::: ) (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "v")) ")" ) ($#r4_modelc_3 :::"is_succ_of"::: ) (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set "(" (Set (Var "f")) ($#k29_modelc_1 :::"|**"::: ) (Set (Var "k")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "v")) ")" )) & (Bool (Set (Var "w")) ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set "(" (Set (Var "f")) ($#k29_modelc_1 :::"|**"::: ) (Set (Var "k")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "v")) ")" ")" ))) ")" )))))) ; theorem :: MODELC_3:49 (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k22_modelc_3 :::"LTLNodes"::: ) (Set (Var "v")) ")" ) "," (Set "(" ($#k22_modelc_3 :::"LTLNodes"::: ) (Set (Var "v")) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r7_modelc_3 :::"is_succ_homomorphism"::: ) (Set (Var "v")) "," (Set (Var "w")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k22_modelc_3 :::"LTLNodes"::: ) (Set (Var "v")))) & (Bool (Bool "not" (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set (Var "x")) "," (Set (Var "v")) ")" ) "is" ($#v3_modelc_3 :::"elementary"::: ) )) & (Bool (Set (Var "w")) ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set (Var "x")) "," (Set (Var "v")) ")" ")" )))) "holds" (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool "not" (Bool (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set "(" (Set (Var "f")) ($#k29_modelc_1 :::"|**"::: ) (Set (Var "i")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "v")) ")" ) "is" ($#v3_modelc_3 :::"elementary"::: ) )) ")" ) & (Bool (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set "(" (Set (Var "f")) ($#k29_modelc_1 :::"|**"::: ) (Set (Var "n")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "v")) ")" ) "is" ($#v3_modelc_3 :::"elementary"::: ) ) ")" )))))) ; theorem :: MODELC_3:50 (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k22_modelc_3 :::"LTLNodes"::: ) (Set (Var "v")) ")" ) "," (Set "(" ($#k22_modelc_3 :::"LTLNodes"::: ) (Set (Var "v")) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r8_modelc_3 :::"is_homomorphism"::: ) (Set (Var "v")) "," (Set (Var "w")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k22_modelc_3 :::"LTLNodes"::: ) (Set (Var "v")))) & (Bool (Bool "not" (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set (Var "x")) "," (Set (Var "v")) ")" ) "is" ($#v3_modelc_3 :::"elementary"::: ) ))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Bool "not" (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set "(" (Set (Var "f")) ($#k29_modelc_1 :::"|**"::: ) (Set (Var "k")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "v")) ")" ) "is" ($#v3_modelc_3 :::"elementary"::: ) )) & (Bool (Set (Var "w")) ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set "(" (Set (Var "f")) ($#k29_modelc_1 :::"|**"::: ) (Set (Var "k")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "v")) ")" ")" )))) "holds" (Bool (Set (Var "w")) ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set "(" (Set (Var "f")) ($#k29_modelc_1 :::"|**"::: ) (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "v")) ")" ")" )))))))) ; theorem :: MODELC_3:51 (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k22_modelc_3 :::"LTLNodes"::: ) (Set (Var "v")) ")" ) "," (Set "(" ($#k22_modelc_3 :::"LTLNodes"::: ) (Set (Var "v")) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r7_modelc_3 :::"is_succ_homomorphism"::: ) (Set (Var "v")) "," (Set (Var "w")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k22_modelc_3 :::"LTLNodes"::: ) (Set (Var "v")))) & (Bool (Bool "not" (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set (Var "x")) "," (Set (Var "v")) ")" ) "is" ($#v3_modelc_3 :::"elementary"::: ) )) & (Bool (Set (Var "w")) ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set (Var "x")) "," (Set (Var "v")) ")" ")" )))) "holds" (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set "(" (Set (Var "f")) ($#k29_modelc_1 :::"|**"::: ) (Set (Var "i")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "v")) ")" ) "is" ($#v3_modelc_3 :::"elementary"::: ) )) & (Bool (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set "(" (Set (Var "f")) ($#k29_modelc_1 :::"|**"::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "v")) ")" ) ($#r4_modelc_3 :::"is_succ_of"::: ) (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set "(" (Set (Var "f")) ($#k29_modelc_1 :::"|**"::: ) (Set (Var "i")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "v")) ")" )) ")" ) ")" ) & (Bool (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set "(" (Set (Var "f")) ($#k29_modelc_1 :::"|**"::: ) (Set (Var "n")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "v")) ")" ) "is" ($#v3_modelc_3 :::"elementary"::: ) ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Var "w")) ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set "(" (Set (Var "f")) ($#k29_modelc_1 :::"|**"::: ) (Set (Var "i")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "v")) ")" ")" ))) ")" ) ")" )))))) ; theorem :: MODELC_3:52 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k23_modelc_3 :::"LTLStates"::: ) (Set (Var "v")) ")" ) (Bool "ex" (Set (Var "s")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#v3_modelc_3 :::"elementary"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "st" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set (Var "v")) ")" )))))) ; theorem :: MODELC_3:53 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "H")) "," (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k23_modelc_3 :::"LTLStates"::: ) (Set (Var "v")) ")" ) "st" (Bool (Bool (Set (Var "H")) "is" ($#v7_modelc_2 :::"Until"::: ) ) & (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "q")) ($#k3_funct_2 :::"."::: ) (Num 1) ")" ) "," (Set (Var "v")) ")" ")" ))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "q")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "v")) ")" ) ($#r6_modelc_3 :::"is_next_of"::: ) (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set (Var "v")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool "not" (Bool (Set ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set (Var "v")) ")" ")" )))) ")" )) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool "(" (Bool (Set ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set (Var "v")) ")" ")" ))) & (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set (Var "v")) ")" ")" ))) ")" ))))) ; theorem :: MODELC_3:54 (Bool "for" (Set (Var "H")) "," (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k23_modelc_3 :::"LTLStates"::: ) (Set (Var "v")) ")" ) "st" (Bool (Bool (Set (Var "H")) "is" ($#v7_modelc_2 :::"Until"::: ) ) & (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "q")) ($#k3_funct_2 :::"."::: ) (Num 1) ")" ) "," (Set (Var "v")) ")" ")" ))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "q")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "v")) ")" ) ($#r6_modelc_3 :::"is_next_of"::: ) (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set (Var "v")) ")" )) ")" ) & (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool "not" (Bool "(" (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set (Var "v")) ")" ")" ))) & (Bool (Set ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set (Var "v")) ")" ")" ))) & (Bool (Bool "not" (Set ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set (Var "v")) ")" ")" )))) ")" )) ")" ))) "holds" (Bool "ex" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "j")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")) ")" ) "," (Set (Var "v")) ")" ")" ))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j")))) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set (Var "v")) ")" ")" ))) & (Bool (Set ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set (Var "v")) ")" ")" ))) ")" ) ")" ) ")" )))) ; theorem :: MODELC_3:55 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k1_orders_1 :::"BOOL"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "X")))) ; theorem :: MODELC_3:56 (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "N")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "st" (Bool (Bool (Bool "not" (Set (Var "N")) "is" ($#v3_modelc_3 :::"elementary"::: ) ))) "holds" (Bool "(" (Bool (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set (Var "N"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set (Var "N"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) (Set (Var "v")) ")" ))) ")" ))) ; registrationlet "v" be ($#m2_finseq_1 :::"LTL-formula":::); cluster (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k1_orders_1 :::"BOOL"::: ) (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) "v" ")" ) ")" )) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) "v" ")" )) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: MODELC_3:57 (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "ex" (Set (Var "f")) "being" ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) (Set (Var "v")) ")" )) "st" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_orders_1 :::"BOOL"::: ) (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) (Set (Var "v")) ")" ) ")" ) "," (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) (Set (Var "v")) ")" )))) ; definitionlet "v" be ($#m2_finseq_1 :::"LTL-formula":::); let "U" be ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) (Set (Const "v")) ")" )); let "N" be ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Const "v")); assume (Bool (Bool "not" (Set (Const "N")) "is" ($#v3_modelc_3 :::"elementary"::: ) )) ; func :::"chosen_formula"::: "(" "U" "," "N" ")" -> ($#m2_finseq_1 :::"LTL-formula":::) equals :: MODELC_3:def 34 (Set "U" ($#k1_funct_1 :::"."::: ) (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" "N")); end; :: deftheorem defines :::"chosen_formula"::: MODELC_3:def 34 : (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "U")) "being" ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) (Set (Var "v")) ")" )) (Bool "for" (Set (Var "N")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "st" (Bool (Bool (Bool "not" (Set (Var "N")) "is" ($#v3_modelc_3 :::"elementary"::: ) ))) "holds" (Bool (Set ($#k24_modelc_3 :::"chosen_formula"::: ) "(" (Set (Var "U")) "," (Set (Var "N")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "U")) ($#k1_funct_1 :::"."::: ) (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set (Var "N")))))))); theorem :: MODELC_3:58 (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "N")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) (Bool "for" (Set (Var "U")) "being" ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) (Set (Var "v")) ")" )) "st" (Bool (Bool (Bool "not" (Set (Var "N")) "is" ($#v3_modelc_3 :::"elementary"::: ) ))) "holds" (Bool (Set ($#k24_modelc_3 :::"chosen_formula"::: ) "(" (Set (Var "U")) "," (Set (Var "N")) ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set (Var "N"))))))) ; definitionlet "w" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )); let "v" be ($#m2_finseq_1 :::"LTL-formula":::); let "U" be ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) (Set (Const "v")) ")" )); let "N" be ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Const "v")); func :::"chosen_succ"::: "(" "w" "," "v" "," "U" "," "N" ")" -> ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" "v" equals :: MODELC_3:def 35 (Set ($#k5_modelc_3 :::"SuccNode1"::: ) "(" (Set "(" ($#k24_modelc_3 :::"chosen_formula"::: ) "(" "U" "," "N" ")" ")" ) "," "N" ")" ) if (Bool "(" (Bool "(" (Bool (Bool "not" (Set ($#k24_modelc_3 :::"chosen_formula"::: ) "(" "U" "," "N" ")" ) "is" ($#v7_modelc_2 :::"Until"::: ) )) & (Bool "w" ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set "(" ($#k5_modelc_3 :::"SuccNode1"::: ) "(" (Set "(" ($#k24_modelc_3 :::"chosen_formula"::: ) "(" "U" "," "N" ")" ")" ) "," "N" ")" ")" ))) ")" ) "or" (Bool "(" (Bool (Set ($#k24_modelc_3 :::"chosen_formula"::: ) "(" "U" "," "N" ")" ) "is" ($#v7_modelc_2 :::"Until"::: ) ) & (Bool "w" ($#r7_modelc_2 :::"|/="::: ) (Set ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set "(" ($#k24_modelc_3 :::"chosen_formula"::: ) "(" "U" "," "N" ")" ")" ))) ")" ) ")" ) otherwise (Set ($#k6_modelc_3 :::"SuccNode2"::: ) "(" (Set "(" ($#k24_modelc_3 :::"chosen_formula"::: ) "(" "U" "," "N" ")" ")" ) "," "N" ")" ); end; :: deftheorem defines :::"chosen_succ"::: MODELC_3:def 35 : (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "U")) "being" ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) (Set (Var "v")) ")" )) (Bool "for" (Set (Var "N")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "holds" (Bool "(" "(" (Bool (Bool "(" (Bool "(" (Bool (Bool "not" (Set ($#k24_modelc_3 :::"chosen_formula"::: ) "(" (Set (Var "U")) "," (Set (Var "N")) ")" ) "is" ($#v7_modelc_2 :::"Until"::: ) )) & (Bool (Set (Var "w")) ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set "(" ($#k5_modelc_3 :::"SuccNode1"::: ) "(" (Set "(" ($#k24_modelc_3 :::"chosen_formula"::: ) "(" (Set (Var "U")) "," (Set (Var "N")) ")" ")" ) "," (Set (Var "N")) ")" ")" ))) ")" ) "or" (Bool "(" (Bool (Set ($#k24_modelc_3 :::"chosen_formula"::: ) "(" (Set (Var "U")) "," (Set (Var "N")) ")" ) "is" ($#v7_modelc_2 :::"Until"::: ) ) & (Bool (Set (Var "w")) ($#r7_modelc_2 :::"|/="::: ) (Set ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set "(" ($#k24_modelc_3 :::"chosen_formula"::: ) "(" (Set (Var "U")) "," (Set (Var "N")) ")" ")" ))) ")" ) ")" )) "implies" (Bool (Set ($#k25_modelc_3 :::"chosen_succ"::: ) "(" (Set (Var "w")) "," (Set (Var "v")) "," (Set (Var "U")) "," (Set (Var "N")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_modelc_3 :::"SuccNode1"::: ) "(" (Set "(" ($#k24_modelc_3 :::"chosen_formula"::: ) "(" (Set (Var "U")) "," (Set (Var "N")) ")" ")" ) "," (Set (Var "N")) ")" )) ")" & (Bool "(" (Bool "(" (Bool (Bool "not" (Set ($#k24_modelc_3 :::"chosen_formula"::: ) "(" (Set (Var "U")) "," (Set (Var "N")) ")" ) "is" ($#v7_modelc_2 :::"Until"::: ) )) & (Bool (Set (Var "w")) ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set "(" ($#k5_modelc_3 :::"SuccNode1"::: ) "(" (Set "(" ($#k24_modelc_3 :::"chosen_formula"::: ) "(" (Set (Var "U")) "," (Set (Var "N")) ")" ")" ) "," (Set (Var "N")) ")" ")" ))) ")" ) "or" (Bool "(" (Bool (Set ($#k24_modelc_3 :::"chosen_formula"::: ) "(" (Set (Var "U")) "," (Set (Var "N")) ")" ) "is" ($#v7_modelc_2 :::"Until"::: ) ) & (Bool (Set (Var "w")) ($#r7_modelc_2 :::"|/="::: ) (Set ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set "(" ($#k24_modelc_3 :::"chosen_formula"::: ) "(" (Set (Var "U")) "," (Set (Var "N")) ")" ")" ))) ")" ) "or" (Bool (Set ($#k25_modelc_3 :::"chosen_succ"::: ) "(" (Set (Var "w")) "," (Set (Var "v")) "," (Set (Var "U")) "," (Set (Var "N")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_modelc_3 :::"SuccNode2"::: ) "(" (Set "(" ($#k24_modelc_3 :::"chosen_formula"::: ) "(" (Set (Var "U")) "," (Set (Var "N")) ")" ")" ) "," (Set (Var "N")) ")" )) ")" ) ")" ))))); theorem :: MODELC_3:59 (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "N")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) (Bool "for" (Set (Var "U")) "being" ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) (Set (Var "v")) ")" )) "st" (Bool (Bool (Set (Var "w")) ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set (Var "N")))) & (Bool (Bool "not" (Set (Var "N")) "is" ($#v3_modelc_3 :::"elementary"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "w")) ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set "(" ($#k25_modelc_3 :::"chosen_succ"::: ) "(" (Set (Var "w")) "," (Set (Var "v")) "," (Set (Var "U")) "," (Set (Var "N")) ")" ")" ))) & (Bool (Set ($#k25_modelc_3 :::"chosen_succ"::: ) "(" (Set (Var "w")) "," (Set (Var "v")) "," (Set (Var "U")) "," (Set (Var "N")) ")" ) ($#r4_modelc_3 :::"is_succ_of"::: ) (Set (Var "N"))) ")" ))))) ; theorem :: MODELC_3:60 (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "N")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) (Bool "for" (Set (Var "U")) "being" ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) (Set (Var "v")) ")" )) "st" (Bool (Bool (Bool "not" (Set (Var "N")) "is" ($#v3_modelc_3 :::"elementary"::: ) )) & (Bool (Set ($#k24_modelc_3 :::"chosen_formula"::: ) "(" (Set (Var "U")) "," (Set (Var "N")) ")" ) "is" ($#v7_modelc_2 :::"Until"::: ) ) & (Bool (Set (Var "w")) ($#r7_modelc_2 :::"|="::: ) (Set ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set "(" ($#k24_modelc_3 :::"chosen_formula"::: ) "(" (Set (Var "U")) "," (Set (Var "N")) ")" ")" )))) "holds" (Bool "(" (Bool "(" (Bool (Set ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set "(" ($#k24_modelc_3 :::"chosen_formula"::: ) "(" (Set (Var "U")) "," (Set (Var "N")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set "the" ($#u2_modelc_3 :::"LTLnew"::: ) "of" (Set "(" ($#k25_modelc_3 :::"chosen_succ"::: ) "(" (Set (Var "w")) "," (Set (Var "v")) "," (Set (Var "U")) "," (Set (Var "N")) ")" ")" ))) "or" (Bool (Set ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set "(" ($#k24_modelc_3 :::"chosen_formula"::: ) "(" (Set (Var "U")) "," (Set (Var "N")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set (Var "N")))) ")" ) & (Bool (Set ($#k24_modelc_3 :::"chosen_formula"::: ) "(" (Set (Var "U")) "," (Set (Var "N")) ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set "(" ($#k25_modelc_3 :::"chosen_succ"::: ) "(" (Set (Var "w")) "," (Set (Var "v")) "," (Set (Var "U")) "," (Set (Var "N")) ")" ")" ))) ")" ))))) ; theorem :: MODELC_3:61 (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "N")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) (Bool "for" (Set (Var "U")) "being" ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) (Set (Var "v")) ")" )) "st" (Bool (Bool (Set (Var "w")) ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set (Var "N")))) & (Bool (Bool "not" (Set (Var "N")) "is" ($#v3_modelc_3 :::"elementary"::: ) ))) "holds" (Bool "(" (Bool (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set (Var "N"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set "(" ($#k25_modelc_3 :::"chosen_succ"::: ) "(" (Set (Var "w")) "," (Set (Var "v")) "," (Set (Var "U")) "," (Set (Var "N")) ")" ")" ))) & (Bool (Set "the" ($#u3_modelc_3 :::"LTLnext"::: ) "of" (Set (Var "N"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u3_modelc_3 :::"LTLnext"::: ) "of" (Set "(" ($#k25_modelc_3 :::"chosen_succ"::: ) "(" (Set (Var "w")) "," (Set (Var "v")) "," (Set (Var "U")) "," (Set (Var "N")) ")" ")" ))) ")" ))))) ; definitionlet "w" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )); let "v" be ($#m2_finseq_1 :::"LTL-formula":::); let "U" be ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) (Set (Const "v")) ")" )); func :::"choice_succ_func"::: "(" "w" "," "v" "," "U" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k22_modelc_3 :::"LTLNodes"::: ) "v" ")" ) "," (Set "(" ($#k22_modelc_3 :::"LTLNodes"::: ) "v" ")" ) means :: MODELC_3:def 36 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k22_modelc_3 :::"LTLNodes"::: ) "v"))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k25_modelc_3 :::"chosen_succ"::: ) "(" "w" "," "v" "," "U" "," (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set (Var "x")) "," "v" ")" ")" ) ")" ))); end; :: deftheorem defines :::"choice_succ_func"::: MODELC_3:def 36 : (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "U")) "being" ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) (Set (Var "v")) ")" )) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k22_modelc_3 :::"LTLNodes"::: ) (Set (Var "v")) ")" ) "," (Set "(" ($#k22_modelc_3 :::"LTLNodes"::: ) (Set (Var "v")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k26_modelc_3 :::"choice_succ_func"::: ) "(" (Set (Var "w")) "," (Set (Var "v")) "," (Set (Var "U")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k22_modelc_3 :::"LTLNodes"::: ) (Set (Var "v"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k25_modelc_3 :::"chosen_succ"::: ) "(" (Set (Var "w")) "," (Set (Var "v")) "," (Set (Var "U")) "," (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set (Var "x")) "," (Set (Var "v")) ")" ")" ) ")" ))) ")" ))))); theorem :: MODELC_3:62 (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) (Bool "for" (Set (Var "U")) "being" ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) (Set (Var "v")) ")" )) "holds" (Bool (Set ($#k26_modelc_3 :::"choice_succ_func"::: ) "(" (Set (Var "w")) "," (Set (Var "v")) "," (Set (Var "U")) ")" ) ($#r7_modelc_3 :::"is_succ_homomorphism"::: ) (Set (Var "v")) "," (Set (Var "w")))))) ; begin definitionlet "H" be ($#m2_finseq_1 :::"LTL-formula":::); attr "H" is :::"neg-inner-most"::: means :: MODELC_3:def 37 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "G")) ($#r2_modelc_2 :::"is_subformula_of"::: ) "H") & (Bool (Set (Var "G")) "is" ($#v3_modelc_2 :::"negative"::: ) )) "holds" (Bool (Set ($#k10_modelc_2 :::"the_argument_of"::: ) (Set (Var "G"))) "is" ($#v2_modelc_2 :::"atomic"::: ) )); end; :: deftheorem defines :::"neg-inner-most"::: MODELC_3:def 37 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v5_modelc_3 :::"neg-inner-most"::: ) ) "iff" (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "G")) ($#r2_modelc_2 :::"is_subformula_of"::: ) (Set (Var "H"))) & (Bool (Set (Var "G")) "is" ($#v3_modelc_2 :::"negative"::: ) )) "holds" (Bool (Set ($#k10_modelc_2 :::"the_argument_of"::: ) (Set (Var "G"))) "is" ($#v2_modelc_2 :::"atomic"::: ) )) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v1_modelc_2 :::"LTL-formula-like"::: ) bbbadV1_VALUED_0() bbbadV2_VALUED_0() bbbadV3_VALUED_0() bbbadV4_VALUED_0() ($#v5_modelc_3 :::"neg-inner-most"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; definitionlet "H" be ($#m2_finseq_1 :::"LTL-formula":::); attr "H" is :::"Sub_atomic"::: means :: MODELC_3:def 38 (Bool "(" (Bool "H" "is" ($#v2_modelc_2 :::"atomic"::: ) ) "or" (Bool "ex" (Set (Var "G")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool "(" (Bool (Set (Var "G")) "is" ($#v2_modelc_2 :::"atomic"::: ) ) & (Bool "H" ($#r1_hidden :::"="::: ) (Set ($#k3_modelc_2 :::"'not'"::: ) (Set (Var "G")))) ")" )) ")" ); end; :: deftheorem defines :::"Sub_atomic"::: MODELC_3:def 38 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v6_modelc_3 :::"Sub_atomic"::: ) ) "iff" (Bool "(" (Bool (Set (Var "H")) "is" ($#v2_modelc_2 :::"atomic"::: ) ) "or" (Bool "ex" (Set (Var "G")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool "(" (Bool (Set (Var "G")) "is" ($#v2_modelc_2 :::"atomic"::: ) ) & (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k3_modelc_2 :::"'not'"::: ) (Set (Var "G")))) ")" )) ")" ) ")" )); theorem :: MODELC_3:63 (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v5_modelc_3 :::"neg-inner-most"::: ) ) & (Bool (Set (Var "F")) ($#r2_modelc_2 :::"is_subformula_of"::: ) (Set (Var "H")))) "holds" (Bool (Set (Var "F")) "is" ($#v5_modelc_3 :::"neg-inner-most"::: ) )) ; theorem :: MODELC_3:64 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v6_modelc_3 :::"Sub_atomic"::: ) ) "iff" (Bool "(" (Bool (Set (Var "H")) "is" ($#v2_modelc_2 :::"atomic"::: ) ) "or" (Bool "(" (Bool (Set (Var "H")) "is" ($#v3_modelc_2 :::"negative"::: ) ) & (Bool (Set ($#k10_modelc_2 :::"the_argument_of"::: ) (Set (Var "H"))) "is" ($#v2_modelc_2 :::"atomic"::: ) ) ")" ) ")" ) ")" )) ; theorem :: MODELC_3:65 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" "not" (Bool (Set (Var "H")) "is" ($#v5_modelc_3 :::"neg-inner-most"::: ) ) "or" (Bool (Set (Var "H")) "is" ($#v6_modelc_3 :::"Sub_atomic"::: ) ) "or" (Bool (Set (Var "H")) "is" ($#v4_modelc_2 :::"conjunctive"::: ) ) "or" (Bool (Set (Var "H")) "is" ($#v5_modelc_2 :::"disjunctive"::: ) ) "or" (Bool (Set (Var "H")) "is" ($#v6_modelc_2 :::"next"::: ) ) "or" (Bool (Set (Var "H")) "is" ($#v7_modelc_2 :::"Until"::: ) ) "or" (Bool (Set (Var "H")) "is" ($#v8_modelc_2 :::"Release"::: ) ) ")" )) ; theorem :: MODELC_3:66 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v6_modelc_2 :::"next"::: ) ) & (Bool (Set (Var "H")) "is" ($#v5_modelc_3 :::"neg-inner-most"::: ) )) "holds" (Bool (Set ($#k10_modelc_2 :::"the_argument_of"::: ) (Set (Var "H"))) "is" ($#v5_modelc_3 :::"neg-inner-most"::: ) )) ; theorem :: MODELC_3:67 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool "(" (Bool (Set (Var "H")) "is" ($#v4_modelc_2 :::"conjunctive"::: ) ) "or" (Bool (Set (Var "H")) "is" ($#v5_modelc_2 :::"disjunctive"::: ) ) "or" (Bool (Set (Var "H")) "is" ($#v7_modelc_2 :::"Until"::: ) ) "or" (Bool (Set (Var "H")) "is" ($#v8_modelc_2 :::"Release"::: ) ) ")" ) & (Bool (Set (Var "H")) "is" ($#v5_modelc_3 :::"neg-inner-most"::: ) )) "holds" (Bool "(" (Bool (Set ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H"))) "is" ($#v5_modelc_3 :::"neg-inner-most"::: ) ) & (Bool (Set ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H"))) "is" ($#v5_modelc_3 :::"neg-inner-most"::: ) ) ")" )) ; begin definitionlet "W" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; attr "c2" is :::"strict"::: ; struct :::"BuchiAutomaton"::: "over" "W" -> ($#l1_struct_0 :::"1-sorted"::: ) ; aggr :::"BuchiAutomaton":::(# :::"carrier":::, :::"Tran":::, :::"InitS":::, :::"FinalS"::: #) -> ($#l2_modelc_3 :::"BuchiAutomaton"::: ) "over" "W"; sel :::"Tran"::: "c2" -> ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c2") "," "W" ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c2"); sel :::"InitS"::: "c2" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c2")); sel :::"FinalS"::: "c2" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c2") ")" ); end; definitionlet "W" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "B" be ($#l2_modelc_3 :::"BuchiAutomaton"::: ) "over" (Set (Const "W")); let "w" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Const "W"))); pred "w" :::"is-accepted-by"::: "B" means :: MODELC_3:def 39 (Bool "ex" (Set (Var "run")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "B") "st" (Bool "(" (Bool (Set (Set (Var "run")) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_hidden :::"in"::: ) (Set "the" ($#u5_modelc_3 :::"InitS"::: ) "of" "B")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "run")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set "(" ($#k27_modelc_2 :::"CastSeq"::: ) "(" "w" "," "W" ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" (Set (Var "run")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_modelc_3 :::"Tran"::: ) "of" "B")) & (Bool "(" "for" (Set (Var "FSet")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "FSet")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u6_modelc_3 :::"FinalS"::: ) "of" "B"))) "holds" (Bool "{" (Set (Var "k")) where k "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Set (Var "run")) ($#k3_funct_2 :::"."::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) (Set (Var "FSet"))) "}" "is" ($#v1_finset_1 :::"infinite"::: ) ($#m1_hidden :::"set"::: ) ) ")" ) ")" ) ")" ) ")" )); end; :: deftheorem defines :::"is-accepted-by"::: MODELC_3:def 39 : (Bool "for" (Set (Var "W")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#l2_modelc_3 :::"BuchiAutomaton"::: ) "over" (Set (Var "W")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "W"))) "holds" (Bool "(" (Bool (Set (Var "w")) ($#r9_modelc_3 :::"is-accepted-by"::: ) (Set (Var "B"))) "iff" (Bool "ex" (Set (Var "run")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "B"))) "st" (Bool "(" (Bool (Set (Set (Var "run")) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_hidden :::"in"::: ) (Set "the" ($#u5_modelc_3 :::"InitS"::: ) "of" (Set (Var "B")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "run")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set "(" ($#k27_modelc_2 :::"CastSeq"::: ) "(" (Set (Var "w")) "," (Set (Var "W")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" (Set (Var "run")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_modelc_3 :::"Tran"::: ) "of" (Set (Var "B")))) & (Bool "(" "for" (Set (Var "FSet")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "FSet")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u6_modelc_3 :::"FinalS"::: ) "of" (Set (Var "B"))))) "holds" (Bool "{" (Set (Var "k")) where k "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Set (Var "run")) ($#k3_funct_2 :::"."::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) (Set (Var "FSet"))) "}" "is" ($#v1_finset_1 :::"infinite"::: ) ($#m1_hidden :::"set"::: ) ) ")" ) ")" ) ")" ) ")" )) ")" )))); definitionlet "v" be ($#v5_modelc_3 :::"neg-inner-most"::: ) ($#m2_finseq_1 :::"LTL-formula":::); let "N" be ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Const "v")); func :::"atomic_LTL"::: "N" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) ) equals :: MODELC_3:def 40 "{" (Set (Var "x")) where x "is" ($#m2_finseq_1 :::"LTL-formula":::) : (Bool "(" (Bool (Set (Var "x")) "is" ($#v2_modelc_2 :::"atomic"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" "N")) ")" ) "}" ; func :::"Neg_atomic_LTL"::: "N" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) ) equals :: MODELC_3:def 41 "{" (Set (Var "x")) where x "is" ($#m2_finseq_1 :::"LTL-formula":::) : (Bool "(" (Bool (Set (Var "x")) "is" ($#v2_modelc_2 :::"atomic"::: ) ) & (Bool (Set ($#k3_modelc_2 :::"'not'"::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" "N")) ")" ) "}" ; end; :: deftheorem defines :::"atomic_LTL"::: MODELC_3:def 40 : (Bool "for" (Set (Var "v")) "being" ($#v5_modelc_3 :::"neg-inner-most"::: ) ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "N")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "holds" (Bool (Set ($#k27_modelc_3 :::"atomic_LTL"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m2_finseq_1 :::"LTL-formula":::) : (Bool "(" (Bool (Set (Var "x")) "is" ($#v2_modelc_2 :::"atomic"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set (Var "N")))) ")" ) "}" ))); :: deftheorem defines :::"Neg_atomic_LTL"::: MODELC_3:def 41 : (Bool "for" (Set (Var "v")) "being" ($#v5_modelc_3 :::"neg-inner-most"::: ) ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "N")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "holds" (Bool (Set ($#k28_modelc_3 :::"Neg_atomic_LTL"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m2_finseq_1 :::"LTL-formula":::) : (Bool "(" (Bool (Set (Var "x")) "is" ($#v2_modelc_2 :::"atomic"::: ) ) & (Bool (Set ($#k3_modelc_2 :::"'not'"::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set (Var "N")))) ")" ) "}" ))); definitionlet "v" be ($#v5_modelc_3 :::"neg-inner-most"::: ) ($#m2_finseq_1 :::"LTL-formula":::); let "N" be ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Const "v")); func :::"Label_"::: "N" -> ($#m1_hidden :::"set"::: ) equals :: MODELC_3:def 42 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k15_modelc_2 :::"atomic_LTL"::: ) ) : (Bool "(" (Bool (Set ($#k27_modelc_3 :::"atomic_LTL"::: ) "N") ($#r1_tarski :::"c="::: ) (Set (Var "x"))) & (Bool (Set ($#k28_modelc_3 :::"Neg_atomic_LTL"::: ) "N") ($#r1_xboole_0 :::"misses"::: ) (Set (Var "x"))) ")" ) "}" ; end; :: deftheorem defines :::"Label_"::: MODELC_3:def 42 : (Bool "for" (Set (Var "v")) "being" ($#v5_modelc_3 :::"neg-inner-most"::: ) ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "N")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "holds" (Bool (Set ($#k29_modelc_3 :::"Label_"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k15_modelc_2 :::"atomic_LTL"::: ) ) : (Bool "(" (Bool (Set ($#k27_modelc_3 :::"atomic_LTL"::: ) (Set (Var "N"))) ($#r1_tarski :::"c="::: ) (Set (Var "x"))) & (Bool (Set ($#k28_modelc_3 :::"Neg_atomic_LTL"::: ) (Set (Var "N"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "x"))) ")" ) "}" ))); definitionlet "v" be ($#v5_modelc_3 :::"neg-inner-most"::: ) ($#m2_finseq_1 :::"LTL-formula":::); func :::"Tran_LTL"::: "v" -> ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k23_modelc_3 :::"LTLStates"::: ) "v" ")" ) "," (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k23_modelc_3 :::"LTLStates"::: ) "v" ")" ) equals :: MODELC_3:def 43 "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "(" ($#k23_modelc_3 :::"LTLStates"::: ) "v" ")" ) "," (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) ) "," (Set "(" ($#k23_modelc_3 :::"LTLStates"::: ) "v" ")" ) ($#k3_zfmisc_1 :::":]"::: ) ) : (Bool "ex" (Set (Var "s")) "," (Set (Var "s1")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#v3_modelc_3 :::"elementary"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" "v"(Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "s")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "s1")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "s1")) ($#r6_modelc_3 :::"is_next_of"::: ) (Set (Var "s"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k29_modelc_3 :::"Label_"::: ) (Set (Var "s1")))) ")" ))) "}" ; func :::"InitS_LTL"::: "v" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k23_modelc_3 :::"LTLStates"::: ) "v" ")" )) equals :: MODELC_3:def 44 (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k11_modelc_3 :::"init"::: ) "v" ")" ) ($#k1_tarski :::"}"::: ) ); end; :: deftheorem defines :::"Tran_LTL"::: MODELC_3:def 43 : (Bool "for" (Set (Var "v")) "being" ($#v5_modelc_3 :::"neg-inner-most"::: ) ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool (Set ($#k30_modelc_3 :::"Tran_LTL"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "(" ($#k23_modelc_3 :::"LTLStates"::: ) (Set (Var "v")) ")" ) "," (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) ) "," (Set "(" ($#k23_modelc_3 :::"LTLStates"::: ) (Set (Var "v")) ")" ) ($#k3_zfmisc_1 :::":]"::: ) ) : (Bool "ex" (Set (Var "s")) "," (Set (Var "s1")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#v3_modelc_3 :::"elementary"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v"))(Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "s")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "s1")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "s1")) ($#r6_modelc_3 :::"is_next_of"::: ) (Set (Var "s"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k29_modelc_3 :::"Label_"::: ) (Set (Var "s1")))) ")" ))) "}" )); :: deftheorem defines :::"InitS_LTL"::: MODELC_3:def 44 : (Bool "for" (Set (Var "v")) "being" ($#v5_modelc_3 :::"neg-inner-most"::: ) ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool (Set ($#k31_modelc_3 :::"InitS_LTL"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k11_modelc_3 :::"init"::: ) (Set (Var "v")) ")" ) ($#k1_tarski :::"}"::: ) ))); definitionlet "v" be ($#v5_modelc_3 :::"neg-inner-most"::: ) ($#m2_finseq_1 :::"LTL-formula":::); let "F" be ($#m2_finseq_1 :::"LTL-formula":::); func :::"FinalS_LTL"::: "(" "F" "," "v" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k23_modelc_3 :::"LTLStates"::: ) "v" ")" )) equals :: MODELC_3:def 45 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k23_modelc_3 :::"LTLStates"::: ) "v") : (Bool "(" "not" (Bool "F" ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set (Var "x")) "," "v" ")" ")" ))) "or" (Bool (Set ($#k12_modelc_2 :::"the_right_argument_of"::: ) "F") ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set (Var "x")) "," "v" ")" ")" ))) ")" ) "}" ; end; :: deftheorem defines :::"FinalS_LTL"::: MODELC_3:def 45 : (Bool "for" (Set (Var "v")) "being" ($#v5_modelc_3 :::"neg-inner-most"::: ) ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool (Set ($#k32_modelc_3 :::"FinalS_LTL"::: ) "(" (Set (Var "F")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k23_modelc_3 :::"LTLStates"::: ) (Set (Var "v"))) : (Bool "(" "not" (Bool (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set (Var "x")) "," (Set (Var "v")) ")" ")" ))) "or" (Bool (Set ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "F"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set (Var "x")) "," (Set (Var "v")) ")" ")" ))) ")" ) "}" ))); definitionlet "v" be ($#v5_modelc_3 :::"neg-inner-most"::: ) ($#m2_finseq_1 :::"LTL-formula":::); func :::"FinalS_LTL"::: "v" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k23_modelc_3 :::"LTLStates"::: ) "v" ")" ) ")" ) equals :: MODELC_3:def 46 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k23_modelc_3 :::"LTLStates"::: ) "v" ")" )) : (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool "(" (Bool (Set (Var "F")) ($#r2_modelc_2 :::"is_subformula_of"::: ) "v") & (Bool (Set (Var "F")) "is" ($#v7_modelc_2 :::"Until"::: ) ) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k32_modelc_3 :::"FinalS_LTL"::: ) "(" (Set (Var "F")) "," "v" ")" )) ")" )) "}" ; end; :: deftheorem defines :::"FinalS_LTL"::: MODELC_3:def 46 : (Bool "for" (Set (Var "v")) "being" ($#v5_modelc_3 :::"neg-inner-most"::: ) ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool (Set ($#k33_modelc_3 :::"FinalS_LTL"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k23_modelc_3 :::"LTLStates"::: ) (Set (Var "v")) ")" )) : (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool "(" (Bool (Set (Var "F")) ($#r2_modelc_2 :::"is_subformula_of"::: ) (Set (Var "v"))) & (Bool (Set (Var "F")) "is" ($#v7_modelc_2 :::"Until"::: ) ) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k32_modelc_3 :::"FinalS_LTL"::: ) "(" (Set (Var "F")) "," (Set (Var "v")) ")" )) ")" )) "}" )); definitionlet "v" be ($#v5_modelc_3 :::"neg-inner-most"::: ) ($#m2_finseq_1 :::"LTL-formula":::); func :::"BAutomaton"::: "v" -> ($#l2_modelc_3 :::"BuchiAutomaton"::: ) "over" (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) ) equals :: MODELC_3:def 47 (Set ($#g2_modelc_3 :::"BuchiAutomaton"::: ) "(#" (Set "(" ($#k23_modelc_3 :::"LTLStates"::: ) "v" ")" ) "," (Set "(" ($#k30_modelc_3 :::"Tran_LTL"::: ) "v" ")" ) "," (Set "(" ($#k31_modelc_3 :::"InitS_LTL"::: ) "v" ")" ) "," (Set "(" ($#k33_modelc_3 :::"FinalS_LTL"::: ) "v" ")" ) "#)" ); end; :: deftheorem defines :::"BAutomaton"::: MODELC_3:def 47 : (Bool "for" (Set (Var "v")) "being" ($#v5_modelc_3 :::"neg-inner-most"::: ) ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool (Set ($#k34_modelc_3 :::"BAutomaton"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#g2_modelc_3 :::"BuchiAutomaton"::: ) "(#" (Set "(" ($#k23_modelc_3 :::"LTLStates"::: ) (Set (Var "v")) ")" ) "," (Set "(" ($#k30_modelc_3 :::"Tran_LTL"::: ) (Set (Var "v")) ")" ) "," (Set "(" ($#k31_modelc_3 :::"InitS_LTL"::: ) (Set (Var "v")) ")" ) "," (Set "(" ($#k33_modelc_3 :::"FinalS_LTL"::: ) (Set (Var "v")) ")" ) "#)" ))); theorem :: MODELC_3:68 (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) (Bool "for" (Set (Var "v")) "being" ($#v5_modelc_3 :::"neg-inner-most"::: ) ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "w")) ($#r9_modelc_3 :::"is-accepted-by"::: ) (Set ($#k34_modelc_3 :::"BAutomaton"::: ) (Set (Var "v"))))) "holds" (Bool (Set (Var "w")) ($#r7_modelc_2 :::"|="::: ) (Set (Var "v"))))) ; definitionlet "w" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )); let "v" be ($#v5_modelc_3 :::"neg-inner-most"::: ) ($#m2_finseq_1 :::"LTL-formula":::); let "U" be ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) (Set (Const "v")) ")" )); let "N" be ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Const "v")); assume that (Bool (Bool "not" (Set (Const "N")) "is" ($#v3_modelc_3 :::"elementary"::: ) )) and (Bool (Set (Const "w")) ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set (Const "N")))) ; func :::"chosen_succ_end_num"::: "(" "w" "," "v" "," "U" "," "N" ")" -> ($#m1_hidden :::"Nat":::) means :: MODELC_3:def 48 (Bool "(" (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) it)) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k26_modelc_3 :::"choice_succ_func"::: ) "(" "w" "," "v" "," "U" ")" ")" ) ($#k29_modelc_1 :::"|**"::: ) (Set (Var "i")) ")" ) ($#k1_funct_1 :::"."::: ) "N" ")" ) "," "v" ")" ) "is" ($#v3_modelc_3 :::"elementary"::: ) )) & (Bool (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k26_modelc_3 :::"choice_succ_func"::: ) "(" "w" "," "v" "," "U" ")" ")" ) ($#k29_modelc_1 :::"|**"::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) "N" ")" ) "," "v" ")" ) ($#r4_modelc_3 :::"is_succ_of"::: ) (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k26_modelc_3 :::"choice_succ_func"::: ) "(" "w" "," "v" "," "U" ")" ")" ) ($#k29_modelc_1 :::"|**"::: ) (Set (Var "i")) ")" ) ($#k1_funct_1 :::"."::: ) "N" ")" ) "," "v" ")" )) ")" ) ")" ) & (Bool (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k26_modelc_3 :::"choice_succ_func"::: ) "(" "w" "," "v" "," "U" ")" ")" ) ($#k29_modelc_1 :::"|**"::: ) it ")" ) ($#k1_funct_1 :::"."::: ) "N" ")" ) "," "v" ")" ) "is" ($#v3_modelc_3 :::"elementary"::: ) ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) it)) "holds" (Bool "w" ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k26_modelc_3 :::"choice_succ_func"::: ) "(" "w" "," "v" "," "U" ")" ")" ) ($#k29_modelc_1 :::"|**"::: ) (Set (Var "i")) ")" ) ($#k1_funct_1 :::"."::: ) "N" ")" ) "," "v" ")" ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"chosen_succ_end_num"::: MODELC_3:def 48 : (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) (Bool "for" (Set (Var "v")) "being" ($#v5_modelc_3 :::"neg-inner-most"::: ) ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "U")) "being" ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) (Set (Var "v")) ")" )) (Bool "for" (Set (Var "N")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "st" (Bool (Bool (Bool "not" (Set (Var "N")) "is" ($#v3_modelc_3 :::"elementary"::: ) )) & (Bool (Set (Var "w")) ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set (Var "N"))))) "holds" (Bool "for" (Set (Var "b5")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k35_modelc_3 :::"chosen_succ_end_num"::: ) "(" (Set (Var "w")) "," (Set (Var "v")) "," (Set (Var "U")) "," (Set (Var "N")) ")" )) "iff" (Bool "(" (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b5")))) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k26_modelc_3 :::"choice_succ_func"::: ) "(" (Set (Var "w")) "," (Set (Var "v")) "," (Set (Var "U")) ")" ")" ) ($#k29_modelc_1 :::"|**"::: ) (Set (Var "i")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "N")) ")" ) "," (Set (Var "v")) ")" ) "is" ($#v3_modelc_3 :::"elementary"::: ) )) & (Bool (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k26_modelc_3 :::"choice_succ_func"::: ) "(" (Set (Var "w")) "," (Set (Var "v")) "," (Set (Var "U")) ")" ")" ) ($#k29_modelc_1 :::"|**"::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "N")) ")" ) "," (Set (Var "v")) ")" ) ($#r4_modelc_3 :::"is_succ_of"::: ) (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k26_modelc_3 :::"choice_succ_func"::: ) "(" (Set (Var "w")) "," (Set (Var "v")) "," (Set (Var "U")) ")" ")" ) ($#k29_modelc_1 :::"|**"::: ) (Set (Var "i")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "N")) ")" ) "," (Set (Var "v")) ")" )) ")" ) ")" ) & (Bool (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k26_modelc_3 :::"choice_succ_func"::: ) "(" (Set (Var "w")) "," (Set (Var "v")) "," (Set (Var "U")) ")" ")" ) ($#k29_modelc_1 :::"|**"::: ) (Set (Var "b5")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "N")) ")" ) "," (Set (Var "v")) ")" ) "is" ($#v3_modelc_3 :::"elementary"::: ) ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b5")))) "holds" (Bool (Set (Var "w")) ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k26_modelc_3 :::"choice_succ_func"::: ) "(" (Set (Var "w")) "," (Set (Var "v")) "," (Set (Var "U")) ")" ")" ) ($#k29_modelc_1 :::"|**"::: ) (Set (Var "i")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "N")) ")" ) "," (Set (Var "v")) ")" ")" ))) ")" ) ")" ) ")" )))))); definitionlet "w" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )); let "v" be ($#v5_modelc_3 :::"neg-inner-most"::: ) ($#m2_finseq_1 :::"LTL-formula":::); let "U" be ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) (Set (Const "v")) ")" )); let "N" be ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Const "v")); assume (Bool (Set (Const "w")) ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set "(" ($#k12_modelc_3 :::"'X'"::: ) (Set (Const "N")) ")" ))) ; func :::"chosen_next"::: "(" "w" "," "v" "," "U" "," "N" ")" -> ($#v1_modelc_3 :::"strict"::: ) ($#v3_modelc_3 :::"elementary"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" "v" equals :: MODELC_3:def 49 (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k26_modelc_3 :::"choice_succ_func"::: ) "(" "w" "," "v" "," "U" ")" ")" ) ($#k29_modelc_1 :::"|**"::: ) (Set "(" ($#k35_modelc_3 :::"chosen_succ_end_num"::: ) "(" "w" "," "v" "," "U" "," (Set "(" ($#k12_modelc_3 :::"'X'"::: ) "N" ")" ) ")" ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k12_modelc_3 :::"'X'"::: ) "N" ")" ) ")" ) "," "v" ")" ) if (Bool (Bool "not" (Set ($#k12_modelc_3 :::"'X'"::: ) "N") "is" ($#v3_modelc_3 :::"elementary"::: ) )) otherwise (Set ($#k9_modelc_3 :::"FinalNode"::: ) "v"); end; :: deftheorem defines :::"chosen_next"::: MODELC_3:def 49 : (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) (Bool "for" (Set (Var "v")) "being" ($#v5_modelc_3 :::"neg-inner-most"::: ) ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "U")) "being" ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) (Set (Var "v")) ")" )) (Bool "for" (Set (Var "N")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "st" (Bool (Bool (Set (Var "w")) ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set "(" ($#k12_modelc_3 :::"'X'"::: ) (Set (Var "N")) ")" )))) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" (Set ($#k12_modelc_3 :::"'X'"::: ) (Set (Var "N"))) "is" ($#v3_modelc_3 :::"elementary"::: ) ))) "implies" (Bool (Set ($#k36_modelc_3 :::"chosen_next"::: ) "(" (Set (Var "w")) "," (Set (Var "v")) "," (Set (Var "U")) "," (Set (Var "N")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k26_modelc_3 :::"choice_succ_func"::: ) "(" (Set (Var "w")) "," (Set (Var "v")) "," (Set (Var "U")) ")" ")" ) ($#k29_modelc_1 :::"|**"::: ) (Set "(" ($#k35_modelc_3 :::"chosen_succ_end_num"::: ) "(" (Set (Var "w")) "," (Set (Var "v")) "," (Set (Var "U")) "," (Set "(" ($#k12_modelc_3 :::"'X'"::: ) (Set (Var "N")) ")" ) ")" ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k12_modelc_3 :::"'X'"::: ) (Set (Var "N")) ")" ) ")" ) "," (Set (Var "v")) ")" )) ")" & "(" (Bool (Bool (Set ($#k12_modelc_3 :::"'X'"::: ) (Set (Var "N"))) "is" ($#v3_modelc_3 :::"elementary"::: ) )) "implies" (Bool (Set ($#k36_modelc_3 :::"chosen_next"::: ) "(" (Set (Var "w")) "," (Set (Var "v")) "," (Set (Var "U")) "," (Set (Var "N")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_modelc_3 :::"FinalNode"::: ) (Set (Var "v")))) ")" ")" ))))); theorem :: MODELC_3:69 (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) (Bool "for" (Set (Var "v")) "being" ($#v5_modelc_3 :::"neg-inner-most"::: ) ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "U")) "being" ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) (Set (Var "v")) ")" )) (Bool "for" (Set (Var "s")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#v3_modelc_3 :::"elementary"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "st" (Bool (Bool (Set (Var "w")) ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set "(" ($#k12_modelc_3 :::"'X'"::: ) (Set (Var "s")) ")" )))) "holds" (Bool "(" (Bool (Set ($#k36_modelc_3 :::"chosen_next"::: ) "(" (Set (Var "w")) "," (Set (Var "v")) "," (Set (Var "U")) "," (Set (Var "s")) ")" ) ($#r6_modelc_3 :::"is_next_of"::: ) (Set (Var "s"))) & (Bool (Set (Var "w")) ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set "(" ($#k36_modelc_3 :::"chosen_next"::: ) "(" (Set (Var "w")) "," (Set (Var "v")) "," (Set (Var "U")) "," (Set (Var "s")) ")" ")" ))) ")" ))))) ; definitionlet "w" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )); let "v" be ($#v5_modelc_3 :::"neg-inner-most"::: ) ($#m2_finseq_1 :::"LTL-formula":::); let "U" be ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) (Set (Const "v")) ")" )); func :::"chosen_run"::: "(" "w" "," "v" "," "U" ")" -> ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k23_modelc_3 :::"LTLStates"::: ) "v" ")" ) means :: MODELC_3:def 50 (Bool "(" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k11_modelc_3 :::"init"::: ) "v")) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k36_modelc_3 :::"chosen_next"::: ) "(" (Set "(" ($#k29_modelc_2 :::"Shift"::: ) "(" "w" "," (Set (Var "n")) ")" ")" ) "," "v" "," "U" "," (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" it ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) "," "v" ")" ")" ) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"chosen_run"::: MODELC_3:def 50 : (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) (Bool "for" (Set (Var "v")) "being" ($#v5_modelc_3 :::"neg-inner-most"::: ) ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "U")) "being" ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) (Set (Var "v")) ")" )) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k23_modelc_3 :::"LTLStates"::: ) (Set (Var "v")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k37_modelc_3 :::"chosen_run"::: ) "(" (Set (Var "w")) "," (Set (Var "v")) "," (Set (Var "U")) ")" )) "iff" (Bool "(" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k11_modelc_3 :::"init"::: ) (Set (Var "v")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k36_modelc_3 :::"chosen_next"::: ) "(" (Set "(" ($#k29_modelc_2 :::"Shift"::: ) "(" (Set (Var "w")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "v")) "," (Set (Var "U")) "," (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set (Var "v")) ")" ")" ) ")" )) ")" ) ")" ) ")" ))))); theorem :: MODELC_3:70 (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) (Bool "for" (Set (Var "v")) "being" ($#v5_modelc_3 :::"neg-inner-most"::: ) ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "N")) "being" ($#v1_modelc_3 :::"strict"::: ) ($#l1_modelc_3 :::"LTLnode"::: ) "over" (Set (Var "v")) "st" (Bool (Bool (Set (Var "w")) ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set (Var "N"))))) "holds" (Bool (Set ($#k29_modelc_2 :::"Shift"::: ) "(" (Set (Var "w")) "," (Num 1) ")" ) ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set "(" ($#k12_modelc_3 :::"'X'"::: ) (Set (Var "N")) ")" )))))) ; theorem :: MODELC_3:71 (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) (Bool "for" (Set (Var "v")) "being" ($#v5_modelc_3 :::"neg-inner-most"::: ) ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "w")) ($#r7_modelc_2 :::"|="::: ) (Set ($#k6_modelc_2 :::"'X'"::: ) (Set (Var "v"))))) "holds" (Bool (Set (Var "w")) ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set "(" ($#k11_modelc_3 :::"init"::: ) (Set (Var "v")) ")" ))))) ; theorem :: MODELC_3:72 (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) (Bool "for" (Set (Var "v")) "being" ($#v5_modelc_3 :::"neg-inner-most"::: ) ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" (Bool (Set (Var "w")) ($#r7_modelc_2 :::"|="::: ) (Set (Var "v"))) "iff" (Bool (Set (Var "w")) ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set "(" ($#k12_modelc_3 :::"'X'"::: ) (Set "(" ($#k11_modelc_3 :::"init"::: ) (Set (Var "v")) ")" ) ")" ))) ")" ))) ; theorem :: MODELC_3:73 (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) (Bool "for" (Set (Var "v")) "being" ($#v5_modelc_3 :::"neg-inner-most"::: ) ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "U")) "being" ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) (Set (Var "v")) ")" )) "st" (Bool (Bool (Set (Var "w")) ($#r7_modelc_2 :::"|="::: ) (Set (Var "v")))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set "(" ($#k37_modelc_3 :::"chosen_run"::: ) "(" (Set (Var "w")) "," (Set (Var "v")) "," (Set (Var "U")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "v")) ")" ) ($#r6_modelc_3 :::"is_next_of"::: ) (Set ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set "(" ($#k37_modelc_3 :::"chosen_run"::: ) "(" (Set (Var "w")) "," (Set (Var "v")) "," (Set (Var "U")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set (Var "v")) ")" )) & (Bool (Set ($#k29_modelc_2 :::"Shift"::: ) "(" (Set (Var "w")) "," (Set (Var "n")) ")" ) ($#r8_modelc_2 :::"|="::: ) (Set ($#k14_modelc_3 :::"*"::: ) (Set "(" ($#k12_modelc_3 :::"'X'"::: ) (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set "(" ($#k37_modelc_3 :::"chosen_run"::: ) "(" (Set (Var "w")) "," (Set (Var "v")) "," (Set (Var "U")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set (Var "v")) ")" ")" ) ")" ))) ")" ))))) ; theorem :: MODELC_3:74 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) (Bool "for" (Set (Var "v")) "being" ($#v5_modelc_3 :::"neg-inner-most"::: ) ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "U")) "being" ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "(" ($#k1_modelc_3 :::"Subformulae"::: ) (Set (Var "v")) ")" )) "st" (Bool (Bool (Set (Var "w")) ($#r7_modelc_2 :::"|="::: ) (Set (Var "v")))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set "(" ($#k37_modelc_3 :::"chosen_run"::: ) "(" (Set (Var "w")) "," (Set (Var "v")) "," (Set (Var "U")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "v")) ")" ")" ))) & (Bool (Set (Var "H")) "is" ($#v7_modelc_2 :::"Until"::: ) ) & (Bool (Set ($#k29_modelc_2 :::"Shift"::: ) "(" (Set (Var "w")) "," (Set (Var "i")) ")" ) ($#r7_modelc_2 :::"|="::: ) (Set ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H"))))) "holds" (Bool (Set ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_modelc_3 :::"LTLold"::: ) "of" (Set "(" ($#k10_modelc_3 :::"CastNode"::: ) "(" (Set "(" (Set "(" ($#k37_modelc_3 :::"chosen_run"::: ) "(" (Set (Var "w")) "," (Set (Var "v")) "," (Set (Var "U")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "v")) ")" ")" )))))))) ; theorem :: MODELC_3:75 (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) (Bool "for" (Set (Var "v")) "being" ($#v5_modelc_3 :::"neg-inner-most"::: ) ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "w")) ($#r7_modelc_2 :::"|="::: ) (Set (Var "v")))) "holds" (Bool (Set (Var "w")) ($#r9_modelc_3 :::"is-accepted-by"::: ) (Set ($#k34_modelc_3 :::"BAutomaton"::: ) (Set (Var "v")))))) ; theorem :: MODELC_3:76 (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) (Bool "for" (Set (Var "v")) "being" ($#v5_modelc_3 :::"neg-inner-most"::: ) ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" (Bool (Set (Var "w")) ($#r9_modelc_3 :::"is-accepted-by"::: ) (Set ($#k34_modelc_3 :::"BAutomaton"::: ) (Set (Var "v")))) "iff" (Bool (Set (Var "w")) ($#r7_modelc_2 :::"|="::: ) (Set (Var "v"))) ")" ))) ;