:: QC_LANG4 semantic presentation begin theorem :: QC_LANG4:1 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "F")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "G")))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set (Var "F")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set (Var "G")) ")" ))))) ; theorem :: QC_LANG4:2 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "F")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "G"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set (Var "G")) ")" )))) "holds" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "G"))))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "p" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))); func :::"list_of_immediate_constituents"::: "p" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) "A") equals :: QC_LANG4:def 1 (Set ($#k6_finseq_1 :::"<*>"::: ) (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) "A" ")" )) if (Bool "(" (Bool "p" ($#r1_hidden :::"="::: ) (Set ($#k12_qc_lang1 :::"VERUM"::: ) "A")) "or" (Bool "p" "is" ($#v2_qc_lang1 :::"atomic"::: ) ) ")" ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) "p" ")" ) ($#k12_finseq_1 :::"*>"::: ) ) if (Bool "p" "is" ($#v3_qc_lang1 :::"negative"::: ) ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set "(" ($#k19_qc_lang1 :::"the_left_argument_of"::: ) "p" ")" ) "," (Set "(" ($#k20_qc_lang1 :::"the_right_argument_of"::: ) "p" ")" ) ($#k2_finseq_4 :::"*>"::: ) ) if (Bool "p" "is" ($#v4_qc_lang1 :::"conjunctive"::: ) ) otherwise (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) "p" ")" ) ($#k12_finseq_1 :::"*>"::: ) ); end; :: deftheorem defines :::"list_of_immediate_constituents"::: QC_LANG4:def 1 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" "(" (Bool (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k12_qc_lang1 :::"VERUM"::: ) (Set (Var "A")))) "or" (Bool (Set (Var "p")) "is" ($#v2_qc_lang1 :::"atomic"::: ) ) ")" )) "implies" (Bool (Set ($#k1_qc_lang4 :::"list_of_immediate_constituents"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k6_finseq_1 :::"<*>"::: ) (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A")) ")" ))) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v3_qc_lang1 :::"negative"::: ) )) "implies" (Bool (Set ($#k1_qc_lang4 :::"list_of_immediate_constituents"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "p")) ")" ) ($#k12_finseq_1 :::"*>"::: ) )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) )) "implies" (Bool (Set ($#k1_qc_lang4 :::"list_of_immediate_constituents"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set "(" ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set (Var "p")) ")" ) "," (Set "(" ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set (Var "p")) ")" ) ($#k2_finseq_4 :::"*>"::: ) )) ")" & (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k12_qc_lang1 :::"VERUM"::: ) (Set (Var "A")))) "or" (Bool (Set (Var "p")) "is" ($#v2_qc_lang1 :::"atomic"::: ) ) "or" (Bool (Set (Var "p")) "is" ($#v3_qc_lang1 :::"negative"::: ) ) "or" (Bool (Set (Var "p")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) ) "or" (Bool (Set ($#k1_qc_lang4 :::"list_of_immediate_constituents"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set (Var "p")) ")" ) ($#k12_finseq_1 :::"*>"::: ) )) ")" ) ")" ))); theorem :: QC_LANG4:3 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k1_qc_lang4 :::"list_of_immediate_constituents"::: ) (Set (Var "F")) ")" ))) & (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_qc_lang4 :::"list_of_immediate_constituents"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))))) "holds" (Bool (Set (Var "G")) ($#r1_qc_lang2 :::"is_immediate_constituent_of"::: ) (Set (Var "F")))))) ; theorem :: QC_LANG4:4 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_qc_lang4 :::"list_of_immediate_constituents"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) "{" (Set (Var "G")) where G "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) : (Bool (Set (Var "G")) ($#r1_qc_lang2 :::"is_immediate_constituent_of"::: ) (Set (Var "F"))) "}" ))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "p" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))); func :::"tree_of_subformulae"::: "p" -> ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"DecoratedTree":::) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) "A") means :: QC_LANG4:def 2 (Bool "(" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) "p") & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) it) "holds" (Bool (Set ($#k2_trees_9 :::"succ"::: ) "(" it "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_qc_lang4 :::"list_of_immediate_constituents"::: ) (Set "(" it ($#k3_trees_2 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"tree_of_subformulae"::: QC_LANG4:def 2 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "b3")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"DecoratedTree":::) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "p")))) "iff" (Bool "(" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) "holds" (Bool (Set ($#k2_trees_9 :::"succ"::: ) "(" (Set (Var "b3")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_qc_lang4 :::"list_of_immediate_constituents"::: ) (Set "(" (Set (Var "b3")) ($#k3_trees_2 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) ")" )))); theorem :: QC_LANG4:5 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ))))) ; theorem :: QC_LANG4:6 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "t")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" )) "st" (Bool (Bool (Set (Set (Var "t")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" )))) "holds" (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool "(" (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "t")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ))) & (Bool (Set (Var "G")) ($#r1_qc_lang2 :::"is_immediate_constituent_of"::: ) (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t")))) ")" )))))) ; theorem :: QC_LANG4:7 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "t")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" )) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r1_qc_lang2 :::"is_immediate_constituent_of"::: ) (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t")))) "iff" (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "t")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ))) & (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "t")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ))) ")" )) ")" )))) ; theorem :: QC_LANG4:8 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "F")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "G")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ))) & (Bool (Set (Var "H")) ($#r1_qc_lang2 :::"is_immediate_constituent_of"::: ) (Set (Var "G")))) "holds" (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ))))) ; theorem :: QC_LANG4:9 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "F")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "G")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ))) & (Bool (Set (Var "H")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "G")))) "holds" (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ))))) ; theorem :: QC_LANG4:10 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "G")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ))) "iff" (Bool (Set (Var "G")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "F"))) ")" ))) ; theorem :: QC_LANG4:11 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k15_qc_lang2 :::"Subformulae"::: ) (Set (Var "F")))))) ; theorem :: QC_LANG4:12 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "t9")) "," (Set (Var "t")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" )) "st" (Bool (Bool (Set (Var "t9")) ($#r2_hidden :::"in"::: ) (Set ($#k1_trees_2 :::"succ"::: ) (Set (Var "t"))))) "holds" (Bool (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t9"))) ($#r1_qc_lang2 :::"is_immediate_constituent_of"::: ) (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t"))))))) ; theorem :: QC_LANG4:13 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "t")) "," (Set (Var "t9")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" )) "st" (Bool (Bool (Set (Var "t")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "t9")))) "holds" (Bool (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t9"))) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t"))))))) ; theorem :: QC_LANG4:14 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "t")) "," (Set (Var "t9")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" )) "st" (Bool (Bool (Set (Var "t")) ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: ) (Set (Var "t9")))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set "(" (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t9")) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set "(" (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t")) ")" ) ")" )))))) ; theorem :: QC_LANG4:15 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "t")) "," (Set (Var "t9")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" )) "st" (Bool (Bool (Set (Var "t")) ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: ) (Set (Var "t9")))) "holds" (Bool (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t9"))) ($#r1_hidden :::"<>"::: ) (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t"))))))) ; theorem :: QC_LANG4:16 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "t")) "," (Set (Var "t9")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" )) "st" (Bool (Bool (Set (Var "t")) ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: ) (Set (Var "t9")))) "holds" (Bool (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t9"))) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t"))))))) ; theorem :: QC_LANG4:17 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "t")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" )) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Var "F"))) "iff" (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )))) ; theorem :: QC_LANG4:18 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "t")) "," (Set (Var "t9")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" )) "st" (Bool (Bool (Set (Var "t")) ($#r1_hidden :::"<>"::: ) (Set (Var "t9"))) & (Bool (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t9"))))) "holds" (Bool "not" (Bool (Set (Var "t")) "," (Set (Var "t9")) ($#r3_xboole_0 :::"are_c=-comparable"::: ) ))))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "F", "G" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))); func "F" :::"-entry_points_in_subformula_tree_of"::: "G" -> ($#m4_trees_1 :::"AntiChain_of_Prefixes"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) "F" ")" )) means :: QC_LANG4:def 3 (Bool "for" (Set (Var "t")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) "F" ")" )) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) "F" ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) "G") ")" )); end; :: deftheorem defines :::"-entry_points_in_subformula_tree_of"::: QC_LANG4:def 3 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "b4")) "being" ($#m4_trees_1 :::"AntiChain_of_Prefixes"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" )) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_qc_lang4 :::"-entry_points_in_subformula_tree_of"::: ) (Set (Var "G")))) "iff" (Bool "for" (Set (Var "t")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" )) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Var "G"))) ")" )) ")" )))); theorem :: QC_LANG4:19 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set (Set (Var "F")) ($#k3_qc_lang4 :::"-entry_points_in_subformula_tree_of"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "t")) where t "is" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" )) : (Bool (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Var "G"))) "}" ))) ; theorem :: QC_LANG4:20 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "G")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "F"))) "iff" (Bool (Set (Set (Var "F")) ($#k3_qc_lang4 :::"-entry_points_in_subformula_tree_of"::: ) (Set (Var "G"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))) ; theorem :: QC_LANG4:21 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "t9")) "," (Set (Var "t")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" )) "st" (Bool (Bool (Set (Var "t9")) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "m")) ($#k12_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t"))) "is" ($#v3_qc_lang1 :::"negative"::: ) )) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t9"))) ($#r1_hidden :::"="::: ) (Set ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set "(" (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t")) ")" ))) & (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))))) ; theorem :: QC_LANG4:22 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "t9")) "," (Set (Var "t")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" )) "st" (Bool (Bool (Set (Var "t9")) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "m")) ($#k12_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t"))) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) ) & (Bool "not" (Bool "(" (Bool (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t9"))) ($#r1_hidden :::"="::: ) (Set ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set "(" (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t")) ")" ))) & (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t9"))) ($#r1_hidden :::"="::: ) (Set ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set "(" (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t")) ")" ))) & (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Num 1)) ")" ))))) ; theorem :: QC_LANG4:23 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "t9")) "," (Set (Var "t")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" )) "st" (Bool (Bool (Set (Var "t9")) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "m")) ($#k12_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t"))) "is" ($#v5_qc_lang1 :::"universal"::: ) )) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t9"))) ($#r1_hidden :::"="::: ) (Set ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set "(" (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t")) ")" ))) & (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))))) ; theorem :: QC_LANG4:24 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "t")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" )) "st" (Bool (Bool (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t"))) "is" ($#v3_qc_lang1 :::"negative"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "t")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ))) & (Bool (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "t")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set "(" (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t")) ")" ))) ")" )))) ; theorem :: QC_LANG4:25 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "t")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" )) "st" (Bool (Bool (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t"))) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "t")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ))) & (Bool (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "t")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set "(" (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t")) ")" ))) & (Bool (Set (Set (Var "t")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ))) & (Bool (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "t")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set "(" (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t")) ")" ))) ")" )))) ; theorem :: QC_LANG4:26 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "t")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" )) "st" (Bool (Bool (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t"))) "is" ($#v5_qc_lang1 :::"universal"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "t")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ))) & (Bool (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "t")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set "(" (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t")) ")" ))) ")" )))) ; theorem :: QC_LANG4:27 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "t")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" )) (Bool "for" (Set (Var "s")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "G")) ")" )) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k3_qc_lang4 :::"-entry_points_in_subformula_tree_of"::: ) (Set (Var "G")))) & (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k3_qc_lang4 :::"-entry_points_in_subformula_tree_of"::: ) (Set (Var "H"))))) "holds" (Bool (Set (Set (Var "t")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "s"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k3_qc_lang4 :::"-entry_points_in_subformula_tree_of"::: ) (Set (Var "H")))))))) ; theorem :: QC_LANG4:28 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "t")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" )) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k3_qc_lang4 :::"-entry_points_in_subformula_tree_of"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "t")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "s"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k3_qc_lang4 :::"-entry_points_in_subformula_tree_of"::: ) (Set (Var "H"))))) "holds" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k3_qc_lang4 :::"-entry_points_in_subformula_tree_of"::: ) (Set (Var "H")))))))) ; theorem :: QC_LANG4:29 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "{" (Set "(" (Set (Var "t")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "s")) ")" ) where t "is" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" )), s "is" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "G")) ")" )) : (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k3_qc_lang4 :::"-entry_points_in_subformula_tree_of"::: ) (Set (Var "G")))) & (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k3_qc_lang4 :::"-entry_points_in_subformula_tree_of"::: ) (Set (Var "H")))) ")" ) "}" ($#r1_tarski :::"c="::: ) (Set (Set (Var "F")) ($#k3_qc_lang4 :::"-entry_points_in_subformula_tree_of"::: ) (Set (Var "H")))))) ; theorem :: QC_LANG4:30 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "t")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" )) "holds" (Bool (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k5_trees_2 :::"|"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set "(" (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t")) ")" )))))) ; theorem :: QC_LANG4:31 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "t")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" )) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k3_qc_lang4 :::"-entry_points_in_subformula_tree_of"::: ) (Set (Var "G")))) "iff" (Bool (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k5_trees_2 :::"|"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "G")))) ")" )))) ; theorem :: QC_LANG4:32 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set (Set (Var "F")) ($#k3_qc_lang4 :::"-entry_points_in_subformula_tree_of"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "t")) where t "is" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" )) : (Bool (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k5_trees_2 :::"|"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "G")))) "}" ))) ; theorem :: QC_LANG4:33 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "C")) "being" ($#m1_trees_2 :::"Chain"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" )) "st" (Bool (Bool (Set (Var "G")) ($#r2_hidden :::"in"::: ) "{" (Set "(" (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t")) ")" ) where t "is" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" )) : (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) "}" ) & (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) "{" (Set "(" (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "t")) ")" ) where t "is" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" )) : (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) "}" ) & (Bool (Bool "not" (Set (Var "G")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "H"))))) "holds" (Bool (Set (Var "H")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "G")))))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "F" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))); mode :::"Subformula"::: "of" "F" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) "A") means :: QC_LANG4:def 4 (Bool it ($#r2_qc_lang2 :::"is_subformula_of"::: ) "F"); end; :: deftheorem defines :::"Subformula"::: QC_LANG4:def 4 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_qc_lang4 :::"Subformula"::: ) "of" (Set (Var "F"))) "iff" (Bool (Set (Var "b3")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "F"))) ")" ))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "F" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))); let "G" be ($#m1_qc_lang4 :::"Subformula"::: ) "of" (Set (Const "F")); mode :::"Entry_Point_in_Subformula_Tree"::: "of" "G" -> ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) "F" ")" )) means :: QC_LANG4:def 5 (Bool (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) "F" ")" ) ($#k3_trees_2 :::"."::: ) it) ($#r1_hidden :::"="::: ) "G"); end; :: deftheorem defines :::"Entry_Point_in_Subformula_Tree"::: QC_LANG4:def 5 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "G")) "being" ($#m1_qc_lang4 :::"Subformula"::: ) "of" (Set (Var "F")) (Bool "for" (Set (Var "b4")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" )) "holds" (Bool "(" (Bool (Set (Var "b4")) "is" ($#m2_qc_lang4 :::"Entry_Point_in_Subformula_Tree"::: ) "of" (Set (Var "G"))) "iff" (Bool (Set (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" ) ($#k3_trees_2 :::"."::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Var "G"))) ")" ))))); theorem :: QC_LANG4:34 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "G")) "being" ($#m1_qc_lang4 :::"Subformula"::: ) "of" (Set (Var "F")) (Bool "for" (Set (Var "t")) "," (Set (Var "t9")) "being" ($#m2_qc_lang4 :::"Entry_Point_in_Subformula_Tree"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "t")) ($#r1_hidden :::"<>"::: ) (Set (Var "t9")))) "holds" (Bool "not" (Bool (Set (Var "t")) "," (Set (Var "t9")) ($#r3_xboole_0 :::"are_c=-comparable"::: ) )))))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "F" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))); let "G" be ($#m1_qc_lang4 :::"Subformula"::: ) "of" (Set (Const "F")); func :::"entry_points_in_subformula_tree"::: "G" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m4_trees_1 :::"AntiChain_of_Prefixes"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) "F" ")" )) equals :: QC_LANG4:def 6 (Set "F" ($#k3_qc_lang4 :::"-entry_points_in_subformula_tree_of"::: ) "G"); end; :: deftheorem defines :::"entry_points_in_subformula_tree"::: QC_LANG4:def 6 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "G")) "being" ($#m1_qc_lang4 :::"Subformula"::: ) "of" (Set (Var "F")) "holds" (Bool (Set ($#k4_qc_lang4 :::"entry_points_in_subformula_tree"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_qc_lang4 :::"-entry_points_in_subformula_tree_of"::: ) (Set (Var "G"))))))); theorem :: QC_LANG4:35 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "G")) "being" ($#m1_qc_lang4 :::"Subformula"::: ) "of" (Set (Var "F")) (Bool "for" (Set (Var "t")) "being" ($#m2_qc_lang4 :::"Entry_Point_in_Subformula_Tree"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k4_qc_lang4 :::"entry_points_in_subformula_tree"::: ) (Set (Var "G")))))))) ; theorem :: QC_LANG4:36 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "G")) "being" ($#m1_qc_lang4 :::"Subformula"::: ) "of" (Set (Var "F")) "holds" (Bool (Set ($#k4_qc_lang4 :::"entry_points_in_subformula_tree"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "t")) where t "is" ($#m2_qc_lang4 :::"Entry_Point_in_Subformula_Tree"::: ) "of" (Set (Var "G")) : (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Var "t"))) "}" )))) ; theorem :: QC_LANG4:37 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_qc_lang4 :::"Subformula"::: ) "of" (Set (Var "F")) (Bool "for" (Set (Var "t1")) "being" ($#m2_qc_lang4 :::"Entry_Point_in_Subformula_Tree"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "s")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "G1")) ")" )) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G1")) ($#k3_qc_lang4 :::"-entry_points_in_subformula_tree_of"::: ) (Set (Var "G2"))))) "holds" (Bool (Set (Set (Var "t1")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "s"))) "is" ($#m2_qc_lang4 :::"Entry_Point_in_Subformula_Tree"::: ) "of" (Set (Var "G2")))))))) ; theorem :: QC_LANG4:38 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "G2")) "," (Set (Var "G1")) "being" ($#m1_qc_lang4 :::"Subformula"::: ) "of" (Set (Var "F")) (Bool "for" (Set (Var "t1")) "being" ($#m2_qc_lang4 :::"Entry_Point_in_Subformula_Tree"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Set (Var "t1")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "s"))) "is" ($#m2_qc_lang4 :::"Entry_Point_in_Subformula_Tree"::: ) "of" (Set (Var "G2")))) "holds" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G1")) ($#k3_qc_lang4 :::"-entry_points_in_subformula_tree_of"::: ) (Set (Var "G2"))))))))) ; theorem :: QC_LANG4:39 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_qc_lang4 :::"Subformula"::: ) "of" (Set (Var "F")) "holds" (Bool "{" (Set "(" (Set (Var "t")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "s")) ")" ) where t "is" ($#m2_qc_lang4 :::"Entry_Point_in_Subformula_Tree"::: ) "of" (Set (Var "G1")), s "is" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "G1")) ")" )) : (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G1")) ($#k3_qc_lang4 :::"-entry_points_in_subformula_tree_of"::: ) (Set (Var "G2")))) "}" ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "t")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "s")) ")" ) where t "is" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "F")) ")" )), s "is" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "G1")) ")" )) : (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k3_qc_lang4 :::"-entry_points_in_subformula_tree_of"::: ) (Set (Var "G1")))) & (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G1")) ($#k3_qc_lang4 :::"-entry_points_in_subformula_tree_of"::: ) (Set (Var "G2")))) ")" ) "}" )))) ; theorem :: QC_LANG4:40 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_qc_lang4 :::"Subformula"::: ) "of" (Set (Var "F")) "holds" (Bool "{" (Set "(" (Set (Var "t")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "s")) ")" ) where t "is" ($#m2_qc_lang4 :::"Entry_Point_in_Subformula_Tree"::: ) "of" (Set (Var "G1")), s "is" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_qc_lang4 :::"tree_of_subformulae"::: ) (Set (Var "G1")) ")" )) : (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G1")) ($#k3_qc_lang4 :::"-entry_points_in_subformula_tree_of"::: ) (Set (Var "G2")))) "}" ($#r1_tarski :::"c="::: ) (Set ($#k4_qc_lang4 :::"entry_points_in_subformula_tree"::: ) (Set (Var "G2"))))))) ; theorem :: QC_LANG4:41 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_qc_lang4 :::"Subformula"::: ) "of" (Set (Var "F")) "st" (Bool (Bool "ex" (Set (Var "t1")) "being" ($#m2_qc_lang4 :::"Entry_Point_in_Subformula_Tree"::: ) "of" (Set (Var "G1"))(Bool "ex" (Set (Var "t2")) "being" ($#m2_qc_lang4 :::"Entry_Point_in_Subformula_Tree"::: ) "of" (Set (Var "G2")) "st" (Bool (Set (Var "t1")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "t2")))))) "holds" (Bool (Set (Var "G2")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "G1")))))) ; theorem :: QC_LANG4:42 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "G2")) "," (Set (Var "G1")) "being" ($#m1_qc_lang4 :::"Subformula"::: ) "of" (Set (Var "F")) "st" (Bool (Bool (Set (Var "G2")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "G1")))) "holds" (Bool "for" (Set (Var "t1")) "being" ($#m2_qc_lang4 :::"Entry_Point_in_Subformula_Tree"::: ) "of" (Set (Var "G1")) (Bool "ex" (Set (Var "t2")) "being" ($#m2_qc_lang4 :::"Entry_Point_in_Subformula_Tree"::: ) "of" (Set (Var "G2")) "st" (Bool (Set (Var "t1")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "t2")))))))) ;