:: MODELC_2 semantic presentation begin definitionlet "x" be ($#m1_hidden :::"set"::: ) ; func :::"CastNat"::: "x" -> ($#m1_hidden :::"Nat":::) equals :: MODELC_2:def 1 "x" if (Bool "x" "is" ($#m1_hidden :::"Nat":::)) otherwise (Set ($#k6_numbers :::"0"::: ) ); end; :: deftheorem defines :::"CastNat"::: MODELC_2:def 1 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) "is" ($#m1_hidden :::"Nat":::))) "implies" (Bool (Set ($#k1_modelc_2 :::"CastNat"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" & "(" (Bool (Bool (Set (Var "x")) "is" (Bool "not" ($#m1_hidden :::"Nat":::)))) "implies" (Bool (Set ($#k1_modelc_2 :::"CastNat"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" )); definitionlet "n" be ($#m1_hidden :::"Nat":::); func :::"atom."::: "n" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: MODELC_2:def 2 (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Num 6) ($#k2_nat_1 :::"+"::: ) "n" ")" ) ($#k12_finseq_1 :::"*>"::: ) ); end; :: deftheorem defines :::"atom."::: MODELC_2:def 2 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k2_modelc_2 :::"atom."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Num 6) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ))); definitionlet "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"'not'"::: "p" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: MODELC_2:def 3 (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) "p"); let "q" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func "p" :::"'&'"::: "q" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: MODELC_2:def 4 (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) "p" ")" ) ($#k8_finseq_1 :::"^"::: ) "q"); func "p" :::"'or'"::: "q" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: MODELC_2:def 5 (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 2) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) "p" ")" ) ($#k8_finseq_1 :::"^"::: ) "q"); end; :: deftheorem defines :::"'not'"::: MODELC_2:def 3 : (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_modelc_2 :::"'not'"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "p"))))); :: deftheorem defines :::"'&'"::: MODELC_2:def 4 : (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k4_modelc_2 :::"'&'"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "q"))))); :: deftheorem defines :::"'or'"::: MODELC_2:def 5 : (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k5_modelc_2 :::"'or'"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 2) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "q"))))); definitionlet "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"'X'"::: "p" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: MODELC_2:def 6 (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Num 3) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) "p"); let "q" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func "p" :::"'U'"::: "q" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: MODELC_2:def 7 (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 4) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) "p" ")" ) ($#k8_finseq_1 :::"^"::: ) "q"); func "p" :::"'R'"::: "q" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: MODELC_2:def 8 (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 5) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) "p" ")" ) ($#k8_finseq_1 :::"^"::: ) "q"); end; :: deftheorem defines :::"'X'"::: MODELC_2:def 6 : (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k6_modelc_2 :::"'X'"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Num 3) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "p"))))); :: deftheorem defines :::"'U'"::: MODELC_2:def 7 : (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k7_modelc_2 :::"'U'"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 4) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "q"))))); :: deftheorem defines :::"'R'"::: MODELC_2:def 8 : (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k8_modelc_2 :::"'R'"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 5) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "q"))))); definitionfunc :::"LTL_WFF"::: -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) means :: MODELC_2:def 9 (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool (Set (Var "a")) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )) ")" ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k2_modelc_2 :::"atom."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) it) ")" ) & (Bool "(" "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool (Set ($#k3_modelc_2 :::"'not'"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) it) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) it) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool (Set (Set (Var "p")) ($#k4_modelc_2 :::"'&'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) it) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) it) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool (Set (Set (Var "p")) ($#k5_modelc_2 :::"'or'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) it) ")" ) & (Bool "(" "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool (Set ($#k6_modelc_2 :::"'X'"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) it) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) it) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool (Set (Set (Var "p")) ($#k7_modelc_2 :::"'U'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) it) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) it) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool (Set (Set (Var "p")) ($#k8_modelc_2 :::"'R'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) it) ")" ) & (Bool "(" "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Var "a")) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )) ")" ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k2_modelc_2 :::"atom."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" ) & (Bool "(" "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set ($#k3_modelc_2 :::"'not'"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set (Var "p")) ($#k4_modelc_2 :::"'&'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set (Var "p")) ($#k5_modelc_2 :::"'or'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" ) & (Bool "(" "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set ($#k6_modelc_2 :::"'X'"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set (Var "p")) ($#k7_modelc_2 :::"'U'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set (Var "p")) ($#k8_modelc_2 :::"'R'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" )) "holds" (Bool it ($#r1_tarski :::"c="::: ) (Set (Var "D"))) ")" ) ")" ); end; :: deftheorem defines :::"LTL_WFF"::: MODELC_2:def 9 : (Bool "for" (Set (Var "b1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) )) "iff" (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b1")))) "holds" (Bool (Set (Var "a")) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )) ")" ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k2_modelc_2 :::"atom."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) ")" ) & (Bool "(" "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "b1")))) "holds" (Bool (Set ($#k3_modelc_2 :::"'not'"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "b1")))) "holds" (Bool (Set (Set (Var "p")) ($#k4_modelc_2 :::"'&'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "b1")))) "holds" (Bool (Set (Set (Var "p")) ($#k5_modelc_2 :::"'or'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) ")" ) & (Bool "(" "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "b1")))) "holds" (Bool (Set ($#k6_modelc_2 :::"'X'"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "b1")))) "holds" (Bool (Set (Set (Var "p")) ($#k7_modelc_2 :::"'U'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "b1")))) "holds" (Bool (Set (Set (Var "p")) ($#k8_modelc_2 :::"'R'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) ")" ) & (Bool "(" "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Var "a")) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )) ")" ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k2_modelc_2 :::"atom."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" ) & (Bool "(" "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set ($#k3_modelc_2 :::"'not'"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set (Var "p")) ($#k4_modelc_2 :::"'&'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set (Var "p")) ($#k5_modelc_2 :::"'or'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" ) & (Bool "(" "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set ($#k6_modelc_2 :::"'X'"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set (Var "p")) ($#k7_modelc_2 :::"'U'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set (Var "p")) ($#k8_modelc_2 :::"'R'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" )) "holds" (Bool (Set (Var "b1")) ($#r1_tarski :::"c="::: ) (Set (Var "D"))) ")" ) ")" ) ")" )); definitionlet "IT" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); attr "IT" is :::"LTL-formula-like"::: means :: MODELC_2:def 10 (Bool "IT" "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) )); end; :: deftheorem defines :::"LTL-formula-like"::: MODELC_2:def 10 : (Bool "for" (Set (Var "IT")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_modelc_2 :::"LTL-formula-like"::: ) ) "iff" (Bool (Set (Var "IT")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) )) ")" )); 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"::: ) bbbadV1_FINSET_1() ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v1_modelc_2 :::"LTL-formula-like"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; definitionmode LTL-formula is ($#v1_modelc_2 :::"LTL-formula-like"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; theorem :: MODELC_2:1 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#m2_finseq_1 :::"LTL-formula":::)) "iff" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) )) ")" )) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k2_modelc_2 :::"atom."::: ) "n") -> ($#v1_modelc_2 :::"LTL-formula-like"::: ) ; end; registrationlet "H" be ($#m2_finseq_1 :::"LTL-formula":::); cluster (Set ($#k3_modelc_2 :::"'not'"::: ) "H") -> ($#v1_modelc_2 :::"LTL-formula-like"::: ) ; cluster (Set ($#k6_modelc_2 :::"'X'"::: ) "H") -> ($#v1_modelc_2 :::"LTL-formula-like"::: ) ; let "G" be ($#m2_finseq_1 :::"LTL-formula":::); cluster (Set "H" ($#k4_modelc_2 :::"'&'"::: ) "G") -> ($#v1_modelc_2 :::"LTL-formula-like"::: ) ; cluster (Set "H" ($#k5_modelc_2 :::"'or'"::: ) "G") -> ($#v1_modelc_2 :::"LTL-formula-like"::: ) ; cluster (Set "H" ($#k7_modelc_2 :::"'U'"::: ) "G") -> ($#v1_modelc_2 :::"LTL-formula-like"::: ) ; cluster (Set "H" ($#k8_modelc_2 :::"'R'"::: ) "G") -> ($#v1_modelc_2 :::"LTL-formula-like"::: ) ; end; definitionlet "H" be ($#m2_finseq_1 :::"LTL-formula":::); attr "H" is :::"atomic"::: means :: MODELC_2:def 11 (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "H" ($#r1_hidden :::"="::: ) (Set ($#k2_modelc_2 :::"atom."::: ) (Set (Var "n"))))); attr "H" is :::"negative"::: means :: MODELC_2:def 12 (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool "H" ($#r1_hidden :::"="::: ) (Set ($#k3_modelc_2 :::"'not'"::: ) (Set (Var "H1"))))); attr "H" is :::"conjunctive"::: means :: MODELC_2:def 13 (Bool "ex" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool "H" ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k4_modelc_2 :::"'&'"::: ) (Set (Var "G"))))); attr "H" is :::"disjunctive"::: means :: MODELC_2:def 14 (Bool "ex" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool "H" ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_modelc_2 :::"'or'"::: ) (Set (Var "G"))))); attr "H" is :::"next"::: means :: MODELC_2:def 15 (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool "H" ($#r1_hidden :::"="::: ) (Set ($#k6_modelc_2 :::"'X'"::: ) (Set (Var "H1"))))); attr "H" is :::"Until"::: means :: MODELC_2:def 16 (Bool "ex" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool "H" ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_modelc_2 :::"'U'"::: ) (Set (Var "G"))))); attr "H" is :::"Release"::: means :: MODELC_2:def 17 (Bool "ex" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool "H" ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k8_modelc_2 :::"'R'"::: ) (Set (Var "G"))))); end; :: deftheorem defines :::"atomic"::: MODELC_2:def 11 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v2_modelc_2 :::"atomic"::: ) ) "iff" (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k2_modelc_2 :::"atom."::: ) (Set (Var "n"))))) ")" )); :: deftheorem defines :::"negative"::: MODELC_2:def 12 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v3_modelc_2 :::"negative"::: ) ) "iff" (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k3_modelc_2 :::"'not'"::: ) (Set (Var "H1"))))) ")" )); :: deftheorem defines :::"conjunctive"::: MODELC_2:def 13 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v4_modelc_2 :::"conjunctive"::: ) ) "iff" (Bool "ex" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k4_modelc_2 :::"'&'"::: ) (Set (Var "G"))))) ")" )); :: deftheorem defines :::"disjunctive"::: MODELC_2:def 14 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v5_modelc_2 :::"disjunctive"::: ) ) "iff" (Bool "ex" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_modelc_2 :::"'or'"::: ) (Set (Var "G"))))) ")" )); :: deftheorem defines :::"next"::: MODELC_2:def 15 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v6_modelc_2 :::"next"::: ) ) "iff" (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k6_modelc_2 :::"'X'"::: ) (Set (Var "H1"))))) ")" )); :: deftheorem defines :::"Until"::: MODELC_2:def 16 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v7_modelc_2 :::"Until"::: ) ) "iff" (Bool "ex" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_modelc_2 :::"'U'"::: ) (Set (Var "G"))))) ")" )); :: deftheorem defines :::"Release"::: MODELC_2:def 17 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v8_modelc_2 :::"Release"::: ) ) "iff" (Bool "ex" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k8_modelc_2 :::"'R'"::: ) (Set (Var "G"))))) ")" )); theorem :: MODELC_2:2 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (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" ($#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_2:3 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H"))))) ; definitionlet "H" be ($#m2_finseq_1 :::"LTL-formula":::); assume (Bool "(" (Bool (Set (Const "H")) "is" ($#v3_modelc_2 :::"negative"::: ) ) "or" (Bool (Set (Const "H")) "is" ($#v6_modelc_2 :::"next"::: ) ) ")" ) ; func :::"the_argument_of"::: "H" -> ($#m2_finseq_1 :::"LTL-formula":::) means :: MODELC_2:def 18 (Bool (Set ($#k3_modelc_2 :::"'not'"::: ) it) ($#r1_hidden :::"="::: ) "H") if (Bool "H" "is" ($#v3_modelc_2 :::"negative"::: ) ) otherwise (Bool (Set ($#k6_modelc_2 :::"'X'"::: ) it) ($#r1_hidden :::"="::: ) "H"); end; :: deftheorem defines :::"the_argument_of"::: MODELC_2:def 18 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool "(" (Bool (Set (Var "H")) "is" ($#v3_modelc_2 :::"negative"::: ) ) "or" (Bool (Set (Var "H")) "is" ($#v6_modelc_2 :::"next"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "H")) "is" ($#v3_modelc_2 :::"negative"::: ) )) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k10_modelc_2 :::"the_argument_of"::: ) (Set (Var "H")))) "iff" (Bool (Set ($#k3_modelc_2 :::"'not'"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Var "H"))) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "H")) "is" ($#v3_modelc_2 :::"negative"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k10_modelc_2 :::"the_argument_of"::: ) (Set (Var "H")))) "iff" (Bool (Set ($#k6_modelc_2 :::"'X'"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Var "H"))) ")" ) ")" ")" ))); definitionlet "H" be ($#m2_finseq_1 :::"LTL-formula":::); assume (Bool "(" (Bool (Set (Const "H")) "is" ($#v4_modelc_2 :::"conjunctive"::: ) ) "or" (Bool (Set (Const "H")) "is" ($#v5_modelc_2 :::"disjunctive"::: ) ) "or" (Bool (Set (Const "H")) "is" ($#v7_modelc_2 :::"Until"::: ) ) "or" (Bool (Set (Const "H")) "is" ($#v8_modelc_2 :::"Release"::: ) ) ")" ) ; func :::"the_left_argument_of"::: "H" -> ($#m2_finseq_1 :::"LTL-formula":::) means :: MODELC_2:def 19 (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Set it ($#k4_modelc_2 :::"'&'"::: ) (Set (Var "H1"))) ($#r1_hidden :::"="::: ) "H")) if (Bool "H" "is" ($#v4_modelc_2 :::"conjunctive"::: ) ) (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Set it ($#k5_modelc_2 :::"'or'"::: ) (Set (Var "H1"))) ($#r1_hidden :::"="::: ) "H")) if (Bool "H" "is" ($#v5_modelc_2 :::"disjunctive"::: ) ) (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Set it ($#k7_modelc_2 :::"'U'"::: ) (Set (Var "H1"))) ($#r1_hidden :::"="::: ) "H")) if (Bool "H" "is" ($#v7_modelc_2 :::"Until"::: ) ) otherwise (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Set it ($#k8_modelc_2 :::"'R'"::: ) (Set (Var "H1"))) ($#r1_hidden :::"="::: ) "H")); func :::"the_right_argument_of"::: "H" -> ($#m2_finseq_1 :::"LTL-formula":::) means :: MODELC_2:def 20 (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Set (Set (Var "H1")) ($#k4_modelc_2 :::"'&'"::: ) it) ($#r1_hidden :::"="::: ) "H")) if (Bool "H" "is" ($#v4_modelc_2 :::"conjunctive"::: ) ) (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Set (Set (Var "H1")) ($#k5_modelc_2 :::"'or'"::: ) it) ($#r1_hidden :::"="::: ) "H")) if (Bool "H" "is" ($#v5_modelc_2 :::"disjunctive"::: ) ) (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Set (Set (Var "H1")) ($#k7_modelc_2 :::"'U'"::: ) it) ($#r1_hidden :::"="::: ) "H")) if (Bool "H" "is" ($#v7_modelc_2 :::"Until"::: ) ) otherwise (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Set (Set (Var "H1")) ($#k8_modelc_2 :::"'R'"::: ) it) ($#r1_hidden :::"="::: ) "H")); end; :: deftheorem defines :::"the_left_argument_of"::: MODELC_2:def 19 : (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"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "H")) "is" ($#v4_modelc_2 :::"conjunctive"::: ) )) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H")))) "iff" (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Set (Set (Var "b2")) ($#k4_modelc_2 :::"'&'"::: ) (Set (Var "H1"))) ($#r1_hidden :::"="::: ) (Set (Var "H")))) ")" ) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v5_modelc_2 :::"disjunctive"::: ) )) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H")))) "iff" (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Set (Set (Var "b2")) ($#k5_modelc_2 :::"'or'"::: ) (Set (Var "H1"))) ($#r1_hidden :::"="::: ) (Set (Var "H")))) ")" ) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v7_modelc_2 :::"Until"::: ) )) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H")))) "iff" (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Set (Set (Var "b2")) ($#k7_modelc_2 :::"'U'"::: ) (Set (Var "H1"))) ($#r1_hidden :::"="::: ) (Set (Var "H")))) ")" ) ")" & "(" (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" ($#v7_modelc_2 :::"Until"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H")))) "iff" (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Set (Set (Var "b2")) ($#k8_modelc_2 :::"'R'"::: ) (Set (Var "H1"))) ($#r1_hidden :::"="::: ) (Set (Var "H")))) ")" ) ")" ")" ))); :: deftheorem defines :::"the_right_argument_of"::: MODELC_2:def 20 : (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"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "H")) "is" ($#v4_modelc_2 :::"conjunctive"::: ) )) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")))) "iff" (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Set (Set (Var "H1")) ($#k4_modelc_2 :::"'&'"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Var "H")))) ")" ) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v5_modelc_2 :::"disjunctive"::: ) )) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")))) "iff" (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Set (Set (Var "H1")) ($#k5_modelc_2 :::"'or'"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Var "H")))) ")" ) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v7_modelc_2 :::"Until"::: ) )) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")))) "iff" (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Set (Set (Var "H1")) ($#k7_modelc_2 :::"'U'"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Var "H")))) ")" ) ")" & "(" (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" ($#v7_modelc_2 :::"Until"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")))) "iff" (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Set (Set (Var "H1")) ($#k8_modelc_2 :::"'R'"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Var "H")))) ")" ) ")" ")" ))); theorem :: MODELC_2:4 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v3_modelc_2 :::"negative"::: ) )) "holds" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k3_modelc_2 :::"'not'"::: ) (Set "(" ($#k10_modelc_2 :::"the_argument_of"::: ) (Set (Var "H")) ")" )))) ; theorem :: MODELC_2:5 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v6_modelc_2 :::"next"::: ) )) "holds" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k6_modelc_2 :::"'X'"::: ) (Set "(" ($#k10_modelc_2 :::"the_argument_of"::: ) (Set (Var "H")) ")" )))) ; theorem :: MODELC_2:6 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v4_modelc_2 :::"conjunctive"::: ) )) "holds" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) ($#k4_modelc_2 :::"'&'"::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")) ")" )))) ; theorem :: MODELC_2:7 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v5_modelc_2 :::"disjunctive"::: ) )) "holds" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) ($#k5_modelc_2 :::"'or'"::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")) ")" )))) ; theorem :: MODELC_2:8 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v7_modelc_2 :::"Until"::: ) )) "holds" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) ($#k7_modelc_2 :::"'U'"::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")) ")" )))) ; theorem :: MODELC_2:9 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v8_modelc_2 :::"Release"::: ) )) "holds" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) ($#k8_modelc_2 :::"'R'"::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")) ")" )))) ; theorem :: MODELC_2:10 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool "(" (Bool (Set (Var "H")) "is" ($#v3_modelc_2 :::"negative"::: ) ) "or" (Bool (Set (Var "H")) "is" ($#v6_modelc_2 :::"next"::: ) ) ")" )) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k10_modelc_2 :::"the_argument_of"::: ) (Set (Var "H")) ")" ) ")" ))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k10_modelc_2 :::"the_argument_of"::: ) (Set (Var "H")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H")))) ")" )) ; theorem :: MODELC_2:11 (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"::: ) ) ")" )) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")) ")" ) ")" ))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H")))) ")" )) ; definitionlet "H", "F" be ($#m2_finseq_1 :::"LTL-formula":::); pred "H" :::"is_immediate_constituent_of"::: "F" means :: MODELC_2:def 21 (Bool "(" (Bool "F" ($#r1_hidden :::"="::: ) (Set ($#k3_modelc_2 :::"'not'"::: ) "H")) "or" (Bool "F" ($#r1_hidden :::"="::: ) (Set ($#k6_modelc_2 :::"'X'"::: ) "H")) "or" (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool "(" (Bool "F" ($#r1_hidden :::"="::: ) (Set "H" ($#k4_modelc_2 :::"'&'"::: ) (Set (Var "H1")))) "or" (Bool "F" ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k4_modelc_2 :::"'&'"::: ) "H")) "or" (Bool "F" ($#r1_hidden :::"="::: ) (Set "H" ($#k5_modelc_2 :::"'or'"::: ) (Set (Var "H1")))) "or" (Bool "F" ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k5_modelc_2 :::"'or'"::: ) "H")) "or" (Bool "F" ($#r1_hidden :::"="::: ) (Set "H" ($#k7_modelc_2 :::"'U'"::: ) (Set (Var "H1")))) "or" (Bool "F" ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k7_modelc_2 :::"'U'"::: ) "H")) "or" (Bool "F" ($#r1_hidden :::"="::: ) (Set "H" ($#k8_modelc_2 :::"'R'"::: ) (Set (Var "H1")))) "or" (Bool "F" ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k8_modelc_2 :::"'R'"::: ) "H")) ")" )) ")" ); end; :: deftheorem defines :::"is_immediate_constituent_of"::: MODELC_2:def 21 : (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r1_modelc_2 :::"is_immediate_constituent_of"::: ) (Set (Var "F"))) "iff" (Bool "(" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k3_modelc_2 :::"'not'"::: ) (Set (Var "H")))) "or" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k6_modelc_2 :::"'X'"::: ) (Set (Var "H")))) "or" (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool "(" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k4_modelc_2 :::"'&'"::: ) (Set (Var "H1")))) "or" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k4_modelc_2 :::"'&'"::: ) (Set (Var "H")))) "or" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k5_modelc_2 :::"'or'"::: ) (Set (Var "H1")))) "or" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k5_modelc_2 :::"'or'"::: ) (Set (Var "H")))) "or" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k7_modelc_2 :::"'U'"::: ) (Set (Var "H1")))) "or" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k7_modelc_2 :::"'U'"::: ) (Set (Var "H")))) "or" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k8_modelc_2 :::"'R'"::: ) (Set (Var "H1")))) "or" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k8_modelc_2 :::"'R'"::: ) (Set (Var "H")))) ")" )) ")" ) ")" )); theorem :: MODELC_2:12 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k3_modelc_2 :::"'not'"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set (Var "F")) ($#k4_modelc_2 :::"'&'"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set "(" (Set (Var "F")) ($#k5_modelc_2 :::"'or'"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Num 2)) & (Bool (Set (Set "(" ($#k6_modelc_2 :::"'X'"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Num 3)) & (Bool (Set (Set "(" (Set (Var "F")) ($#k7_modelc_2 :::"'U'"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Num 4)) & (Bool (Set (Set "(" (Set (Var "F")) ($#k8_modelc_2 :::"'R'"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Num 5)) ")" )) ; theorem :: MODELC_2:13 (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r1_modelc_2 :::"is_immediate_constituent_of"::: ) (Set ($#k3_modelc_2 :::"'not'"::: ) (Set (Var "F")))) "iff" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Var "F"))) ")" )) ; theorem :: MODELC_2:14 (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r1_modelc_2 :::"is_immediate_constituent_of"::: ) (Set ($#k6_modelc_2 :::"'X'"::: ) (Set (Var "F")))) "iff" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Var "F"))) ")" )) ; theorem :: MODELC_2:15 (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r1_modelc_2 :::"is_immediate_constituent_of"::: ) (Set (Set (Var "F")) ($#k4_modelc_2 :::"'&'"::: ) (Set (Var "G")))) "iff" (Bool "(" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Var "F"))) "or" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Var "G"))) ")" ) ")" )) ; theorem :: MODELC_2:16 (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r1_modelc_2 :::"is_immediate_constituent_of"::: ) (Set (Set (Var "F")) ($#k5_modelc_2 :::"'or'"::: ) (Set (Var "G")))) "iff" (Bool "(" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Var "F"))) "or" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Var "G"))) ")" ) ")" )) ; theorem :: MODELC_2:17 (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r1_modelc_2 :::"is_immediate_constituent_of"::: ) (Set (Set (Var "F")) ($#k7_modelc_2 :::"'U'"::: ) (Set (Var "G")))) "iff" (Bool "(" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Var "F"))) "or" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Var "G"))) ")" ) ")" )) ; theorem :: MODELC_2:18 (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r1_modelc_2 :::"is_immediate_constituent_of"::: ) (Set (Set (Var "F")) ($#k8_modelc_2 :::"'R'"::: ) (Set (Var "G")))) "iff" (Bool "(" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Var "F"))) "or" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Var "G"))) ")" ) ")" )) ; theorem :: MODELC_2:19 (Bool "for" (Set (Var "F")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_modelc_2 :::"atomic"::: ) )) "holds" (Bool "not" (Bool (Set (Var "H")) ($#r1_modelc_2 :::"is_immediate_constituent_of"::: ) (Set (Var "F"))))) ; theorem :: MODELC_2:20 (Bool "for" (Set (Var "F")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "F")) "is" ($#v3_modelc_2 :::"negative"::: ) )) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r1_modelc_2 :::"is_immediate_constituent_of"::: ) (Set (Var "F"))) "iff" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k10_modelc_2 :::"the_argument_of"::: ) (Set (Var "F")))) ")" )) ; theorem :: MODELC_2:21 (Bool "for" (Set (Var "F")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "F")) "is" ($#v6_modelc_2 :::"next"::: ) )) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r1_modelc_2 :::"is_immediate_constituent_of"::: ) (Set (Var "F"))) "iff" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k10_modelc_2 :::"the_argument_of"::: ) (Set (Var "F")))) ")" )) ; theorem :: MODELC_2:22 (Bool "for" (Set (Var "F")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "F")) "is" ($#v4_modelc_2 :::"conjunctive"::: ) )) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r1_modelc_2 :::"is_immediate_constituent_of"::: ) (Set (Var "F"))) "iff" (Bool "(" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "F")))) "or" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "F")))) ")" ) ")" )) ; theorem :: MODELC_2:23 (Bool "for" (Set (Var "F")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "F")) "is" ($#v5_modelc_2 :::"disjunctive"::: ) )) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r1_modelc_2 :::"is_immediate_constituent_of"::: ) (Set (Var "F"))) "iff" (Bool "(" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "F")))) "or" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "F")))) ")" ) ")" )) ; theorem :: MODELC_2:24 (Bool "for" (Set (Var "F")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "F")) "is" ($#v7_modelc_2 :::"Until"::: ) )) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r1_modelc_2 :::"is_immediate_constituent_of"::: ) (Set (Var "F"))) "iff" (Bool "(" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "F")))) "or" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "F")))) ")" ) ")" )) ; theorem :: MODELC_2:25 (Bool "for" (Set (Var "F")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "F")) "is" ($#v8_modelc_2 :::"Release"::: ) )) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r1_modelc_2 :::"is_immediate_constituent_of"::: ) (Set (Var "F"))) "iff" (Bool "(" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "F")))) "or" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "F")))) ")" ) ")" )) ; theorem :: MODELC_2:26 (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" "not" (Bool (Set (Var "H")) ($#r1_modelc_2 :::"is_immediate_constituent_of"::: ) (Set (Var "F"))) "or" (Bool (Set (Var "F")) "is" ($#v3_modelc_2 :::"negative"::: ) ) "or" (Bool (Set (Var "F")) "is" ($#v6_modelc_2 :::"next"::: ) ) "or" (Bool (Set (Var "F")) "is" ($#v4_modelc_2 :::"conjunctive"::: ) ) "or" (Bool (Set (Var "F")) "is" ($#v5_modelc_2 :::"disjunctive"::: ) ) "or" (Bool (Set (Var "F")) "is" ($#v7_modelc_2 :::"Until"::: ) ) "or" (Bool (Set (Var "F")) "is" ($#v8_modelc_2 :::"Release"::: ) ) ")" )) ; definitionlet "H", "F" be ($#m2_finseq_1 :::"LTL-formula":::); pred "H" :::"is_subformula_of"::: "F" means :: MODELC_2:def 22 (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::)(Bool "ex" (Set (Var "L")) "being" ($#m1_hidden :::"FinSequence":::) "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 :::"="::: ) "H") & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) "F") & (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 (Var "n")))) "holds" (Bool "ex" (Set (Var "H1")) "," (Set (Var "F1")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool "(" (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Var "H1"))) & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "F1"))) & (Bool (Set (Var "H1")) ($#r1_modelc_2 :::"is_immediate_constituent_of"::: ) (Set (Var "F1"))) ")" )) ")" ) ")" ))); reflexivity (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::)(Bool "ex" (Set (Var "L")) "being" ($#m1_hidden :::"FinSequence":::) "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 "H"))) & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "H"))) & (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 (Var "n")))) "holds" (Bool "ex" (Set (Var "H1")) "," (Set (Var "F1")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool "(" (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Var "H1"))) & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "F1"))) & (Bool (Set (Var "H1")) ($#r1_modelc_2 :::"is_immediate_constituent_of"::: ) (Set (Var "F1"))) ")" )) ")" ) ")" )))) ; end; :: deftheorem defines :::"is_subformula_of"::: MODELC_2:def 22 : (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r2_modelc_2 :::"is_subformula_of"::: ) (Set (Var "F"))) "iff" (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::)(Bool "ex" (Set (Var "L")) "being" ($#m1_hidden :::"FinSequence":::) "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 "H"))) & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "F"))) & (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 (Var "n")))) "holds" (Bool "ex" (Set (Var "H1")) "," (Set (Var "F1")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool "(" (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Var "H1"))) & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "F1"))) & (Bool (Set (Var "H1")) ($#r1_modelc_2 :::"is_immediate_constituent_of"::: ) (Set (Var "F1"))) ")" )) ")" ) ")" ))) ")" )); theorem :: MODELC_2:27 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool (Set (Var "H")) ($#r2_modelc_2 :::"is_subformula_of"::: ) (Set (Var "H")))) ; definitionlet "H", "F" be ($#m2_finseq_1 :::"LTL-formula":::); pred "H" :::"is_proper_subformula_of"::: "F" means :: MODELC_2:def 23 (Bool "(" (Bool "H" ($#r2_modelc_2 :::"is_subformula_of"::: ) "F") & (Bool "H" ($#r1_hidden :::"<>"::: ) "F") ")" ); irreflexivity (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" "not" (Bool (Set (Var "H")) ($#r2_modelc_2 :::"is_subformula_of"::: ) (Set (Var "H"))) "or" "not" (Bool (Set (Var "H")) ($#r1_hidden :::"<>"::: ) (Set (Var "H"))) ")" )) ; end; :: deftheorem defines :::"is_proper_subformula_of"::: MODELC_2:def 23 : (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r3_modelc_2 :::"is_proper_subformula_of"::: ) (Set (Var "F"))) "iff" (Bool "(" (Bool (Set (Var "H")) ($#r2_modelc_2 :::"is_subformula_of"::: ) (Set (Var "F"))) & (Bool (Set (Var "H")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) ")" ) ")" )); theorem :: MODELC_2:28 (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "H")) ($#r1_modelc_2 :::"is_immediate_constituent_of"::: ) (Set (Var "F")))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))))) ; theorem :: MODELC_2:29 (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "H")) ($#r1_modelc_2 :::"is_immediate_constituent_of"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "H")) ($#r3_modelc_2 :::"is_proper_subformula_of"::: ) (Set (Var "F")))) ; theorem :: MODELC_2:30 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool "(" (Bool (Set (Var "G")) "is" ($#v3_modelc_2 :::"negative"::: ) ) "or" (Bool (Set (Var "G")) "is" ($#v6_modelc_2 :::"next"::: ) ) ")" )) "holds" (Bool (Set ($#k10_modelc_2 :::"the_argument_of"::: ) (Set (Var "G"))) ($#r2_modelc_2 :::"is_subformula_of"::: ) (Set (Var "G")))) ; theorem :: MODELC_2:31 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool "(" (Bool (Set (Var "G")) "is" ($#v4_modelc_2 :::"conjunctive"::: ) ) "or" (Bool (Set (Var "G")) "is" ($#v5_modelc_2 :::"disjunctive"::: ) ) "or" (Bool (Set (Var "G")) "is" ($#v7_modelc_2 :::"Until"::: ) ) "or" (Bool (Set (Var "G")) "is" ($#v8_modelc_2 :::"Release"::: ) ) ")" )) "holds" (Bool "(" (Bool (Set ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "G"))) ($#r2_modelc_2 :::"is_subformula_of"::: ) (Set (Var "G"))) & (Bool (Set ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "G"))) ($#r2_modelc_2 :::"is_subformula_of"::: ) (Set (Var "G"))) ")" )) ; theorem :: MODELC_2:32 (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "H")) ($#r3_modelc_2 :::"is_proper_subformula_of"::: ) (Set (Var "F")))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))))) ; theorem :: MODELC_2:33 (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "H")) ($#r3_modelc_2 :::"is_proper_subformula_of"::: ) (Set (Var "F")))) "holds" (Bool "ex" (Set (Var "G")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Set (Var "G")) ($#r1_modelc_2 :::"is_immediate_constituent_of"::: ) (Set (Var "F"))))) ; theorem :: MODELC_2:34 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "F")) ($#r3_modelc_2 :::"is_proper_subformula_of"::: ) (Set (Var "G"))) & (Bool (Set (Var "G")) ($#r3_modelc_2 :::"is_proper_subformula_of"::: ) (Set (Var "H")))) "holds" (Bool (Set (Var "F")) ($#r3_modelc_2 :::"is_proper_subformula_of"::: ) (Set (Var "H")))) ; theorem :: MODELC_2:35 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "F")) ($#r2_modelc_2 :::"is_subformula_of"::: ) (Set (Var "G"))) & (Bool (Set (Var "G")) ($#r2_modelc_2 :::"is_subformula_of"::: ) (Set (Var "H")))) "holds" (Bool (Set (Var "F")) ($#r2_modelc_2 :::"is_subformula_of"::: ) (Set (Var "H")))) ; theorem :: MODELC_2:36 (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "G")) ($#r2_modelc_2 :::"is_subformula_of"::: ) (Set (Var "H"))) & (Bool (Set (Var "H")) ($#r2_modelc_2 :::"is_subformula_of"::: ) (Set (Var "G")))) "holds" (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Var "H")))) ; theorem :: MODELC_2:37 (Bool "for" (Set (Var "G")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool "(" (Bool (Set (Var "G")) "is" ($#v3_modelc_2 :::"negative"::: ) ) "or" (Bool (Set (Var "G")) "is" ($#v6_modelc_2 :::"next"::: ) ) ")" ) & (Bool (Set (Var "F")) ($#r3_modelc_2 :::"is_proper_subformula_of"::: ) (Set (Var "G")))) "holds" (Bool (Set (Var "F")) ($#r2_modelc_2 :::"is_subformula_of"::: ) (Set ($#k10_modelc_2 :::"the_argument_of"::: ) (Set (Var "G"))))) ; theorem :: MODELC_2:38 (Bool "for" (Set (Var "G")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool "(" (Bool (Set (Var "G")) "is" ($#v4_modelc_2 :::"conjunctive"::: ) ) "or" (Bool (Set (Var "G")) "is" ($#v5_modelc_2 :::"disjunctive"::: ) ) "or" (Bool (Set (Var "G")) "is" ($#v7_modelc_2 :::"Until"::: ) ) "or" (Bool (Set (Var "G")) "is" ($#v8_modelc_2 :::"Release"::: ) ) ")" ) & (Bool (Set (Var "F")) ($#r3_modelc_2 :::"is_proper_subformula_of"::: ) (Set (Var "G"))) & (Bool (Bool "not" (Set (Var "F")) ($#r2_modelc_2 :::"is_subformula_of"::: ) (Set ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "G")))))) "holds" (Bool (Set (Var "F")) ($#r2_modelc_2 :::"is_subformula_of"::: ) (Set ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "G"))))) ; theorem :: MODELC_2:39 (Bool "for" (Set (Var "F")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "F")) ($#r3_modelc_2 :::"is_proper_subformula_of"::: ) (Set ($#k3_modelc_2 :::"'not'"::: ) (Set (Var "H"))))) "holds" (Bool (Set (Var "F")) ($#r2_modelc_2 :::"is_subformula_of"::: ) (Set (Var "H")))) ; theorem :: MODELC_2:40 (Bool "for" (Set (Var "F")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "F")) ($#r3_modelc_2 :::"is_proper_subformula_of"::: ) (Set ($#k6_modelc_2 :::"'X'"::: ) (Set (Var "H"))))) "holds" (Bool (Set (Var "F")) ($#r2_modelc_2 :::"is_subformula_of"::: ) (Set (Var "H")))) ; theorem :: MODELC_2:41 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" "not" (Bool (Set (Var "F")) ($#r3_modelc_2 :::"is_proper_subformula_of"::: ) (Set (Set (Var "G")) ($#k4_modelc_2 :::"'&'"::: ) (Set (Var "H")))) "or" (Bool (Set (Var "F")) ($#r2_modelc_2 :::"is_subformula_of"::: ) (Set (Var "G"))) "or" (Bool (Set (Var "F")) ($#r2_modelc_2 :::"is_subformula_of"::: ) (Set (Var "H"))) ")" )) ; theorem :: MODELC_2:42 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" "not" (Bool (Set (Var "F")) ($#r3_modelc_2 :::"is_proper_subformula_of"::: ) (Set (Set (Var "G")) ($#k5_modelc_2 :::"'or'"::: ) (Set (Var "H")))) "or" (Bool (Set (Var "F")) ($#r2_modelc_2 :::"is_subformula_of"::: ) (Set (Var "G"))) "or" (Bool (Set (Var "F")) ($#r2_modelc_2 :::"is_subformula_of"::: ) (Set (Var "H"))) ")" )) ; theorem :: MODELC_2:43 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" "not" (Bool (Set (Var "F")) ($#r3_modelc_2 :::"is_proper_subformula_of"::: ) (Set (Set (Var "G")) ($#k7_modelc_2 :::"'U'"::: ) (Set (Var "H")))) "or" (Bool (Set (Var "F")) ($#r2_modelc_2 :::"is_subformula_of"::: ) (Set (Var "G"))) "or" (Bool (Set (Var "F")) ($#r2_modelc_2 :::"is_subformula_of"::: ) (Set (Var "H"))) ")" )) ; theorem :: MODELC_2:44 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" "not" (Bool (Set (Var "F")) ($#r3_modelc_2 :::"is_proper_subformula_of"::: ) (Set (Set (Var "G")) ($#k8_modelc_2 :::"'R'"::: ) (Set (Var "H")))) "or" (Bool (Set (Var "F")) ($#r2_modelc_2 :::"is_subformula_of"::: ) (Set (Var "G"))) "or" (Bool (Set (Var "F")) ($#r2_modelc_2 :::"is_subformula_of"::: ) (Set (Var "H"))) ")" )) ; definitionlet "H" be ($#m2_finseq_1 :::"LTL-formula":::); func :::"Subformulae"::: "H" -> ($#m1_hidden :::"set"::: ) means :: MODELC_2:def 24 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool "(" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "F")) ($#r2_modelc_2 :::"is_subformula_of"::: ) "H") ")" )) ")" )); end; :: deftheorem defines :::"Subformulae"::: MODELC_2:def 24 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k13_modelc_2 :::"Subformulae"::: ) (Set (Var "H")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool "(" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "F")) ($#r2_modelc_2 :::"is_subformula_of"::: ) (Set (Var "H"))) ")" )) ")" )) ")" ))); theorem :: MODELC_2:45 (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" (Bool (Set (Var "G")) ($#r2_hidden :::"in"::: ) (Set ($#k13_modelc_2 :::"Subformulae"::: ) (Set (Var "H")))) "iff" (Bool (Set (Var "G")) ($#r2_modelc_2 :::"is_subformula_of"::: ) (Set (Var "H"))) ")" )) ; registrationlet "H" be ($#m2_finseq_1 :::"LTL-formula":::); cluster (Set ($#k13_modelc_2 :::"Subformulae"::: ) "H") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: MODELC_2:46 (Bool "for" (Set (Var "F")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "F")) ($#r2_modelc_2 :::"is_subformula_of"::: ) (Set (Var "H")))) "holds" (Bool (Set ($#k13_modelc_2 :::"Subformulae"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set ($#k13_modelc_2 :::"Subformulae"::: ) (Set (Var "H"))))) ; theorem :: MODELC_2:47 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "a")) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k13_modelc_2 :::"Subformulae"::: ) (Set (Var "H")) ")" ))) "holds" (Bool (Set (Var "a")) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) )))) ; scheme :: MODELC_2:sch 1 LTLInd{ P1[ ($#m2_finseq_1 :::"LTL-formula":::)] } : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool P1[(Set (Var "H"))])) provided (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v2_modelc_2 :::"atomic"::: ) )) "holds" (Bool P1[(Set (Var "H"))])) and (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool "(" (Bool (Set (Var "H")) "is" ($#v3_modelc_2 :::"negative"::: ) ) "or" (Bool (Set (Var "H")) "is" ($#v6_modelc_2 :::"next"::: ) ) ")" ) & (Bool P1[(Set ($#k10_modelc_2 :::"the_argument_of"::: ) (Set (Var "H")))])) "holds" (Bool P1[(Set (Var "H"))])) and (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 P1[(Set ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H")))]) & (Bool P1[(Set ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")))])) "holds" (Bool P1[(Set (Var "H"))])) proof end; scheme :: MODELC_2:sch 2 LTLCompInd{ P1[ ($#m2_finseq_1 :::"LTL-formula":::)] } : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool P1[(Set (Var "H"))])) provided (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool "(" "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "F")) ($#r3_modelc_2 :::"is_proper_subformula_of"::: ) (Set (Var "H")))) "holds" (Bool P1[(Set (Var "F"))]) ")" )) "holds" (Bool P1[(Set (Var "H"))])) proof end; definitionlet "x" be ($#m1_hidden :::"set"::: ) ; func :::"CastLTL"::: "x" -> ($#m2_finseq_1 :::"LTL-formula":::) equals :: MODELC_2:def 25 "x" if (Bool "x" ($#r2_hidden :::"in"::: ) (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) )) otherwise (Set ($#k2_modelc_2 :::"atom."::: ) (Set ($#k6_numbers :::"0"::: ) )); end; :: deftheorem defines :::"CastLTL"::: MODELC_2:def 25 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) ))) "implies" (Bool (Set ($#k14_modelc_2 :::"CastLTL"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) )))) "implies" (Bool (Set ($#k14_modelc_2 :::"CastLTL"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_modelc_2 :::"atom."::: ) (Set ($#k6_numbers :::"0"::: ) ))) ")" ")" )); definitionattr "c1" is :::"strict"::: ; struct :::"LTLModelStr"::: -> ($#l4_robbins1 :::"OrthoLattStr"::: ) ; aggr :::"LTLModelStr":::(# :::"carrier":::, :::"BasicAssign":::, :::"L_meet":::, :::"L_join":::, :::"Compl":::, :::"NEXT":::, :::"UNTIL":::, :::"RELEASE"::: #) -> ($#l1_modelc_2 :::"LTLModelStr"::: ) ; sel :::"BasicAssign"::: "c1" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1"); sel :::"NEXT"::: "c1" -> ($#m1_subset_1 :::"UnOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1"); sel :::"UNTIL"::: "c1" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1"); sel :::"RELEASE"::: "c1" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1"); end; definitionlet "V" be ($#l1_modelc_2 :::"LTLModelStr"::: ) ; mode Assign of "V" is ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V"); end; definitionfunc :::"atomic_LTL"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) ) equals :: MODELC_2:def 26 "{" (Set (Var "x")) where x "is" ($#m2_finseq_1 :::"LTL-formula":::) : (Bool (Set (Var "x")) "is" ($#v2_modelc_2 :::"atomic"::: ) ) "}" ; end; :: deftheorem defines :::"atomic_LTL"::: MODELC_2:def 26 : (Bool (Set ($#k15_modelc_2 :::"atomic_LTL"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m2_finseq_1 :::"LTL-formula":::) : (Bool (Set (Var "x")) "is" ($#v2_modelc_2 :::"atomic"::: ) ) "}" ); definitionlet "V" be ($#l1_modelc_2 :::"LTLModelStr"::: ) ; let "Kai" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k15_modelc_2 :::"atomic_LTL"::: ) ) "," (Set "the" ($#u1_modelc_2 :::"BasicAssign"::: ) "of" (Set (Const "V"))); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "V"))); pred "f" :::"is-Evaluation-for"::: "Kai" means :: MODELC_2:def 27 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "H")) "is" ($#v2_modelc_2 :::"atomic"::: ) )) "implies" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set "Kai" ($#k1_funct_1 :::"."::: ) (Set (Var "H")))) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v3_modelc_2 :::"negative"::: ) )) "implies" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" "V") ($#k1_funct_1 :::"."::: ) (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_modelc_2 :::"the_argument_of"::: ) (Set (Var "H")) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v4_modelc_2 :::"conjunctive"::: ) )) "implies" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" "V") ($#k1_binop_1 :::"."::: ) "(" (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) "," (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v5_modelc_2 :::"disjunctive"::: ) )) "implies" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_lattices :::"L_join"::: ) "of" "V") ($#k1_binop_1 :::"."::: ) "(" (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) "," (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v6_modelc_2 :::"next"::: ) )) "implies" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_modelc_2 :::"NEXT"::: ) "of" "V") ($#k1_funct_1 :::"."::: ) (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_modelc_2 :::"the_argument_of"::: ) (Set (Var "H")) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v7_modelc_2 :::"Until"::: ) )) "implies" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_modelc_2 :::"UNTIL"::: ) "of" "V") ($#k1_binop_1 :::"."::: ) "(" (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) "," (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v8_modelc_2 :::"Release"::: ) )) "implies" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u4_modelc_2 :::"RELEASE"::: ) "of" "V") ($#k1_binop_1 :::"."::: ) "(" (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) "," (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) ")" )) ")" ")" )); end; :: deftheorem defines :::"is-Evaluation-for"::: MODELC_2:def 27 : (Bool "for" (Set (Var "V")) "being" ($#l1_modelc_2 :::"LTLModelStr"::: ) (Bool "for" (Set (Var "Kai")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k15_modelc_2 :::"atomic_LTL"::: ) ) "," (Set "the" ($#u1_modelc_2 :::"BasicAssign"::: ) "of" (Set (Var "V"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r4_modelc_2 :::"is-Evaluation-for"::: ) (Set (Var "Kai"))) "iff" (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "H")) "is" ($#v2_modelc_2 :::"atomic"::: ) )) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "Kai")) ($#k1_funct_1 :::"."::: ) (Set (Var "H")))) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v3_modelc_2 :::"negative"::: ) )) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" (Set (Var "V"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_modelc_2 :::"the_argument_of"::: ) (Set (Var "H")) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v4_modelc_2 :::"conjunctive"::: ) )) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "V"))) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v5_modelc_2 :::"disjunctive"::: ) )) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "V"))) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v6_modelc_2 :::"next"::: ) )) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_modelc_2 :::"NEXT"::: ) "of" (Set (Var "V"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_modelc_2 :::"the_argument_of"::: ) (Set (Var "H")) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v7_modelc_2 :::"Until"::: ) )) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_modelc_2 :::"UNTIL"::: ) "of" (Set (Var "V"))) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v8_modelc_2 :::"Release"::: ) )) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u4_modelc_2 :::"RELEASE"::: ) "of" (Set (Var "V"))) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) ")" )) ")" ")" )) ")" )))); definitionlet "V" be ($#l1_modelc_2 :::"LTLModelStr"::: ) ; let "Kai" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k15_modelc_2 :::"atomic_LTL"::: ) ) "," (Set "the" ($#u1_modelc_2 :::"BasicAssign"::: ) "of" (Set (Const "V"))); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "V"))); let "n" be ($#m1_hidden :::"Nat":::); pred "f" :::"is-PreEvaluation-for"::: "n" "," "Kai" means :: MODELC_2:def 28 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H"))) ($#r1_xxreal_0 :::"<="::: ) "n")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "H")) "is" ($#v2_modelc_2 :::"atomic"::: ) )) "implies" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set "Kai" ($#k1_funct_1 :::"."::: ) (Set (Var "H")))) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v3_modelc_2 :::"negative"::: ) )) "implies" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" "V") ($#k1_funct_1 :::"."::: ) (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_modelc_2 :::"the_argument_of"::: ) (Set (Var "H")) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v4_modelc_2 :::"conjunctive"::: ) )) "implies" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" "V") ($#k1_binop_1 :::"."::: ) "(" (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) "," (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v5_modelc_2 :::"disjunctive"::: ) )) "implies" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_lattices :::"L_join"::: ) "of" "V") ($#k1_binop_1 :::"."::: ) "(" (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) "," (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v6_modelc_2 :::"next"::: ) )) "implies" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_modelc_2 :::"NEXT"::: ) "of" "V") ($#k1_funct_1 :::"."::: ) (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_modelc_2 :::"the_argument_of"::: ) (Set (Var "H")) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v7_modelc_2 :::"Until"::: ) )) "implies" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_modelc_2 :::"UNTIL"::: ) "of" "V") ($#k1_binop_1 :::"."::: ) "(" (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) "," (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v8_modelc_2 :::"Release"::: ) )) "implies" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u4_modelc_2 :::"RELEASE"::: ) "of" "V") ($#k1_binop_1 :::"."::: ) "(" (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) "," (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) ")" )) ")" ")" )); end; :: deftheorem defines :::"is-PreEvaluation-for"::: MODELC_2:def 28 : (Bool "for" (Set (Var "V")) "being" ($#l1_modelc_2 :::"LTLModelStr"::: ) (Bool "for" (Set (Var "Kai")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k15_modelc_2 :::"atomic_LTL"::: ) ) "," (Set "the" ($#u1_modelc_2 :::"BasicAssign"::: ) "of" (Set (Var "V"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r5_modelc_2 :::"is-PreEvaluation-for"::: ) (Set (Var "n")) "," (Set (Var "Kai"))) "iff" (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "H")) "is" ($#v2_modelc_2 :::"atomic"::: ) )) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "Kai")) ($#k1_funct_1 :::"."::: ) (Set (Var "H")))) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v3_modelc_2 :::"negative"::: ) )) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" (Set (Var "V"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_modelc_2 :::"the_argument_of"::: ) (Set (Var "H")) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v4_modelc_2 :::"conjunctive"::: ) )) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "V"))) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v5_modelc_2 :::"disjunctive"::: ) )) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "V"))) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v6_modelc_2 :::"next"::: ) )) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_modelc_2 :::"NEXT"::: ) "of" (Set (Var "V"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_modelc_2 :::"the_argument_of"::: ) (Set (Var "H")) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v7_modelc_2 :::"Until"::: ) )) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_modelc_2 :::"UNTIL"::: ) "of" (Set (Var "V"))) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v8_modelc_2 :::"Release"::: ) )) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u4_modelc_2 :::"RELEASE"::: ) "of" (Set (Var "V"))) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) ")" )) ")" ")" )) ")" ))))); definitionlet "V" be ($#l1_modelc_2 :::"LTLModelStr"::: ) ; let "Kai" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k15_modelc_2 :::"atomic_LTL"::: ) ) "," (Set "the" ($#u1_modelc_2 :::"BasicAssign"::: ) "of" (Set (Const "V"))); let "f", "h" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "V"))); let "n" be ($#m1_hidden :::"Nat":::); let "H" be ($#m2_finseq_1 :::"LTL-formula":::); func :::"GraftEval"::: "(" "V" "," "Kai" "," "f" "," "h" "," "n" "," "H" ")" -> ($#m1_hidden :::"set"::: ) equals :: MODELC_2:def 29 (Set "f" ($#k1_funct_1 :::"."::: ) "H") if (Bool (Set ($#k3_finseq_1 :::"len"::: ) "H") ($#r1_xxreal_0 :::">"::: ) (Set "n" ($#k1_nat_1 :::"+"::: ) (Num 1))) (Set "Kai" ($#k1_funct_1 :::"."::: ) "H") if (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) "H") ($#r1_hidden :::"="::: ) (Set "n" ($#k1_nat_1 :::"+"::: ) (Num 1))) & (Bool "H" "is" ($#v2_modelc_2 :::"atomic"::: ) ) ")" ) (Set (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" "V") ($#k1_funct_1 :::"."::: ) (Set "(" "h" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_modelc_2 :::"the_argument_of"::: ) "H" ")" ) ")" )) if (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) "H") ($#r1_hidden :::"="::: ) (Set "n" ($#k1_nat_1 :::"+"::: ) (Num 1))) & (Bool "H" "is" ($#v3_modelc_2 :::"negative"::: ) ) ")" ) (Set (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" "V") ($#k1_binop_1 :::"."::: ) "(" (Set "(" "h" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) "H" ")" ) ")" ) "," (Set "(" "h" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) "H" ")" ) ")" ) ")" ) if (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) "H") ($#r1_hidden :::"="::: ) (Set "n" ($#k1_nat_1 :::"+"::: ) (Num 1))) & (Bool "H" "is" ($#v4_modelc_2 :::"conjunctive"::: ) ) ")" ) (Set (Set "the" ($#u2_lattices :::"L_join"::: ) "of" "V") ($#k1_binop_1 :::"."::: ) "(" (Set "(" "h" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) "H" ")" ) ")" ) "," (Set "(" "h" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) "H" ")" ) ")" ) ")" ) if (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) "H") ($#r1_hidden :::"="::: ) (Set "n" ($#k1_nat_1 :::"+"::: ) (Num 1))) & (Bool "H" "is" ($#v5_modelc_2 :::"disjunctive"::: ) ) ")" ) (Set (Set "the" ($#u2_modelc_2 :::"NEXT"::: ) "of" "V") ($#k1_funct_1 :::"."::: ) (Set "(" "h" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_modelc_2 :::"the_argument_of"::: ) "H" ")" ) ")" )) if (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) "H") ($#r1_hidden :::"="::: ) (Set "n" ($#k1_nat_1 :::"+"::: ) (Num 1))) & (Bool "H" "is" ($#v6_modelc_2 :::"next"::: ) ) ")" ) (Set (Set "the" ($#u3_modelc_2 :::"UNTIL"::: ) "of" "V") ($#k1_binop_1 :::"."::: ) "(" (Set "(" "h" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) "H" ")" ) ")" ) "," (Set "(" "h" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) "H" ")" ) ")" ) ")" ) if (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) "H") ($#r1_hidden :::"="::: ) (Set "n" ($#k1_nat_1 :::"+"::: ) (Num 1))) & (Bool "H" "is" ($#v7_modelc_2 :::"Until"::: ) ) ")" ) (Set (Set "the" ($#u4_modelc_2 :::"RELEASE"::: ) "of" "V") ($#k1_binop_1 :::"."::: ) "(" (Set "(" "h" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) "H" ")" ) ")" ) "," (Set "(" "h" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) "H" ")" ) ")" ) ")" ) if (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) "H") ($#r1_hidden :::"="::: ) (Set "n" ($#k1_nat_1 :::"+"::: ) (Num 1))) & (Bool "H" "is" ($#v8_modelc_2 :::"Release"::: ) ) ")" ) (Set "h" ($#k1_funct_1 :::"."::: ) "H") if (Bool (Set ($#k3_finseq_1 :::"len"::: ) "H") ($#r1_xxreal_0 :::"<"::: ) (Set "n" ($#k1_nat_1 :::"+"::: ) (Num 1))) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); end; :: deftheorem defines :::"GraftEval"::: MODELC_2:def 29 : (Bool "for" (Set (Var "V")) "being" ($#l1_modelc_2 :::"LTLModelStr"::: ) (Bool "for" (Set (Var "Kai")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k15_modelc_2 :::"atomic_LTL"::: ) ) "," (Set "the" ($#u1_modelc_2 :::"BasicAssign"::: ) "of" (Set (Var "V"))) (Bool "for" (Set (Var "f")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H"))) ($#r1_xxreal_0 :::">"::: ) (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1)))) "implies" (Bool (Set ($#k16_modelc_2 :::"GraftEval"::: ) "(" (Set (Var "V")) "," (Set (Var "Kai")) "," (Set (Var "f")) "," (Set (Var "h")) "," (Set (Var "n")) "," (Set (Var "H")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "H")))) ")" & "(" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "H")) "is" ($#v2_modelc_2 :::"atomic"::: ) )) "implies" (Bool (Set ($#k16_modelc_2 :::"GraftEval"::: ) "(" (Set (Var "V")) "," (Set (Var "Kai")) "," (Set (Var "f")) "," (Set (Var "h")) "," (Set (Var "n")) "," (Set (Var "H")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "Kai")) ($#k1_funct_1 :::"."::: ) (Set (Var "H")))) ")" & "(" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "H")) "is" ($#v3_modelc_2 :::"negative"::: ) )) "implies" (Bool (Set ($#k16_modelc_2 :::"GraftEval"::: ) "(" (Set (Var "V")) "," (Set (Var "Kai")) "," (Set (Var "f")) "," (Set (Var "h")) "," (Set (Var "n")) "," (Set (Var "H")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" (Set (Var "V"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_modelc_2 :::"the_argument_of"::: ) (Set (Var "H")) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "H")) "is" ($#v4_modelc_2 :::"conjunctive"::: ) )) "implies" (Bool (Set ($#k16_modelc_2 :::"GraftEval"::: ) "(" (Set (Var "V")) "," (Set (Var "Kai")) "," (Set (Var "f")) "," (Set (Var "h")) "," (Set (Var "n")) "," (Set (Var "H")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "V"))) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "H")) "is" ($#v5_modelc_2 :::"disjunctive"::: ) )) "implies" (Bool (Set ($#k16_modelc_2 :::"GraftEval"::: ) "(" (Set (Var "V")) "," (Set (Var "Kai")) "," (Set (Var "f")) "," (Set (Var "h")) "," (Set (Var "n")) "," (Set (Var "H")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "V"))) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "H")) "is" ($#v6_modelc_2 :::"next"::: ) )) "implies" (Bool (Set ($#k16_modelc_2 :::"GraftEval"::: ) "(" (Set (Var "V")) "," (Set (Var "Kai")) "," (Set (Var "f")) "," (Set (Var "h")) "," (Set (Var "n")) "," (Set (Var "H")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_modelc_2 :::"NEXT"::: ) "of" (Set (Var "V"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_modelc_2 :::"the_argument_of"::: ) (Set (Var "H")) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "H")) "is" ($#v7_modelc_2 :::"Until"::: ) )) "implies" (Bool (Set ($#k16_modelc_2 :::"GraftEval"::: ) "(" (Set (Var "V")) "," (Set (Var "Kai")) "," (Set (Var "f")) "," (Set (Var "h")) "," (Set (Var "n")) "," (Set (Var "H")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_modelc_2 :::"UNTIL"::: ) "of" (Set (Var "V"))) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "H")) "is" ($#v8_modelc_2 :::"Release"::: ) )) "implies" (Bool (Set ($#k16_modelc_2 :::"GraftEval"::: ) "(" (Set (Var "V")) "," (Set (Var "Kai")) "," (Set (Var "f")) "," (Set (Var "h")) "," (Set (Var "n")) "," (Set (Var "H")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u4_modelc_2 :::"RELEASE"::: ) "of" (Set (Var "V"))) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k11_modelc_2 :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k12_modelc_2 :::"the_right_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1)))) "implies" (Bool (Set ($#k16_modelc_2 :::"GraftEval"::: ) "(" (Set (Var "V")) "," (Set (Var "Kai")) "," (Set (Var "f")) "," (Set (Var "h")) "," (Set (Var "n")) "," (Set (Var "H")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "H")))) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H"))) ($#r1_xxreal_0 :::">"::: ) (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1)))) & (Bool "(" "not" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1))) "or" "not" (Bool (Set (Var "H")) "is" ($#v2_modelc_2 :::"atomic"::: ) ) ")" ) & (Bool "(" "not" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1))) "or" "not" (Bool (Set (Var "H")) "is" ($#v3_modelc_2 :::"negative"::: ) ) ")" ) & (Bool "(" "not" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1))) "or" "not" (Bool (Set (Var "H")) "is" ($#v4_modelc_2 :::"conjunctive"::: ) ) ")" ) & (Bool "(" "not" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1))) "or" "not" (Bool (Set (Var "H")) "is" ($#v5_modelc_2 :::"disjunctive"::: ) ) ")" ) & (Bool "(" "not" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1))) "or" "not" (Bool (Set (Var "H")) "is" ($#v6_modelc_2 :::"next"::: ) ) ")" ) & (Bool "(" "not" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1))) "or" "not" (Bool (Set (Var "H")) "is" ($#v7_modelc_2 :::"Until"::: ) ) ")" ) & (Bool "(" "not" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1))) "or" "not" (Bool (Set (Var "H")) "is" ($#v8_modelc_2 :::"Release"::: ) ) ")" ) & (Bool (Bool "not" (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1))))) "implies" (Bool (Set ($#k16_modelc_2 :::"GraftEval"::: ) "(" (Set (Var "V")) "," (Set (Var "Kai")) "," (Set (Var "f")) "," (Set (Var "h")) "," (Set (Var "n")) "," (Set (Var "H")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" )))))); definitionlet "C" be ($#l1_modelc_2 :::"LTLModelStr"::: ) ; attr "C" is :::"with_basic"::: means :: MODELC_2:def 30 (Bool (Bool "not" (Set "the" ($#u1_modelc_2 :::"BasicAssign"::: ) "of" "C") "is" ($#v1_xboole_0 :::"empty"::: ) )); end; :: deftheorem defines :::"with_basic"::: MODELC_2:def 30 : (Bool "for" (Set (Var "C")) "being" ($#l1_modelc_2 :::"LTLModelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "C")) "is" ($#v10_modelc_2 :::"with_basic"::: ) ) "iff" (Bool (Bool "not" (Set "the" ($#u1_modelc_2 :::"BasicAssign"::: ) "of" (Set (Var "C"))) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" )); definitionfunc :::"TrivialLTLModel"::: -> ($#l1_modelc_2 :::"LTLModelStr"::: ) equals :: MODELC_2:def 31 (Set ($#g1_modelc_2 :::"LTLModelStr"::: ) "(#" (Num 1) "," (Set "(" ($#k2_subset_1 :::"[#]"::: ) (Num 1) ")" ) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k8_funct_5 :::"op1"::: ) ) "," (Set ($#k8_funct_5 :::"op1"::: ) ) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "#)" ); end; :: deftheorem defines :::"TrivialLTLModel"::: MODELC_2:def 31 : (Bool (Set ($#k17_modelc_2 :::"TrivialLTLModel"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_modelc_2 :::"LTLModelStr"::: ) "(#" (Num 1) "," (Set "(" ($#k2_subset_1 :::"[#]"::: ) (Num 1) ")" ) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k8_funct_5 :::"op1"::: ) ) "," (Set ($#k8_funct_5 :::"op1"::: ) ) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "#)" )); registration cluster (Set ($#k17_modelc_2 :::"TrivialLTLModel"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v9_modelc_2 :::"strict"::: ) ($#v10_modelc_2 :::"with_basic"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) for ($#l1_modelc_2 :::"LTLModelStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_modelc_2 :::"with_basic"::: ) for ($#l1_modelc_2 :::"LTLModelStr"::: ) ; end; definitionmode LTLModel is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_modelc_2 :::"with_basic"::: ) ($#l1_modelc_2 :::"LTLModelStr"::: ) ; end; registrationlet "C" be ($#l1_modelc_2 :::"LTLModel":::); cluster (Set "the" ($#u1_modelc_2 :::"BasicAssign"::: ) "of" "C") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "V" be ($#l1_modelc_2 :::"LTLModel":::); let "Kai" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k15_modelc_2 :::"atomic_LTL"::: ) ) "," (Set "the" ($#u1_modelc_2 :::"BasicAssign"::: ) "of" (Set (Const "V"))); let "n" be ($#m1_hidden :::"Nat":::); func :::"EvalSet"::: "(" "V" "," "Kai" "," "n" ")" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) equals :: MODELC_2:def 32 "{" (Set (Var "h")) where h "is" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") : (Bool (Set (Var "h")) ($#r5_modelc_2 :::"is-PreEvaluation-for"::: ) "n" "," "Kai") "}" ; end; :: deftheorem defines :::"EvalSet"::: MODELC_2:def 32 : (Bool "for" (Set (Var "V")) "being" ($#l1_modelc_2 :::"LTLModel":::) (Bool "for" (Set (Var "Kai")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k15_modelc_2 :::"atomic_LTL"::: ) ) "," (Set "the" ($#u1_modelc_2 :::"BasicAssign"::: ) "of" (Set (Var "V"))) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k18_modelc_2 :::"EvalSet"::: ) "(" (Set (Var "V")) "," (Set (Var "Kai")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "h")) where h "is" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) : (Bool (Set (Var "h")) ($#r5_modelc_2 :::"is-PreEvaluation-for"::: ) (Set (Var "n")) "," (Set (Var "Kai"))) "}" )))); definitionlet "V" be ($#l1_modelc_2 :::"LTLModel":::); let "v0" be ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "V"))); let "x" be ($#m1_hidden :::"set"::: ) ; func :::"CastEval"::: "(" "V" "," "x" "," "v0" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") equals :: MODELC_2:def 33 "x" if (Bool "x" ($#r2_hidden :::"in"::: ) (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ")" )) otherwise (Set (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) ) ($#k1_margrel1 :::"-->"::: ) "v0"); end; :: deftheorem defines :::"CastEval"::: MODELC_2:def 33 : (Bool "for" (Set (Var "V")) "being" ($#l1_modelc_2 :::"LTLModel":::) (Bool "for" (Set (Var "v0")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) ")" ))) "implies" (Bool (Set ($#k19_modelc_2 :::"CastEval"::: ) "(" (Set (Var "V")) "," (Set (Var "x")) "," (Set (Var "v0")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) ")" )))) "implies" (Bool (Set ($#k19_modelc_2 :::"CastEval"::: ) "(" (Set (Var "V")) "," (Set (Var "x")) "," (Set (Var "v0")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) ) ($#k1_margrel1 :::"-->"::: ) (Set (Var "v0")))) ")" ")" )))); definitionlet "V" be ($#l1_modelc_2 :::"LTLModel":::); let "Kai" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k15_modelc_2 :::"atomic_LTL"::: ) ) "," (Set "the" ($#u1_modelc_2 :::"BasicAssign"::: ) "of" (Set (Const "V"))); func :::"EvalFamily"::: "(" "V" "," "Kai" ")" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) means :: MODELC_2:def 34 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ")" ")" ))) & (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k18_modelc_2 :::"EvalSet"::: ) "(" "V" "," "Kai" "," (Set (Var "n")) ")" ))) ")" ) ")" )); end; :: deftheorem defines :::"EvalFamily"::: MODELC_2:def 34 : (Bool "for" (Set (Var "V")) "being" ($#l1_modelc_2 :::"LTLModel":::) (Bool "for" (Set (Var "Kai")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k15_modelc_2 :::"atomic_LTL"::: ) ) "," (Set "the" ($#u1_modelc_2 :::"BasicAssign"::: ) "of" (Set (Var "V"))) (Bool "for" (Set (Var "b3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k20_modelc_2 :::"EvalFamily"::: ) "(" (Set (Var "V")) "," (Set (Var "Kai")) ")" )) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) ")" ")" ))) & (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k18_modelc_2 :::"EvalSet"::: ) "(" (Set (Var "V")) "," (Set (Var "Kai")) "," (Set (Var "n")) ")" ))) ")" ) ")" )) ")" )))); theorem :: MODELC_2:48 (Bool "for" (Set (Var "V")) "being" ($#l1_modelc_2 :::"LTLModel":::) (Bool "for" (Set (Var "Kai")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k15_modelc_2 :::"atomic_LTL"::: ) ) "," (Set "the" ($#u1_modelc_2 :::"BasicAssign"::: ) "of" (Set (Var "V"))) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "st" (Bool (Set (Var "f")) ($#r4_modelc_2 :::"is-Evaluation-for"::: ) (Set (Var "Kai")))))) ; theorem :: MODELC_2:49 (Bool "for" (Set (Var "V")) "being" ($#l1_modelc_2 :::"LTLModel":::) (Bool "for" (Set (Var "Kai")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k15_modelc_2 :::"atomic_LTL"::: ) ) "," (Set "the" ($#u1_modelc_2 :::"BasicAssign"::: ) "of" (Set (Var "V"))) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "st" (Bool (Bool (Set (Var "f1")) ($#r4_modelc_2 :::"is-Evaluation-for"::: ) (Set (Var "Kai"))) & (Bool (Set (Var "f2")) ($#r4_modelc_2 :::"is-Evaluation-for"::: ) (Set (Var "Kai")))) "holds" (Bool (Set (Var "f1")) ($#r2_funct_2 :::"="::: ) (Set (Var "f2")))))) ; definitionlet "V" be ($#l1_modelc_2 :::"LTLModel":::); let "Kai" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k15_modelc_2 :::"atomic_LTL"::: ) ) "," (Set "the" ($#u1_modelc_2 :::"BasicAssign"::: ) "of" (Set (Const "V"))); let "H" be ($#m2_finseq_1 :::"LTL-formula":::); func :::"Evaluate"::: "(" "H" "," "Kai" ")" -> ($#m1_subset_1 :::"Assign":::) "of" "V" means :: MODELC_2:def 35 (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "st" (Bool "(" (Bool (Set (Var "f")) ($#r4_modelc_2 :::"is-Evaluation-for"::: ) "Kai") & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) "H")) ")" )); end; :: deftheorem defines :::"Evaluate"::: MODELC_2:def 35 : (Bool "for" (Set (Var "V")) "being" ($#l1_modelc_2 :::"LTLModel":::) (Bool "for" (Set (Var "Kai")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k15_modelc_2 :::"atomic_LTL"::: ) ) "," (Set "the" ($#u1_modelc_2 :::"BasicAssign"::: ) "of" (Set (Var "V"))) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Assign":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k21_modelc_2 :::"Evaluate"::: ) "(" (Set (Var "H")) "," (Set (Var "Kai")) ")" )) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "st" (Bool "(" (Bool (Set (Var "f")) ($#r4_modelc_2 :::"is-Evaluation-for"::: ) (Set (Var "Kai"))) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "H")))) ")" )) ")" ))))); notationlet "V" be ($#l1_modelc_2 :::"LTLModel":::); let "f" be ($#m1_subset_1 :::"Assign":::) "of" (Set (Const "V")); synonym :::"'not'"::: "f" for "f" :::"`"::: ; let "g" be ($#m1_subset_1 :::"Assign":::) "of" (Set (Const "V")); synonym "f" :::"'&'"::: "g" for "f" :::""/\""::: "g"; synonym "f" :::"'or'"::: "g" for "f" :::""\/""::: "g"; end; definitionlet "V" be ($#l1_modelc_2 :::"LTLModel":::); let "f" be ($#m1_subset_1 :::"Assign":::) "of" (Set (Const "V")); func :::"'X'"::: "f" -> ($#m1_subset_1 :::"Assign":::) "of" "V" equals :: MODELC_2:def 36 (Set (Set "the" ($#u2_modelc_2 :::"NEXT"::: ) "of" "V") ($#k3_funct_2 :::"."::: ) "f"); end; :: deftheorem defines :::"'X'"::: MODELC_2:def 36 : (Bool "for" (Set (Var "V")) "being" ($#l1_modelc_2 :::"LTLModel":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Assign":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k22_modelc_2 :::"'X'"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_modelc_2 :::"NEXT"::: ) "of" (Set (Var "V"))) ($#k3_funct_2 :::"."::: ) (Set (Var "f")))))); definitionlet "V" be ($#l1_modelc_2 :::"LTLModel":::); let "f", "g" be ($#m1_subset_1 :::"Assign":::) "of" (Set (Const "V")); func "f" :::"'U'"::: "g" -> ($#m1_subset_1 :::"Assign":::) "of" "V" equals :: MODELC_2:def 37 (Set (Set "the" ($#u3_modelc_2 :::"UNTIL"::: ) "of" "V") ($#k5_binop_1 :::"."::: ) "(" "f" "," "g" ")" ); func "f" :::"'R'"::: "g" -> ($#m1_subset_1 :::"Assign":::) "of" "V" equals :: MODELC_2:def 38 (Set (Set "the" ($#u4_modelc_2 :::"RELEASE"::: ) "of" "V") ($#k5_binop_1 :::"."::: ) "(" "f" "," "g" ")" ); end; :: deftheorem defines :::"'U'"::: MODELC_2:def 37 : (Bool "for" (Set (Var "V")) "being" ($#l1_modelc_2 :::"LTLModel":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Assign":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "f")) ($#k23_modelc_2 :::"'U'"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_modelc_2 :::"UNTIL"::: ) "of" (Set (Var "V"))) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" )))); :: deftheorem defines :::"'R'"::: MODELC_2:def 38 : (Bool "for" (Set (Var "V")) "being" ($#l1_modelc_2 :::"LTLModel":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Assign":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "f")) ($#k24_modelc_2 :::"'R'"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u4_modelc_2 :::"RELEASE"::: ) "of" (Set (Var "V"))) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" )))); theorem :: MODELC_2:50 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "V")) "being" ($#l1_modelc_2 :::"LTLModel":::) (Bool "for" (Set (Var "Kai")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k15_modelc_2 :::"atomic_LTL"::: ) ) "," (Set "the" ($#u1_modelc_2 :::"BasicAssign"::: ) "of" (Set (Var "V"))) "holds" (Bool (Set ($#k21_modelc_2 :::"Evaluate"::: ) "(" (Set "(" ($#k3_modelc_2 :::"'not'"::: ) (Set (Var "H")) ")" ) "," (Set (Var "Kai")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_robbins1 :::"'not'"::: ) (Set "(" ($#k21_modelc_2 :::"Evaluate"::: ) "(" (Set (Var "H")) "," (Set (Var "Kai")) ")" ")" )))))) ; theorem :: MODELC_2:51 (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "V")) "being" ($#l1_modelc_2 :::"LTLModel":::) (Bool "for" (Set (Var "Kai")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k15_modelc_2 :::"atomic_LTL"::: ) ) "," (Set "the" ($#u1_modelc_2 :::"BasicAssign"::: ) "of" (Set (Var "V"))) "holds" (Bool (Set ($#k21_modelc_2 :::"Evaluate"::: ) "(" (Set "(" (Set (Var "H1")) ($#k4_modelc_2 :::"'&'"::: ) (Set (Var "H2")) ")" ) "," (Set (Var "Kai")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k21_modelc_2 :::"Evaluate"::: ) "(" (Set (Var "H1")) "," (Set (Var "Kai")) ")" ")" ) ($#k2_lattices :::"'&'"::: ) (Set "(" ($#k21_modelc_2 :::"Evaluate"::: ) "(" (Set (Var "H2")) "," (Set (Var "Kai")) ")" ")" )))))) ; theorem :: MODELC_2:52 (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "V")) "being" ($#l1_modelc_2 :::"LTLModel":::) (Bool "for" (Set (Var "Kai")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k15_modelc_2 :::"atomic_LTL"::: ) ) "," (Set "the" ($#u1_modelc_2 :::"BasicAssign"::: ) "of" (Set (Var "V"))) "holds" (Bool (Set ($#k21_modelc_2 :::"Evaluate"::: ) "(" (Set "(" (Set (Var "H1")) ($#k5_modelc_2 :::"'or'"::: ) (Set (Var "H2")) ")" ) "," (Set (Var "Kai")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k21_modelc_2 :::"Evaluate"::: ) "(" (Set (Var "H1")) "," (Set (Var "Kai")) ")" ")" ) ($#k1_lattices :::"'or'"::: ) (Set "(" ($#k21_modelc_2 :::"Evaluate"::: ) "(" (Set (Var "H2")) "," (Set (Var "Kai")) ")" ")" )))))) ; theorem :: MODELC_2:53 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "V")) "being" ($#l1_modelc_2 :::"LTLModel":::) (Bool "for" (Set (Var "Kai")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k15_modelc_2 :::"atomic_LTL"::: ) ) "," (Set "the" ($#u1_modelc_2 :::"BasicAssign"::: ) "of" (Set (Var "V"))) "holds" (Bool (Set ($#k21_modelc_2 :::"Evaluate"::: ) "(" (Set "(" ($#k6_modelc_2 :::"'X'"::: ) (Set (Var "H")) ")" ) "," (Set (Var "Kai")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k22_modelc_2 :::"'X'"::: ) (Set "(" ($#k21_modelc_2 :::"Evaluate"::: ) "(" (Set (Var "H")) "," (Set (Var "Kai")) ")" ")" )))))) ; theorem :: MODELC_2:54 (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "V")) "being" ($#l1_modelc_2 :::"LTLModel":::) (Bool "for" (Set (Var "Kai")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k15_modelc_2 :::"atomic_LTL"::: ) ) "," (Set "the" ($#u1_modelc_2 :::"BasicAssign"::: ) "of" (Set (Var "V"))) "holds" (Bool (Set ($#k21_modelc_2 :::"Evaluate"::: ) "(" (Set "(" (Set (Var "H1")) ($#k7_modelc_2 :::"'U'"::: ) (Set (Var "H2")) ")" ) "," (Set (Var "Kai")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k21_modelc_2 :::"Evaluate"::: ) "(" (Set (Var "H1")) "," (Set (Var "Kai")) ")" ")" ) ($#k23_modelc_2 :::"'U'"::: ) (Set "(" ($#k21_modelc_2 :::"Evaluate"::: ) "(" (Set (Var "H2")) "," (Set (Var "Kai")) ")" ")" )))))) ; theorem :: MODELC_2:55 (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "V")) "being" ($#l1_modelc_2 :::"LTLModel":::) (Bool "for" (Set (Var "Kai")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k15_modelc_2 :::"atomic_LTL"::: ) ) "," (Set "the" ($#u1_modelc_2 :::"BasicAssign"::: ) "of" (Set (Var "V"))) "holds" (Bool (Set ($#k21_modelc_2 :::"Evaluate"::: ) "(" (Set "(" (Set (Var "H1")) ($#k8_modelc_2 :::"'R'"::: ) (Set (Var "H2")) ")" ) "," (Set (Var "Kai")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k21_modelc_2 :::"Evaluate"::: ) "(" (Set (Var "H1")) "," (Set (Var "Kai")) ")" ")" ) ($#k24_modelc_2 :::"'R'"::: ) (Set "(" ($#k21_modelc_2 :::"Evaluate"::: ) "(" (Set (Var "H2")) "," (Set (Var "Kai")) ")" ")" )))))) ; definitionlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"Inf_seq"::: "S" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) equals :: MODELC_2:def 39 (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k5_numbers :::"NAT"::: ) ) "," "S" ")" ); end; :: deftheorem defines :::"Inf_seq"::: MODELC_2:def 39 : (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) ")" ))); definitionlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "t" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "S")); func :::"CastSeq"::: "t" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) "S") equals :: MODELC_2:def 40 "t"; end; :: deftheorem defines :::"CastSeq"::: MODELC_2:def 40 : (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k26_modelc_2 :::"CastSeq"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Var "t"))))); definitionlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "t" be ($#m1_hidden :::"set"::: ) ; assume (Bool (Set (Const "t")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Const "S")))) ; func :::"CastSeq"::: "(" "t" "," "S" ")" -> ($#m1_subset_1 :::"sequence":::) "of" "S" equals :: MODELC_2:def 41 "t"; end; :: deftheorem defines :::"CastSeq"::: MODELC_2:def 41 : (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "t")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "t")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S"))))) "holds" (Bool (Set ($#k27_modelc_2 :::"CastSeq"::: ) "(" (Set (Var "t")) "," (Set (Var "S")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "t"))))); definitionlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "t" be ($#m1_hidden :::"set"::: ) ; let "k" be ($#m1_hidden :::"Nat":::); func :::"Shift"::: "(" "t" "," "k" "," "S" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) "S") equals :: MODELC_2:def 42 (Set ($#k26_modelc_2 :::"CastSeq"::: ) (Set "(" (Set "(" ($#k27_modelc_2 :::"CastSeq"::: ) "(" "t" "," "S" ")" ")" ) ($#k10_nat_1 :::"^\"::: ) "k" ")" )); end; :: deftheorem defines :::"Shift"::: MODELC_2:def 42 : (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "t")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k28_modelc_2 :::"Shift"::: ) "(" (Set (Var "t")) "," (Set (Var "k")) "," (Set (Var "S")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k26_modelc_2 :::"CastSeq"::: ) (Set "(" (Set "(" ($#k27_modelc_2 :::"CastSeq"::: ) "(" (Set (Var "t")) "," (Set (Var "S")) ")" ")" ) ($#k10_nat_1 :::"^\"::: ) (Set (Var "k")) ")" )))))); definitionlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "t" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Const "S"))); let "k" be ($#m1_hidden :::"Nat":::); func :::"Shift"::: "(" "t" "," "k" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) "S") equals :: MODELC_2:def 43 (Set ($#k28_modelc_2 :::"Shift"::: ) "(" "t" "," "k" "," "S" ")" ); end; :: deftheorem defines :::"Shift"::: MODELC_2:def 43 : (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S"))) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k29_modelc_2 :::"Shift"::: ) "(" (Set (Var "t")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k28_modelc_2 :::"Shift"::: ) "(" (Set (Var "t")) "," (Set (Var "k")) "," (Set (Var "S")) ")" ))))); definitionlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_hidden :::"set"::: ) ; func :::"Not_0"::: "(" "f" "," "S" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) "S" ")" )) means :: MODELC_2:def 44 (Bool "for" (Set (Var "t")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k25_modelc_2 :::"Inf_seq"::: ) "S"))) "holds" (Bool "(" (Bool (Set ($#k3_xboolean :::"'not'"::: ) (Set "(" ($#k4_modelc_1 :::"Castboolean"::: ) (Set "(" (Set "(" ($#k31_modelc_1 :::"Fid"::: ) "(" "f" "," (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) "S" ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "t")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) "iff" (Bool (Set (Set "(" ($#k31_modelc_1 :::"Fid"::: ) "(" it "," (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) "S" ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" )); end; :: deftheorem defines :::"Not_0"::: MODELC_2:def 44 : (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" )) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k30_modelc_2 :::"Not_0"::: ) "(" (Set (Var "f")) "," (Set (Var "S")) ")" )) "iff" (Bool "for" (Set (Var "t")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S"))))) "holds" (Bool "(" (Bool (Set ($#k3_xboolean :::"'not'"::: ) (Set "(" ($#k4_modelc_1 :::"Castboolean"::: ) (Set "(" (Set "(" ($#k31_modelc_1 :::"Fid"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "t")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) "iff" (Bool (Set (Set "(" ($#k31_modelc_1 :::"Fid"::: ) "(" (Set (Var "b3")) "," (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" )) ")" )))); definitionlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"Not_"::: "S" -> ($#m1_subset_1 :::"UnOp":::) "of" (Set "(" ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) "S" ")" ) ")" ) means :: MODELC_2:def 45 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) "S" ")" )))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k30_modelc_2 :::"Not_0"::: ) "(" (Set (Var "f")) "," "S" ")" ))); end; :: deftheorem defines :::"Not_"::: MODELC_2:def 45 : (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set "(" ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k31_modelc_2 :::"Not_"::: ) (Set (Var "S")))) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" )))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k30_modelc_2 :::"Not_0"::: ) "(" (Set (Var "f")) "," (Set (Var "S")) ")" ))) ")" ))); definitionlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Const "S")) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); let "t" be ($#m1_hidden :::"set"::: ) ; func :::"Next_univ"::: "(" "t" "," "f" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) equals :: MODELC_2:def 46 (Set ($#k8_margrel1 :::"TRUE"::: ) ) if (Bool "(" (Bool "t" "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) "S")) & (Bool (Set "f" ($#k3_funct_2 :::"."::: ) (Set "(" ($#k28_modelc_2 :::"Shift"::: ) "(" "t" "," (Num 1) "," "S" ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" ) otherwise (Set ($#k7_margrel1 :::"FALSE"::: ) ); end; :: deftheorem defines :::"Next_univ"::: MODELC_2:def 46 : (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "t")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "t")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")))) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k28_modelc_2 :::"Shift"::: ) "(" (Set (Var "t")) "," (Num 1) "," (Set (Var "S")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) "implies" (Bool (Set ($#k32_modelc_2 :::"Next_univ"::: ) "(" (Set (Var "t")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" & "(" (Bool (Bool "(" "not" (Bool (Set (Var "t")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")))) "or" "not" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k28_modelc_2 :::"Shift"::: ) "(" (Set (Var "t")) "," (Num 1) "," (Set (Var "S")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" )) "implies" (Bool (Set ($#k32_modelc_2 :::"Next_univ"::: ) "(" (Set (Var "t")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )) ")" ")" )))); definitionlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_hidden :::"set"::: ) ; func :::"Next_0"::: "(" "f" "," "S" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) "S" ")" )) means :: MODELC_2:def 47 (Bool "for" (Set (Var "t")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k25_modelc_2 :::"Inf_seq"::: ) "S"))) "holds" (Bool "(" (Bool (Set ($#k32_modelc_2 :::"Next_univ"::: ) "(" (Set (Var "t")) "," (Set "(" ($#k31_modelc_1 :::"Fid"::: ) "(" "f" "," (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) "S" ")" ) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) "iff" (Bool (Set (Set "(" ($#k31_modelc_1 :::"Fid"::: ) "(" it "," (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) "S" ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" )); end; :: deftheorem defines :::"Next_0"::: MODELC_2:def 47 : (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" )) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k33_modelc_2 :::"Next_0"::: ) "(" (Set (Var "f")) "," (Set (Var "S")) ")" )) "iff" (Bool "for" (Set (Var "t")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S"))))) "holds" (Bool "(" (Bool (Set ($#k32_modelc_2 :::"Next_univ"::: ) "(" (Set (Var "t")) "," (Set "(" ($#k31_modelc_1 :::"Fid"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" ) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) "iff" (Bool (Set (Set "(" ($#k31_modelc_1 :::"Fid"::: ) "(" (Set (Var "b3")) "," (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" )) ")" )))); definitionlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"Next_"::: "S" -> ($#m1_subset_1 :::"UnOp":::) "of" (Set "(" ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) "S" ")" ) ")" ) means :: MODELC_2:def 48 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) "S" ")" )))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k33_modelc_2 :::"Next_0"::: ) "(" (Set (Var "f")) "," "S" ")" ))); end; :: deftheorem defines :::"Next_"::: MODELC_2:def 48 : (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set "(" ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k34_modelc_2 :::"Next_"::: ) (Set (Var "S")))) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" )))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k33_modelc_2 :::"Next_0"::: ) "(" (Set (Var "f")) "," (Set (Var "S")) ")" ))) ")" ))); definitionlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f", "g" be ($#m1_hidden :::"set"::: ) ; func :::"And_0"::: "(" "f" "," "g" "," "S" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) "S" ")" )) means :: MODELC_2:def 49 (Bool "for" (Set (Var "t")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k25_modelc_2 :::"Inf_seq"::: ) "S"))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_modelc_1 :::"Castboolean"::: ) (Set "(" (Set "(" ($#k31_modelc_1 :::"Fid"::: ) "(" "f" "," (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) "S" ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "t")) ")" ) ")" ) ($#k4_xboolean :::"'&'"::: ) (Set "(" ($#k4_modelc_1 :::"Castboolean"::: ) (Set "(" (Set "(" ($#k31_modelc_1 :::"Fid"::: ) "(" "g" "," (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) "S" ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "t")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) "iff" (Bool (Set (Set "(" ($#k31_modelc_1 :::"Fid"::: ) "(" it "," (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) "S" ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" )); end; :: deftheorem defines :::"And_0"::: MODELC_2:def 49 : (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" )) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k35_modelc_2 :::"And_0"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "S")) ")" )) "iff" (Bool "for" (Set (Var "t")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S"))))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_modelc_1 :::"Castboolean"::: ) (Set "(" (Set "(" ($#k31_modelc_1 :::"Fid"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "t")) ")" ) ")" ) ($#k4_xboolean :::"'&'"::: ) (Set "(" ($#k4_modelc_1 :::"Castboolean"::: ) (Set "(" (Set "(" ($#k31_modelc_1 :::"Fid"::: ) "(" (Set (Var "g")) "," (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "t")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) "iff" (Bool (Set (Set "(" ($#k31_modelc_1 :::"Fid"::: ) "(" (Set (Var "b4")) "," (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" )) ")" )))); definitionlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"And_"::: "S" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) "S" ")" ) ")" ) means :: MODELC_2:def 50 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) "S" ")" ))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) "S" ")" )))) "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k35_modelc_2 :::"And_0"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) "," "S" ")" ))); end; :: deftheorem defines :::"And_"::: MODELC_2:def 50 : (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k36_modelc_2 :::"And_"::: ) (Set (Var "S")))) "iff" (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" ))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" )))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k35_modelc_2 :::"And_0"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "S")) ")" ))) ")" ))); definitionlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f", "g" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Const "S")) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); let "t" be ($#m1_hidden :::"set"::: ) ; func :::"Until_univ"::: "(" "t" "," "f" "," "g" "," "S" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) equals :: MODELC_2:def 51 (Set ($#k8_margrel1 :::"TRUE"::: ) ) if (Bool "(" (Bool "t" "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) "S")) & (Bool "ex" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool "(" "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool (Set "f" ($#k3_funct_2 :::"."::: ) (Set "(" ($#k28_modelc_2 :::"Shift"::: ) "(" "t" "," (Set (Var "j")) "," "S" ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" ) & (Bool (Set "g" ($#k3_funct_2 :::"."::: ) (Set "(" ($#k28_modelc_2 :::"Shift"::: ) "(" "t" "," (Set (Var "m")) "," "S" ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" )) ")" ) otherwise (Set ($#k7_margrel1 :::"FALSE"::: ) ); end; :: deftheorem defines :::"Until_univ"::: MODELC_2:def 51 : (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "t")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "t")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")))) & (Bool "ex" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool "(" "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k28_modelc_2 :::"Shift"::: ) "(" (Set (Var "t")) "," (Set (Var "j")) "," (Set (Var "S")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" ) & (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k28_modelc_2 :::"Shift"::: ) "(" (Set (Var "t")) "," (Set (Var "m")) "," (Set (Var "S")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" ))) "implies" (Bool (Set ($#k37_modelc_2 :::"Until_univ"::: ) "(" (Set (Var "t")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "S")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" & "(" (Bool (Bool "(" "not" (Bool (Set (Var "t")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")))) "or" (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool "ex" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m"))) & (Bool (Bool "not" (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k28_modelc_2 :::"Shift"::: ) "(" (Set (Var "t")) "," (Set (Var "j")) "," (Set (Var "S")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) ")" )) "or" "not" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k28_modelc_2 :::"Shift"::: ) "(" (Set (Var "t")) "," (Set (Var "m")) "," (Set (Var "S")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" )) ")" )) "implies" (Bool (Set ($#k37_modelc_2 :::"Until_univ"::: ) "(" (Set (Var "t")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "S")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )) ")" ")" )))); definitionlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f", "g" be ($#m1_hidden :::"set"::: ) ; func :::"Until_0"::: "(" "f" "," "g" "," "S" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) "S" ")" )) means :: MODELC_2:def 52 (Bool "for" (Set (Var "t")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k25_modelc_2 :::"Inf_seq"::: ) "S"))) "holds" (Bool "(" (Bool (Set ($#k37_modelc_2 :::"Until_univ"::: ) "(" (Set (Var "t")) "," (Set "(" ($#k31_modelc_1 :::"Fid"::: ) "(" "f" "," (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) "S" ")" ) ")" ")" ) "," (Set "(" ($#k31_modelc_1 :::"Fid"::: ) "(" "g" "," (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) "S" ")" ) ")" ")" ) "," "S" ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) "iff" (Bool (Set (Set "(" ($#k31_modelc_1 :::"Fid"::: ) "(" it "," (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) "S" ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" )); end; :: deftheorem defines :::"Until_0"::: MODELC_2:def 52 : (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" )) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k38_modelc_2 :::"Until_0"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "S")) ")" )) "iff" (Bool "for" (Set (Var "t")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S"))))) "holds" (Bool "(" (Bool (Set ($#k37_modelc_2 :::"Until_univ"::: ) "(" (Set (Var "t")) "," (Set "(" ($#k31_modelc_1 :::"Fid"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" ) ")" ")" ) "," (Set "(" ($#k31_modelc_1 :::"Fid"::: ) "(" (Set (Var "g")) "," (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" ) ")" ")" ) "," (Set (Var "S")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) "iff" (Bool (Set (Set "(" ($#k31_modelc_1 :::"Fid"::: ) "(" (Set (Var "b4")) "," (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" )) ")" )))); definitionlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"Until_"::: "S" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) "S" ")" ) ")" ) means :: MODELC_2:def 53 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) "S" ")" ))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) "S" ")" )))) "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k38_modelc_2 :::"Until_0"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) "," "S" ")" ))); end; :: deftheorem defines :::"Until_"::: MODELC_2:def 53 : (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k39_modelc_2 :::"Until_"::: ) (Set (Var "S")))) "iff" (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" ))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" )))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k38_modelc_2 :::"Until_0"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "S")) ")" ))) ")" ))); definitionlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"Or_"::: "S" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) "S" ")" ) ")" ) means :: MODELC_2:def 54 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) "S" ")" ))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) "S" ")" )))) "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k31_modelc_2 :::"Not_"::: ) "S" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k36_modelc_2 :::"And_"::: ) "S" ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set "(" ($#k31_modelc_2 :::"Not_"::: ) "S" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "f")) ")" ) "," (Set "(" (Set "(" ($#k31_modelc_2 :::"Not_"::: ) "S" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "g")) ")" ) ")" ")" )))); func :::"Release_"::: "S" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) "S" ")" ) ")" ) means :: MODELC_2:def 55 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) "S" ")" ))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) "S" ")" )))) "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k31_modelc_2 :::"Not_"::: ) "S" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k39_modelc_2 :::"Until_"::: ) "S" ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set "(" ($#k31_modelc_2 :::"Not_"::: ) "S" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "f")) ")" ) "," (Set "(" (Set "(" ($#k31_modelc_2 :::"Not_"::: ) "S" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "g")) ")" ) ")" ")" )))); end; :: deftheorem defines :::"Or_"::: MODELC_2:def 54 : (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k40_modelc_2 :::"Or_"::: ) (Set (Var "S")))) "iff" (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" ))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" )))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k31_modelc_2 :::"Not_"::: ) (Set (Var "S")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k36_modelc_2 :::"And_"::: ) (Set (Var "S")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set "(" ($#k31_modelc_2 :::"Not_"::: ) (Set (Var "S")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "f")) ")" ) "," (Set "(" (Set "(" ($#k31_modelc_2 :::"Not_"::: ) (Set (Var "S")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "g")) ")" ) ")" ")" )))) ")" ))); :: deftheorem defines :::"Release_"::: MODELC_2:def 55 : (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k41_modelc_2 :::"Release_"::: ) (Set (Var "S")))) "iff" (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" ))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" )))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k31_modelc_2 :::"Not_"::: ) (Set (Var "S")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k39_modelc_2 :::"Until_"::: ) (Set (Var "S")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set "(" ($#k31_modelc_2 :::"Not_"::: ) (Set (Var "S")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "f")) ")" ) "," (Set "(" (Set "(" ($#k31_modelc_2 :::"Not_"::: ) (Set (Var "S")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "g")) ")" ) ")" ")" )))) ")" ))); definitionlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "BASSIGN" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Const "S")) ")" ) ")" ); func :::"Inf_seqModel"::: "(" "S" "," "BASSIGN" ")" -> ($#l1_modelc_2 :::"LTLModelStr"::: ) equals :: MODELC_2:def 56 (Set ($#g1_modelc_2 :::"LTLModelStr"::: ) "(#" (Set "(" ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) "S" ")" ) ")" ) "," "BASSIGN" "," (Set "(" ($#k36_modelc_2 :::"And_"::: ) "S" ")" ) "," (Set "(" ($#k40_modelc_2 :::"Or_"::: ) "S" ")" ) "," (Set "(" ($#k31_modelc_2 :::"Not_"::: ) "S" ")" ) "," (Set "(" ($#k34_modelc_2 :::"Next_"::: ) "S" ")" ) "," (Set "(" ($#k39_modelc_2 :::"Until_"::: ) "S" ")" ) "," (Set "(" ($#k41_modelc_2 :::"Release_"::: ) "S" ")" ) "#)" ); end; :: deftheorem defines :::"Inf_seqModel"::: MODELC_2:def 56 : (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "BASSIGN")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" ) ")" ) "holds" (Bool (Set ($#k42_modelc_2 :::"Inf_seqModel"::: ) "(" (Set (Var "S")) "," (Set (Var "BASSIGN")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g1_modelc_2 :::"LTLModelStr"::: ) "(#" (Set "(" ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" ) ")" ) "," (Set (Var "BASSIGN")) "," (Set "(" ($#k36_modelc_2 :::"And_"::: ) (Set (Var "S")) ")" ) "," (Set "(" ($#k40_modelc_2 :::"Or_"::: ) (Set (Var "S")) ")" ) "," (Set "(" ($#k31_modelc_2 :::"Not_"::: ) (Set (Var "S")) ")" ) "," (Set "(" ($#k34_modelc_2 :::"Next_"::: ) (Set (Var "S")) ")" ) "," (Set "(" ($#k39_modelc_2 :::"Until_"::: ) (Set (Var "S")) ")" ) "," (Set "(" ($#k41_modelc_2 :::"Release_"::: ) (Set (Var "S")) ")" ) "#)" )))); registrationlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "BASSIGN" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Const "S")) ")" ) ")" ); cluster (Set ($#k42_modelc_2 :::"Inf_seqModel"::: ) "(" "S" "," "BASSIGN" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v9_modelc_2 :::"strict"::: ) ($#v10_modelc_2 :::"with_basic"::: ) ; end; definitionlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "BASSIGN" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Const "S")) ")" ) ")" ); let "t" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Const "S"))); let "f" be ($#m1_subset_1 :::"Assign":::) "of" (Set "(" ($#k42_modelc_2 :::"Inf_seqModel"::: ) "(" (Set (Const "S")) "," (Set (Const "BASSIGN")) ")" ")" ); pred "t" :::"|="::: "f" means :: MODELC_2:def 57 (Bool (Set (Set "(" ($#k31_modelc_1 :::"Fid"::: ) "(" "f" "," (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) "S" ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) "t") ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )); end; :: deftheorem defines :::"|="::: MODELC_2:def 57 : (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "BASSIGN")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" ) ")" ) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Assign":::) "of" (Set "(" ($#k42_modelc_2 :::"Inf_seqModel"::: ) "(" (Set (Var "S")) "," (Set (Var "BASSIGN")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r6_modelc_2 :::"|="::: ) (Set (Var "f"))) "iff" (Bool (Set (Set "(" ($#k31_modelc_1 :::"Fid"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" ))))); notationlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "BASSIGN" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Const "S")) ")" ) ")" ); let "t" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Const "S"))); let "f" be ($#m1_subset_1 :::"Assign":::) "of" (Set "(" ($#k42_modelc_2 :::"Inf_seqModel"::: ) "(" (Set (Const "S")) "," (Set (Const "BASSIGN")) ")" ")" ); antonym "t" :::"|/="::: "f" for "t" :::"|="::: "f"; end; theorem :: MODELC_2:56 (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "BASSIGN")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" ) ")" ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Assign":::) "of" (Set "(" ($#k42_modelc_2 :::"Inf_seqModel"::: ) "(" (Set (Var "S")) "," (Set (Var "BASSIGN")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_lattices :::"'or'"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k3_robbins1 :::"'not'"::: ) (Set "(" (Set "(" ($#k3_robbins1 :::"'not'"::: ) (Set (Var "f")) ")" ) ($#k2_lattices :::"'&'"::: ) (Set "(" ($#k3_robbins1 :::"'not'"::: ) (Set (Var "g")) ")" ) ")" ))) & (Bool (Set (Set (Var "f")) ($#k24_modelc_2 :::"'R'"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k3_robbins1 :::"'not'"::: ) (Set "(" (Set "(" ($#k3_robbins1 :::"'not'"::: ) (Set (Var "f")) ")" ) ($#k23_modelc_2 :::"'U'"::: ) (Set "(" ($#k3_robbins1 :::"'not'"::: ) (Set (Var "g")) ")" ) ")" ))) ")" )))) ; theorem :: MODELC_2:57 (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "BASSIGN")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" ) ")" ) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Assign":::) "of" (Set "(" ($#k42_modelc_2 :::"Inf_seqModel"::: ) "(" (Set (Var "S")) "," (Set (Var "BASSIGN")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r6_modelc_2 :::"|="::: ) (Set ($#k3_robbins1 :::"'not'"::: ) (Set (Var "f")))) "iff" (Bool (Set (Var "t")) ($#r6_modelc_2 :::"|/="::: ) (Set (Var "f"))) ")" ))))) ; theorem :: MODELC_2:58 (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "BASSIGN")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" ) ")" ) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S"))) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Assign":::) "of" (Set "(" ($#k42_modelc_2 :::"Inf_seqModel"::: ) "(" (Set (Var "S")) "," (Set (Var "BASSIGN")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r6_modelc_2 :::"|="::: ) (Set (Set (Var "f")) ($#k2_lattices :::"'&'"::: ) (Set (Var "g")))) "iff" (Bool "(" (Bool (Set (Var "t")) ($#r6_modelc_2 :::"|="::: ) (Set (Var "f"))) & (Bool (Set (Var "t")) ($#r6_modelc_2 :::"|="::: ) (Set (Var "g"))) ")" ) ")" ))))) ; theorem :: MODELC_2:59 (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "BASSIGN")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" ) ")" ) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Assign":::) "of" (Set "(" ($#k42_modelc_2 :::"Inf_seqModel"::: ) "(" (Set (Var "S")) "," (Set (Var "BASSIGN")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r6_modelc_2 :::"|="::: ) (Set ($#k22_modelc_2 :::"'X'"::: ) (Set (Var "f")))) "iff" (Bool (Set ($#k29_modelc_2 :::"Shift"::: ) "(" (Set (Var "t")) "," (Num 1) ")" ) ($#r6_modelc_2 :::"|="::: ) (Set (Var "f"))) ")" ))))) ; theorem :: MODELC_2:60 (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "BASSIGN")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" ) ")" ) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S"))) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Assign":::) "of" (Set "(" ($#k42_modelc_2 :::"Inf_seqModel"::: ) "(" (Set (Var "S")) "," (Set (Var "BASSIGN")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r6_modelc_2 :::"|="::: ) (Set (Set (Var "f")) ($#k23_modelc_2 :::"'U'"::: ) (Set (Var "g")))) "iff" (Bool "ex" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool "(" "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k29_modelc_2 :::"Shift"::: ) "(" (Set (Var "t")) "," (Set (Var "j")) ")" ) ($#r6_modelc_2 :::"|="::: ) (Set (Var "f"))) ")" ) & (Bool (Set ($#k29_modelc_2 :::"Shift"::: ) "(" (Set (Var "t")) "," (Set (Var "m")) ")" ) ($#r6_modelc_2 :::"|="::: ) (Set (Var "g"))) ")" )) ")" ))))) ; theorem :: MODELC_2:61 (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "BASSIGN")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" ) ")" ) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S"))) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Assign":::) "of" (Set "(" ($#k42_modelc_2 :::"Inf_seqModel"::: ) "(" (Set (Var "S")) "," (Set (Var "BASSIGN")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r6_modelc_2 :::"|="::: ) (Set (Set (Var "f")) ($#k1_lattices :::"'or'"::: ) (Set (Var "g")))) "iff" (Bool "(" (Bool (Set (Var "t")) ($#r6_modelc_2 :::"|="::: ) (Set (Var "f"))) "or" (Bool (Set (Var "t")) ($#r6_modelc_2 :::"|="::: ) (Set (Var "g"))) ")" ) ")" ))))) ; theorem :: MODELC_2:62 (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "BASSIGN")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S")) ")" ) ")" ) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S"))) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Assign":::) "of" (Set "(" ($#k42_modelc_2 :::"Inf_seqModel"::: ) "(" (Set (Var "S")) "," (Set (Var "BASSIGN")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r6_modelc_2 :::"|="::: ) (Set (Set (Var "f")) ($#k24_modelc_2 :::"'R'"::: ) (Set (Var "g")))) "iff" (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool "(" "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k29_modelc_2 :::"Shift"::: ) "(" (Set (Var "t")) "," (Set (Var "j")) ")" ) ($#r6_modelc_2 :::"|="::: ) (Set ($#k3_robbins1 :::"'not'"::: ) (Set (Var "f")))) ")" )) "holds" (Bool (Set ($#k29_modelc_2 :::"Shift"::: ) "(" (Set (Var "t")) "," (Set (Var "m")) ")" ) ($#r6_modelc_2 :::"|="::: ) (Set (Var "g")))) ")" ))))) ; definitionfunc :::"AtomicFamily"::: -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) equals :: MODELC_2:def 58 (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k15_modelc_2 :::"atomic_LTL"::: ) )); end; :: deftheorem defines :::"AtomicFamily"::: MODELC_2:def 58 : (Bool (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k15_modelc_2 :::"atomic_LTL"::: ) ))); definitionlet "a", "t" be ($#m1_hidden :::"set"::: ) ; func :::"AtomicFunc"::: "(" "a" "," "t" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) equals :: MODELC_2:def 59 (Set ($#k8_margrel1 :::"TRUE"::: ) ) if (Bool "(" (Bool "t" ($#r2_hidden :::"in"::: ) (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) ))) & (Bool "a" ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k27_modelc_2 :::"CastSeq"::: ) "(" "t" "," (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) ) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) ")" ) otherwise (Set ($#k7_margrel1 :::"FALSE"::: ) ); end; :: deftheorem defines :::"AtomicFunc"::: MODELC_2:def 59 : (Bool "for" (Set (Var "a")) "," (Set (Var "t")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) ))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k27_modelc_2 :::"CastSeq"::: ) "(" (Set (Var "t")) "," (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) ) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )))) "implies" (Bool (Set ($#k44_modelc_2 :::"AtomicFunc"::: ) "(" (Set (Var "a")) "," (Set (Var "t")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" & "(" (Bool (Bool "(" "not" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) ))) "or" "not" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k27_modelc_2 :::"CastSeq"::: ) "(" (Set (Var "t")) "," (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) ) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) ")" )) "implies" (Bool (Set ($#k44_modelc_2 :::"AtomicFunc"::: ) "(" (Set (Var "a")) "," (Set (Var "t")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )) ")" ")" )); definitionlet "a" be ($#m1_hidden :::"set"::: ) ; func :::"AtomicAsgn"::: "a" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) ) ")" )) means :: MODELC_2:def 60 (Bool "for" (Set (Var "t")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )))) "holds" (Bool (Set (Set "(" ($#k31_modelc_1 :::"Fid"::: ) "(" it "," (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) ) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k44_modelc_2 :::"AtomicFunc"::: ) "(" "a" "," (Set (Var "t")) ")" ))); end; :: deftheorem defines :::"AtomicAsgn"::: MODELC_2:def 60 : (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) ) ")" )) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k45_modelc_2 :::"AtomicAsgn"::: ) (Set (Var "a")))) "iff" (Bool "for" (Set (Var "t")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )))) "holds" (Bool (Set (Set "(" ($#k31_modelc_1 :::"Fid"::: ) "(" (Set (Var "b2")) "," (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) ) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k44_modelc_2 :::"AtomicFunc"::: ) "(" (Set (Var "a")) "," (Set (Var "t")) ")" ))) ")" ))); definitionfunc :::"AtomicBasicAsgn"::: -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) ) ")" ) ")" ) equals :: MODELC_2:def 61 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) ) ")" )) : (Bool "ex" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k45_modelc_2 :::"AtomicAsgn"::: ) (Set (Var "a"))))) "}" ; end; :: deftheorem defines :::"AtomicBasicAsgn"::: MODELC_2:def 61 : (Bool (Set ($#k46_modelc_2 :::"AtomicBasicAsgn"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k30_modelc_1 :::"ModelSP"::: ) (Set "(" ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) ) ")" )) : (Bool "ex" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k45_modelc_2 :::"AtomicAsgn"::: ) (Set (Var "a"))))) "}" ); definitionfunc :::"AtomicKai"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k15_modelc_2 :::"atomic_LTL"::: ) ) "," (Set "the" ($#u1_modelc_2 :::"BasicAssign"::: ) "of" (Set "(" ($#k42_modelc_2 :::"Inf_seqModel"::: ) "(" (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) ) "," (Set ($#k46_modelc_2 :::"AtomicBasicAsgn"::: ) ) ")" ")" )) means :: MODELC_2:def 62 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k15_modelc_2 :::"atomic_LTL"::: ) ))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k45_modelc_2 :::"AtomicAsgn"::: ) (Set (Var "a"))))); end; :: deftheorem defines :::"AtomicKai"::: MODELC_2:def 62 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k15_modelc_2 :::"atomic_LTL"::: ) ) "," (Set "the" ($#u1_modelc_2 :::"BasicAssign"::: ) "of" (Set "(" ($#k42_modelc_2 :::"Inf_seqModel"::: ) "(" (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) ) "," (Set ($#k46_modelc_2 :::"AtomicBasicAsgn"::: ) ) ")" ")" )) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k47_modelc_2 :::"AtomicKai"::: ) )) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k15_modelc_2 :::"atomic_LTL"::: ) ))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k45_modelc_2 :::"AtomicAsgn"::: ) (Set (Var "a"))))) ")" )); definitionlet "r" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )); let "H" be ($#m2_finseq_1 :::"LTL-formula":::); pred "r" :::"|="::: "H" means :: MODELC_2:def 63 (Bool "r" ($#r6_modelc_2 :::"|="::: ) (Set ($#k21_modelc_2 :::"Evaluate"::: ) "(" "H" "," (Set ($#k47_modelc_2 :::"AtomicKai"::: ) ) ")" )); end; :: deftheorem defines :::"|="::: MODELC_2:def 63 : (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r7_modelc_2 :::"|="::: ) (Set (Var "H"))) "iff" (Bool (Set (Var "r")) ($#r6_modelc_2 :::"|="::: ) (Set ($#k21_modelc_2 :::"Evaluate"::: ) "(" (Set (Var "H")) "," (Set ($#k47_modelc_2 :::"AtomicKai"::: ) ) ")" )) ")" ))); notationlet "r" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )); let "H" be ($#m2_finseq_1 :::"LTL-formula":::); antonym "r" :::"|/="::: "H" for "r" :::"|="::: "H"; end; definitionlet "r" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )); let "W" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) ); pred "r" :::"|="::: "W" means :: MODELC_2:def 64 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) "W")) "holds" (Bool "r" ($#r7_modelc_2 :::"|="::: ) (Set (Var "H")))); end; :: deftheorem defines :::"|="::: MODELC_2:def 64 : (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r8_modelc_2 :::"|="::: ) (Set (Var "W"))) "iff" (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set (Var "W")))) "holds" (Bool (Set (Var "r")) ($#r7_modelc_2 :::"|="::: ) (Set (Var "H")))) ")" ))); notationlet "r" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )); let "W" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) ); antonym "r" :::"|/="::: "W" for "r" :::"|="::: "W"; end; definitionlet "W" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) ); func :::"'X'"::: "W" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) ) equals :: MODELC_2:def 65 "{" (Set (Var "x")) where x "is" ($#m2_finseq_1 :::"LTL-formula":::) : (Bool "ex" (Set (Var "u")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool "(" (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) "W") & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_modelc_2 :::"'X'"::: ) (Set (Var "u")))) ")" )) "}" ; end; :: deftheorem defines :::"'X'"::: MODELC_2:def 65 : (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) ) "holds" (Bool (Set ($#k48_modelc_2 :::"'X'"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m2_finseq_1 :::"LTL-formula":::) : (Bool "ex" (Set (Var "u")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "st" (Bool "(" (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_modelc_2 :::"'X'"::: ) (Set (Var "u")))) ")" )) "}" )); theorem :: MODELC_2:63 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) "st" (Bool (Bool (Set (Var "H")) "is" ($#v2_modelc_2 :::"atomic"::: ) )) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r7_modelc_2 :::"|="::: ) (Set (Var "H"))) "iff" (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k27_modelc_2 :::"CastSeq"::: ) "(" (Set (Var "r")) "," (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) ) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) ")" ))) ; theorem :: MODELC_2:64 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r7_modelc_2 :::"|="::: ) (Set ($#k3_modelc_2 :::"'not'"::: ) (Set (Var "H")))) "iff" (Bool (Set (Var "r")) ($#r7_modelc_2 :::"|/="::: ) (Set (Var "H"))) ")" ))) ; theorem :: MODELC_2:65 (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r7_modelc_2 :::"|="::: ) (Set (Set (Var "H1")) ($#k4_modelc_2 :::"'&'"::: ) (Set (Var "H2")))) "iff" (Bool "(" (Bool (Set (Var "r")) ($#r7_modelc_2 :::"|="::: ) (Set (Var "H1"))) & (Bool (Set (Var "r")) ($#r7_modelc_2 :::"|="::: ) (Set (Var "H2"))) ")" ) ")" ))) ; theorem :: MODELC_2:66 (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r7_modelc_2 :::"|="::: ) (Set (Set (Var "H1")) ($#k5_modelc_2 :::"'or'"::: ) (Set (Var "H2")))) "iff" (Bool "(" (Bool (Set (Var "r")) ($#r7_modelc_2 :::"|="::: ) (Set (Var "H1"))) "or" (Bool (Set (Var "r")) ($#r7_modelc_2 :::"|="::: ) (Set (Var "H2"))) ")" ) ")" ))) ; theorem :: MODELC_2:67 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r7_modelc_2 :::"|="::: ) (Set ($#k6_modelc_2 :::"'X'"::: ) (Set (Var "H")))) "iff" (Bool (Set ($#k29_modelc_2 :::"Shift"::: ) "(" (Set (Var "r")) "," (Num 1) ")" ) ($#r7_modelc_2 :::"|="::: ) (Set (Var "H"))) ")" ))) ; theorem :: MODELC_2:68 (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r7_modelc_2 :::"|="::: ) (Set (Set (Var "H1")) ($#k7_modelc_2 :::"'U'"::: ) (Set (Var "H2")))) "iff" (Bool "ex" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool "(" "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k29_modelc_2 :::"Shift"::: ) "(" (Set (Var "r")) "," (Set (Var "j")) ")" ) ($#r7_modelc_2 :::"|="::: ) (Set (Var "H1"))) ")" ) & (Bool (Set ($#k29_modelc_2 :::"Shift"::: ) "(" (Set (Var "r")) "," (Set (Var "m")) ")" ) ($#r7_modelc_2 :::"|="::: ) (Set (Var "H2"))) ")" )) ")" ))) ; theorem :: MODELC_2:69 (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r7_modelc_2 :::"|="::: ) (Set (Set (Var "H1")) ($#k8_modelc_2 :::"'R'"::: ) (Set (Var "H2")))) "iff" (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool "(" "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k29_modelc_2 :::"Shift"::: ) "(" (Set (Var "r")) "," (Set (Var "j")) ")" ) ($#r7_modelc_2 :::"|="::: ) (Set ($#k3_modelc_2 :::"'not'"::: ) (Set (Var "H1")))) ")" )) "holds" (Bool (Set ($#k29_modelc_2 :::"Shift"::: ) "(" (Set (Var "r")) "," (Set (Var "m")) ")" ) ($#r7_modelc_2 :::"|="::: ) (Set (Var "H2")))) ")" ))) ; theorem :: MODELC_2:70 (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r7_modelc_2 :::"|="::: ) (Set ($#k3_modelc_2 :::"'not'"::: ) (Set "(" (Set (Var "H1")) ($#k5_modelc_2 :::"'or'"::: ) (Set (Var "H2")) ")" ))) "iff" (Bool (Set (Var "r")) ($#r7_modelc_2 :::"|="::: ) (Set (Set "(" ($#k3_modelc_2 :::"'not'"::: ) (Set (Var "H1")) ")" ) ($#k4_modelc_2 :::"'&'"::: ) (Set "(" ($#k3_modelc_2 :::"'not'"::: ) (Set (Var "H2")) ")" ))) ")" ))) ; theorem :: MODELC_2:71 (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r7_modelc_2 :::"|="::: ) (Set ($#k3_modelc_2 :::"'not'"::: ) (Set "(" (Set (Var "H1")) ($#k4_modelc_2 :::"'&'"::: ) (Set (Var "H2")) ")" ))) "iff" (Bool (Set (Var "r")) ($#r7_modelc_2 :::"|="::: ) (Set (Set "(" ($#k3_modelc_2 :::"'not'"::: ) (Set (Var "H1")) ")" ) ($#k5_modelc_2 :::"'or'"::: ) (Set "(" ($#k3_modelc_2 :::"'not'"::: ) (Set (Var "H2")) ")" ))) ")" ))) ; theorem :: MODELC_2:72 (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r7_modelc_2 :::"|="::: ) (Set (Set (Var "H1")) ($#k8_modelc_2 :::"'R'"::: ) (Set (Var "H2")))) "iff" (Bool (Set (Var "r")) ($#r7_modelc_2 :::"|="::: ) (Set ($#k3_modelc_2 :::"'not'"::: ) (Set "(" (Set "(" ($#k3_modelc_2 :::"'not'"::: ) (Set (Var "H1")) ")" ) ($#k7_modelc_2 :::"'U'"::: ) (Set "(" ($#k3_modelc_2 :::"'not'"::: ) (Set (Var "H2")) ")" ) ")" ))) ")" ))) ; theorem :: MODELC_2:73 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r7_modelc_2 :::"|/="::: ) (Set ($#k3_modelc_2 :::"'not'"::: ) (Set (Var "H")))) "iff" (Bool (Set (Var "r")) ($#r7_modelc_2 :::"|="::: ) (Set (Var "H"))) ")" ))) ; theorem :: MODELC_2:74 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r7_modelc_2 :::"|="::: ) (Set ($#k6_modelc_2 :::"'X'"::: ) (Set "(" ($#k3_modelc_2 :::"'not'"::: ) (Set (Var "H")) ")" ))) "iff" (Bool (Set (Var "r")) ($#r7_modelc_2 :::"|="::: ) (Set ($#k3_modelc_2 :::"'not'"::: ) (Set "(" ($#k6_modelc_2 :::"'X'"::: ) (Set (Var "H")) ")" ))) ")" ))) ; theorem :: MODELC_2:75 (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r7_modelc_2 :::"|="::: ) (Set (Set (Var "H1")) ($#k7_modelc_2 :::"'U'"::: ) (Set (Var "H2")))) "iff" (Bool (Set (Var "r")) ($#r7_modelc_2 :::"|="::: ) (Set (Set (Var "H2")) ($#k5_modelc_2 :::"'or'"::: ) (Set "(" (Set (Var "H1")) ($#k4_modelc_2 :::"'&'"::: ) (Set "(" ($#k6_modelc_2 :::"'X'"::: ) (Set "(" (Set (Var "H1")) ($#k7_modelc_2 :::"'U'"::: ) (Set (Var "H2")) ")" ) ")" ) ")" ))) ")" ))) ; theorem :: MODELC_2:76 (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r7_modelc_2 :::"|="::: ) (Set (Set (Var "H1")) ($#k8_modelc_2 :::"'R'"::: ) (Set (Var "H2")))) "iff" (Bool (Set (Var "r")) ($#r7_modelc_2 :::"|="::: ) (Set (Set "(" (Set (Var "H1")) ($#k4_modelc_2 :::"'&'"::: ) (Set (Var "H2")) ")" ) ($#k5_modelc_2 :::"'or'"::: ) (Set "(" (Set (Var "H2")) ($#k4_modelc_2 :::"'&'"::: ) (Set "(" ($#k6_modelc_2 :::"'X'"::: ) (Set "(" (Set (Var "H1")) ($#k8_modelc_2 :::"'R'"::: ) (Set (Var "H2")) ")" ) ")" ) ")" ))) ")" ))) ; theorem :: MODELC_2:77 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r8_modelc_2 :::"|="::: ) (Set ($#k48_modelc_2 :::"'X'"::: ) (Set (Var "W")))) "iff" (Bool (Set ($#k29_modelc_2 :::"Shift"::: ) "(" (Set (Var "r")) "," (Num 1) ")" ) ($#r8_modelc_2 :::"|="::: ) (Set (Var "W"))) ")" ))) ; theorem :: MODELC_2:78 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "H")) "is" ($#v2_modelc_2 :::"atomic"::: ) )) "implies" (Bool "(" (Bool (Bool "not" (Set (Var "H")) "is" ($#v3_modelc_2 :::"negative"::: ) )) & (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"::: ) )) ")" ) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v3_modelc_2 :::"negative"::: ) )) "implies" (Bool "(" (Bool (Bool "not" (Set (Var "H")) "is" ($#v2_modelc_2 :::"atomic"::: ) )) & (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"::: ) )) ")" ) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v4_modelc_2 :::"conjunctive"::: ) )) "implies" (Bool "(" (Bool (Bool "not" (Set (Var "H")) "is" ($#v2_modelc_2 :::"atomic"::: ) )) & (Bool (Bool "not" (Set (Var "H")) "is" ($#v3_modelc_2 :::"negative"::: ) )) & (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"::: ) )) ")" ) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v5_modelc_2 :::"disjunctive"::: ) )) "implies" (Bool "(" (Bool (Bool "not" (Set (Var "H")) "is" ($#v2_modelc_2 :::"atomic"::: ) )) & (Bool (Bool "not" (Set (Var "H")) "is" ($#v3_modelc_2 :::"negative"::: ) )) & (Bool (Bool "not" (Set (Var "H")) "is" ($#v4_modelc_2 :::"conjunctive"::: ) )) & (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"::: ) )) ")" ) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v6_modelc_2 :::"next"::: ) )) "implies" (Bool "(" (Bool (Bool "not" (Set (Var "H")) "is" ($#v2_modelc_2 :::"atomic"::: ) )) & (Bool (Bool "not" (Set (Var "H")) "is" ($#v3_modelc_2 :::"negative"::: ) )) & (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" ($#v7_modelc_2 :::"Until"::: ) )) & (Bool (Bool "not" (Set (Var "H")) "is" ($#v8_modelc_2 :::"Release"::: ) )) ")" ) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v7_modelc_2 :::"Until"::: ) )) "implies" (Bool "(" (Bool (Bool "not" (Set (Var "H")) "is" ($#v2_modelc_2 :::"atomic"::: ) )) & (Bool (Bool "not" (Set (Var "H")) "is" ($#v3_modelc_2 :::"negative"::: ) )) & (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" ($#v8_modelc_2 :::"Release"::: ) )) ")" ) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v8_modelc_2 :::"Release"::: ) )) "implies" (Bool "(" (Bool (Bool "not" (Set (Var "H")) "is" ($#v2_modelc_2 :::"atomic"::: ) )) & (Bool (Bool "not" (Set (Var "H")) "is" ($#v3_modelc_2 :::"negative"::: ) )) & (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"::: ) )) ")" ) ")" ")" )) ; theorem :: MODELC_2:79 (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S"))) "holds" (Bool (Set ($#k29_modelc_2 :::"Shift"::: ) "(" (Set (Var "t")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "t"))))) ; theorem :: MODELC_2:80 (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S"))) "holds" (Bool (Set ($#k29_modelc_2 :::"Shift"::: ) "(" (Set "(" ($#k29_modelc_2 :::"Shift"::: ) "(" (Set (Var "seq")) "," (Set (Var "k")) ")" ")" ) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k29_modelc_2 :::"Shift"::: ) "(" (Set (Var "seq")) "," (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "k")) ")" ) ")" ))))) ; theorem :: MODELC_2:81 (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k27_modelc_2 :::"CastSeq"::: ) "(" (Set "(" ($#k26_modelc_2 :::"CastSeq"::: ) (Set (Var "seq")) ")" ) "," (Set (Var "S")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Var "seq"))))) ; theorem :: MODELC_2:82 (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set (Var "S"))) "holds" (Bool (Set ($#k26_modelc_2 :::"CastSeq"::: ) (Set "(" ($#k27_modelc_2 :::"CastSeq"::: ) "(" (Set (Var "seq")) "," (Set (Var "S")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "seq"))))) ; theorem :: MODELC_2:83 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"LTL-formula":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k25_modelc_2 :::"Inf_seq"::: ) (Set ($#k43_modelc_2 :::"AtomicFamily"::: ) )) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k9_modelc_2 :::"LTL_WFF"::: ) ) "st" (Bool (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) & (Bool (Set ($#k3_modelc_2 :::"'not'"::: ) (Set (Var "H"))) ($#r2_hidden :::"in"::: ) (Set (Var "W")))) "holds" (Bool (Set (Var "r")) ($#r8_modelc_2 :::"|/="::: ) (Set (Var "W")))))) ;