:: SUBSTUT2 semantic presentation begin theorem :: SUBSTUT2:1 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) (Bool "ex" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) "st" (Bool "(" (Bool (Set (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "Al")))) & (Bool (Set (Set (Var "S")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "Sub"))) ")" )))) ; theorem :: SUBSTUT2:2 (Bool "for" (Set (Var "Al")) "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 "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "Al")) (Bool "for" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "Al")) (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) (Bool "ex" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) "st" (Bool "(" (Bool (Set (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "ll")))) & (Bool (Set (Set (Var "S")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "Sub"))) ")" ))))))) ; theorem :: SUBSTUT2:3 (Bool "for" (Set (Var "Al")) "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 "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "Al")) (Bool "for" (Set (Var "k")) "," (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "P")) "is" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "Al"))) & (Bool (Set (Var "P")) "is" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "l")) "," (Set (Var "Al")))) "holds" (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Var "l"))))))) ; theorem :: SUBSTUT2:4 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool "(" "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) (Bool "ex" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) "st" (Bool "(" (Bool (Set (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set (Var "S")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "Sub"))) ")" )) ")" )) "holds" (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) (Bool "ex" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) "st" (Bool "(" (Bool (Set (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "S")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "Sub"))) ")" ))))) ; theorem :: SUBSTUT2:5 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool "(" "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) (Bool "ex" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) "st" (Bool "(" (Bool (Set (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set (Var "S")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "Sub"))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) (Bool "ex" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) "st" (Bool "(" (Bool (Set (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Set (Var "S")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "Sub"))) ")" )) ")" )) "holds" (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) (Bool "ex" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) "st" (Bool "(" (Bool (Set (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")))) & (Bool (Set (Set (Var "S")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "Sub"))) ")" ))))) ; definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "p" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "Al"))); let "Sub" be ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Const "Al")); :: original: :::"["::: redefine func :::"[":::"p" "," "Sub":::"]"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) "Al" ")" ) "," (Set "(" ($#k1_substut1 :::"vSUB"::: ) "Al" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ); end; theorem :: SUBSTUT2:6 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k7_substut1 :::"RestrictSub"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "Sub")) ")" ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )))))) ; theorem :: SUBSTUT2:7 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k7_substut1 :::"RestrictSub"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "Sub")) ")" ")" )))) "holds" (Bool (Set ($#k35_substut1 :::"S_Bound"::: ) (Set ($#k1_substut2 :::"["::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "Sub")) ($#k1_substut2 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_qc_lang3 :::"x."::: ) (Set "(" ($#k13_substut1 :::"upVar"::: ) "(" (Set "(" ($#k7_substut1 :::"RestrictSub"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "Sub")) ")" ")" ) "," (Set (Var "p")) ")" ")" ))))))) ; theorem :: SUBSTUT2:8 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k7_substut1 :::"RestrictSub"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "Sub")) ")" ")" ))))) "holds" (Bool (Set ($#k35_substut1 :::"S_Bound"::: ) (Set ($#k1_substut2 :::"["::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "Sub")) ($#k1_substut2 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "x"))))))) ; theorem :: SUBSTUT2:9 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) "holds" (Bool (Set ($#k14_substut1 :::"ExpandSub"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) "," (Set "(" ($#k7_substut1 :::"RestrictSub"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "Sub")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_substut1 :::"@"::: ) (Set "(" ($#k7_substut1 :::"RestrictSub"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "Sub")) ")" ")" ) ")" ) ($#k14_sublemma :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k12_sublemma :::"|"::: ) (Set "(" ($#k35_substut1 :::"S_Bound"::: ) (Set ($#k1_substut2 :::"["::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "Sub")) ($#k1_substut2 :::"]"::: ) ) ")" ) ")" ))))))) ; theorem :: SUBSTUT2:10 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool (Set (Set (Var "S")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_substut1 :::"@"::: ) (Set "(" ($#k7_substut1 :::"RestrictSub"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "Sub")) ")" ")" ) ")" ) ($#k14_sublemma :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k12_sublemma :::"|"::: ) (Set "(" ($#k35_substut1 :::"S_Bound"::: ) (Set ($#k1_substut2 :::"["::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "Sub")) ($#k1_substut2 :::"]"::: ) ) ")" ) ")" ))) & (Bool (Set (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "p")))) "holds" (Bool "(" (Bool (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "is" ($#v3_substut1 :::"quantifiable"::: ) ) & (Bool "ex" (Set (Var "S1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Set (Var "S1")) ($#r1_hidden :::"="::: ) (Set ($#k1_substut2 :::"["::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "Sub")) ($#k1_substut2 :::"]"::: ) ))) ")" )))))) ; theorem :: SUBSTUT2:11 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool "(" "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) (Bool "ex" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) "st" (Bool "(" (Bool (Set (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set (Var "S")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "Sub"))) ")" )) ")" )) "holds" (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) (Bool "ex" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) "st" (Bool "(" (Bool (Set (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" )) & (Bool (Set (Set (Var "S")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "Sub"))) ")" )))))) ; theorem :: SUBSTUT2:12 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) (Bool "ex" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) "st" (Bool "(" (Bool (Set (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set (Var "S")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "Sub"))) ")" ))))) ; definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "p" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "Al"))); let "Sub" be ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Const "Al")); :: original: :::"["::: redefine func :::"[":::"p" "," "Sub":::"]"::: -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) "Al"); end; notationlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "x", "y" be ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Const "Al")); synonym :::"Sbst"::: "(" "x" "," "y" ")" for "Al" :::".-->"::: "x"; end; definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "x", "y" be ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Const "Al")); :: original: :::"Sbst"::: redefine func :::"Sbst"::: "(" "x" "," "y" ")" -> ($#m1_subset_1 :::"CQC_Substitution":::) "of" "Al"; end; begin definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "p" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "Al"))); let "x", "y" be ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Const "Al")); func "p" :::"."::: "(" "x" "," "y" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "Al") equals :: SUBSTUT2:def 1 (Set ($#k39_substut1 :::"CQC_Sub"::: ) (Set ($#k2_substut2 :::"["::: ) "p" "," (Set "(" ($#k3_substut2 :::"Sbst"::: ) "(" "x" "," "y" ")" ")" ) ($#k2_substut2 :::"]"::: ) )); end; :: deftheorem defines :::"."::: SUBSTUT2:def 1 : (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "holds" (Bool (Set (Set (Var "p")) ($#k4_substut2 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k39_substut1 :::"CQC_Sub"::: ) (Set ($#k2_substut2 :::"["::: ) (Set (Var "p")) "," (Set "(" ($#k3_substut2 :::"Sbst"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k2_substut2 :::"]"::: ) )))))); scheme :: SUBSTUT2:sch 1 CQCInd1{ F1() -> ($#m1_qc_lang1 :::"QC-alphabet"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) "holds" (Bool P1[(Set (Var "p"))])) provided (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) "st" (Bool (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool P1[(Set (Var "p"))])) and (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) "st" (Bool (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "k")))) "holds" (Bool P1[(Set (Var "p"))]) ")" )) "holds" (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) "st" (Bool (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool P1[(Set (Var "p"))]))) proof end; scheme :: SUBSTUT2:sch 2 CQCInd2{ F1() -> ($#m1_qc_lang1 :::"QC-alphabet"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) "holds" (Bool P1[(Set (Var "p"))])) provided (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) "st" (Bool (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool P1[(Set (Var "p"))])) and (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) "st" (Bool (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool P1[(Set (Var "p"))]) ")" )) "holds" (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) "st" (Bool (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool P1[(Set (Var "p"))]))) proof end; theorem :: SUBSTUT2:13 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "holds" (Bool (Set (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "Al")) ")" ) ($#k4_substut2 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "Al")))))) ; theorem :: SUBSTUT2:14 (Bool "for" (Set (Var "Al")) "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 "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "Al")) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "Al")) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "l")) ")" ) ($#k4_substut2 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set "(" ($#k3_substut1 :::"CQC_Subst"::: ) "(" (Set (Var "l")) "," (Set "(" ($#k3_substut2 :::"Sbst"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" ")" ))) & (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "l")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "l")) ")" ) ($#k4_substut2 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ))) ")" )))))) ; theorem :: SUBSTUT2:15 (Bool "for" (Set (Var "Al")) "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 "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "Al")) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "Al")) (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) "holds" (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "l")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set "(" ($#k39_substut1 :::"CQC_Sub"::: ) (Set ($#k2_substut2 :::"["::: ) (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "l")) ")" ) "," (Set (Var "Sub")) ($#k2_substut2 :::"]"::: ) ) ")" )))))))) ; definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "S" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Const "Al"))); :: original: :::"`2"::: redefine func "S" :::"`2"::: -> ($#m1_subset_1 :::"CQC_Substitution":::) "of" "Al"; end; theorem :: SUBSTUT2:16 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) "holds" (Bool (Set ($#k2_substut2 :::"["::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) "," (Set (Var "Sub")) ($#k2_substut2 :::"]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_sublemma :::"Sub_not"::: ) (Set ($#k2_substut2 :::"["::: ) (Set (Var "p")) "," (Set (Var "Sub")) ($#k2_substut2 :::"]"::: ) )))))) ; theorem :: SUBSTUT2:17 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "holds" (Bool "(" (Bool (Set ($#k6_cqc_lang :::"'not'"::: ) (Set "(" (Set (Var "p")) ($#k4_substut2 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_cqc_lang :::"'not'"::: ) (Set "(" (Set (Var "p")) ($#k4_substut2 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ))) & "(" (Bool (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set "(" (Set (Var "p")) ($#k4_substut2 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )))) "implies" (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" (Set (Var "p")) ($#k4_substut2 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" ))) ")" ")" )))) ; theorem :: SUBSTUT2:18 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool "(" "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) "holds" (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set "(" ($#k39_substut1 :::"CQC_Sub"::: ) (Set ($#k2_substut2 :::"["::: ) (Set (Var "p")) "," (Set (Var "Sub")) ($#k2_substut2 :::"]"::: ) ) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) "holds" (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set "(" ($#k39_substut1 :::"CQC_Sub"::: ) (Set ($#k2_substut2 :::"["::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) "," (Set (Var "Sub")) ($#k2_substut2 :::"]"::: ) ) ")" )))))) ; theorem :: SUBSTUT2:19 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) "holds" (Bool (Set ($#k2_substut2 :::"["::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) "," (Set (Var "Sub")) ($#k2_substut2 :::"]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_sublemma :::"CQCSub_&"::: ) "(" (Set ($#k2_substut2 :::"["::: ) (Set (Var "p")) "," (Set (Var "Sub")) ($#k2_substut2 :::"]"::: ) ) "," (Set ($#k2_substut2 :::"["::: ) (Set (Var "q")) "," (Set (Var "Sub")) ($#k2_substut2 :::"]"::: ) ) ")" ))))) ; theorem :: SUBSTUT2:20 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k4_substut2 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k4_substut2 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k7_cqc_lang :::"'&'"::: ) (Set "(" (Set (Var "q")) ($#k4_substut2 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ))) & "(" (Bool (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set "(" (Set (Var "p")) ($#k4_substut2 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ))) & (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set "(" (Set (Var "q")) ($#k4_substut2 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )))) "implies" (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k4_substut2 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ))) ")" ")" )))) ; theorem :: SUBSTUT2:21 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool "(" "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) "holds" (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set "(" ($#k39_substut1 :::"CQC_Sub"::: ) (Set ($#k2_substut2 :::"["::: ) (Set (Var "p")) "," (Set (Var "Sub")) ($#k2_substut2 :::"]"::: ) ) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) "holds" (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set "(" ($#k39_substut1 :::"CQC_Sub"::: ) (Set ($#k2_substut2 :::"["::: ) (Set (Var "q")) "," (Set (Var "Sub")) ($#k2_substut2 :::"]"::: ) ) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) "holds" (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set "(" ($#k39_substut1 :::"CQC_Sub"::: ) (Set ($#k2_substut2 :::"["::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) "," (Set (Var "Sub")) ($#k2_substut2 :::"]"::: ) ) ")" )))))) ; definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; func :::"CFQ"::: "Al" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k38_substut1 :::"CQC-Sub-WFF"::: ) "Al" ")" ) "," (Set "(" ($#k1_substut1 :::"vSUB"::: ) "Al" ")" ) equals :: SUBSTUT2:def 2 (Set (Set "(" ($#k15_substut1 :::"QSub"::: ) "Al" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k38_substut1 :::"CQC-Sub-WFF"::: ) "Al" ")" )); end; :: deftheorem defines :::"CFQ"::: SUBSTUT2:def 2 : (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k6_substut2 :::"CFQ"::: ) (Set (Var "Al"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k15_substut1 :::"QSub"::: ) (Set (Var "Al")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al")) ")" )))); definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "p" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "Al"))); let "x" be ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Const "Al")); let "Sub" be ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Const "Al")); func :::"QScope"::: "(" "p" "," "x" "," "Sub" ")" -> ($#v1_sublemma :::"CQC-WFF-like"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k16_substut1 :::"QC-Sub-WFF"::: ) "Al" ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "Al" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) equals :: SUBSTUT2:def 3 (Set ($#k7_sublemma :::"["::: ) (Set ($#k2_substut2 :::"["::: ) "p" "," (Set "(" (Set "(" ($#k6_substut2 :::"CFQ"::: ) "Al" ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k2_substut2 :::"["::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" "x" "," "p" ")" ")" ) "," "Sub" ($#k2_substut2 :::"]"::: ) ) ")" ) ($#k2_substut2 :::"]"::: ) ) "," "x" ($#k7_sublemma :::"]"::: ) ); end; :: deftheorem defines :::"QScope"::: SUBSTUT2:def 3 : (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) "holds" (Bool (Set ($#k7_substut2 :::"QScope"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) "," (Set (Var "Sub")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_sublemma :::"["::: ) (Set ($#k2_substut2 :::"["::: ) (Set (Var "p")) "," (Set "(" (Set "(" ($#k6_substut2 :::"CFQ"::: ) (Set (Var "Al")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k2_substut2 :::"["::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "Sub")) ($#k2_substut2 :::"]"::: ) ) ")" ) ($#k2_substut2 :::"]"::: ) ) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) )))))); definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "p" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "Al"))); let "x" be ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Const "Al")); let "Sub" be ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Const "Al")); func :::"Qsc"::: "(" "p" "," "x" "," "Sub" ")" -> ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set ($#k7_substut2 :::"QScope"::: ) "(" "p" "," "x" "," "Sub" ")" ) equals :: SUBSTUT2:def 4 "Sub"; end; :: deftheorem defines :::"Qsc"::: SUBSTUT2:def 4 : (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) "holds" (Bool (Set ($#k8_substut2 :::"Qsc"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) "," (Set (Var "Sub")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "Sub"))))))); theorem :: SUBSTUT2:22 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) "holds" (Bool "(" (Bool (Set ($#k2_substut2 :::"["::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "Sub")) ($#k2_substut2 :::"]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set "(" ($#k7_substut2 :::"QScope"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) "," (Set (Var "Sub")) ")" ")" ) "," (Set "(" ($#k8_substut2 :::"Qsc"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) "," (Set (Var "Sub")) ")" ")" ) ")" )) & (Bool (Set ($#k7_substut2 :::"QScope"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) "," (Set (Var "Sub")) ")" ) "is" ($#v3_substut1 :::"quantifiable"::: ) ) ")" ))))) ; theorem :: SUBSTUT2:23 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool "(" "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) "holds" (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set "(" ($#k39_substut1 :::"CQC_Sub"::: ) (Set ($#k2_substut2 :::"["::: ) (Set (Var "p")) "," (Set (Var "Sub")) ($#k2_substut2 :::"]"::: ) ) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) "holds" (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set "(" ($#k39_substut1 :::"CQC_Sub"::: ) (Set ($#k2_substut2 :::"["::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "Sub")) ($#k2_substut2 :::"]"::: ) ) ")" ))))))) ; theorem :: SUBSTUT2:24 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) "holds" (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "Al")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set "(" ($#k39_substut1 :::"CQC_Sub"::: ) (Set ($#k2_substut2 :::"["::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "Al")) ")" ) "," (Set (Var "Sub")) ($#k2_substut2 :::"]"::: ) ) ")" ))))) ; theorem :: SUBSTUT2:25 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) "holds" (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set "(" ($#k39_substut1 :::"CQC_Sub"::: ) (Set ($#k2_substut2 :::"["::: ) (Set (Var "p")) "," (Set (Var "Sub")) ($#k2_substut2 :::"]"::: ) ) ")" )))))) ; theorem :: SUBSTUT2:26 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool (Set (Var "p")) "is" ($#v2_qc_lang1 :::"atomic"::: ) )) "holds" (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "Al"))(Bool "ex" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "Al")) "st" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "ll"))))))))) ; scheme :: SUBSTUT2:sch 3 CQCInd3{ F1() -> ($#m1_qc_lang1 :::"QC-alphabet"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) "st" (Bool (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool P1[(Set (Var "p"))])) provided (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set F1 "(" ")" ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set F1 "(" ")" ) "holds" (Bool "(" (Bool P1[(Set ($#k5_cqc_lang :::"VERUM"::: ) (Set F1 "(" ")" ))]) & (Bool P1[(Set (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "l")))]) & "(" (Bool (Bool P1[(Set (Var "r"))])) "implies" (Bool P1[(Set ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "r")))]) ")" & "(" (Bool (Bool P1[(Set (Var "r"))]) & (Bool P1[(Set (Var "s"))])) "implies" (Bool P1[(Set (Set (Var "r")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "s")))]) ")" ")" )))))) proof end; begin definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "G", "H" be ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Const "Al")); assume (Bool (Set (Const "G")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Const "H"))) ; mode :::"PATH"::: "of" "G" "," "H" -> ($#m1_hidden :::"FinSequence":::) means :: SUBSTUT2:def 5 (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) it)) & (Bool (Set it ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) "G") & (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) it ")" )) ($#r1_hidden :::"="::: ) "H") & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) it))) "holds" (Bool "ex" (Set (Var "G1")) "," (Set (Var "H1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) "Al") "st" (Bool "(" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Var "G1"))) & (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "H1"))) & (Bool (Set (Var "G1")) ($#r1_qc_lang2 :::"is_immediate_constituent_of"::: ) (Set (Var "H1"))) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"PATH"::: SUBSTUT2:def 5 : (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "G")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "H")))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "b4")) "is" ($#m1_substut2 :::"PATH"::: ) "of" (Set (Var "G")) "," (Set (Var "H"))) "iff" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b4")))) & (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "G"))) & (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "b4")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "H"))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b4"))))) "holds" (Bool "ex" (Set (Var "G1")) "," (Set (Var "H1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "Al"))) "st" (Bool "(" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Var "G1"))) & (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "H1"))) & (Bool (Set (Var "G1")) ($#r1_qc_lang2 :::"is_immediate_constituent_of"::: ) (Set (Var "H1"))) ")" )) ")" ) ")" ) ")" )))); theorem :: SUBSTUT2:27 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "L")) "being" ($#m1_substut2 :::"PATH"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "F2"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "L"))))) "holds" (Bool "ex" (Set (Var "F3")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "Al")) "st" (Bool "(" (Bool (Set (Var "F3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "F3")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "F2"))) ")" )))))) ; theorem :: SUBSTUT2:28 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "F1")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "L")) "being" ($#m1_substut2 :::"PATH"::: ) "of" (Set (Var "F1")) "," (Set (Var "p")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "p"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "L"))))) "holds" (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))))))))) ; theorem :: SUBSTUT2:29 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "L")) "being" ($#m1_substut2 :::"PATH"::: ) "of" (Set (Var "q")) "," (Set (Var "p")) "st" (Bool (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "q")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "p"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "L"))))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "r"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) ")" )))))) ; theorem :: SUBSTUT2:30 (Bool "for" (Set (Var "Al")) "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 "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Var "q")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "p")))) "holds" (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "q"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))))) ; theorem :: SUBSTUT2:31 (Bool "for" (Set (Var "Al")) "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 "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool "(" "for" (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool (Set (Var "q")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "p")))) "holds" (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) ")" )) "holds" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: SUBSTUT2:32 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool "(" "for" (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool (Set (Var "q")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "p")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "r")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "holds" (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )))) ")" )) "holds" (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: SUBSTUT2:33 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool "(" "for" (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool (Set (Var "q")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "p")))) "holds" (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "q"))) ($#r1_hidden :::"<>"::: ) (Num 1)) ")" )) "holds" (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: SUBSTUT2:34 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "p"))))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "st" (Bool "(" (Bool (Set (Var "q")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "p"))) & (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" )))) ;