:: INTPRO_1 semantic presentation begin definitionlet "E" be ($#m1_hidden :::"set"::: ) ; attr "E" is :::"with_FALSUM"::: means :: INTPRO_1:def 1 (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_hidden :::"in"::: ) "E"); end; :: deftheorem defines :::"with_FALSUM"::: INTPRO_1:def 1 : (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "E")) "is" ($#v1_intpro_1 :::"with_FALSUM"::: ) ) "iff" (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "E"))) ")" )); definitionlet "E" be ($#m1_hidden :::"set"::: ) ; attr "E" is :::"with_int_implication"::: means :: INTPRO_1:def 2 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "E") & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) "E")) "holds" (Bool (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) "E")); end; :: deftheorem defines :::"with_int_implication"::: INTPRO_1:def 2 : (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "E")) "is" ($#v2_intpro_1 :::"with_int_implication"::: ) ) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "E"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) "holds" (Bool (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) ")" )); definitionlet "E" be ($#m1_hidden :::"set"::: ) ; attr "E" is :::"with_int_conjunction"::: means :: INTPRO_1:def 3 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "E") & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) "E")) "holds" (Bool (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 2) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) "E")); end; :: deftheorem defines :::"with_int_conjunction"::: INTPRO_1:def 3 : (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "E")) "is" ($#v3_intpro_1 :::"with_int_conjunction"::: ) ) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "E"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) "holds" (Bool (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 2) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) ")" )); definitionlet "E" be ($#m1_hidden :::"set"::: ) ; attr "E" is :::"with_int_disjunction"::: means :: INTPRO_1:def 4 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "E") & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) "E")) "holds" (Bool (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 3) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) "E")); end; :: deftheorem defines :::"with_int_disjunction"::: INTPRO_1:def 4 : (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "E")) "is" ($#v4_intpro_1 :::"with_int_disjunction"::: ) ) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "E"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) "holds" (Bool (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 3) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) ")" )); definitionlet "E" be ($#m1_hidden :::"set"::: ) ; attr "E" is :::"with_int_propositional_variables"::: means :: INTPRO_1:def 5 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Num 5) ($#k2_nat_1 :::"+"::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_hidden :::"in"::: ) "E")); end; :: deftheorem defines :::"with_int_propositional_variables"::: INTPRO_1:def 5 : (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "E")) "is" ($#v5_intpro_1 :::"with_int_propositional_variables"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Num 5) ($#k2_nat_1 :::"+"::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) ")" )); definitionlet "E" be ($#m1_hidden :::"set"::: ) ; attr "E" is :::"with_modal_operator"::: means :: INTPRO_1:def 6 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "E")) "holds" (Bool (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Num 6) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) "E")); end; :: deftheorem defines :::"with_modal_operator"::: INTPRO_1:def 6 : (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "E")) "is" ($#v6_intpro_1 :::"with_modal_operator"::: ) ) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) "holds" (Bool (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Num 6) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) ")" )); definitionlet "E" be ($#m1_hidden :::"set"::: ) ; attr "E" is :::"MC-closed"::: means :: INTPRO_1:def 7 (Bool "(" (Bool "E" ($#r1_tarski :::"c="::: ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k13_finseq_1 :::"*"::: ) )) & (Bool "E" "is" ($#v1_intpro_1 :::"with_FALSUM"::: ) ) & (Bool "E" "is" ($#v2_intpro_1 :::"with_int_implication"::: ) ) & (Bool "E" "is" ($#v3_intpro_1 :::"with_int_conjunction"::: ) ) & (Bool "E" "is" ($#v4_intpro_1 :::"with_int_disjunction"::: ) ) & (Bool "E" "is" ($#v5_intpro_1 :::"with_int_propositional_variables"::: ) ) & (Bool "E" "is" ($#v6_intpro_1 :::"with_modal_operator"::: ) ) ")" ); end; :: deftheorem defines :::"MC-closed"::: INTPRO_1:def 7 : (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "E")) "is" ($#v7_intpro_1 :::"MC-closed"::: ) ) "iff" (Bool "(" (Bool (Set (Var "E")) ($#r1_tarski :::"c="::: ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k13_finseq_1 :::"*"::: ) )) & (Bool (Set (Var "E")) "is" ($#v1_intpro_1 :::"with_FALSUM"::: ) ) & (Bool (Set (Var "E")) "is" ($#v2_intpro_1 :::"with_int_implication"::: ) ) & (Bool (Set (Var "E")) "is" ($#v3_intpro_1 :::"with_int_conjunction"::: ) ) & (Bool (Set (Var "E")) "is" ($#v4_intpro_1 :::"with_int_disjunction"::: ) ) & (Bool (Set (Var "E")) "is" ($#v5_intpro_1 :::"with_int_propositional_variables"::: ) ) & (Bool (Set (Var "E")) "is" ($#v6_intpro_1 :::"with_modal_operator"::: ) ) ")" ) ")" )); registration cluster ($#v7_intpro_1 :::"MC-closed"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_intpro_1 :::"with_FALSUM"::: ) ($#v2_intpro_1 :::"with_int_implication"::: ) ($#v3_intpro_1 :::"with_int_conjunction"::: ) ($#v4_intpro_1 :::"with_int_disjunction"::: ) ($#v5_intpro_1 :::"with_int_propositional_variables"::: ) ($#v6_intpro_1 :::"with_modal_operator"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_intpro_1 :::"with_FALSUM"::: ) ($#v2_intpro_1 :::"with_int_implication"::: ) ($#v3_intpro_1 :::"with_int_conjunction"::: ) ($#v4_intpro_1 :::"with_int_disjunction"::: ) ($#v5_intpro_1 :::"with_int_propositional_variables"::: ) ($#v6_intpro_1 :::"with_modal_operator"::: ) -> ($#v7_intpro_1 :::"MC-closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "(" (Set ($#k5_numbers :::"NAT"::: ) ) ($#k13_finseq_1 :::"*"::: ) ")" ))); end; definitionfunc :::"MC-wff"::: -> ($#m1_hidden :::"set"::: ) means :: INTPRO_1:def 8 (Bool "(" (Bool it "is" ($#v7_intpro_1 :::"MC-closed"::: ) ) & (Bool "(" "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "E")) "is" ($#v7_intpro_1 :::"MC-closed"::: ) )) "holds" (Bool it ($#r1_tarski :::"c="::: ) (Set (Var "E"))) ")" ) ")" ); end; :: deftheorem defines :::"MC-wff"::: INTPRO_1:def 8 : (Bool "for" (Set (Var "b1")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_intpro_1 :::"MC-wff"::: ) )) "iff" (Bool "(" (Bool (Set (Var "b1")) "is" ($#v7_intpro_1 :::"MC-closed"::: ) ) & (Bool "(" "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "E")) "is" ($#v7_intpro_1 :::"MC-closed"::: ) )) "holds" (Bool (Set (Var "b1")) ($#r1_tarski :::"c="::: ) (Set (Var "E"))) ")" ) ")" ) ")" )); registration cluster (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) -> ($#v7_intpro_1 :::"MC-closed"::: ) ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v7_intpro_1 :::"MC-closed"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) -> ($#v4_funct_1 :::"functional"::: ) ; end; registration cluster -> ($#v1_finseq_1 :::"FinSequence-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ); end; definitionmode MC-formula is ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ); end; definitionfunc :::"FALSUM"::: -> ($#m1_subset_1 :::"MC-formula":::) equals :: INTPRO_1:def 9 (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ); let "p", "q" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ); func "p" :::"=>"::: "q" -> ($#m1_subset_1 :::"MC-formula":::) equals :: INTPRO_1:def 10 (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) "p" ")" ) ($#k7_finseq_1 :::"^"::: ) "q"); func "p" :::"'&'"::: "q" -> ($#m1_subset_1 :::"MC-formula":::) equals :: INTPRO_1:def 11 (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 2) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) "p" ")" ) ($#k7_finseq_1 :::"^"::: ) "q"); func "p" :::"'or'"::: "q" -> ($#m1_subset_1 :::"MC-formula":::) equals :: INTPRO_1:def 12 (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 3) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) "p" ")" ) ($#k7_finseq_1 :::"^"::: ) "q"); end; :: deftheorem defines :::"FALSUM"::: INTPRO_1:def 9 : (Bool (Set ($#k2_intpro_1 :::"FALSUM"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) )); :: deftheorem defines :::"=>"::: INTPRO_1:def 10 : (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))))); :: deftheorem defines :::"'&'"::: INTPRO_1:def 11 : (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 2) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))))); :: deftheorem defines :::"'or'"::: INTPRO_1:def 12 : (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 3) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))))); definitionlet "p" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ); func :::"Nes"::: "p" -> ($#m1_subset_1 :::"MC-formula":::) equals :: INTPRO_1:def 13 (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Num 6) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) "p"); end; :: deftheorem defines :::"Nes"::: INTPRO_1:def 13 : (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set ($#k6_intpro_1 :::"Nes"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Num 6) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p"))))); definitionlet "T" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ); attr "T" is :::"IPC_theory"::: means :: INTPRO_1:def 14 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set ($#k2_intpro_1 :::"FALSUM"::: ) ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) "T") & "(" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) "T")) "implies" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) "T") ")" ")" )); end; :: deftheorem defines :::"IPC_theory"::: INTPRO_1:def 14 : (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v8_intpro_1 :::"IPC_theory"::: ) ) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set ($#k2_intpro_1 :::"FALSUM"::: ) ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & "(" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "T")))) "implies" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) ")" ")" )) ")" )); definitionlet "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ); func :::"CnIPC"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) means :: INTPRO_1:def 15 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "st" (Bool (Bool (Set (Var "T")) "is" ($#v8_intpro_1 :::"IPC_theory"::: ) ) & (Bool "X" ($#r1_tarski :::"c="::: ) (Set (Var "T")))) "holds" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "T")))) ")" )); end; :: deftheorem defines :::"CnIPC"::: INTPRO_1:def 15 : (Bool "for" (Set (Var "X")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k7_intpro_1 :::"CnIPC"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "st" (Bool (Bool (Set (Var "T")) "is" ($#v8_intpro_1 :::"IPC_theory"::: ) ) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "T")))) "holds" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "T")))) ")" )) ")" )); definitionfunc :::"IPC-Taut"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) equals :: INTPRO_1:def 16 (Set ($#k7_intpro_1 :::"CnIPC"::: ) (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) ")" )); end; :: deftheorem defines :::"IPC-Taut"::: INTPRO_1:def 16 : (Bool (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_intpro_1 :::"CnIPC"::: ) (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) ")" ))); definitionlet "p" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ); func :::"neg"::: "p" -> ($#m1_subset_1 :::"MC-formula":::) equals :: INTPRO_1:def 17 (Set "p" ($#k3_intpro_1 :::"=>"::: ) (Set ($#k2_intpro_1 :::"FALSUM"::: ) )); end; :: deftheorem defines :::"neg"::: INTPRO_1:def 17 : (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set ($#k9_intpro_1 :::"neg"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set ($#k2_intpro_1 :::"FALSUM"::: ) )))); definitionfunc :::"IVERUM"::: -> ($#m1_subset_1 :::"MC-formula":::) equals :: INTPRO_1:def 18 (Set (Set ($#k2_intpro_1 :::"FALSUM"::: ) ) ($#k3_intpro_1 :::"=>"::: ) (Set ($#k2_intpro_1 :::"FALSUM"::: ) )); end; :: deftheorem defines :::"IVERUM"::: INTPRO_1:def 18 : (Bool (Set ($#k10_intpro_1 :::"IVERUM"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_intpro_1 :::"FALSUM"::: ) ) ($#k3_intpro_1 :::"=>"::: ) (Set ($#k2_intpro_1 :::"FALSUM"::: ) ))); theorem :: INTPRO_1:1 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k7_intpro_1 :::"CnIPC"::: ) (Set (Var "X")))))) ; theorem :: INTPRO_1:2 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k7_intpro_1 :::"CnIPC"::: ) (Set (Var "X")))))) ; theorem :: INTPRO_1:3 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k7_intpro_1 :::"CnIPC"::: ) (Set (Var "X")))))) ; theorem :: INTPRO_1:4 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k7_intpro_1 :::"CnIPC"::: ) (Set (Var "X")))))) ; theorem :: INTPRO_1:5 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k7_intpro_1 :::"CnIPC"::: ) (Set (Var "X")))))) ; theorem :: INTPRO_1:6 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k7_intpro_1 :::"CnIPC"::: ) (Set (Var "X")))))) ; theorem :: INTPRO_1:7 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k7_intpro_1 :::"CnIPC"::: ) (Set (Var "X")))))) ; theorem :: INTPRO_1:8 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "r")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k7_intpro_1 :::"CnIPC"::: ) (Set (Var "X")))))) ; theorem :: INTPRO_1:9 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set ($#k2_intpro_1 :::"FALSUM"::: ) ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k7_intpro_1 :::"CnIPC"::: ) (Set (Var "X")))))) ; theorem :: INTPRO_1:10 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k7_intpro_1 :::"CnIPC"::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k7_intpro_1 :::"CnIPC"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k7_intpro_1 :::"CnIPC"::: ) (Set (Var "X")))))) ; theorem :: INTPRO_1:11 (Bool "for" (Set (Var "T")) "," (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "st" (Bool (Bool (Set (Var "T")) "is" ($#v8_intpro_1 :::"IPC_theory"::: ) ) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "T")))) "holds" (Bool (Set ($#k7_intpro_1 :::"CnIPC"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "T")))) ; theorem :: INTPRO_1:12 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k7_intpro_1 :::"CnIPC"::: ) (Set (Var "X"))))) ; theorem :: INTPRO_1:13 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k7_intpro_1 :::"CnIPC"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k7_intpro_1 :::"CnIPC"::: ) (Set (Var "Y"))))) ; theorem :: INTPRO_1:14 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set ($#k7_intpro_1 :::"CnIPC"::: ) (Set "(" ($#k7_intpro_1 :::"CnIPC"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_intpro_1 :::"CnIPC"::: ) (Set (Var "X"))))) ; registrationlet "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ); cluster (Set ($#k7_intpro_1 :::"CnIPC"::: ) "X") -> ($#v8_intpro_1 :::"IPC_theory"::: ) ; end; theorem :: INTPRO_1:15 (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v8_intpro_1 :::"IPC_theory"::: ) ) "iff" (Bool (Set ($#k7_intpro_1 :::"CnIPC"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set (Var "T"))) ")" )) ; theorem :: INTPRO_1:16 (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "st" (Bool (Bool (Set (Var "T")) "is" ($#v8_intpro_1 :::"IPC_theory"::: ) )) "holds" (Bool (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "T")))) ; registration cluster (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ) -> ($#v8_intpro_1 :::"IPC_theory"::: ) ; end; begin theorem :: INTPRO_1:17 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:18 (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "st" (Bool (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) "holds" (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:19 (Bool (Set ($#k10_intpro_1 :::"IVERUM"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) )) ; theorem :: INTPRO_1:20 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:21 (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:22 (Bool "for" (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:23 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) "holds" (Bool (Set (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:24 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:25 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:26 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) )) & (Bool (Set (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r"))) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) "holds" (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r"))) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:27 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "s")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "s")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:28 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:29 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:30 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q")) ")" ) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:31 (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:32 (Bool "for" (Set (Var "s")) "," (Set (Var "q")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) )) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) "holds" (Bool (Set (Set (Var "s")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; begin theorem :: INTPRO_1:33 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:34 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) )) "iff" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) )) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) )) ")" ) ")" )) ; theorem :: INTPRO_1:35 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) )) "iff" (Bool (Set (Set (Var "q")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) )) ")" )) ; theorem :: INTPRO_1:36 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:37 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:38 (Bool "for" (Set (Var "r")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "r")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "r")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:39 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "p")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:40 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "p")) ")" ) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "s")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:41 (Bool "for" (Set (Var "q")) "," (Set (Var "s")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "s")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "s")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:42 (Bool "for" (Set (Var "q")) "," (Set (Var "s")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "s")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "q")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "p")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "s")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:43 (Bool "for" (Set (Var "p")) "," (Set (Var "s")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "s")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "s")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "s")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:44 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "s")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "s")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:45 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k4_intpro_1 :::"'&'"::: ) (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "s")) ")" ) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "s")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:46 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:47 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k4_intpro_1 :::"'&'"::: ) (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "s")) ")" ) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "s")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:48 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "s")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "s")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:49 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "s")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "p")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "s")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:50 (Bool "for" (Set (Var "p")) "," (Set (Var "s")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set "(" (Set (Var "s")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set "(" (Set (Var "q")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "s")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:51 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k4_intpro_1 :::"'&'"::: ) (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "s")) ")" ) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "s")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:52 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "s")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set "(" (Set (Var "q")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "s")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:53 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set "(" (Set (Var "q")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "s")) ")" ) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "s")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; begin theorem :: INTPRO_1:54 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "p")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:55 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "st" (Bool (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) )) "or" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) )) ")" )) "holds" (Bool (Set (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:56 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:57 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) )) "iff" (Bool (Set (Set (Var "q")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) )) ")" )) ; theorem :: INTPRO_1:58 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "s")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:59 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "s")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:60 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "s")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "s")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:61 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "s")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "s")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:62 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "s")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "p")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "s")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:63 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "s")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "p")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "s")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:64 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set "(" (Set (Var "q")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "s")) ")" ) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k5_intpro_1 :::"'or'"::: ) (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "s")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:65 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set "(" (Set (Var "q")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "s")) ")" ) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q")) ")" ) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "s")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; theorem :: INTPRO_1:66 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q")) ")" ) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "s")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set "(" (Set (Var "q")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "s")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ))) ; begin definitionlet "T" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ); attr "T" is :::"CPC_theory"::: means :: INTPRO_1:def 19 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set ($#k2_intpro_1 :::"FALSUM"::: ) ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set ($#k2_intpro_1 :::"FALSUM"::: ) ) ")" )) ($#r2_hidden :::"in"::: ) "T") & "(" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) "T")) "implies" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) "T") ")" ")" )); end; :: deftheorem defines :::"CPC_theory"::: INTPRO_1:def 19 : (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v9_intpro_1 :::"CPC_theory"::: ) ) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set ($#k2_intpro_1 :::"FALSUM"::: ) ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set ($#k2_intpro_1 :::"FALSUM"::: ) ) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & "(" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "T")))) "implies" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) ")" ")" )) ")" )); theorem :: INTPRO_1:67 (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "st" (Bool (Bool (Set (Var "T")) "is" ($#v9_intpro_1 :::"CPC_theory"::: ) )) "holds" (Bool (Set (Var "T")) "is" ($#v8_intpro_1 :::"IPC_theory"::: ) )) ; definitionlet "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ); func :::"CnCPC"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) means :: INTPRO_1:def 20 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "st" (Bool (Bool (Set (Var "T")) "is" ($#v9_intpro_1 :::"CPC_theory"::: ) ) & (Bool "X" ($#r1_tarski :::"c="::: ) (Set (Var "T")))) "holds" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "T")))) ")" )); end; :: deftheorem defines :::"CnCPC"::: INTPRO_1:def 20 : (Bool "for" (Set (Var "X")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k11_intpro_1 :::"CnCPC"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "st" (Bool (Bool (Set (Var "T")) "is" ($#v9_intpro_1 :::"CPC_theory"::: ) ) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "T")))) "holds" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "T")))) ")" )) ")" )); definitionfunc :::"CPC-Taut"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) equals :: INTPRO_1:def 21 (Set ($#k11_intpro_1 :::"CnCPC"::: ) (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) ")" )); end; :: deftheorem defines :::"CPC-Taut"::: INTPRO_1:def 21 : (Bool (Set ($#k12_intpro_1 :::"CPC-Taut"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k11_intpro_1 :::"CnCPC"::: ) (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) ")" ))); theorem :: INTPRO_1:68 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set ($#k7_intpro_1 :::"CnIPC"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k11_intpro_1 :::"CnCPC"::: ) (Set (Var "X"))))) ; theorem :: INTPRO_1:69 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k11_intpro_1 :::"CnCPC"::: ) (Set (Var "X")))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k11_intpro_1 :::"CnCPC"::: ) (Set (Var "X")))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k11_intpro_1 :::"CnCPC"::: ) (Set (Var "X")))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k11_intpro_1 :::"CnCPC"::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k11_intpro_1 :::"CnCPC"::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k11_intpro_1 :::"CnCPC"::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k11_intpro_1 :::"CnCPC"::: ) (Set (Var "X")))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k11_intpro_1 :::"CnCPC"::: ) (Set (Var "X")))) & (Bool (Set (Set ($#k2_intpro_1 :::"FALSUM"::: ) ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k11_intpro_1 :::"CnCPC"::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set ($#k2_intpro_1 :::"FALSUM"::: ) ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k11_intpro_1 :::"CnCPC"::: ) (Set (Var "X")))) ")" ))) ; theorem :: INTPRO_1:70 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k11_intpro_1 :::"CnCPC"::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k11_intpro_1 :::"CnCPC"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k11_intpro_1 :::"CnCPC"::: ) (Set (Var "X")))))) ; theorem :: INTPRO_1:71 (Bool "for" (Set (Var "T")) "," (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "st" (Bool (Bool (Set (Var "T")) "is" ($#v9_intpro_1 :::"CPC_theory"::: ) ) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "T")))) "holds" (Bool (Set ($#k11_intpro_1 :::"CnCPC"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "T")))) ; theorem :: INTPRO_1:72 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k11_intpro_1 :::"CnCPC"::: ) (Set (Var "X"))))) ; theorem :: INTPRO_1:73 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k11_intpro_1 :::"CnCPC"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k11_intpro_1 :::"CnCPC"::: ) (Set (Var "Y"))))) ; theorem :: INTPRO_1:74 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set ($#k11_intpro_1 :::"CnCPC"::: ) (Set "(" ($#k11_intpro_1 :::"CnCPC"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_intpro_1 :::"CnCPC"::: ) (Set (Var "X"))))) ; registrationlet "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ); cluster (Set ($#k11_intpro_1 :::"CnCPC"::: ) "X") -> ($#v9_intpro_1 :::"CPC_theory"::: ) ; end; theorem :: INTPRO_1:75 (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v9_intpro_1 :::"CPC_theory"::: ) ) "iff" (Bool (Set ($#k11_intpro_1 :::"CnCPC"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set (Var "T"))) ")" )) ; theorem :: INTPRO_1:76 (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "st" (Bool (Bool (Set (Var "T")) "is" ($#v9_intpro_1 :::"CPC_theory"::: ) )) "holds" (Bool (Set ($#k12_intpro_1 :::"CPC-Taut"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "T")))) ; registration cluster (Set ($#k12_intpro_1 :::"CPC-Taut"::: ) ) -> ($#v9_intpro_1 :::"CPC_theory"::: ) ; end; theorem :: INTPRO_1:77 (Bool (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k12_intpro_1 :::"CPC-Taut"::: ) )) ; begin definitionlet "T" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ); attr "T" is :::"S4_theory"::: means :: INTPRO_1:def 22 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set ($#k2_intpro_1 :::"FALSUM"::: ) ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set ($#k2_intpro_1 :::"FALSUM"::: ) ) ")" )) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set "(" ($#k6_intpro_1 :::"Nes"::: ) (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q")) ")" ) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" ($#k6_intpro_1 :::"Nes"::: ) (Set (Var "p")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" ($#k6_intpro_1 :::"Nes"::: ) (Set (Var "q")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set "(" ($#k6_intpro_1 :::"Nes"::: ) (Set (Var "p")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set "(" ($#k6_intpro_1 :::"Nes"::: ) (Set (Var "p")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" ($#k6_intpro_1 :::"Nes"::: ) (Set "(" ($#k6_intpro_1 :::"Nes"::: ) (Set (Var "p")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) "T") & "(" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) "T")) "implies" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) "T") ")" & "(" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "T")) "implies" (Bool (Set ($#k6_intpro_1 :::"Nes"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) "T") ")" ")" )); end; :: deftheorem defines :::"S4_theory"::: INTPRO_1:def 22 : (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v10_intpro_1 :::"S4_theory"::: ) ) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set ($#k2_intpro_1 :::"FALSUM"::: ) ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set ($#k2_intpro_1 :::"FALSUM"::: ) ) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set "(" ($#k6_intpro_1 :::"Nes"::: ) (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q")) ")" ) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" ($#k6_intpro_1 :::"Nes"::: ) (Set (Var "p")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" ($#k6_intpro_1 :::"Nes"::: ) (Set (Var "q")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set "(" ($#k6_intpro_1 :::"Nes"::: ) (Set (Var "p")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set "(" ($#k6_intpro_1 :::"Nes"::: ) (Set (Var "p")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" ($#k6_intpro_1 :::"Nes"::: ) (Set "(" ($#k6_intpro_1 :::"Nes"::: ) (Set (Var "p")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & "(" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "T")))) "implies" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) ")" & "(" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "T")))) "implies" (Bool (Set ($#k6_intpro_1 :::"Nes"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) ")" ")" )) ")" )); theorem :: INTPRO_1:78 (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "st" (Bool (Bool (Set (Var "T")) "is" ($#v10_intpro_1 :::"S4_theory"::: ) )) "holds" (Bool (Set (Var "T")) "is" ($#v9_intpro_1 :::"CPC_theory"::: ) )) ; theorem :: INTPRO_1:79 (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "st" (Bool (Bool (Set (Var "T")) "is" ($#v10_intpro_1 :::"S4_theory"::: ) )) "holds" (Bool (Set (Var "T")) "is" ($#v8_intpro_1 :::"IPC_theory"::: ) )) ; definitionlet "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ); func :::"CnS4"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) means :: INTPRO_1:def 23 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "st" (Bool (Bool (Set (Var "T")) "is" ($#v10_intpro_1 :::"S4_theory"::: ) ) & (Bool "X" ($#r1_tarski :::"c="::: ) (Set (Var "T")))) "holds" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "T")))) ")" )); end; :: deftheorem defines :::"CnS4"::: INTPRO_1:def 23 : (Bool "for" (Set (Var "X")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k13_intpro_1 :::"CnS4"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "st" (Bool (Bool (Set (Var "T")) "is" ($#v10_intpro_1 :::"S4_theory"::: ) ) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "T")))) "holds" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "T")))) ")" )) ")" )); definitionfunc :::"S4-Taut"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) equals :: INTPRO_1:def 24 (Set ($#k13_intpro_1 :::"CnS4"::: ) (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) ")" )); end; :: deftheorem defines :::"S4-Taut"::: INTPRO_1:def 24 : (Bool (Set ($#k14_intpro_1 :::"S4-Taut"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k13_intpro_1 :::"CnS4"::: ) (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) ")" ))); theorem :: INTPRO_1:80 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set ($#k11_intpro_1 :::"CnCPC"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k13_intpro_1 :::"CnS4"::: ) (Set (Var "X"))))) ; theorem :: INTPRO_1:81 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set ($#k7_intpro_1 :::"CnIPC"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k13_intpro_1 :::"CnS4"::: ) (Set (Var "X"))))) ; theorem :: INTPRO_1:82 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k13_intpro_1 :::"CnS4"::: ) (Set (Var "X")))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k13_intpro_1 :::"CnS4"::: ) (Set (Var "X")))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k13_intpro_1 :::"CnS4"::: ) (Set (Var "X")))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k13_intpro_1 :::"CnS4"::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k4_intpro_1 :::"'&'"::: ) (Set (Var "q")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k13_intpro_1 :::"CnS4"::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k13_intpro_1 :::"CnS4"::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k13_intpro_1 :::"CnS4"::: ) (Set (Var "X")))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "q")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set (Var "q")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k13_intpro_1 :::"CnS4"::: ) (Set (Var "X")))) & (Bool (Set (Set ($#k2_intpro_1 :::"FALSUM"::: ) ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k13_intpro_1 :::"CnS4"::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "p")) ($#k5_intpro_1 :::"'or'"::: ) (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set ($#k2_intpro_1 :::"FALSUM"::: ) ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k13_intpro_1 :::"CnS4"::: ) (Set (Var "X")))) ")" ))) ; theorem :: INTPRO_1:83 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k13_intpro_1 :::"CnS4"::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k13_intpro_1 :::"CnS4"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k13_intpro_1 :::"CnS4"::: ) (Set (Var "X")))))) ; theorem :: INTPRO_1:84 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" ($#k6_intpro_1 :::"Nes"::: ) (Set "(" (Set (Var "p")) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "q")) ")" ) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" (Set "(" ($#k6_intpro_1 :::"Nes"::: ) (Set (Var "p")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" ($#k6_intpro_1 :::"Nes"::: ) (Set (Var "q")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k13_intpro_1 :::"CnS4"::: ) (Set (Var "X")))))) ; theorem :: INTPRO_1:85 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" ($#k6_intpro_1 :::"Nes"::: ) (Set (Var "p")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k13_intpro_1 :::"CnS4"::: ) (Set (Var "X")))))) ; theorem :: INTPRO_1:86 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Set "(" ($#k6_intpro_1 :::"Nes"::: ) (Set (Var "p")) ")" ) ($#k3_intpro_1 :::"=>"::: ) (Set "(" ($#k6_intpro_1 :::"Nes"::: ) (Set "(" ($#k6_intpro_1 :::"Nes"::: ) (Set (Var "p")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k13_intpro_1 :::"CnS4"::: ) (Set (Var "X")))))) ; theorem :: INTPRO_1:87 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k13_intpro_1 :::"CnS4"::: ) (Set (Var "X"))))) "holds" (Bool (Set ($#k6_intpro_1 :::"Nes"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k13_intpro_1 :::"CnS4"::: ) (Set (Var "X")))))) ; theorem :: INTPRO_1:88 (Bool "for" (Set (Var "T")) "," (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "st" (Bool (Bool (Set (Var "T")) "is" ($#v10_intpro_1 :::"S4_theory"::: ) ) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "T")))) "holds" (Bool (Set ($#k13_intpro_1 :::"CnS4"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "T")))) ; theorem :: INTPRO_1:89 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k13_intpro_1 :::"CnS4"::: ) (Set (Var "X"))))) ; theorem :: INTPRO_1:90 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k13_intpro_1 :::"CnS4"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k13_intpro_1 :::"CnS4"::: ) (Set (Var "Y"))))) ; theorem :: INTPRO_1:91 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool (Set ($#k13_intpro_1 :::"CnS4"::: ) (Set "(" ($#k13_intpro_1 :::"CnS4"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k13_intpro_1 :::"CnS4"::: ) (Set (Var "X"))))) ; registrationlet "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ); cluster (Set ($#k13_intpro_1 :::"CnS4"::: ) "X") -> ($#v10_intpro_1 :::"S4_theory"::: ) ; end; theorem :: INTPRO_1:92 (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v10_intpro_1 :::"S4_theory"::: ) ) "iff" (Bool (Set ($#k13_intpro_1 :::"CnS4"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set (Var "T"))) ")" )) ; theorem :: INTPRO_1:93 (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_intpro_1 :::"MC-wff"::: ) ) "st" (Bool (Bool (Set (Var "T")) "is" ($#v10_intpro_1 :::"S4_theory"::: ) )) "holds" (Bool (Set ($#k14_intpro_1 :::"S4-Taut"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "T")))) ; registration cluster (Set ($#k14_intpro_1 :::"S4-Taut"::: ) ) -> ($#v10_intpro_1 :::"S4_theory"::: ) ; end; theorem :: INTPRO_1:94 (Bool (Set ($#k12_intpro_1 :::"CPC-Taut"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k14_intpro_1 :::"S4-Taut"::: ) )) ; theorem :: INTPRO_1:95 (Bool (Set ($#k8_intpro_1 :::"IPC-Taut"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k14_intpro_1 :::"S4-Taut"::: ) )) ;