:: HILBERT2  semantic presentation begin  




theorem :: HILBERT2:1 (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "Z"))  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set (Var "M"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x"))) "is"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "x")))  ")" )) "holds"  (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_card_3 :::"Union"::: )  (Set (Var "M"))))) "holds"  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "Z"))))))) ; 
 
theorem :: HILBERT2:2 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"FinSequence":::)  "st" (Bool (Bool (Set (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) )  ($#k7_finseq_1 :::"^"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k9_finseq_1 :::"*>"::: ) )  ($#k7_finseq_1 :::"^"::: )  (Set (Var "g"))))) "holds"  (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "g"))))) ; 
 
theorem :: HILBERT2:3 (Bool  "for" (Set (Var "x")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) ) "is"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "X")))) "holds"  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) ; 
 
theorem :: HILBERT2:4 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool  "ex" (Set (Var "g")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "X"))(Bool  "ex" (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X")) "st" (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k7_finseq_1 :::"^"::: )  (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "d")) ($#k9_finseq_1 :::"*>"::: ) ))))))) ; 
 

















theorem :: HILBERT2:5 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T1")) "," (Set (Var "T2")) "being"   ($#m1_hidden :::"Tree":::) "holds"   (Bool  "("  (Bool (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k13_trees_3 :::"tree"::: )   "(" (Set (Var "T1")) "," (Set (Var "T2")) ")" )) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )  ")" ))) ; 
 scheme  :: HILBERT2:sch 1 InTreeInd{ F1() ->   ($#m1_hidden :::"Tree":::), P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "for" (Set (Var "f")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) "holds"  (Bool P1[(Set (Var "f"))]))
 provided
(Bool P1[(Set   ($#k6_finseq_1 :::"<*>"::: )  (Set  ($#k5_numbers :::"NAT"::: ) ))])
 and  
(Bool  "for" (Set (Var "f")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  "st" (Bool (Bool P1[(Set (Var "f"))])) "holds"  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) ))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" ))) "holds"  (Bool P1[(Set (Set (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) ))])))
 proof 


end; 




theorem :: HILBERT2:6 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T1")) "," (Set (Var "T2")) "being"   ($#m1_hidden :::"DecoratedTree":::) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k6_trees_4 :::"-tree"::: )   "(" (Set (Var "T1")) "," (Set (Var "T2")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "x"))))) ; 
 
theorem :: HILBERT2:7 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T1")) "," (Set (Var "T2")) "being"   ($#m1_hidden :::"DecoratedTree":::) "holds"   (Bool  "("  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k6_trees_4 :::"-tree"::: )   "(" (Set (Var "T1")) "," (Set (Var "T2")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "T1"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))) & (Bool (Set (Set  "(" (Set (Var "x"))  ($#k6_trees_4 :::"-tree"::: )   "(" (Set (Var "T1")) "," (Set (Var "T2")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "T2"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) )))  ")" ))) ; 
 
theorem :: HILBERT2:8 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T1")) "," (Set (Var "T2")) "being"   ($#m1_hidden :::"DecoratedTree":::) "holds"   (Bool  "("  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k6_trees_4 :::"-tree"::: )   "(" (Set (Var "T1")) "," (Set (Var "T2")) ")"  ")" )  ($#k5_trees_2 :::"|"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "T1"))) & (Bool (Set (Set  "(" (Set (Var "x"))  ($#k6_trees_4 :::"-tree"::: )   "(" (Set (Var "T1")) "," (Set (Var "T2")) ")"  ")" )  ($#k5_trees_2 :::"|"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "T2")))  ")" ))) ; 
 registrationlet "x" be    ($#m1_hidden :::"set"::: )  ; let "p" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v6_trees_3 :::"DTree-yielding"::: )    ($#m1_hidden :::"FinSequence":::); 
cluster (Set "x"  ($#k4_trees_4 :::"-tree"::: )  "p") ->  ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"root"::: )   )  ; 
end; registrationlet "x" be    ($#m1_hidden :::"set"::: )  ; let "T1" be   ($#m1_hidden :::"DecoratedTree":::); 
cluster (Set "x"  ($#k5_trees_4 :::"-tree"::: )  "T1") ->  ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"root"::: )   )  ; 
let "T2" be   ($#m1_hidden :::"DecoratedTree":::); 
cluster (Set "x"  ($#k6_trees_4 :::"-tree"::: )   "(" "T1" "," "T2" ")" ) ->  ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"root"::: )   )  ; 
end; begin  definitionlet "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); func  :::"prop"::: "n" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  ) equals :: HILBERT2:def 1 (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  "(" (Num 3)  ($#k2_nat_1 :::"+"::: )  "n" ")" ) ($#k12_finseq_1 :::"*>"::: ) ); end; 





:: deftheorem    defines :::"prop"::: HILBERT2:def 1 :  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k1_hilbert2 :::"prop"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  "(" (Num 3)  ($#k2_nat_1 :::"+"::: )  (Set (Var "n")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ))); 
 definitionlet "D" be    ($#m1_hidden :::"set"::: )  ; redefine attr "D" is  :::"with_VERUM":::  means :: HILBERT2:def 2 (Bool (Set   ($#k2_hilbert1 :::"VERUM"::: )  )  ($#r2_hidden :::"in"::: )  "D"); redefine attr "D" is  :::"with_propositional_variables":::  means :: HILBERT2:def 3 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k1_hilbert2 :::"prop"::: )  (Set (Var "n")))  ($#r2_hidden :::"in"::: )  "D")); end; 








:: deftheorem    defines :::"with_VERUM"::: HILBERT2:def 2 :  (Bool  "for" (Set (Var "D")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "D")) "is"   ($#v1_hilbert1 :::"with_VERUM"::: )  ) "iff" (Bool (Set   ($#k2_hilbert1 :::"VERUM"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "D")))  ")" )); 
 
:: deftheorem    defines :::"with_propositional_variables"::: HILBERT2:def 3 :  (Bool  "for" (Set (Var "D")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "D")) "is"   ($#v4_hilbert1 :::"with_propositional_variables"::: )  ) "iff" (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k1_hilbert2 :::"prop"::: )  (Set (Var "n")))  ($#r2_hidden :::"in"::: )  (Set (Var "D"))))  ")" )); 
 definitionlet "D" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_hilbert1 :::"HP-WFF"::: ) ); redefine attr "D" is  :::"with_implication":::  means :: HILBERT2:def 4 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  )  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  "D") & (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  "D")) "holds"  (Bool (Set (Set (Var "p"))  ($#k3_hilbert1 :::"=>"::: )  (Set (Var "q")))  ($#r2_hidden :::"in"::: )  "D")); redefine attr "D" is  :::"with_conjunction":::  means :: HILBERT2:def 5 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  )  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  "D") & (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  "D")) "holds"  (Bool (Set (Set (Var "p"))  ($#k4_hilbert1 :::"'&'"::: )  (Set (Var "q")))  ($#r2_hidden :::"in"::: )  "D")); end; 








:: deftheorem    defines :::"with_implication"::: HILBERT2:def 4 :  (Bool  "for" (Set (Var "D")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "D")) "is"   ($#v2_hilbert1 :::"with_implication"::: )  ) "iff" (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  )  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "D"))) & (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set (Var "D")))) "holds"  (Bool (Set (Set (Var "p"))  ($#k3_hilbert1 :::"=>"::: )  (Set (Var "q")))  ($#r2_hidden :::"in"::: )  (Set (Var "D"))))  ")" )); 
 
:: deftheorem    defines :::"with_conjunction"::: HILBERT2:def 5 :  (Bool  "for" (Set (Var "D")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "D")) "is"   ($#v3_hilbert1 :::"with_conjunction"::: )  ) "iff" (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  )  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "D"))) & (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set (Var "D")))) "holds"  (Bool (Set (Set (Var "p"))  ($#k4_hilbert1 :::"'&'"::: )  (Set (Var "q")))  ($#r2_hidden :::"in"::: )  (Set (Var "D"))))  ")" )); 
 



definitionlet "p" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  ); attr "p" is  :::"conjunctive":::  means :: HILBERT2:def 6 (Bool  "ex" (Set (Var "r")) "," (Set (Var "s")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  ) "st" (Bool "p"  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k4_hilbert1 :::"'&'"::: )  (Set (Var "s"))))); attr "p" is  :::"conditional":::  means :: HILBERT2:def 7 (Bool  "ex" (Set (Var "r")) "," (Set (Var "s")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  ) "st" (Bool "p"  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k3_hilbert1 :::"=>"::: )  (Set (Var "s"))))); attr "p" is  :::"simple":::  means :: HILBERT2:def 8 (Bool  "ex" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st" (Bool "p"  ($#r1_hidden :::"="::: )  (Set   ($#k1_hilbert2 :::"prop"::: )  (Set (Var "n"))))); end; 












:: deftheorem    defines :::"conjunctive"::: HILBERT2:def 6 :  (Bool  "for" (Set (Var "p")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "p")) "is"   ($#v1_hilbert2 :::"conjunctive"::: )  ) "iff" (Bool  "ex" (Set (Var "r")) "," (Set (Var "s")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  ) "st" (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k4_hilbert1 :::"'&'"::: )  (Set (Var "s")))))  ")" )); 
 
:: deftheorem    defines :::"conditional"::: HILBERT2:def 7 :  (Bool  "for" (Set (Var "p")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "p")) "is"   ($#v2_hilbert2 :::"conditional"::: )  ) "iff" (Bool  "ex" (Set (Var "r")) "," (Set (Var "s")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  ) "st" (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k3_hilbert1 :::"=>"::: )  (Set (Var "s")))))  ")" )); 
 
:: deftheorem    defines :::"simple"::: HILBERT2:def 8 :  (Bool  "for" (Set (Var "p")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "p")) "is"   ($#v3_hilbert2 :::"simple"::: )  ) "iff" (Bool  "ex" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st" (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_hilbert2 :::"prop"::: )  (Set (Var "n")))))  ")" )); 
 scheme  :: HILBERT2:sch 2 HPInd{ P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "for" (Set (Var "r")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  ) "holds"  (Bool P1[(Set (Var "r"))]))
 provided
(Bool P1[(Set   ($#k2_hilbert1 :::"VERUM"::: )  )])
 and  
(Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool P1[(Set   ($#k1_hilbert2 :::"prop"::: )  (Set (Var "n")))]))
 and  
(Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  )  "st" (Bool (Bool P1[(Set (Var "r"))]) & (Bool P1[(Set (Var "s"))])) "holds"  (Bool  "("  (Bool P1[(Set (Set (Var "r"))  ($#k4_hilbert1 :::"'&'"::: )  (Set (Var "s")))]) & (Bool P1[(Set (Set (Var "r"))  ($#k3_hilbert1 :::"=>"::: )  (Set (Var "s")))])  ")" ))
 proof 


end; 
theorem :: HILBERT2:9 (Bool  "for" (Set (Var "p")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  )  "holds"  (Bool  "("  (Bool (Set (Var "p")) "is"   ($#v1_hilbert2 :::"conjunctive"::: )  ) "or" (Bool (Set (Var "p")) "is"   ($#v2_hilbert2 :::"conditional"::: )  ) "or" (Bool (Set (Var "p")) "is"   ($#v3_hilbert2 :::"simple"::: )  ) "or" (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_hilbert1 :::"VERUM"::: )  ))  ")" )) ; 
 
theorem :: HILBERT2:10 (Bool  "for" (Set (Var "p")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  ) "holds"  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) ; 
 
theorem :: HILBERT2:11 (Bool  "for" (Set (Var "p")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  )  "st" (Bool (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Var "p")) "is"   ($#v2_hilbert2 :::"conditional"::: )  )) ; 
 
theorem :: HILBERT2:12 (Bool  "for" (Set (Var "p")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  )  "st" (Bool (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Num 2))) "holds"  (Bool (Set (Var "p")) "is"   ($#v1_hilbert2 :::"conjunctive"::: )  )) ; 
 
theorem :: HILBERT2:13 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  )  "st" (Bool (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Num 3)  ($#k2_nat_1 :::"+"::: )  (Set (Var "n"))))) "holds"  (Bool (Set (Var "p")) "is"   ($#v3_hilbert2 :::"simple"::: )  ))) ; 
 
theorem :: HILBERT2:14 (Bool  "for" (Set (Var "p")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  )  "st" (Bool (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_hilbert1 :::"VERUM"::: )  ))) ; 
 
theorem :: HILBERT2:15 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  ) "holds"   (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "(" (Set (Var "p"))  ($#k4_hilbert1 :::"'&'"::: )  (Set (Var "q")) ")" ))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "q")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "(" (Set (Var "p"))  ($#k4_hilbert1 :::"'&'"::: )  (Set (Var "q")) ")" )))  ")" )) ; 
 
theorem :: HILBERT2:16 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  ) "holds"   (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "(" (Set (Var "p"))  ($#k3_hilbert1 :::"=>"::: )  (Set (Var "q")) ")" ))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "q")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "(" (Set (Var "p"))  ($#k3_hilbert1 :::"=>"::: )  (Set (Var "q")) ")" )))  ")" )) ; 
 
theorem :: HILBERT2:17 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  )  (Bool  "for" (Set (Var "t")) "being"   ($#m1_hidden :::"FinSequence":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "q"))  ($#k7_finseq_1 :::"^"::: )  (Set (Var "t"))))) "holds"  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "q"))))) ; 
 
theorem :: HILBERT2:18 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  )  "st" (Bool (Bool (Set (Set (Var "p"))  ($#k7_finseq_1 :::"^"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k7_finseq_1 :::"^"::: )  (Set (Var "s"))))) "holds"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "r"))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Var "s")))  ")" )) ; 
 
theorem :: HILBERT2:19 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  )  "st" (Bool (Bool (Set (Set (Var "p"))  ($#k4_hilbert1 :::"'&'"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k4_hilbert1 :::"'&'"::: )  (Set (Var "s"))))) "holds"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "r"))) & (Bool (Set (Var "s"))  ($#r1_hidden :::"="::: )  (Set (Var "q")))  ")" )) ; 
 
theorem :: HILBERT2:20 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  )  "st" (Bool (Bool (Set (Set (Var "p"))  ($#k3_hilbert1 :::"=>"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k3_hilbert1 :::"=>"::: )  (Set (Var "s"))))) "holds"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "r"))) & (Bool (Set (Var "s"))  ($#r1_hidden :::"="::: )  (Set (Var "q")))  ")" )) ; 
 
theorem :: HILBERT2:21 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set   ($#k1_hilbert2 :::"prop"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_hilbert2 :::"prop"::: )  (Set (Var "m"))))) "holds"  (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set (Var "m")))) ; 
 
theorem :: HILBERT2:22 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  )  "holds" (Bool (Set (Set (Var "p"))  ($#k4_hilbert1 :::"'&'"::: )  (Set (Var "q")))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "r"))  ($#k3_hilbert1 :::"=>"::: )  (Set (Var "s"))))) ; 
 
theorem :: HILBERT2:23 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  )  "holds" (Bool (Set (Set (Var "p"))  ($#k4_hilbert1 :::"'&'"::: )  (Set (Var "q")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_hilbert1 :::"VERUM"::: )  ))) ; 
 
theorem :: HILBERT2:24 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  )  "holds" (Bool (Set (Set (Var "p"))  ($#k4_hilbert1 :::"'&'"::: )  (Set (Var "q")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_hilbert2 :::"prop"::: )  (Set (Var "n")))))) ; 
 
theorem :: HILBERT2:25 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  )  "holds" (Bool (Set (Set (Var "p"))  ($#k3_hilbert1 :::"=>"::: )  (Set (Var "q")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_hilbert1 :::"VERUM"::: )  ))) ; 
 
theorem :: HILBERT2:26 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  )  "holds" (Bool (Set (Set (Var "p"))  ($#k3_hilbert1 :::"=>"::: )  (Set (Var "q")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_hilbert2 :::"prop"::: )  (Set (Var "n")))))) ; 
 
theorem :: HILBERT2:27 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  ) "holds"   (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k4_hilbert1 :::"'&'"::: )  (Set (Var "q")))  ($#r1_hidden :::"<>"::: )  (Set (Var "p"))) & (Bool (Set (Set (Var "p"))  ($#k4_hilbert1 :::"'&'"::: )  (Set (Var "q")))  ($#r1_hidden :::"<>"::: )  (Set (Var "q")))  ")" )) ; 
 
theorem :: HILBERT2:28 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  ) "holds"   (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k3_hilbert1 :::"=>"::: )  (Set (Var "q")))  ($#r1_hidden :::"<>"::: )  (Set (Var "p"))) & (Bool (Set (Set (Var "p"))  ($#k3_hilbert1 :::"=>"::: )  (Set (Var "q")))  ($#r1_hidden :::"<>"::: )  (Set (Var "q")))  ")" )) ; 
 
theorem :: HILBERT2:29 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds" (Bool (Set   ($#k2_hilbert1 :::"VERUM"::: )  )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_hilbert2 :::"prop"::: )  (Set (Var "n"))))) ; 
 begin  scheme  :: HILBERT2:sch 3 HPMSSExL{ F1() ->    ($#m1_hidden :::"set"::: )  , F2(   ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )) ->    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  ) ","    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  ) ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ], P2[   ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  ) ","    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  ) ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "M")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  ) "st"  (Bool  "("  (Bool (Set (Set (Var "M"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k2_hilbert1 :::"VERUM"::: ) ))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "M"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_hilbert2 :::"prop"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "n")) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  ) "holds"   (Bool  "("  (Bool P1[(Set (Var "p")) "," (Set (Var "q")) "," (Set (Set (Var "M"))  ($#k1_funct_1 :::"."::: )  (Set (Var "p"))) "," (Set (Set (Var "M"))  ($#k1_funct_1 :::"."::: )  (Set (Var "q"))) "," (Set (Set (Var "M"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "p"))  ($#k4_hilbert1 :::"'&'"::: )  (Set (Var "q")) ")" ))]) & (Bool P2[(Set (Var "p")) "," (Set (Var "q")) "," (Set (Set (Var "M"))  ($#k1_funct_1 :::"."::: )  (Set (Var "p"))) "," (Set (Set (Var "M"))  ($#k1_funct_1 :::"."::: )  (Set (Var "q"))) "," (Set (Set (Var "M"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "p"))  ($#k3_hilbert1 :::"=>"::: )  (Set (Var "q")) ")" ))])  ")" )  ")" )  ")" ))
 provided
(Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  )  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )   (Bool  "ex" (Set (Var "c")) "being"    ($#m1_hidden :::"set"::: )   "st" (Bool P1[(Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))]))))
 and  
(Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  )  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )   (Bool  "ex" (Set (Var "d")) "being"    ($#m1_hidden :::"set"::: )   "st" (Bool P2[(Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d"))]))))
 and  
(Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  )  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool P1[(Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))]) & (Bool P1[(Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d"))])) "holds"  (Bool (Set (Var "c"))  ($#r1_hidden :::"="::: )  (Set (Var "d")))))
 and  
(Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  )  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool P2[(Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))]) & (Bool P2[(Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d"))])) "holds"  (Bool (Set (Var "c"))  ($#r1_hidden :::"="::: )  (Set (Var "d")))))
 proof 


end; scheme  :: HILBERT2:sch 4 HPMSSLambda{ F1() ->    ($#m1_hidden :::"set"::: )  , F2(   ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )) ->    ($#m1_hidden :::"set"::: )  , F3(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , F4(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool  "ex" (Set (Var "M")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  ) "st"  (Bool  "("  (Bool (Set (Set (Var "M"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k2_hilbert1 :::"VERUM"::: ) ))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "M"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_hilbert2 :::"prop"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "n")) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  ) "holds"   (Bool  "("  (Bool (Set (Set (Var "M"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "p"))  ($#k4_hilbert1 :::"'&'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set  "(" (Set (Var "M"))  ($#k1_funct_1 :::"."::: )  (Set (Var "p")) ")" ) "," (Set  "(" (Set (Var "M"))  ($#k1_funct_1 :::"."::: )  (Set (Var "q")) ")" ) ")" )) & (Bool (Set (Set (Var "M"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "p"))  ($#k3_hilbert1 :::"=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set  "(" (Set (Var "M"))  ($#k1_funct_1 :::"."::: )  (Set (Var "p")) ")" ) "," (Set  "(" (Set (Var "M"))  ($#k1_funct_1 :::"."::: )  (Set (Var "q")) ")" ) ")" ))  ")" )  ")" )  ")" ))
 proof 


end; begin  definitionfunc  :::"HP-Subformulae":::  ->   ($#m1_hidden :::"ManySortedSet":::) "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  ) means :: HILBERT2:def 9 (Bool  "("  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set  ($#k2_hilbert1 :::"VERUM"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_trees_4 :::"root-tree"::: )  (Set  ($#k2_hilbert1 :::"VERUM"::: ) ))) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_hilbert2 :::"prop"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_trees_4 :::"root-tree"::: )  (Set  "("  ($#k1_hilbert2 :::"prop"::: )  (Set (Var "n")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  ) (Bool  "ex" (Set (Var "p9")) "," (Set (Var "q9")) "being"   ($#m1_hidden :::"DecoratedTree":::) "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "p9"))  ($#r1_hidden :::"="::: )  (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "p")))) & (Bool (Set (Var "q9"))  ($#r1_hidden :::"="::: )  (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "q")))) & (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "p"))  ($#k4_hilbert1 :::"'&'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k4_hilbert1 :::"'&'"::: )  (Set (Var "q")) ")" )  ($#k6_trees_4 :::"-tree"::: )   "(" (Set (Var "p9")) "," (Set (Var "q9")) ")" )) & (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "p"))  ($#k3_hilbert1 :::"=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k3_hilbert1 :::"=>"::: )  (Set (Var "q")) ")" )  ($#k6_trees_4 :::"-tree"::: )   "(" (Set (Var "p9")) "," (Set (Var "q9")) ")" ))  ")" ))  ")" )  ")" ); end; 




:: deftheorem    defines :::"HP-Subformulae"::: HILBERT2:def 9 :  (Bool  "for" (Set (Var "b1")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_hilbert2 :::"HP-Subformulae"::: )  )) "iff" (Bool  "("  (Bool (Set (Set (Var "b1"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k2_hilbert1 :::"VERUM"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_trees_4 :::"root-tree"::: )  (Set  ($#k2_hilbert1 :::"VERUM"::: ) ))) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "b1"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_hilbert2 :::"prop"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_trees_4 :::"root-tree"::: )  (Set  "("  ($#k1_hilbert2 :::"prop"::: )  (Set (Var "n")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  ) (Bool  "ex" (Set (Var "p9")) "," (Set (Var "q9")) "being"   ($#m1_hidden :::"DecoratedTree":::) "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "p9"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "p")))) & (Bool (Set (Var "q9"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "q")))) & (Bool (Set (Set (Var "b1"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "p"))  ($#k4_hilbert1 :::"'&'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k4_hilbert1 :::"'&'"::: )  (Set (Var "q")) ")" )  ($#k6_trees_4 :::"-tree"::: )   "(" (Set (Var "p9")) "," (Set (Var "q9")) ")" )) & (Bool (Set (Set (Var "b1"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "p"))  ($#k3_hilbert1 :::"=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k3_hilbert1 :::"=>"::: )  (Set (Var "q")) ")" )  ($#k6_trees_4 :::"-tree"::: )   "(" (Set (Var "p9")) "," (Set (Var "q9")) ")" ))  ")" ))  ")" )  ")" )  ")" )); 
 definitionlet "p" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  ); func  :::"Subformulae"::: "p" ->   ($#m1_hidden :::"DecoratedTree":::) "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  ) equals :: HILBERT2:def 10 (Set (Set  ($#k2_hilbert2 :::"HP-Subformulae"::: ) )  ($#k1_funct_1 :::"."::: )  "p"); end; 





:: deftheorem    defines :::"Subformulae"::: HILBERT2:def 10 :  (Bool  "for" (Set (Var "p")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  ) "holds"  (Bool (Set   ($#k3_hilbert2 :::"Subformulae"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k2_hilbert2 :::"HP-Subformulae"::: ) )  ($#k1_funct_1 :::"."::: )  (Set (Var "p"))))); 
 
theorem :: HILBERT2:30 (Bool (Set   ($#k3_hilbert2 :::"Subformulae"::: )  (Set  ($#k2_hilbert1 :::"VERUM"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_trees_4 :::"root-tree"::: )  (Set  ($#k2_hilbert1 :::"VERUM"::: ) ))) ; 
 
theorem :: HILBERT2:31 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k3_hilbert2 :::"Subformulae"::: )  (Set  "("  ($#k1_hilbert2 :::"prop"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_trees_4 :::"root-tree"::: )  (Set  "("  ($#k1_hilbert2 :::"prop"::: )  (Set (Var "n")) ")" )))) ; 
 
theorem :: HILBERT2:32 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  ) "holds"  (Bool (Set   ($#k3_hilbert2 :::"Subformulae"::: )  (Set  "(" (Set (Var "p"))  ($#k4_hilbert1 :::"'&'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k4_hilbert1 :::"'&'"::: )  (Set (Var "q")) ")" )  ($#k6_trees_4 :::"-tree"::: )   "(" (Set  "("  ($#k3_hilbert2 :::"Subformulae"::: )  (Set (Var "p")) ")" ) "," (Set  "("  ($#k3_hilbert2 :::"Subformulae"::: )  (Set (Var "q")) ")" ) ")" ))) ; 
 
theorem :: HILBERT2:33 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  ) "holds"  (Bool (Set   ($#k3_hilbert2 :::"Subformulae"::: )  (Set  "(" (Set (Var "p"))  ($#k3_hilbert1 :::"=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k3_hilbert1 :::"=>"::: )  (Set (Var "q")) ")" )  ($#k6_trees_4 :::"-tree"::: )   "(" (Set  "("  ($#k3_hilbert2 :::"Subformulae"::: )  (Set (Var "p")) ")" ) "," (Set  "("  ($#k3_hilbert2 :::"Subformulae"::: )  (Set (Var "q")) ")" ) ")" ))) ; 
 
theorem :: HILBERT2:34 (Bool  "for" (Set (Var "p")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k3_hilbert2 :::"Subformulae"::: )  (Set (Var "p")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "p")))) ; 
 
theorem :: HILBERT2:35 (Bool  "for" (Set (Var "p")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  )  (Bool  "for" (Set (Var "f")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k3_hilbert2 :::"Subformulae"::: )  (Set (Var "p")) ")" )) "holds"  (Bool (Set (Set  "("  ($#k3_hilbert2 :::"Subformulae"::: )  (Set (Var "p")) ")" )  ($#k5_trees_2 :::"|"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_hilbert2 :::"Subformulae"::: )  (Set  "(" (Set  "("  ($#k3_hilbert2 :::"Subformulae"::: )  (Set (Var "p")) ")" )  ($#k3_trees_2 :::"."::: )  (Set (Var "f")) ")" ))))) ; 
 
theorem :: HILBERT2:36 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_hilbert1 :::"HP-WFF"::: )  )  "holds"  (Bool  "("   "not" (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_trees_2 :::"Leaves"::: )  (Set  "("  ($#k3_hilbert2 :::"Subformulae"::: )  (Set (Var "q")) ")" ))) "or" (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_hilbert1 :::"VERUM"::: )  )) "or" (Bool (Set (Var "p")) "is"   ($#v3_hilbert2 :::"simple"::: )  )  ")" )) ;