:: CALCUL_2  semantic presentation begin  




























definitionlet "m", "n" be   ($#v7_ordinal1 :::"natural"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"seq":::  "(" "m" "," "n" ")"  ->    ($#m1_hidden :::"set"::: )   equals :: CALCUL_2:def 1  "{"  (Set (Var "k")) where k "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool  "("  (Bool (Set (Num 1)  ($#k2_nat_1 :::"+"::: )  "m")  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set "n"  ($#k2_xcmplx_0 :::"+"::: )  "m"))  ")" )  "}"  ; end; 






:: deftheorem    defines :::"seq"::: CALCUL_2:def 1 :  (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#v7_ordinal1 :::"natural"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k1_calcul_2 :::"seq"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set (Var "k")) where k "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool  "("  (Bool (Set (Num 1)  ($#k2_nat_1 :::"+"::: )  (Set (Var "m")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "m"))))  ")" )  "}"  )); 
 definitionlet "m", "n" be   ($#v7_ordinal1 :::"natural"::: )     ($#m1_hidden :::"number"::: )  ; :: original: :::"seq"::: redefine func  :::"seq":::  "(" "m" "," "n" ")"  ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ); end; 
theorem :: CALCUL_2:1 (Bool  "for" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v7_ordinal1 :::"natural"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_calcul_2 :::"seq"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool  "("  (Bool (Set (Num 1)  ($#k2_nat_1 :::"+"::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "c"))) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "b"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a"))))  ")" )  ")" )) ; 
 
theorem :: CALCUL_2:2 (Bool  "for" (Set (Var "a")) "being"   ($#v7_ordinal1 :::"natural"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k2_calcul_2 :::"seq"::: )   "(" (Set (Var "a")) "," (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: CALCUL_2:3 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#v7_ordinal1 :::"natural"::: )     ($#m1_hidden :::"number"::: )    "holds"  (Bool  "("  (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Set (Var "b"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a")))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_calcul_2 :::"seq"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))  ")" )) ; 
 
theorem :: CALCUL_2:4 (Bool  "for" (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "a")) "being"   ($#v7_ordinal1 :::"natural"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b2"))) "iff" (Bool (Set   ($#k2_calcul_2 :::"seq"::: )   "(" (Set (Var "a")) "," (Set (Var "b1")) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k2_calcul_2 :::"seq"::: )   "(" (Set (Var "a")) "," (Set (Var "b2")) ")" ))  ")" )) ; 
 
theorem :: CALCUL_2:5 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v7_ordinal1 :::"natural"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k2_calcul_2 :::"seq"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "(" (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_calcul_2 :::"seq"::: )   "(" (Set (Var "a")) "," (Set  "(" (Set (Var "b"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))) ; 
 
theorem :: CALCUL_2:6 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k2_calcul_2 :::"seq"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" ) "," (Set (Var "n"))  ($#r2_wellord2 :::"are_equipotent"::: )  )) ; 
 registrationlet "m", "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set   ($#k1_calcul_2 :::"seq"::: )   "(" "m" "," "n" ")" ) ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; registrationlet "Al" be    ($#m1_qc_lang1 :::"QC-alphabet"::: )  ; let "f" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Const "Al"))); 
cluster (Set   ($#k1_card_1 :::"card"::: )  "f") ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; 
theorem :: CALCUL_2:7 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k2_calcul_2 :::"seq"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "(" (Set (Var "m"))  ($#k2_nat_1 :::"+"::: )  (Set (Var "n")) ")" )))) ; 
 
theorem :: CALCUL_2:8 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")))  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k2_calcul_2 :::"seq"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) ")" ))) ; 
 
theorem :: CALCUL_2:9 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set  "(" (Set (Var "f"))  ($#k7_finseq_1 :::"^"::: )  (Set (Var "g")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_calcul_2 :::"seq"::: )   "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")) ")" ) ")"  ")" )))) ; 
 
theorem :: CALCUL_2:10 (Bool  "for" (Set (Var "Al")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "g")) "," (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al"))) "holds"  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k14_finseq_1 :::"Sgm"::: )  (Set  "("  ($#k2_calcul_2 :::"seq"::: )   "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")) ")" ) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ) ")"  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))))) ; 
 
theorem :: CALCUL_2:11 (Bool  "for" (Set (Var "Al")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "g")) "," (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al"))) "holds"  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set  "("  ($#k14_finseq_1 :::"Sgm"::: )  (Set  "("  ($#k2_calcul_2 :::"seq"::: )   "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")) ")" ) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ) ")"  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))))) ; 
 
theorem :: CALCUL_2:12 (Bool  "for" (Set (Var "Al")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "g")) "," (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al"))) "holds"  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set  "("  ($#k14_finseq_1 :::"Sgm"::: )  (Set  "("  ($#k2_calcul_2 :::"seq"::: )   "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")) ")" ) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ) ")"  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_calcul_2 :::"seq"::: )   "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")) ")" ) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ) ")" )))) ; 
 
theorem :: CALCUL_2:13 (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 "g")) "," (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")))  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set  "("  ($#k14_finseq_1 :::"Sgm"::: )  (Set  "("  ($#k2_calcul_2 :::"seq"::: )   "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")) ")" ) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ) ")"  ")" ) ")" )))) "holds"  (Bool (Set (Set  "("  ($#k14_finseq_1 :::"Sgm"::: )  (Set  "("  ($#k2_calcul_2 :::"seq"::: )   "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")) ")" ) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ) ")"  ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")) ")" )  ($#k2_nat_1 :::"+"::: )  (Set (Var "i"))))))) ; 
 
theorem :: CALCUL_2:14 (Bool  "for" (Set (Var "Al")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "g")) "," (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al"))) "holds"  (Bool (Set   ($#k2_calcul_2 :::"seq"::: )   "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")) ")" ) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set  "(" (Set (Var "g"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "f")) ")" ))))) ; 
 
theorem :: CALCUL_2:15 (Bool  "for" (Set (Var "Al")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "g")) "," (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al"))) "holds"  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set  "(" (Set  "(" (Set (Var "g"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "f")) ")" )  ($#k5_relset_1 :::"|"::: )  (Set  "("  ($#k2_calcul_2 :::"seq"::: )   "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")) ")" ) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ) ")"  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_calcul_2 :::"seq"::: )   "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")) ")" ) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ) ")" )))) ; 
 
theorem :: CALCUL_2:16 (Bool  "for" (Set (Var "Al")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "g")) "," (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al"))) "holds"  (Bool (Set   ($#k15_finseq_1 :::"Seq"::: )  (Set  "(" (Set  "(" (Set (Var "g"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "f")) ")" )  ($#k5_relset_1 :::"|"::: )  (Set  "("  ($#k2_calcul_2 :::"seq"::: )   "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")) ")" ) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ) ")"  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k14_finseq_1 :::"Sgm"::: )  (Set  "("  ($#k2_calcul_2 :::"seq"::: )   "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")) ")" ) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ) ")"  ")" ) ")" )  ($#k4_relset_1 :::"*"::: )  (Set  "(" (Set (Var "g"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "f")) ")" ))))) ; 
 
theorem :: CALCUL_2:17 (Bool  "for" (Set (Var "Al")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "g")) "," (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al"))) "holds"  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set  "("  ($#k15_finseq_1 :::"Seq"::: )  (Set  "(" (Set  "(" (Set (Var "g"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "f")) ")" )  ($#k5_relset_1 :::"|"::: )  (Set  "("  ($#k2_calcul_2 :::"seq"::: )   "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")) ")" ) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ) ")"  ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))))) ; 
 
theorem :: CALCUL_2:18 (Bool  "for" (Set (Var "Al")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al"))) "holds"  (Bool (Set (Var "f"))  ($#r2_calcul_1 :::"is_Subsequence_of"::: )  (Set (Set (Var "g"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "f")))))) ; 
 definitionlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "f" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Const "D")); let "P" be   ($#m1_subset_1 :::"Permutation":::) "of" (Set  "("  ($#k1_relset_1 :::"dom"::: )  (Set (Const "f")) ")" ); func  :::"Per":::  "(" "f" "," "P" ")"  ->    ($#m2_finseq_1 :::"FinSequence"::: )   "of" "D" equals :: CALCUL_2:def 2 (Set "P"  ($#k4_relset_1 :::"*"::: )  "f"); end; 







:: deftheorem    defines :::"Per"::: CALCUL_2:def 2 :  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set  "("  ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")) ")" ) "holds"  (Bool (Set   ($#k3_calcul_2 :::"Per"::: )   "(" (Set (Var "f")) "," (Set (Var "P")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "P"))  ($#k4_relset_1 :::"*"::: )  (Set (Var "f"))))))); 
 



theorem :: CALCUL_2:19 (Bool  "for" (Set (Var "Al")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")))  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set  "("  ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")) ")" ) "holds"  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set  "("  ($#k3_calcul_2 :::"Per"::: )   "(" (Set (Var "f")) "," (Set (Var "P")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f"))))))) ; 
 
theorem :: CALCUL_2:20 (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 "f")) "," (Set (Var "g")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")))  "st" (Bool (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) )))) "holds"  (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set  "(" (Set (Var "g"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "f")) ")" )  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) )))))) ; 
 begin  definitionlet "Al" be    ($#m1_qc_lang1 :::"QC-alphabet"::: )  ; let "f" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Const "Al"))); func  :::"Begin"::: "f" ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  "Al") means :: CALCUL_2:def 3 (Bool it  ($#r1_hidden :::"="::: )  (Set "f"  ($#k1_funct_1 :::"."::: )  (Num 1))) if (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "f"))  otherwise (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k5_cqc_lang :::"VERUM"::: )  "Al")); end; 






:: deftheorem    defines :::"Begin"::: CALCUL_2:def 3 :  (Bool  "for" (Set (Var "Al")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")))  (Bool  "for" (Set (Var "b3")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al"))) "holds"   (Bool  "("   "("  (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f"))))) "implies" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_calcul_2 :::"Begin"::: )  (Set (Var "f")))) "iff" (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Num 1)))  ")" )  ")"  &  "("  (Bool (Bool (Bool  "not" (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))))) "implies" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_calcul_2 :::"Begin"::: )  (Set (Var "f")))) "iff" (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_cqc_lang :::"VERUM"::: )  (Set (Var "Al"))))  ")" )  ")"   ")" )))); 
 definitionlet "Al" be    ($#m1_qc_lang1 :::"QC-alphabet"::: )  ; let "f" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Const "Al"))); assume 
(Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Const "f"))))
 ; func  :::"Impl"::: "f" ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  "Al") means :: CALCUL_2:def 4 (Bool  "ex" (Set (Var "F")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  "Al") "st"  (Bool  "("  (Bool it  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  "f" ")" ))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "f")) & (Bool  "("  (Bool (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set   ($#k4_calcul_2 :::"Begin"::: )  "f")) "or" (Bool (Set   ($#k3_finseq_1 :::"len"::: )  "f")  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "f"))) "holds"  (Bool  "ex" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  "Al") "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set "f"  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))) & (Bool (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q"))))  ")" ))  ")" )  ")" )); end; 







:: deftheorem    defines :::"Impl"::: CALCUL_2:def 4 :  (Bool  "for" (Set (Var "Al")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")))  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f"))))) "holds"  (Bool  "for" (Set (Var "b3")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al"))) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_calcul_2 :::"Impl"::: )  (Set (Var "f")))) "iff" (Bool  "ex" (Set (Var "F")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al"))) "st"  (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool  "("  (Bool (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set   ($#k4_calcul_2 :::"Begin"::: )  (Set (Var "f")))) "or" (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f"))))) "holds"  (Bool  "ex" (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 (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))) & (Bool (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q"))))  ")" ))  ")" )  ")" ))  ")" )))); 
 
theorem :: CALCUL_2:21 (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 "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al"))) "holds"  (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set  "(" (Set (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) ) ")" )  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) )))))) ; 
 
theorem :: CALCUL_2:22 (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 "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")))  "st" (Bool (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  "(" (Set (Var "p"))  ($#k7_cqc_lang :::"'&'"::: )  (Set (Var "q")) ")" ) ($#k12_finseq_1 :::"*>"::: ) )))) "holds"  (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) )))))) ; 
 
theorem :: CALCUL_2:23 (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 "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")))  "st" (Bool (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  "(" (Set (Var "p"))  ($#k7_cqc_lang :::"'&'"::: )  (Set (Var "q")) ")" ) ($#k12_finseq_1 :::"*>"::: ) )))) "holds"  (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "q")) ($#k12_finseq_1 :::"*>"::: ) )))))) ; 
 
theorem :: CALCUL_2:24 (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 "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")))  "st" (Bool (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) ))) & (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set  "(" (Set (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) ) ")" )  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "q")) ($#k12_finseq_1 :::"*>"::: ) )))) "holds"  (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "q")) ($#k12_finseq_1 :::"*>"::: ) )))))) ; 
 
theorem :: CALCUL_2:25 (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 "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")))  "st" (Bool (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) ))) & (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" ) ($#k12_finseq_1 :::"*>"::: ) )))) "holds"  (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "q")) ($#k12_finseq_1 :::"*>"::: ) )))))) ; 
 
theorem :: CALCUL_2:26 (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 "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")))  "st" (Bool (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set  "(" (Set (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) ) ")" )  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "q")) ($#k12_finseq_1 :::"*>"::: ) ))) & (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set  "(" (Set (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ")" )  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "q")) ($#k12_finseq_1 :::"*>"::: ) )))) "holds"  (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "q")) ($#k12_finseq_1 :::"*>"::: ) )))))) ; 
 
theorem :: CALCUL_2:27 (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 "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")))  "st" (Bool (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set  "(" (Set (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) ) ")" )  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "q")) ($#k12_finseq_1 :::"*>"::: ) )))) "holds"  (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")) ")" ) ($#k12_finseq_1 :::"*>"::: ) )))))) ; 
 
theorem :: CALCUL_2:28 (Bool  "for" (Set (Var "Al")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "g")) "," (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")))  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")))) & (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "g"))))) "holds"  (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  "("  ($#k5_calcul_2 :::"Impl"::: )  (Set  "("  ($#k4_finseq_5 :::"Rev"::: )  (Set (Var "g")) ")" ) ")" ) ($#k12_finseq_1 :::"*>"::: ) ))))) ; 
 
theorem :: CALCUL_2:29 (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 "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")))  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set  "("  ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")) ")" )  "st" (Bool (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set  "("  ($#k3_calcul_2 :::"Per"::: )   "(" (Set (Var "f")) "," (Set (Var "P")) ")"  ")" )  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  "("  ($#k5_calcul_2 :::"Impl"::: )  (Set  "("  ($#k4_finseq_5 :::"Rev"::: )  (Set  "(" (Set (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ")" ) ($#k12_finseq_1 :::"*>"::: ) )))) "holds"  (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set  "("  ($#k3_calcul_2 :::"Per"::: )   "(" (Set (Var "f")) "," (Set (Var "P")) ")"  ")" )  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) ))))))) ; 
 
theorem :: CALCUL_2:30 (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 "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")))  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set  "("  ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")) ")" )  "st" (Bool (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) )))) "holds"  (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set  "("  ($#k3_calcul_2 :::"Per"::: )   "(" (Set (Var "f")) "," (Set (Var "P")) ")"  ")" )  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) ))))))) ; 
 begin  notationlet "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "c" be    ($#m1_hidden :::"set"::: )  ; synonym  :::"IdFinS":::  "(" "c" "," "n" ")"  for "n" :::"|->"::: "c"; end; 
theorem :: CALCUL_2:31 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "c")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k2_finseq_2 :::"IdFinS"::: )   "(" (Set (Var "c")) "," (Set (Var "n")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "c")) ($#k9_finseq_1 :::"*>"::: ) ))))) ; 
 definitionlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "p" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "D")); :: original: :::"IdFinS"::: redefine func  :::"IdFinS":::  "(" "p" "," "n" ")"  ->    ($#m2_finseq_1 :::"FinSequence"::: )   "of" "D"; end; 
theorem :: CALCUL_2:32 (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 "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")))  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set  "(" (Set (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set  "("  ($#k6_calcul_2 :::"IdFinS"::: )   "(" (Set (Var "p")) "," (Set (Var "n")) ")"  ")" ) ")" )  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "q")) ($#k12_finseq_1 :::"*>"::: ) )))) "holds"  (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set  "(" (Set (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) ) ")" )  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "q")) ($#k12_finseq_1 :::"*>"::: ) ))))))) ;