:: LTLAXIO1 semantic presentation begin theorem :: LTLAXIO1:1 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k6_xboolean :::"=>"::: ) (Set "(" (Set (Var "b")) ($#k4_xboolean :::"'&'"::: ) (Set (Var "c")) ")" ) ")" ) ($#k6_xboolean :::"=>"::: ) (Set "(" (Set (Var "a")) ($#k6_xboolean :::"=>"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: LTLAXIO1:2 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k6_xboolean :::"=>"::: ) (Set "(" (Set (Var "b")) ($#k6_xboolean :::"=>"::: ) (Set (Var "c")) ")" ) ")" ) ($#k6_xboolean :::"=>"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k4_xboolean :::"'&'"::: ) (Set (Var "b")) ")" ) ($#k6_xboolean :::"=>"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: LTLAXIO1:3 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k4_xboolean :::"'&'"::: ) (Set (Var "b")) ")" ) ($#k6_xboolean :::"=>"::: ) (Set (Var "c")) ")" ) ($#k6_xboolean :::"=>"::: ) (Set "(" (Set (Var "a")) ($#k6_xboolean :::"=>"::: ) (Set "(" (Set (Var "b")) ($#k6_xboolean :::"=>"::: ) (Set (Var "c")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) ; begin notationsynonym :::"LTLB_WFF"::: for :::"HP-WFF"::: ; end; notationsynonym :::"TFALSUM"::: for :::"VERUM"::: ; end; notationlet "p", "q" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ); synonym "p" :::"'Us'"::: "q" for "p" :::"'&'"::: "q"; end; theorem :: LTLAXIO1:4 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_hilbert1 :::"TFALSUM"::: ) )) "or" (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_hilbert2 :::"prop"::: ) (Set (Var "n")))) "or" (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")))) "or" (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "q"))))) ")" )) ")" )) ")" )) ; definitionlet "p" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ); func :::"'not'"::: "p" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) equals :: LTLAXIO1:def 1 (Set "p" ($#k3_hilbert1 :::"=>"::: ) (Set ($#k2_hilbert1 :::"TFALSUM"::: ) )); func :::"'X'"::: "p" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) equals :: LTLAXIO1:def 2 (Set (Set ($#k2_hilbert1 :::"TFALSUM"::: ) ) ($#k4_hilbert1 :::"'Us'"::: ) "p"); end; :: deftheorem defines :::"'not'"::: LTLAXIO1:def 1 : (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool (Set ($#k1_ltlaxio1 :::"'not'"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set ($#k2_hilbert1 :::"TFALSUM"::: ) )))); :: deftheorem defines :::"'X'"::: LTLAXIO1:def 2 : (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool (Set ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_hilbert1 :::"TFALSUM"::: ) ) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "p"))))); definitionfunc :::"TVERUM"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) equals :: LTLAXIO1:def 3 (Set ($#k1_ltlaxio1 :::"'not'"::: ) (Set ($#k2_hilbert1 :::"TFALSUM"::: ) )); end; :: deftheorem defines :::"TVERUM"::: LTLAXIO1:def 3 : (Bool (Set ($#k3_ltlaxio1 :::"TVERUM"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_ltlaxio1 :::"'not'"::: ) (Set ($#k2_hilbert1 :::"TFALSUM"::: ) ))); definitionlet "p", "q" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ); func "p" :::"'&&'"::: "q" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) equals :: LTLAXIO1:def 4 (Set (Set "(" "p" ($#k3_hilbert1 :::"=>"::: ) (Set "(" "q" ($#k3_hilbert1 :::"=>"::: ) (Set ($#k2_hilbert1 :::"TFALSUM"::: ) ) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set ($#k2_hilbert1 :::"TFALSUM"::: ) )); end; :: deftheorem defines :::"'&&'"::: LTLAXIO1:def 4 : (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k4_ltlaxio1 :::"'&&'"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_hilbert1 :::"=>"::: ) (Set ($#k2_hilbert1 :::"TFALSUM"::: ) ) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set ($#k2_hilbert1 :::"TFALSUM"::: ) )))); definitionlet "p", "q" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ); func "p" :::"'or'"::: "q" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) equals :: LTLAXIO1:def 5 (Set ($#k1_ltlaxio1 :::"'not'"::: ) (Set "(" (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) "p" ")" ) ($#k4_ltlaxio1 :::"'&&'"::: ) (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) "q" ")" ) ")" )); end; :: deftheorem defines :::"'or'"::: LTLAXIO1:def 5 : (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k5_ltlaxio1 :::"'or'"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ltlaxio1 :::"'not'"::: ) (Set "(" (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) (Set (Var "p")) ")" ) ($#k4_ltlaxio1 :::"'&&'"::: ) (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) (Set (Var "q")) ")" ) ")" )))); definitionlet "p" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ); func :::"'G'"::: "p" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) equals :: LTLAXIO1:def 6 (Set ($#k1_ltlaxio1 :::"'not'"::: ) (Set "(" (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) "p" ")" ) ($#k5_ltlaxio1 :::"'or'"::: ) (Set "(" (Set ($#k3_ltlaxio1 :::"TVERUM"::: ) ) ($#k4_ltlaxio1 :::"'&&'"::: ) (Set "(" (Set ($#k3_ltlaxio1 :::"TVERUM"::: ) ) ($#k4_hilbert1 :::"'Us'"::: ) (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) "p" ")" ) ")" ) ")" ) ")" )); end; :: deftheorem defines :::"'G'"::: LTLAXIO1:def 6 : (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool (Set ($#k6_ltlaxio1 :::"'G'"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ltlaxio1 :::"'not'"::: ) (Set "(" (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) (Set (Var "p")) ")" ) ($#k5_ltlaxio1 :::"'or'"::: ) (Set "(" (Set ($#k3_ltlaxio1 :::"TVERUM"::: ) ) ($#k4_ltlaxio1 :::"'&&'"::: ) (Set "(" (Set ($#k3_ltlaxio1 :::"TVERUM"::: ) ) ($#k4_hilbert1 :::"'Us'"::: ) (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) (Set (Var "p")) ")" ) ")" ) ")" ) ")" )))); definitionlet "p" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ); func :::"'F'"::: "p" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) equals :: LTLAXIO1:def 7 (Set ($#k1_ltlaxio1 :::"'not'"::: ) (Set "(" ($#k6_ltlaxio1 :::"'G'"::: ) (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) "p" ")" ) ")" )); end; :: deftheorem defines :::"'F'"::: LTLAXIO1:def 7 : (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool (Set ($#k7_ltlaxio1 :::"'F'"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ltlaxio1 :::"'not'"::: ) (Set "(" ($#k6_ltlaxio1 :::"'G'"::: ) (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) (Set (Var "p")) ")" ) ")" )))); definitionlet "p", "q" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ); func "p" :::"'U'"::: "q" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) equals :: LTLAXIO1:def 8 (Set "q" ($#k5_ltlaxio1 :::"'or'"::: ) (Set "(" "p" ($#k4_ltlaxio1 :::"'&&'"::: ) (Set "(" "p" ($#k4_hilbert1 :::"'Us'"::: ) "q" ")" ) ")" )); end; :: deftheorem defines :::"'U'"::: LTLAXIO1:def 8 : (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k8_ltlaxio1 :::"'U'"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k5_ltlaxio1 :::"'or'"::: ) (Set "(" (Set (Var "p")) ($#k4_ltlaxio1 :::"'&&'"::: ) (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "q")) ")" ) ")" )))); definitionlet "p", "q" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ); func "p" :::"'R'"::: "q" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) equals :: LTLAXIO1:def 9 (Set ($#k1_ltlaxio1 :::"'not'"::: ) (Set "(" (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) "p" ")" ) ($#k8_ltlaxio1 :::"'U'"::: ) (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) "q" ")" ) ")" )); end; :: deftheorem defines :::"'R'"::: LTLAXIO1:def 9 : (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k9_ltlaxio1 :::"'R'"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ltlaxio1 :::"'not'"::: ) (Set "(" (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) (Set (Var "p")) ")" ) ($#k8_ltlaxio1 :::"'U'"::: ) (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) (Set (Var "q")) ")" ) ")" )))); begin definitionfunc :::"props"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) means :: LTLAXIO1:def 10 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_hilbert2 :::"prop"::: ) (Set (Var "n"))))) ")" )); end; :: deftheorem defines :::"props"::: LTLAXIO1:def 10 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k10_ltlaxio1 :::"props"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) "iff" (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_hilbert2 :::"prop"::: ) (Set (Var "n"))))) ")" )) ")" )); definitionmode LTLModel is ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k10_ltlaxio1 :::"props"::: ) ) ")" ); end; definitionlet "M" be ($#m1_subset_1 :::"LTLModel":::); func :::"SAT"::: "M" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: LTLAXIO1:def 11 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set ($#k2_hilbert1 :::"TFALSUM"::: ) ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set "(" ($#k1_hilbert2 :::"prop"::: ) (Set (Var "k")) ")" ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) "iff" (Bool (Set ($#k1_hilbert2 :::"prop"::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) (Set "M" ($#k3_funct_2 :::"."::: ) (Set (Var "n")))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool "(" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" it ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set (Var "p")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ($#k6_xboolean :::"=>"::: ) (Set "(" it ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set (Var "q")) ($#k1_domain_1 :::"]"::: ) ) ")" ))) & "(" (Bool (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "q")) ")" ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1))) "implies" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) & (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "i")) ")" ) "," (Set (Var "q")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i")))) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "j")) ")" ) "," (Set (Var "p")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ")" )) ")" & "(" (Bool (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) & (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "i")) ")" ) "," (Set (Var "q")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i")))) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "j")) ")" ) "," (Set (Var "p")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ")" ))) "implies" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "q")) ")" ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ")" ) ")" ) ")" )); end; :: deftheorem defines :::"SAT"::: LTLAXIO1:def 11 : (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"LTLModel":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set ($#k2_hilbert1 :::"TFALSUM"::: ) ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set "(" ($#k1_hilbert2 :::"prop"::: ) (Set (Var "k")) ")" ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) "iff" (Bool (Set ($#k1_hilbert2 :::"prop"::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "M")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set (Var "p")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ($#k6_xboolean :::"=>"::: ) (Set "(" (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set (Var "q")) ($#k1_domain_1 :::"]"::: ) ) ")" ))) & "(" (Bool (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "q")) ")" ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1))) "implies" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "i")) ")" ) "," (Set (Var "q")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i")))) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "j")) ")" ) "," (Set (Var "p")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ")" )) ")" & "(" (Bool (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "i")) ")" ) "," (Set (Var "q")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i")))) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "j")) ")" ) "," (Set (Var "p")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ")" ))) "implies" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "q")) ")" ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ")" ) ")" ) ")" )) ")" ))); theorem :: LTLAXIO1:5 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"LTLModel":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) (Set (Var "A")) ")" ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) "iff" (Bool (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set (Var "A")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))) ; theorem :: LTLAXIO1:6 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"LTLModel":::) "holds" (Bool (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set ($#k3_ltlaxio1 :::"TVERUM"::: ) ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)))) ; theorem :: LTLAXIO1:7 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"LTLModel":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set "(" (Set (Var "A")) ($#k4_ltlaxio1 :::"'&&'"::: ) (Set (Var "B")) ")" ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) "iff" (Bool "(" (Bool (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set (Var "A")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set (Var "B")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ")" )))) ; theorem :: LTLAXIO1:8 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"LTLModel":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set "(" (Set (Var "A")) ($#k5_ltlaxio1 :::"'or'"::: ) (Set (Var "B")) ")" ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) "iff" (Bool "(" (Bool (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set (Var "A")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) "or" (Bool (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set (Var "B")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ")" )))) ; theorem :: LTLAXIO1:9 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"LTLModel":::) "holds" (Bool (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "A")) ")" ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "A")) ($#k1_domain_1 :::"]"::: ) )))))) ; theorem :: LTLAXIO1:10 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"LTLModel":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set "(" ($#k6_ltlaxio1 :::"'G'"::: ) (Set (Var "A")) ")" ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "i")) ")" ) "," (Set (Var "A")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1))) ")" )))) ; theorem :: LTLAXIO1:11 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"LTLModel":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set "(" ($#k7_ltlaxio1 :::"'F'"::: ) (Set (Var "A")) ")" ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) "iff" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "i")) ")" ) "," (Set (Var "A")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1))) ")" )))) ; theorem :: LTLAXIO1:12 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"LTLModel":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set "(" (Set (Var "p")) ($#k8_ltlaxio1 :::"'U'"::: ) (Set (Var "q")) ")" ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) "iff" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "i")) ")" ) "," (Set (Var "q")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i")))) "holds" (Bool (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "j")) ")" ) "," (Set (Var "p")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ")" )) ")" )))) ; theorem :: LTLAXIO1:13 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"LTLModel":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set "(" (Set (Var "p")) ($#k9_ltlaxio1 :::"'R'"::: ) (Set (Var "q")) ")" ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) "iff" (Bool "(" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "i")) ")" ) "," (Set (Var "p")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i")))) "holds" (Bool (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "j")) ")" ) "," (Set (Var "q")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ")" )) "or" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "i")) ")" ) "," (Set (Var "q")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1))) ")" ) ")" )))) ; theorem :: LTLAXIO1:14 (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"LTLModel":::) "holds" (Bool (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "B")) ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) (Set (Var "B")) ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) )))))) ; theorem :: LTLAXIO1:15 (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"LTLModel":::) "holds" (Bool (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set "(" (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "B")) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) (Set (Var "B")) ")" ) ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1))))) ; theorem :: LTLAXIO1:16 (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"LTLModel":::) "holds" (Bool (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set "(" (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) (Set (Var "B")) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "B")) ")" ) ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1))))) ; theorem :: LTLAXIO1:17 (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"LTLModel":::) "holds" (Bool (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set "(" (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" (Set (Var "B")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "C")) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "B")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "C")) ")" ) ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1))))) ; theorem :: LTLAXIO1:18 (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"LTLModel":::) "holds" (Bool (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set "(" (Set "(" ($#k6_ltlaxio1 :::"'G'"::: ) (Set (Var "B")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "B")) ($#k4_ltlaxio1 :::"'&&'"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" ($#k6_ltlaxio1 :::"'G'"::: ) (Set (Var "B")) ")" ) ")" ) ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1))))) ; theorem :: LTLAXIO1:19 (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"LTLModel":::) "holds" (Bool (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set "(" (Set "(" (Set (Var "B")) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "C")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "C")) ")" ) ($#k5_ltlaxio1 :::"'or'"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" (Set (Var "B")) ($#k4_ltlaxio1 :::"'&&'"::: ) (Set "(" (Set (Var "B")) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "C")) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1))))) ; theorem :: LTLAXIO1:20 (Bool "for" (Set (Var "C")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"LTLModel":::) "holds" (Bool (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set "(" (Set "(" (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "C")) ")" ) ($#k5_ltlaxio1 :::"'or'"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" (Set (Var "B")) ($#k4_ltlaxio1 :::"'&&'"::: ) (Set "(" (Set (Var "B")) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "C")) ")" ) ")" ) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "B")) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "C")) ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1))))) ; theorem :: LTLAXIO1:21 (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"LTLModel":::) "holds" (Bool (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set "(" (Set "(" (Set (Var "B")) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "C")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" ($#k7_ltlaxio1 :::"'F'"::: ) (Set (Var "C")) ")" ) ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1))))) ; begin definitionlet "M" be ($#m1_subset_1 :::"LTLModel":::); let "p" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ); pred "M" :::"|="::: "p" means :: LTLAXIO1:def 12 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) "M" ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," "p" ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1))); end; :: deftheorem defines :::"|="::: LTLAXIO1:def 12 : (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"LTLModel":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Var "M")) ($#r1_ltlaxio1 :::"|="::: ) (Set (Var "p"))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set (Var "p")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1))) ")" ))); definitionlet "M" be ($#m1_subset_1 :::"LTLModel":::); let "F" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ); pred "M" :::"|="::: "F" means :: LTLAXIO1:def 13 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "F")) "holds" (Bool "M" ($#r1_ltlaxio1 :::"|="::: ) (Set (Var "p")))); end; :: deftheorem defines :::"|="::: LTLAXIO1:def 13 : (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"LTLModel":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Var "M")) ($#r2_ltlaxio1 :::"|="::: ) (Set (Var "F"))) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "M")) ($#r1_ltlaxio1 :::"|="::: ) (Set (Var "p")))) ")" ))); definitionlet "F" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ); let "p" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ); pred "F" :::"|="::: "p" means :: LTLAXIO1:def 14 (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"LTLModel":::) "st" (Bool (Bool (Set (Var "M")) ($#r2_ltlaxio1 :::"|="::: ) "F")) "holds" (Bool (Set (Var "M")) ($#r1_ltlaxio1 :::"|="::: ) "p")); end; :: deftheorem defines :::"|="::: LTLAXIO1:def 14 : (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r3_ltlaxio1 :::"|="::: ) (Set (Var "p"))) "iff" (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"LTLModel":::) "st" (Bool (Bool (Set (Var "M")) ($#r2_ltlaxio1 :::"|="::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "M")) ($#r1_ltlaxio1 :::"|="::: ) (Set (Var "p")))) ")" ))); theorem :: LTLAXIO1:22 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"LTLModel":::) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "M")) ($#r2_ltlaxio1 :::"|="::: ) (Set (Var "F"))) & (Bool (Set (Var "M")) ($#r2_ltlaxio1 :::"|="::: ) (Set (Var "G"))) ")" ) "iff" (Bool (Set (Var "M")) ($#r2_ltlaxio1 :::"|="::: ) (Set (Set (Var "F")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "G")))) ")" ))) ; theorem :: LTLAXIO1:23 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"LTLModel":::) "holds" (Bool "(" (Bool (Set (Var "M")) ($#r1_ltlaxio1 :::"|="::: ) (Set (Var "A"))) "iff" (Bool (Set (Var "M")) ($#r2_ltlaxio1 :::"|="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "A")) ($#k6_domain_1 :::"}"::: ) )) ")" ))) ; theorem :: LTLAXIO1:24 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r3_ltlaxio1 :::"|="::: ) (Set (Var "A"))) & (Bool (Set (Var "F")) ($#r3_ltlaxio1 :::"|="::: ) (Set (Set (Var "A")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "B"))))) "holds" (Bool (Set (Var "F")) ($#r3_ltlaxio1 :::"|="::: ) (Set (Var "B"))))) ; theorem :: LTLAXIO1:25 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r3_ltlaxio1 :::"|="::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "F")) ($#r3_ltlaxio1 :::"|="::: ) (Set ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "A")))))) ; theorem :: LTLAXIO1:26 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r3_ltlaxio1 :::"|="::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "F")) ($#r3_ltlaxio1 :::"|="::: ) (Set ($#k6_ltlaxio1 :::"'G'"::: ) (Set (Var "A")))))) ; theorem :: LTLAXIO1:27 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r3_ltlaxio1 :::"|="::: ) (Set (Set (Var "A")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "B")))) & (Bool (Set (Var "F")) ($#r3_ltlaxio1 :::"|="::: ) (Set (Set (Var "A")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "A")) ")" )))) "holds" (Bool (Set (Var "F")) ($#r3_ltlaxio1 :::"|="::: ) (Set (Set (Var "A")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" ($#k6_ltlaxio1 :::"'G'"::: ) (Set (Var "B")) ")" ))))) ; theorem :: LTLAXIO1:28 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"LTLModel":::) "holds" (Bool (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set "(" (Set (Var "M")) ($#k10_nat_1 :::"^\"::: ) (Set (Var "i")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "j")) "," (Set (Var "A")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Set (Var "j")) ")" ) "," (Set (Var "A")) ($#k1_domain_1 :::"]"::: ) )))))) ; theorem :: LTLAXIO1:29 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"LTLModel":::) "st" (Bool (Bool (Set (Var "M")) ($#r2_ltlaxio1 :::"|="::: ) (Set (Var "F")))) "holds" (Bool (Set (Set (Var "M")) ($#k10_nat_1 :::"^\"::: ) (Set (Var "i"))) ($#r2_ltlaxio1 :::"|="::: ) (Set (Var "F")))))) ; theorem :: LTLAXIO1:30 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "A")) ($#k6_domain_1 :::"}"::: ) )) ($#r3_ltlaxio1 :::"|="::: ) (Set (Var "B"))) "iff" (Bool (Set (Var "F")) ($#r3_ltlaxio1 :::"|="::: ) (Set (Set "(" ($#k6_ltlaxio1 :::"'G'"::: ) (Set (Var "A")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "B")))) ")" ))) ; definitionlet "f" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); func :::"VAL"::: "f" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: LTLAXIO1:def 15 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set ($#k2_hilbert1 :::"TFALSUM"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set "(" ($#k1_hilbert2 :::"prop"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set "f" ($#k3_funct_2 :::"."::: ) (Set "(" ($#k1_hilbert2 :::"prop"::: ) (Set (Var "n")) ")" ))) & (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "A")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" it ($#k3_funct_2 :::"."::: ) (Set (Var "A")) ")" ) ($#k6_xboolean :::"=>"::: ) (Set "(" it ($#k3_funct_2 :::"."::: ) (Set (Var "B")) ")" ))) & (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "A")) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set "f" ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "A")) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "B")) ")" ))) ")" ))); end; :: deftheorem defines :::"VAL"::: LTLAXIO1:def 15 : (Bool "for" (Set (Var "f")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k12_ltlaxio1 :::"VAL"::: ) (Set (Var "f")))) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set ($#k2_hilbert1 :::"TFALSUM"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k1_hilbert2 :::"prop"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k1_hilbert2 :::"prop"::: ) (Set (Var "n")) ")" ))) & (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "A")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "A")) ")" ) ($#k6_xboolean :::"=>"::: ) (Set "(" (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "B")) ")" ))) & (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "A")) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "A")) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "B")) ")" ))) ")" ))) ")" )); theorem :: LTLAXIO1:31 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool (Set (Set "(" ($#k12_ltlaxio1 :::"VAL"::: ) (Set (Var "f")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "p")) ($#k4_ltlaxio1 :::"'&&'"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k12_ltlaxio1 :::"VAL"::: ) (Set (Var "f")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" (Set "(" ($#k12_ltlaxio1 :::"VAL"::: ) (Set (Var "f")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "q")) ")" ))))) ; theorem :: LTLAXIO1:32 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"LTLModel":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "n")) "," (Set (Var "B")) ($#k4_tarski :::"]"::: ) ))) ")" )) "holds" (Bool (Set (Set "(" ($#k12_ltlaxio1 :::"VAL"::: ) (Set (Var "f")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_ltlaxio1 :::"SAT"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set (Var "A")) ($#k1_domain_1 :::"]"::: ) ))))))) ; definitionlet "p" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ); attr "p" is :::"LTL_TAUT_OF_PL"::: means :: LTLAXIO1:def 16 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set "(" ($#k12_ltlaxio1 :::"VAL"::: ) (Set (Var "f")) ")" ) ($#k3_funct_2 :::"."::: ) "p") ($#r1_hidden :::"="::: ) (Num 1))); end; :: deftheorem defines :::"LTL_TAUT_OF_PL"::: LTLAXIO1:def 16 : (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v1_ltlaxio1 :::"LTL_TAUT_OF_PL"::: ) ) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set "(" ($#k12_ltlaxio1 :::"VAL"::: ) (Set (Var "f")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Num 1))) ")" )); theorem :: LTLAXIO1:33 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_ltlaxio1 :::"LTL_TAUT_OF_PL"::: ) )) "holds" (Bool (Set (Var "F")) ($#r3_ltlaxio1 :::"|="::: ) (Set (Var "A"))))) ; begin definitionlet "D" be ($#m1_hidden :::"set"::: ) ; attr "D" is :::"with_LTL_axioms"::: means :: LTLAXIO1:def 17 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "p")) "is" ($#v1_ltlaxio1 :::"LTL_TAUT_OF_PL"::: ) )) "implies" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "D") ")" & (Bool (Set (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "p")) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) (Set (Var "p")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) "D") & (Bool (Set (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) (Set (Var "p")) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "p")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) "D") & (Bool (Set (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "p")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "q")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) "D") & (Bool (Set (Set "(" ($#k6_ltlaxio1 :::"'G'"::: ) (Set (Var "p")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k4_ltlaxio1 :::"'&&'"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" ($#k6_ltlaxio1 :::"'G'"::: ) (Set (Var "p")) ")" ) ")" ) ")" )) ($#r2_hidden :::"in"::: ) "D") & (Bool (Set (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "q")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "q")) ")" ) ($#k5_ltlaxio1 :::"'or'"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" (Set (Var "p")) ($#k4_ltlaxio1 :::"'&&'"::: ) (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ")" )) ($#r2_hidden :::"in"::: ) "D") & (Bool (Set (Set "(" (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "q")) ")" ) ($#k5_ltlaxio1 :::"'or'"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" (Set (Var "p")) ($#k4_ltlaxio1 :::"'&&'"::: ) (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) "D") & (Bool (Set (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "q")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" ($#k7_ltlaxio1 :::"'F'"::: ) (Set (Var "q")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) "D") ")" )); end; :: deftheorem defines :::"with_LTL_axioms"::: LTLAXIO1:def 17 : (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "D")) "is" ($#v2_ltlaxio1 :::"with_LTL_axioms"::: ) ) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "p")) "is" ($#v1_ltlaxio1 :::"LTL_TAUT_OF_PL"::: ) )) "implies" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" & (Bool (Set (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "p")) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) (Set (Var "p")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) (Set (Var "p")) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "p")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "p")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "q")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Set "(" ($#k6_ltlaxio1 :::"'G'"::: ) (Set (Var "p")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k4_ltlaxio1 :::"'&&'"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" ($#k6_ltlaxio1 :::"'G'"::: ) (Set (Var "p")) ")" ) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "q")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "q")) ")" ) ($#k5_ltlaxio1 :::"'or'"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" (Set (Var "p")) ($#k4_ltlaxio1 :::"'&&'"::: ) (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Set "(" (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "q")) ")" ) ($#k5_ltlaxio1 :::"'or'"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" (Set (Var "p")) ($#k4_ltlaxio1 :::"'&&'"::: ) (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "q")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" ($#k7_ltlaxio1 :::"'F'"::: ) (Set (Var "q")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" )) ")" )); definitionfunc :::"LTL_axioms"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) means :: LTLAXIO1:def 18 (Bool "(" (Bool it "is" ($#v2_ltlaxio1 :::"with_LTL_axioms"::: ) ) & (Bool "(" "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Bool (Set (Var "D")) "is" ($#v2_ltlaxio1 :::"with_LTL_axioms"::: ) )) "holds" (Bool it ($#r1_tarski :::"c="::: ) (Set (Var "D"))) ")" ) ")" ); end; :: deftheorem defines :::"LTL_axioms"::: LTLAXIO1:def 18 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k13_ltlaxio1 :::"LTL_axioms"::: ) )) "iff" (Bool "(" (Bool (Set (Var "b1")) "is" ($#v2_ltlaxio1 :::"with_LTL_axioms"::: ) ) & (Bool "(" "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Bool (Set (Var "D")) "is" ($#v2_ltlaxio1 :::"with_LTL_axioms"::: ) )) "holds" (Bool (Set (Var "b1")) ($#r1_tarski :::"c="::: ) (Set (Var "D"))) ")" ) ")" ) ")" )); registration cluster (Set ($#k13_ltlaxio1 :::"LTL_axioms"::: ) ) -> ($#v2_ltlaxio1 :::"with_LTL_axioms"::: ) ; end; theorem :: LTLAXIO1:34 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k13_ltlaxio1 :::"LTL_axioms"::: ) ))) ; theorem :: LTLAXIO1:35 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k13_ltlaxio1 :::"LTL_axioms"::: ) ))) ; definitionlet "p", "q" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ); pred "p" :::"NEX_rule"::: "q" means :: LTLAXIO1:def 19 (Bool "q" ($#r1_hidden :::"="::: ) (Set ($#k2_ltlaxio1 :::"'X'"::: ) "p")); let "r" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ); pred "p" "," "q" :::"MP_rule"::: "r" means :: LTLAXIO1:def 20 (Bool "q" ($#r1_hidden :::"="::: ) (Set "p" ($#k3_hilbert1 :::"=>"::: ) "r")); pred "p" "," "q" :::"IND_rule"::: "r" means :: LTLAXIO1:def 21 (Bool "ex" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool "(" (Bool "p" ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "B")))) & (Bool "q" ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "A")) ")" ))) & (Bool "r" ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" ($#k6_ltlaxio1 :::"'G'"::: ) (Set (Var "B")) ")" ))) ")" )); end; :: deftheorem defines :::"NEX_rule"::: LTLAXIO1:def 19 : (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r4_ltlaxio1 :::"NEX_rule"::: ) (Set (Var "q"))) "iff" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "p")))) ")" )); :: deftheorem defines :::"MP_rule"::: LTLAXIO1:def 20 : (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r5_ltlaxio1 :::"MP_rule"::: ) (Set (Var "r"))) "iff" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r")))) ")" )); :: deftheorem defines :::"IND_rule"::: LTLAXIO1:def 21 : (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r6_ltlaxio1 :::"IND_rule"::: ) (Set (Var "r"))) "iff" (Bool "ex" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "B")))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "A")) ")" ))) & (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" ($#k6_ltlaxio1 :::"'G'"::: ) (Set (Var "B")) ")" ))) ")" )) ")" )); registration cluster (Set ($#k13_ltlaxio1 :::"LTL_axioms"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "A" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ); attr "A" is :::"axltl1"::: means :: LTLAXIO1:def 22 (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool "A" ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "B")) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) (Set (Var "B")) ")" ) ")" )))); attr "A" is :::"axltl1a"::: means :: LTLAXIO1:def 23 (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool "A" ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) (Set (Var "B")) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "B")) ")" ) ")" )))); attr "A" is :::"axltl2"::: means :: LTLAXIO1:def 24 (Bool "ex" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool "A" ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" (Set (Var "B")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "C")) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "B")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "C")) ")" ) ")" )))); attr "A" is :::"axltl3"::: means :: LTLAXIO1:def 25 (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool "A" ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_ltlaxio1 :::"'G'"::: ) (Set (Var "B")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "B")) ($#k4_ltlaxio1 :::"'&&'"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" ($#k6_ltlaxio1 :::"'G'"::: ) (Set (Var "B")) ")" ) ")" ) ")" )))); attr "A" is :::"axltl4"::: means :: LTLAXIO1:def 26 (Bool "ex" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool "A" ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "B")) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "C")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "C")) ")" ) ($#k5_ltlaxio1 :::"'or'"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" (Set (Var "B")) ($#k4_ltlaxio1 :::"'&&'"::: ) (Set "(" (Set (Var "B")) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "C")) ")" ) ")" ) ")" ) ")" )))); attr "A" is :::"axltl5"::: means :: LTLAXIO1:def 27 (Bool "ex" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool "A" ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "C")) ")" ) ($#k5_ltlaxio1 :::"'or'"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" (Set (Var "B")) ($#k4_ltlaxio1 :::"'&&'"::: ) (Set "(" (Set (Var "B")) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "C")) ")" ) ")" ) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "B")) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "C")) ")" )))); attr "A" is :::"axltl6"::: means :: LTLAXIO1:def 28 (Bool "ex" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool "A" ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "B")) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "C")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" ($#k7_ltlaxio1 :::"'F'"::: ) (Set (Var "C")) ")" ) ")" )))); end; :: deftheorem defines :::"axltl1"::: LTLAXIO1:def 22 : (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_ltlaxio1 :::"axltl1"::: ) ) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "B")) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) (Set (Var "B")) ")" ) ")" )))) ")" )); :: deftheorem defines :::"axltl1a"::: LTLAXIO1:def 23 : (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v4_ltlaxio1 :::"axltl1a"::: ) ) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) (Set (Var "B")) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "B")) ")" ) ")" )))) ")" )); :: deftheorem defines :::"axltl2"::: LTLAXIO1:def 24 : (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v5_ltlaxio1 :::"axltl2"::: ) ) "iff" (Bool "ex" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" (Set (Var "B")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "C")) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "B")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "C")) ")" ) ")" )))) ")" )); :: deftheorem defines :::"axltl3"::: LTLAXIO1:def 25 : (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v6_ltlaxio1 :::"axltl3"::: ) ) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_ltlaxio1 :::"'G'"::: ) (Set (Var "B")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "B")) ($#k4_ltlaxio1 :::"'&&'"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" ($#k6_ltlaxio1 :::"'G'"::: ) (Set (Var "B")) ")" ) ")" ) ")" )))) ")" )); :: deftheorem defines :::"axltl4"::: LTLAXIO1:def 26 : (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v7_ltlaxio1 :::"axltl4"::: ) ) "iff" (Bool "ex" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "B")) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "C")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "C")) ")" ) ($#k5_ltlaxio1 :::"'or'"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" (Set (Var "B")) ($#k4_ltlaxio1 :::"'&&'"::: ) (Set "(" (Set (Var "B")) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "C")) ")" ) ")" ) ")" ) ")" )))) ")" )); :: deftheorem defines :::"axltl5"::: LTLAXIO1:def 27 : (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v8_ltlaxio1 :::"axltl5"::: ) ) "iff" (Bool "ex" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "C")) ")" ) ($#k5_ltlaxio1 :::"'or'"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" (Set (Var "B")) ($#k4_ltlaxio1 :::"'&&'"::: ) (Set "(" (Set (Var "B")) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "C")) ")" ) ")" ) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "B")) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "C")) ")" )))) ")" )); :: deftheorem defines :::"axltl6"::: LTLAXIO1:def 28 : (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v9_ltlaxio1 :::"axltl6"::: ) ) "iff" (Bool "ex" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "B")) ($#k4_hilbert1 :::"'Us'"::: ) (Set (Var "C")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" ($#k7_ltlaxio1 :::"'F'"::: ) (Set (Var "C")) ")" ) ")" )))) ")" )); theorem :: LTLAXIO1:36 (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k13_ltlaxio1 :::"LTL_axioms"::: ) ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_ltlaxio1 :::"LTL_TAUT_OF_PL"::: ) ) "or" (Bool (Set (Var "A")) "is" ($#v3_ltlaxio1 :::"axltl1"::: ) ) "or" (Bool (Set (Var "A")) "is" ($#v4_ltlaxio1 :::"axltl1a"::: ) ) "or" (Bool (Set (Var "A")) "is" ($#v5_ltlaxio1 :::"axltl2"::: ) ) "or" (Bool (Set (Var "A")) "is" ($#v6_ltlaxio1 :::"axltl3"::: ) ) "or" (Bool (Set (Var "A")) "is" ($#v7_ltlaxio1 :::"axltl4"::: ) ) "or" (Bool (Set (Var "A")) "is" ($#v8_ltlaxio1 :::"axltl5"::: ) ) "or" (Bool (Set (Var "A")) "is" ($#v9_ltlaxio1 :::"axltl6"::: ) ) ")" )) ; theorem :: LTLAXIO1:37 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_ltlaxio1 :::"axltl1"::: ) ) "or" (Bool (Set (Var "A")) "is" ($#v4_ltlaxio1 :::"axltl1a"::: ) ) "or" (Bool (Set (Var "A")) "is" ($#v5_ltlaxio1 :::"axltl2"::: ) ) "or" (Bool (Set (Var "A")) "is" ($#v6_ltlaxio1 :::"axltl3"::: ) ) "or" (Bool (Set (Var "A")) "is" ($#v7_ltlaxio1 :::"axltl4"::: ) ) "or" (Bool (Set (Var "A")) "is" ($#v8_ltlaxio1 :::"axltl5"::: ) ) "or" (Bool (Set (Var "A")) "is" ($#v9_ltlaxio1 :::"axltl6"::: ) ) ")" )) "holds" (Bool (Set (Var "F")) ($#r3_ltlaxio1 :::"|="::: ) (Set (Var "A"))))) ; definitionlet "i" be ($#m1_hidden :::"Nat":::); let "f" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ); let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ); pred :::"prc"::: "f" "," "X" "," "i" means :: LTLAXIO1:def 29 (Bool "(" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) "i") ($#r2_hidden :::"in"::: ) (Set ($#k13_ltlaxio1 :::"LTL_axioms"::: ) )) "or" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) "i") ($#r2_hidden :::"in"::: ) "X") "or" (Bool "ex" (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) "i") & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) "i") & (Bool "(" (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Set (Var "j"))) "," (Set "f" ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r5_ltlaxio1 :::"MP_rule"::: ) (Set "f" ($#k7_partfun1 :::"/."::: ) "i")) "or" (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Set (Var "j"))) "," (Set "f" ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r6_ltlaxio1 :::"IND_rule"::: ) (Set "f" ($#k7_partfun1 :::"/."::: ) "i")) ")" ) ")" )) "or" (Bool "ex" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) "i") & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Set (Var "j"))) ($#r4_ltlaxio1 :::"NEX_rule"::: ) (Set "f" ($#k7_partfun1 :::"/."::: ) "i")) ")" )) ")" ); end; :: deftheorem defines :::"prc"::: LTLAXIO1:def 29 : (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool "(" (Bool ($#r7_ltlaxio1 :::"prc"::: ) (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "i"))) "iff" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set ($#k13_ltlaxio1 :::"LTL_axioms"::: ) )) "or" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "or" (Bool "ex" (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) & (Bool "(" (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "j"))) "," (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r5_ltlaxio1 :::"MP_rule"::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")))) "or" (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "j"))) "," (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r6_ltlaxio1 :::"IND_rule"::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")))) ")" ) ")" )) "or" (Bool "ex" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "j"))) ($#r4_ltlaxio1 :::"NEX_rule"::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")))) ")" )) ")" ) ")" )))); definitionlet "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ); let "p" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ); pred "X" :::"|-"::: "p" means :: LTLAXIO1:def 30 (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) "p") & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool ($#r7_ltlaxio1 :::"prc"::: ) (Set (Var "f")) "," "X" "," (Set (Var "i"))) ")" ) ")" )); end; :: deftheorem defines :::"|-"::: LTLAXIO1:def 30 : (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Var "p"))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool ($#r7_ltlaxio1 :::"prc"::: ) (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "i"))) ")" ) ")" )) ")" ))); theorem :: LTLAXIO1:38 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "f")) "," (Set (Var "f2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "i")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f2")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "n")) ")" ))) ")" ) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool ($#r7_ltlaxio1 :::"prc"::: ) (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "i")))) "holds" (Bool ($#r7_ltlaxio1 :::"prc"::: ) (Set (Var "f2")) "," (Set (Var "X")) "," (Set (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "n"))))))) ; theorem :: LTLAXIO1:39 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "f2")) "," (Set (Var "f")) "," (Set (Var "f1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Bool (Set (Var "f2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "f1")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f1")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool ($#r7_ltlaxio1 :::"prc"::: ) (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "i"))) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f1"))))) "holds" (Bool ($#r7_ltlaxio1 :::"prc"::: ) (Set (Var "f1")) "," (Set (Var "X")) "," (Set (Var "i"))) ")" )) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f2"))))) "holds" (Bool ($#r7_ltlaxio1 :::"prc"::: ) (Set (Var "f2")) "," (Set (Var "X")) "," (Set (Var "i")))))) ; theorem :: LTLAXIO1:40 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "f")) "," (Set (Var "f1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) ))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f1")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f1"))))) "holds" (Bool ($#r7_ltlaxio1 :::"prc"::: ) (Set (Var "f1")) "," (Set (Var "X")) "," (Set (Var "i"))) ")" ) & (Bool ($#r7_ltlaxio1 :::"prc"::: ) (Set (Var "f")) "," (Set (Var "X")) "," (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool ($#r7_ltlaxio1 :::"prc"::: ) (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "i"))) ")" ) & (Bool (Set (Var "X")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Var "p"))) ")" )))) ; theorem :: LTLAXIO1:41 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "F")) ($#r3_ltlaxio1 :::"|="::: ) (Set (Var "A"))))) ; begin theorem :: LTLAXIO1:42 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k13_ltlaxio1 :::"LTL_axioms"::: ) )) "or" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )) "holds" (Bool (Set (Var "X")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Var "p"))))) ; theorem :: LTLAXIO1:43 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Var "p"))) & (Bool (Set (Var "X")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Var "X")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Var "q"))))) ; theorem :: LTLAXIO1:44 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Var "p")))) "holds" (Bool (Set (Var "X")) ($#r8_ltlaxio1 :::"|-"::: ) (Set ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "p")))))) ; theorem :: LTLAXIO1:45 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")))) & (Bool (Set (Var "X")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "p")) ")" )))) "holds" (Bool (Set (Var "X")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" ($#k6_ltlaxio1 :::"'G'"::: ) (Set (Var "q")) ")" ))))) ; theorem :: LTLAXIO1:46 (Bool "for" (Set (Var "r")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Set (Var "r")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k4_ltlaxio1 :::"'&&'"::: ) (Set (Var "q")) ")" )))) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Set (Var "r")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "p")))) & (Bool (Set (Var "X")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Set (Var "r")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")))) ")" ))) ; theorem :: LTLAXIO1:47 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")))) & (Bool (Set (Var "X")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Set (Var "q")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r"))))) "holds" (Bool (Set (Var "X")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r")))))) ; theorem :: LTLAXIO1:48 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r")) ")" )))) "holds" (Bool (Set (Var "X")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Set "(" (Set (Var "p")) ($#k4_ltlaxio1 :::"'&&'"::: ) (Set (Var "q")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r")))))) ; theorem :: LTLAXIO1:49 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Set "(" (Set (Var "p")) ($#k4_ltlaxio1 :::"'&&'"::: ) (Set (Var "q")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r"))))) "holds" (Bool (Set (Var "X")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r")) ")" ))))) ; theorem :: LTLAXIO1:50 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Set "(" (Set (Var "p")) ($#k4_ltlaxio1 :::"'&&'"::: ) (Set (Var "q")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r")))) & (Bool (Set (Var "X")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "s"))))) "holds" (Bool (Set (Var "X")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Set "(" (Set (Var "p")) ($#k4_ltlaxio1 :::"'&&'"::: ) (Set (Var "q")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "s")) ($#k4_ltlaxio1 :::"'&&'"::: ) (Set (Var "r")) ")" ))))) ; theorem :: LTLAXIO1:51 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r")) ")" ))) & (Bool (Set (Var "X")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Set (Var "r")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "s"))))) "holds" (Bool (Set (Var "X")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "s")) ")" ))))) ; theorem :: LTLAXIO1:52 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Var "X")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) (Set (Var "q")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" ($#k1_ltlaxio1 :::"'not'"::: ) (Set (Var "p")) ")" ))))) ; theorem :: LTLAXIO1:53 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool (Set (Var "X")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Set "(" (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "p")) ")" ) ($#k4_ltlaxio1 :::"'&&'"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set (Var "q")) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" ($#k2_ltlaxio1 :::"'X'"::: ) (Set "(" (Set (Var "p")) ($#k4_ltlaxio1 :::"'&&'"::: ) (Set (Var "q")) ")" ) ")" ))))) ; theorem :: LTLAXIO1:54 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Var "p")))) "holds" (Bool (Set (Var "F")) ($#r8_ltlaxio1 :::"|-"::: ) (Set ($#k6_ltlaxio1 :::"'G'"::: ) (Set (Var "p")))))) ; theorem :: LTLAXIO1:55 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Set (Var "F")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) )) ($#r8_ltlaxio1 :::"|-"::: ) (Set ($#k6_ltlaxio1 :::"'G'"::: ) (Set (Var "q")))))) ; theorem :: LTLAXIO1:56 (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Var "q")))) "holds" (Bool (Set (Set (Var "F")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) )) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Var "q"))))) ; theorem :: LTLAXIO1:57 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Bool (Set (Set (Var "F")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) )) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Var "q")))) "holds" (Bool (Set (Var "F")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Set "(" ($#k6_ltlaxio1 :::"'G'"::: ) (Set (Var "p")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")))))) ; theorem :: LTLAXIO1:58 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Set (Var "F")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) )) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Var "q"))))) ; theorem :: LTLAXIO1:59 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Set "(" ($#k6_ltlaxio1 :::"'G'"::: ) (Set (Var "p")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Set (Var "F")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) )) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Var "q"))))) ; theorem :: LTLAXIO1:60 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"LTLB_WFF"::: ) ) "holds" (Bool (Set (Var "F")) ($#r8_ltlaxio1 :::"|-"::: ) (Set (Set "(" ($#k6_ltlaxio1 :::"'G'"::: ) (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set "(" ($#k6_ltlaxio1 :::"'G'"::: ) (Set (Var "p")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" ($#k6_ltlaxio1 :::"'G'"::: ) (Set (Var "q")) ")" ) ")" ))))) ;