:: MODAL_1  semantic presentation begin  























definitionlet "Z" be   ($#m1_hidden :::"Tree":::); func  :::"Root"::: "Z" ->    ($#m1_trees_1 :::"Element"::: )   "of" "Z" equals :: MODAL_1:def 1 (Set   ($#k1_xboole_0 :::"{}"::: )  ); end; 





:: deftheorem    defines :::"Root"::: MODAL_1:def 1 :  (Bool  "for" (Set (Var "Z")) "being"   ($#m1_hidden :::"Tree":::) "holds"  (Bool (Set   ($#k1_modal_1 :::"Root"::: )  (Set (Var "Z")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))); 
 definitionlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "T" be   ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Const "D")); func  :::"Root"::: "T" ->    ($#m1_subset_1 :::"Element"::: )   "of" "D" equals :: MODAL_1:def 2 (Set "T"  ($#k3_trees_2 :::"."::: )  (Set  "("  ($#k1_modal_1 :::"Root"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  "T" ")" ) ")" )); end; 






:: deftheorem    defines :::"Root"::: MODAL_1:def 2 :  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Var "D")) "holds"  (Bool (Set   ($#k2_modal_1 :::"Root"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "T"))  ($#k3_trees_2 :::"."::: )  (Set  "("  ($#k1_modal_1 :::"Root"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "T")) ")" ) ")" ))))); 
 
theorem :: MODAL_1:1 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "s")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set (Var "m")))) "holds"  (Bool  "not" (Bool (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "m")) ($#k12_finseq_1 :::"*>"::: ) )  ($#k8_finseq_1 :::"^"::: )  (Set (Var "s")))  ($#r3_xboole_0 :::"are_c=-comparable"::: )  )))) ; 
 
theorem :: MODAL_1:2 (Bool  "for" (Set (Var "s")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "s"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool  "ex" (Set (Var "w")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )(Bool  "ex" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st" (Bool (Set (Var "s"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) )  ($#k8_finseq_1 :::"^"::: )  (Set (Var "w"))))))) ; 
 
theorem :: MODAL_1:3 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "s")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set (Var "m")))) "holds"  (Bool  "not" (Bool (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) )  ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: )  (Set (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "m")) ($#k12_finseq_1 :::"*>"::: ) )  ($#k8_finseq_1 :::"^"::: )  (Set (Var "s"))))))) ; 
 
theorem :: MODAL_1:4 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "s")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set (Var "m")))) "holds"  (Bool  "not" (Bool (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) )  ($#r1_tarski :::"is_a_prefix_of"::: )  (Set (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "m")) ($#k12_finseq_1 :::"*>"::: ) )  ($#k8_finseq_1 :::"^"::: )  (Set (Var "s"))))))) ; 
 
theorem :: MODAL_1:5 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds" (Bool (Bool  "not" (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) )  ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "m")) ($#k12_finseq_1 :::"*>"::: ) )))) ; 
 
theorem :: MODAL_1:6 (Bool (Set   ($#k2_trees_1 :::"elementary_tree"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ($#k2_tarski :::"}"::: ) )) ; 
 
theorem :: MODAL_1:7 (Bool (Set   ($#k2_trees_1 :::"elementary_tree"::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set  ($#k1_enumset1 :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set  ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) ($#k1_enumset1 :::"}"::: ) )) ; 
 
theorem :: MODAL_1:8 (Bool  "for" (Set (Var "Z")) "being"   ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m"))) & (Bool (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "m")) ($#k12_finseq_1 :::"*>"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "Z"))))) ; 
 
theorem :: MODAL_1:9 (Bool  "for" (Set (Var "w")) "," (Set (Var "t")) "," (Set (Var "s")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Set (Var "w"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "t")))  ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: )  (Set (Set (Var "w"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "s"))))) "holds"  (Bool (Set (Var "t"))  ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: )  (Set (Var "s")))) ; 
 
theorem :: MODAL_1:10 (Bool  "for" (Set (Var "t1")) "being"   ($#m1_hidden :::"DecoratedTree":::) "of" (Set  ($#k8_mcart_1 :::"[:"::: ) (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k5_numbers :::"NAT"::: ) ) ($#k8_mcart_1 :::":]"::: ) ) "holds"  (Bool (Set (Var "t1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_partfun1 :::"PFuncs"::: )   "(" (Set  "(" (Set  ($#k5_numbers :::"NAT"::: ) )  ($#k3_finseq_2 :::"*"::: )  ")" ) "," (Set  ($#k8_mcart_1 :::"[:"::: ) (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k5_numbers :::"NAT"::: ) ) ($#k8_mcart_1 :::":]"::: ) ) ")" ))) ; 
 
theorem :: MODAL_1:11 (Bool  "for" (Set (Var "Z")) "," (Set (Var "Z1")) "," (Set (Var "Z2")) "being"   ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "z")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Var "Z"))  "st" (Bool (Bool (Set (Set (Var "Z"))  ($#k5_trees_1 :::"with-replacement"::: )   "(" (Set (Var "z")) "," (Set (Var "Z1")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "Z"))  ($#k5_trees_1 :::"with-replacement"::: )   "(" (Set (Var "z")) "," (Set (Var "Z2")) ")" ))) "holds"  (Bool (Set (Var "Z1"))  ($#r1_hidden :::"="::: )  (Set (Var "Z2"))))) ; 
 
theorem :: MODAL_1:12 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Z")) "," (Set (Var "Z1")) "," (Set (Var "Z2")) "being"   ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Var "D"))  (Bool  "for" (Set (Var "z")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "Z")))  "st" (Bool (Bool (Set (Set (Var "Z"))  ($#k7_trees_2 :::"with-replacement"::: )   "(" (Set (Var "z")) "," (Set (Var "Z1")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "Z"))  ($#k7_trees_2 :::"with-replacement"::: )   "(" (Set (Var "z")) "," (Set (Var "Z2")) ")" ))) "holds"  (Bool (Set (Var "Z1"))  ($#r1_hidden :::"="::: )  (Set (Var "Z2")))))) ; 
 
theorem :: MODAL_1:13 (Bool  "for" (Set (Var "Z1")) "," (Set (Var "Z2")) "being"   ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z1")))) "holds"  (Bool  "for" (Set (Var "v")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Set (Var "Z1"))  ($#k5_trees_1 :::"with-replacement"::: )   "(" (Set (Var "p")) "," (Set (Var "Z2")) ")" )  (Bool  "for" (Set (Var "w")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Var "Z1"))  "st" (Bool (Bool (Set (Var "v"))  ($#r1_hidden :::"="::: )  (Set (Var "w"))) & (Bool (Set (Var "w"))  ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: )  (Set (Var "p")))) "holds"  (Bool (Set   ($#k1_trees_2 :::"succ"::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_trees_2 :::"succ"::: )  (Set (Var "w")))))))) ; 
 
theorem :: MODAL_1:14 (Bool  "for" (Set (Var "Z1")) "," (Set (Var "Z2")) "being"   ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z1")))) "holds"  (Bool  "for" (Set (Var "v")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Set (Var "Z1"))  ($#k5_trees_1 :::"with-replacement"::: )   "(" (Set (Var "p")) "," (Set (Var "Z2")) ")" )  (Bool  "for" (Set (Var "w")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Var "Z1"))  "st" (Bool (Bool (Set (Var "v"))  ($#r1_hidden :::"="::: )  (Set (Var "w"))) & (Bool (Bool  "not" (Set (Var "p")) "," (Set (Var "w"))  ($#r3_xboole_0 :::"are_c=-comparable"::: )  ))) "holds"  (Bool (Set   ($#k1_trees_2 :::"succ"::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_trees_2 :::"succ"::: )  (Set (Var "w")))))))) ; 
 
theorem :: MODAL_1:15 (Bool  "for" (Set (Var "Z1")) "," (Set (Var "Z2")) "being"   ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z1")))) "holds"  (Bool  "for" (Set (Var "v")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Set (Var "Z1"))  ($#k5_trees_1 :::"with-replacement"::: )   "(" (Set (Var "p")) "," (Set (Var "Z2")) ")" )  (Bool  "for" (Set (Var "w")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Var "Z2"))  "st" (Bool (Bool (Set (Var "v"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "w"))))) "holds"  (Bool (Set   ($#k1_trees_2 :::"succ"::: )  (Set (Var "v"))) "," (Set   ($#k1_trees_2 :::"succ"::: )  (Set (Var "w")))  ($#r2_wellord2 :::"are_equipotent"::: )  ))))) ; 
 
theorem :: MODAL_1:16 (Bool  "for" (Set (Var "Z1")) "being"   ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z1")))) "holds"  (Bool  "for" (Set (Var "v")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Var "Z1"))  (Bool  "for" (Set (Var "w")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Set (Var "Z1"))  ($#k4_trees_1 :::"|"::: )  (Set (Var "p")))  "st" (Bool (Bool (Set (Var "v"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "w"))))) "holds"  (Bool (Set   ($#k1_trees_2 :::"succ"::: )  (Set (Var "v"))) "," (Set   ($#k1_trees_2 :::"succ"::: )  (Set (Var "w")))  ($#r2_wellord2 :::"are_equipotent"::: )  ))))) ; 
 
theorem :: MODAL_1:17 (Bool  "for" (Set (Var "Z")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"Tree":::)  "st" (Bool (Bool (Set   ($#k8_trees_2 :::"branchdeg"::: )  (Set  "("  ($#k1_modal_1 :::"Root"::: )  (Set (Var "Z")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "Z")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Var "Z"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))  ")" )) ; 
 
theorem :: MODAL_1:18 (Bool  "for" (Set (Var "Z")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"Tree":::)  "st" (Bool (Bool (Set   ($#k8_trees_2 :::"branchdeg"::: )  (Set  "("  ($#k1_modal_1 :::"Root"::: )  (Set (Var "Z")) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set   ($#k1_trees_2 :::"succ"::: )  (Set  "("  ($#k1_modal_1 :::"Root"::: )  (Set (Var "Z")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ($#k6_domain_1 :::"}"::: ) ))) ; 
 
theorem :: MODAL_1:19 (Bool  "for" (Set (Var "Z")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"Tree":::)  "st" (Bool (Bool (Set   ($#k8_trees_2 :::"branchdeg"::: )  (Set  "("  ($#k1_modal_1 :::"Root"::: )  (Set (Var "Z")) ")" ))  ($#r1_hidden :::"="::: )  (Num 2))) "holds"  (Bool (Set   ($#k1_trees_2 :::"succ"::: )  (Set  "("  ($#k1_modal_1 :::"Root"::: )  (Set (Var "Z")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k7_domain_1 :::"{"::: ) (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set  ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_domain_1 :::"}"::: ) ))) ; 
 





theorem :: MODAL_1:20 (Bool  "for" (Set (Var "Z")) "being"   ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "o")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Var "Z"))  "st" (Bool (Bool (Set (Var "o"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_modal_1 :::"Root"::: )  (Set (Var "Z"))))) "holds"  (Bool  "("  (Bool (Set (Set (Var "Z"))  ($#k4_trees_1 :::"|"::: )  (Set (Var "o"))) ","  "{"  (Set  "(" (Set (Var "o"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "s9")) ")" ) where s9 "is"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set  ($#k5_numbers :::"NAT"::: ) )  ($#k3_finseq_2 :::"*"::: )  ) : (Bool (Set (Set (Var "o"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "s9")))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))  "}"    ($#r2_wellord2 :::"are_equipotent"::: )  ) & (Bool (Bool  "not" (Set   ($#k1_modal_1 :::"Root"::: )  (Set (Var "Z")))  ($#r2_hidden :::"in"::: )   "{"  (Set  "(" (Set (Var "o"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "w9")) ")" ) where w9 "is"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set  ($#k5_numbers :::"NAT"::: ) )  ($#k3_finseq_2 :::"*"::: )  ) : (Bool (Set (Set (Var "o"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "w9")))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))  "}"  ))  ")" ))) ; 
 
theorem :: MODAL_1:21 (Bool  "for" (Set (Var "Z")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "o")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Var "Z"))  "st" (Bool (Bool (Set (Var "o"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_modal_1 :::"Root"::: )  (Set (Var "Z"))))) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "(" (Set (Var "Z"))  ($#k4_trees_1 :::"|"::: )  (Set (Var "o")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "Z")))))) ; 
 
theorem :: MODAL_1:22 (Bool  "for" (Set (Var "Z")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "z")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Var "Z"))  "st" (Bool (Bool (Set   ($#k1_trees_2 :::"succ"::: )  (Set  "("  ($#k1_modal_1 :::"Root"::: )  (Set (Var "Z")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "z")) ($#k6_domain_1 :::"}"::: ) ))) "holds"  (Bool (Set (Var "Z"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_trees_1 :::"elementary_tree"::: )  (Num 1) ")" )  ($#k5_trees_1 :::"with-replacement"::: )   "(" (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set  "(" (Set (Var "Z"))  ($#k4_trees_1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )))) ; 
 
theorem :: MODAL_1:23 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Z")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Var "D"))  (Bool  "for" (Set (Var "z")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "Z")))  "st" (Bool (Bool (Set   ($#k1_trees_2 :::"succ"::: )  (Set  "("  ($#k1_modal_1 :::"Root"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "Z")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "z")) ($#k6_domain_1 :::"}"::: ) ))) "holds"  (Bool (Set (Var "Z"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k2_trees_1 :::"elementary_tree"::: )  (Num 1) ")" )  ($#k8_funcop_1 :::"-->"::: )  (Set  "("  ($#k2_modal_1 :::"Root"::: )  (Set (Var "Z")) ")" ) ")" )  ($#k7_trees_2 :::"with-replacement"::: )   "(" (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set  "(" (Set (Var "Z"))  ($#k5_trees_2 :::"|"::: )  (Set (Var "z")) ")" ) ")" ))))) ; 
 
theorem :: MODAL_1:24 (Bool  "for" (Set (Var "Z")) "being"   ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Var "Z"))  "st" (Bool (Bool (Set (Var "x1"))  ($#r1_hidden :::"="::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "x2"))  ($#r1_hidden :::"="::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) )) & (Bool (Set   ($#k1_trees_2 :::"succ"::: )  (Set  "("  ($#k1_modal_1 :::"Root"::: )  (Set (Var "Z")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k7_domain_1 :::"}"::: ) ))) "holds"  (Bool (Set (Var "Z"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k2_trees_1 :::"elementary_tree"::: )  (Num 2) ")" )  ($#k5_trees_1 :::"with-replacement"::: )   "(" (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set  "(" (Set (Var "Z"))  ($#k4_trees_1 :::"|"::: )  (Set (Var "x1")) ")" ) ")"  ")" )  ($#k5_trees_1 :::"with-replacement"::: )   "(" (Set  ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set  "(" (Set (Var "Z"))  ($#k4_trees_1 :::"|"::: )  (Set (Var "x2")) ")" ) ")" )))) ; 
 
theorem :: MODAL_1:25 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Z")) "being"   ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Var "D"))  (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "Z")))  "st" (Bool (Bool (Set (Var "x1"))  ($#r1_hidden :::"="::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "x2"))  ($#r1_hidden :::"="::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) )) & (Bool (Set   ($#k1_trees_2 :::"succ"::: )  (Set  "("  ($#k1_modal_1 :::"Root"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "Z")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k7_domain_1 :::"}"::: ) ))) "holds"  (Bool (Set (Var "Z"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k2_trees_1 :::"elementary_tree"::: )  (Num 2) ")" )  ($#k8_funcop_1 :::"-->"::: )  (Set  "("  ($#k2_modal_1 :::"Root"::: )  (Set (Var "Z")) ")" ) ")" )  ($#k7_trees_2 :::"with-replacement"::: )   "(" (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set  "(" (Set (Var "Z"))  ($#k5_trees_2 :::"|"::: )  (Set (Var "x1")) ")" ) ")"  ")" )  ($#k7_trees_2 :::"with-replacement"::: )   "(" (Set  ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set  "(" (Set (Var "Z"))  ($#k5_trees_2 :::"|"::: )  (Set (Var "x2")) ")" ) ")" ))))) ; 
 definitionfunc  :::"MP-variables":::  ->    ($#m1_hidden :::"set"::: )   equals :: MODAL_1:def 3 (Set  ($#k8_mcart_1 :::"[:"::: ) (Set  ($#k6_domain_1 :::"{"::: ) (Num 3) ($#k6_domain_1 :::"}"::: ) ) "," (Set  ($#k5_numbers :::"NAT"::: ) ) ($#k8_mcart_1 :::":]"::: ) ); end; 




:: deftheorem    defines :::"MP-variables"::: MODAL_1:def 3 :  (Bool (Set   ($#k3_modal_1 :::"MP-variables"::: )  )  ($#r1_hidden :::"="::: )  (Set  ($#k8_mcart_1 :::"[:"::: ) (Set  ($#k6_domain_1 :::"{"::: ) (Num 3) ($#k6_domain_1 :::"}"::: ) ) "," (Set  ($#k5_numbers :::"NAT"::: ) ) ($#k8_mcart_1 :::":]"::: ) )); 
 registration
cluster (Set   ($#k3_modal_1 :::"MP-variables"::: )  ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; definitionmode MP-variable is    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k3_modal_1 :::"MP-variables"::: )  ); end; definitionfunc  :::"MP-conectives":::  ->    ($#m1_hidden :::"set"::: )   equals :: MODAL_1:def 4 (Set  ($#k8_mcart_1 :::"[:"::: ) (Set  ($#k8_domain_1 :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) ($#k8_domain_1 :::"}"::: ) ) "," (Set  ($#k5_numbers :::"NAT"::: ) ) ($#k8_mcart_1 :::":]"::: ) ); end; 




:: deftheorem    defines :::"MP-conectives"::: MODAL_1:def 4 :  (Bool (Set   ($#k4_modal_1 :::"MP-conectives"::: )  )  ($#r1_hidden :::"="::: )  (Set  ($#k8_mcart_1 :::"[:"::: ) (Set  ($#k8_domain_1 :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) ($#k8_domain_1 :::"}"::: ) ) "," (Set  ($#k5_numbers :::"NAT"::: ) ) ($#k8_mcart_1 :::":]"::: ) )); 
 registration
cluster (Set   ($#k4_modal_1 :::"MP-conectives"::: )  ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; definitionmode MP-conective is    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_modal_1 :::"MP-conectives"::: )  ); end; 
theorem :: MODAL_1:26 (Bool (Set   ($#k4_modal_1 :::"MP-conectives"::: )  )  ($#r1_subset_1 :::"misses"::: )  (Set   ($#k3_modal_1 :::"MP-variables"::: )  )) ; 
 



definitionlet "T" be   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"Tree":::); let "v" be    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Const "T")); :: original: :::"branchdeg"::: redefine func  :::"branchdeg"::: "v" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); end; definitionfunc  :::"MP-WFF":::  ->    ($#m1_trees_3 :::"DTree-set"::: )   "of" (Set  ($#k8_mcart_1 :::"[:"::: ) (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k5_numbers :::"NAT"::: ) ) ($#k8_mcart_1 :::":]"::: ) ) means :: MODAL_1:def 5 (Bool  "("  (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_hidden :::"DecoratedTree":::) "of" (Set  ($#k8_mcart_1 :::"[:"::: ) (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k5_numbers :::"NAT"::: ) ) ($#k8_mcart_1 :::":]"::: ) )  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it)) "holds"  (Bool (Set (Var "x")) "is"   ($#v1_finset_1 :::"finite"::: )  )  ")" ) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"DecoratedTree":::) "of" (Set  ($#k8_mcart_1 :::"[:"::: ) (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k5_numbers :::"NAT"::: ) ) ($#k8_mcart_1 :::":]"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "for" (Set (Var "v")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "x"))) "holds"   (Bool  "("  (Bool (Set   ($#k5_modal_1 :::"branchdeg"::: )  (Set (Var "v")))  ($#r1_xxreal_0 :::"<="::: )  (Num 2)) & (Bool  "("   "not" (Bool (Set   ($#k5_modal_1 :::"branchdeg"::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Set (Var "x"))  ($#k3_trees_2 :::"."::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) )) "or" (Bool  "ex" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st" (Bool (Set (Set (Var "x"))  ($#k3_trees_2 :::"."::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Num 3) "," (Set (Var "k")) ($#k1_domain_1 :::"]"::: ) )))  ")" ) & (Bool  "("   "not" (Bool (Set   ($#k5_modal_1 :::"branchdeg"::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Num 1)) "or" (Bool (Set (Set (Var "x"))  ($#k3_trees_2 :::"."::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Num 1) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) )) "or" (Bool (Set (Set (Var "x"))  ($#k3_trees_2 :::"."::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Num 1) "," (Num 1) ($#k1_domain_1 :::"]"::: ) ))  ")" ) &  "("  (Bool (Bool (Set   ($#k5_modal_1 :::"branchdeg"::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Num 2))) "implies" (Bool (Set (Set (Var "x"))  ($#k3_trees_2 :::"."::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Num 2) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ))  ")"   ")" ))  ")" )  ")" )  ")" ); end; 




:: deftheorem    defines :::"MP-WFF"::: MODAL_1:def 5 :  (Bool  "for" (Set (Var "b1")) "being"    ($#m1_trees_3 :::"DTree-set"::: )   "of" (Set  ($#k8_mcart_1 :::"[:"::: ) (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k5_numbers :::"NAT"::: ) ) ($#k8_mcart_1 :::":]"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_modal_1 :::"MP-WFF"::: )  )) "iff" (Bool  "("  (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_hidden :::"DecoratedTree":::) "of" (Set  ($#k8_mcart_1 :::"[:"::: ) (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k5_numbers :::"NAT"::: ) ) ($#k8_mcart_1 :::":]"::: ) )  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b1")))) "holds"  (Bool (Set (Var "x")) "is"   ($#v1_finset_1 :::"finite"::: )  )  ")" ) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"DecoratedTree":::) "of" (Set  ($#k8_mcart_1 :::"[:"::: ) (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k5_numbers :::"NAT"::: ) ) ($#k8_mcart_1 :::":]"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b1"))) "iff" (Bool  "for" (Set (Var "v")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "x"))) "holds"   (Bool  "("  (Bool (Set   ($#k5_modal_1 :::"branchdeg"::: )  (Set (Var "v")))  ($#r1_xxreal_0 :::"<="::: )  (Num 2)) & (Bool  "("   "not" (Bool (Set   ($#k5_modal_1 :::"branchdeg"::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Set (Var "x"))  ($#k3_trees_2 :::"."::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) )) "or" (Bool  "ex" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st" (Bool (Set (Set (Var "x"))  ($#k3_trees_2 :::"."::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Num 3) "," (Set (Var "k")) ($#k1_domain_1 :::"]"::: ) )))  ")" ) & (Bool  "("   "not" (Bool (Set   ($#k5_modal_1 :::"branchdeg"::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Num 1)) "or" (Bool (Set (Set (Var "x"))  ($#k3_trees_2 :::"."::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Num 1) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) )) "or" (Bool (Set (Set (Var "x"))  ($#k3_trees_2 :::"."::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Num 1) "," (Num 1) ($#k1_domain_1 :::"]"::: ) ))  ")" ) &  "("  (Bool (Bool (Set   ($#k5_modal_1 :::"branchdeg"::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Num 2))) "implies" (Bool (Set (Set (Var "x"))  ($#k3_trees_2 :::"."::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Num 2) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ))  ")"   ")" ))  ")" )  ")" )  ")" )  ")" )); 
 definitionmode MP-wff is    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_modal_1 :::"MP-WFF"::: )  ); end; registration
cluster   ->   ($#v1_finset_1 :::"finite"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_modal_1 :::"MP-WFF"::: )  ); 
end; 







definitionlet "A" be   ($#m1_subset_1 :::"MP-wff":::); let "a" be    ($#m1_trees_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Const "A"))); :: original: :::"|"::: redefine func "A" :::"|"::: "a" ->   ($#m1_subset_1 :::"MP-wff":::); end; definitionlet "a" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_modal_1 :::"MP-conectives"::: )  ); func  :::"the_arity_of"::: "a" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) equals :: MODAL_1:def 6 (Set "a"  ($#k1_xtuple_0 :::"`1"::: )  ); end; 





:: deftheorem    defines :::"the_arity_of"::: MODAL_1:def 6 :  (Bool  "for" (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_modal_1 :::"MP-conectives"::: )  ) "holds"  (Bool (Set   ($#k8_modal_1 :::"the_arity_of"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_xtuple_0 :::"`1"::: )  ))); 
 definitionlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "T", "T1" be   ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Const "D")); let "p" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); assume 
(Bool (Set (Const "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Const "T"))))
 ; func  :::"@":::  "(" "T" "," "p" "," "T1" ")"  ->   ($#m1_hidden :::"DecoratedTree":::) "of" "D" equals :: MODAL_1:def 7 (Set "T"  ($#k7_trees_2 :::"with-replacement"::: )   "(" "p" "," "T1" ")" ); end; 









:: deftheorem    defines :::"@"::: MODAL_1:def 7 :  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "," (Set (Var "T1")) "being"   ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Var "D"))  (Bool  "for" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "T"))))) "holds"  (Bool (Set   ($#k9_modal_1 :::"@"::: )   "(" (Set (Var "T")) "," (Set (Var "p")) "," (Set (Var "T1")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "T"))  ($#k7_trees_2 :::"with-replacement"::: )   "(" (Set (Var "p")) "," (Set (Var "T1")) ")" ))))); 
 
theorem :: MODAL_1:27 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"MP-wff":::) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k2_trees_1 :::"elementary_tree"::: )  (Num 1) ")" )  ($#k8_funcop_1 :::"-->"::: )  (Set  ($#k1_domain_1 :::"["::: ) (Num 1) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ")" )  ($#k7_trees_2 :::"with-replacement"::: )   "(" (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set (Var "A")) ")" ) "is"   ($#m1_subset_1 :::"MP-wff":::))) ; 
 
theorem :: MODAL_1:28 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"MP-wff":::) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k2_trees_1 :::"elementary_tree"::: )  (Num 1) ")" )  ($#k8_funcop_1 :::"-->"::: )  (Set  ($#k1_domain_1 :::"["::: ) (Num 1) "," (Num 1) ($#k1_domain_1 :::"]"::: ) ) ")" )  ($#k7_trees_2 :::"with-replacement"::: )   "(" (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set (Var "A")) ")" ) "is"   ($#m1_subset_1 :::"MP-wff":::))) ; 
 
theorem :: MODAL_1:29 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"MP-wff":::) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "("  ($#k2_trees_1 :::"elementary_tree"::: )  (Num 2) ")" )  ($#k8_funcop_1 :::"-->"::: )  (Set  ($#k1_domain_1 :::"["::: ) (Num 2) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ")" )  ($#k7_trees_2 :::"with-replacement"::: )   "(" (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set (Var "A")) ")"  ")" )  ($#k7_trees_2 :::"with-replacement"::: )   "(" (Set  ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set (Var "B")) ")" ) "is"   ($#m1_subset_1 :::"MP-wff":::))) ; 
 definitionlet "A" be   ($#m1_subset_1 :::"MP-wff":::); func  :::"'not'"::: "A" ->   ($#m1_subset_1 :::"MP-wff":::) equals :: MODAL_1:def 8 (Set (Set  "(" (Set  "("  ($#k2_trees_1 :::"elementary_tree"::: )  (Num 1) ")" )  ($#k8_funcop_1 :::"-->"::: )  (Set  ($#k1_domain_1 :::"["::: ) (Num 1) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ")" )  ($#k7_trees_2 :::"with-replacement"::: )   "(" (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) "," "A" ")" ); func  :::"(#)"::: "A" ->   ($#m1_subset_1 :::"MP-wff":::) equals :: MODAL_1:def 9 (Set (Set  "(" (Set  "("  ($#k2_trees_1 :::"elementary_tree"::: )  (Num 1) ")" )  ($#k8_funcop_1 :::"-->"::: )  (Set  ($#k1_domain_1 :::"["::: ) (Num 1) "," (Num 1) ($#k1_domain_1 :::"]"::: ) ) ")" )  ($#k7_trees_2 :::"with-replacement"::: )   "(" (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) "," "A" ")" ); let "B" be   ($#m1_subset_1 :::"MP-wff":::); func "A" :::"'&'"::: "B" ->   ($#m1_subset_1 :::"MP-wff":::) equals :: MODAL_1:def 10 (Set (Set  "(" (Set  "(" (Set  "("  ($#k2_trees_1 :::"elementary_tree"::: )  (Num 2) ")" )  ($#k8_funcop_1 :::"-->"::: )  (Set  ($#k1_domain_1 :::"["::: ) (Num 2) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ")" )  ($#k7_trees_2 :::"with-replacement"::: )   "(" (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) "," "A" ")"  ")" )  ($#k7_trees_2 :::"with-replacement"::: )   "(" (Set  ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) "," "B" ")" ); end; 
















:: deftheorem    defines :::"'not'"::: MODAL_1:def 8 :  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"MP-wff":::) "holds"  (Bool (Set   ($#k10_modal_1 :::"'not'"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k2_trees_1 :::"elementary_tree"::: )  (Num 1) ")" )  ($#k8_funcop_1 :::"-->"::: )  (Set  ($#k1_domain_1 :::"["::: ) (Num 1) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ")" )  ($#k7_trees_2 :::"with-replacement"::: )   "(" (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set (Var "A")) ")" ))); 
 
:: deftheorem    defines :::"(#)"::: MODAL_1:def 9 :  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"MP-wff":::) "holds"  (Bool (Set   ($#k11_modal_1 :::"(#)"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k2_trees_1 :::"elementary_tree"::: )  (Num 1) ")" )  ($#k8_funcop_1 :::"-->"::: )  (Set  ($#k1_domain_1 :::"["::: ) (Num 1) "," (Num 1) ($#k1_domain_1 :::"]"::: ) ) ")" )  ($#k7_trees_2 :::"with-replacement"::: )   "(" (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set (Var "A")) ")" ))); 
 
:: deftheorem    defines :::"'&'"::: MODAL_1:def 10 :  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"MP-wff":::) "holds"  (Bool (Set (Set (Var "A"))  ($#k12_modal_1 :::"'&'"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k2_trees_1 :::"elementary_tree"::: )  (Num 2) ")" )  ($#k8_funcop_1 :::"-->"::: )  (Set  ($#k1_domain_1 :::"["::: ) (Num 2) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ")" )  ($#k7_trees_2 :::"with-replacement"::: )   "(" (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set (Var "A")) ")"  ")" )  ($#k7_trees_2 :::"with-replacement"::: )   "(" (Set  ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set (Var "B")) ")" ))); 
 definitionlet "A" be   ($#m1_subset_1 :::"MP-wff":::); func  :::"?"::: "A" ->   ($#m1_subset_1 :::"MP-wff":::) equals :: MODAL_1:def 11 (Set   ($#k10_modal_1 :::"'not'"::: )  (Set  "("  ($#k11_modal_1 :::"(#)"::: )  (Set  "("  ($#k10_modal_1 :::"'not'"::: )  "A" ")" ) ")" )); let "B" be   ($#m1_subset_1 :::"MP-wff":::); func "A" :::"'or'"::: "B" ->   ($#m1_subset_1 :::"MP-wff":::) equals :: MODAL_1:def 12 (Set   ($#k10_modal_1 :::"'not'"::: )  (Set  "(" (Set  "("  ($#k10_modal_1 :::"'not'"::: )  "A" ")" )  ($#k12_modal_1 :::"'&'"::: )  (Set  "("  ($#k10_modal_1 :::"'not'"::: )  "B" ")" ) ")" )); func "A" :::"=>"::: "B" ->   ($#m1_subset_1 :::"MP-wff":::) equals :: MODAL_1:def 13 (Set   ($#k10_modal_1 :::"'not'"::: )  (Set  "(" "A"  ($#k12_modal_1 :::"'&'"::: )  (Set  "("  ($#k10_modal_1 :::"'not'"::: )  "B" ")" ) ")" )); end; 

















:: deftheorem    defines :::"?"::: MODAL_1:def 11 :  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"MP-wff":::) "holds"  (Bool (Set   ($#k13_modal_1 :::"?"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k10_modal_1 :::"'not'"::: )  (Set  "("  ($#k11_modal_1 :::"(#)"::: )  (Set  "("  ($#k10_modal_1 :::"'not'"::: )  (Set (Var "A")) ")" ) ")" )))); 
 
:: deftheorem    defines :::"'or'"::: MODAL_1:def 12 :  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"MP-wff":::) "holds"  (Bool (Set (Set (Var "A"))  ($#k14_modal_1 :::"'or'"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set   ($#k10_modal_1 :::"'not'"::: )  (Set  "(" (Set  "("  ($#k10_modal_1 :::"'not'"::: )  (Set (Var "A")) ")" )  ($#k12_modal_1 :::"'&'"::: )  (Set  "("  ($#k10_modal_1 :::"'not'"::: )  (Set (Var "B")) ")" ) ")" )))); 
 
:: deftheorem    defines :::"=>"::: MODAL_1:def 13 :  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"MP-wff":::) "holds"  (Bool (Set (Set (Var "A"))  ($#k15_modal_1 :::"=>"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set   ($#k10_modal_1 :::"'not'"::: )  (Set  "(" (Set (Var "A"))  ($#k12_modal_1 :::"'&'"::: )  (Set  "("  ($#k10_modal_1 :::"'not'"::: )  (Set (Var "B")) ")" ) ")" )))); 
 
theorem :: MODAL_1:30 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k2_trees_1 :::"elementary_tree"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k8_funcop_1 :::"-->"::: )  (Set  ($#k1_domain_1 :::"["::: ) (Num 3) "," (Set (Var "n")) ($#k1_domain_1 :::"]"::: ) )) "is"   ($#m1_subset_1 :::"MP-wff":::))) ; 
 
theorem :: MODAL_1:31 (Bool (Set (Set  "("  ($#k2_trees_1 :::"elementary_tree"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k8_funcop_1 :::"-->"::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) )) "is"   ($#m1_subset_1 :::"MP-wff":::)) ; 
 definitionlet "p" be   ($#m1_subset_1 :::"MP-variable":::); func  :::"@"::: "p" ->   ($#m1_subset_1 :::"MP-wff":::) equals :: MODAL_1:def 14 (Set (Set  "("  ($#k2_trees_1 :::"elementary_tree"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k8_funcop_1 :::"-->"::: )  "p"); end; 





:: deftheorem    defines :::"@"::: MODAL_1:def 14 :  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"MP-variable":::) "holds"  (Bool (Set   ($#k16_modal_1 :::"@"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_trees_1 :::"elementary_tree"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k8_funcop_1 :::"-->"::: )  (Set (Var "p"))))); 
 
theorem :: MODAL_1:32 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"MP-variable":::)  "st" (Bool (Bool (Set   ($#k16_modal_1 :::"@"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k16_modal_1 :::"@"::: )  (Set (Var "q"))))) "holds"  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "q")))) ; 
 
theorem :: MODAL_1:33 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"MP-wff":::)  "st" (Bool (Bool (Set   ($#k10_modal_1 :::"'not'"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k10_modal_1 :::"'not'"::: )  (Set (Var "B"))))) "holds"  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Var "B")))) ; 
 
theorem :: MODAL_1:34 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"MP-wff":::)  "st" (Bool (Bool (Set   ($#k11_modal_1 :::"(#)"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k11_modal_1 :::"(#)"::: )  (Set (Var "B"))))) "holds"  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Var "B")))) ; 
 
theorem :: MODAL_1:35 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "A1")) "," (Set (Var "B1")) "being"   ($#m1_subset_1 :::"MP-wff":::)  "st" (Bool (Bool (Set (Set (Var "A"))  ($#k12_modal_1 :::"'&'"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A1"))  ($#k12_modal_1 :::"'&'"::: )  (Set (Var "B1"))))) "holds"  (Bool  "("  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Var "A1"))) & (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set (Var "B1")))  ")" )) ; 
 definitionfunc  :::"VERUM":::  ->   ($#m1_subset_1 :::"MP-wff":::) equals :: MODAL_1:def 15 (Set (Set  "("  ($#k2_trees_1 :::"elementary_tree"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k8_funcop_1 :::"-->"::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) )); end; 




:: deftheorem    defines :::"VERUM"::: MODAL_1:def 15 :  (Bool (Set   ($#k17_modal_1 :::"VERUM"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_trees_1 :::"elementary_tree"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k8_funcop_1 :::"-->"::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ))); 
 
theorem :: MODAL_1:36 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"MP-wff":::)  "holds"  (Bool  "("   "not" (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Num 1)) "or" (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k17_modal_1 :::"VERUM"::: )  )) "or" (Bool  "ex" (Set (Var "p")) "being"   ($#m1_subset_1 :::"MP-variable":::) "st" (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k16_modal_1 :::"@"::: )  (Set (Var "p")))))  ")" )) ; 
 
theorem :: MODAL_1:37 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"MP-wff":::)  "holds"  (Bool  "("   "not" (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "A")) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Num 2)) "or" (Bool  "ex" (Set (Var "B")) "being"   ($#m1_subset_1 :::"MP-wff":::) "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_modal_1 :::"'not'"::: )  (Set (Var "B")))) "or" (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_modal_1 :::"(#)"::: )  (Set (Var "B"))))  ")" )) "or" (Bool  "ex" (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_subset_1 :::"MP-wff":::) "st" (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "B"))  ($#k12_modal_1 :::"'&'"::: )  (Set (Var "C")))))  ")" )) ; 
 
theorem :: MODAL_1:38 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"MP-wff":::)  "holds" (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "A")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k10_modal_1 :::"'not'"::: )  (Set (Var "A")) ")" ) ")" )))) ; 
 
theorem :: MODAL_1:39 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"MP-wff":::)  "holds" (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "A")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k11_modal_1 :::"(#)"::: )  (Set (Var "A")) ")" ) ")" )))) ; 
 
theorem :: MODAL_1:40 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"MP-wff":::) "holds"   (Bool  "("  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "A")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set (Var "A"))  ($#k12_modal_1 :::"'&'"::: )  (Set (Var "B")) ")" ) ")" ))) & (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "B")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set (Var "A"))  ($#k12_modal_1 :::"'&'"::: )  (Set (Var "B")) ")" ) ")" )))  ")" )) ; 
 definitionlet "IT" be   ($#m1_subset_1 :::"MP-wff":::); attr "IT" is  :::"atomic":::  means :: MODAL_1:def 16 (Bool  "ex" (Set (Var "p")) "being"   ($#m1_subset_1 :::"MP-variable":::) "st" (Bool "IT"  ($#r1_hidden :::"="::: )  (Set   ($#k16_modal_1 :::"@"::: )  (Set (Var "p"))))); attr "IT" is  :::"negative":::  means :: MODAL_1:def 17 (Bool  "ex" (Set (Var "A")) "being"   ($#m1_subset_1 :::"MP-wff":::) "st" (Bool "IT"  ($#r1_hidden :::"="::: )  (Set   ($#k10_modal_1 :::"'not'"::: )  (Set (Var "A"))))); attr "IT" is  :::"necessitive":::  means :: MODAL_1:def 18 (Bool  "ex" (Set (Var "A")) "being"   ($#m1_subset_1 :::"MP-wff":::) "st" (Bool "IT"  ($#r1_hidden :::"="::: )  (Set   ($#k11_modal_1 :::"(#)"::: )  (Set (Var "A"))))); attr "IT" is  :::"conjunctive":::  means :: MODAL_1:def 19 (Bool  "ex" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"MP-wff":::) "st" (Bool "IT"  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k12_modal_1 :::"'&'"::: )  (Set (Var "B"))))); end; 
















:: deftheorem    defines :::"atomic"::: MODAL_1:def 16 :  (Bool  "for" (Set (Var "IT")) "being"   ($#m1_subset_1 :::"MP-wff":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_modal_1 :::"atomic"::: )  ) "iff" (Bool  "ex" (Set (Var "p")) "being"   ($#m1_subset_1 :::"MP-variable":::) "st" (Bool (Set (Var "IT"))  ($#r1_hidden :::"="::: )  (Set   ($#k16_modal_1 :::"@"::: )  (Set (Var "p")))))  ")" )); 
 
:: deftheorem    defines :::"negative"::: MODAL_1:def 17 :  (Bool  "for" (Set (Var "IT")) "being"   ($#m1_subset_1 :::"MP-wff":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v2_modal_1 :::"negative"::: )  ) "iff" (Bool  "ex" (Set (Var "A")) "being"   ($#m1_subset_1 :::"MP-wff":::) "st" (Bool (Set (Var "IT"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_modal_1 :::"'not'"::: )  (Set (Var "A")))))  ")" )); 
 
:: deftheorem    defines :::"necessitive"::: MODAL_1:def 18 :  (Bool  "for" (Set (Var "IT")) "being"   ($#m1_subset_1 :::"MP-wff":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v3_modal_1 :::"necessitive"::: )  ) "iff" (Bool  "ex" (Set (Var "A")) "being"   ($#m1_subset_1 :::"MP-wff":::) "st" (Bool (Set (Var "IT"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_modal_1 :::"(#)"::: )  (Set (Var "A")))))  ")" )); 
 
:: deftheorem    defines :::"conjunctive"::: MODAL_1:def 19 :  (Bool  "for" (Set (Var "IT")) "being"   ($#m1_subset_1 :::"MP-wff":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v4_modal_1 :::"conjunctive"::: )  ) "iff" (Bool  "ex" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"MP-wff":::) "st" (Bool (Set (Var "IT"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k12_modal_1 :::"'&'"::: )  (Set (Var "B")))))  ")" )); 
 registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set  ($#k8_mcart_1 :::"[:"::: ) (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k5_numbers :::"NAT"::: ) ) ($#k8_mcart_1 :::":]"::: ) )  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_finset_1 :::"finite"::: )     ($#v3_trees_2 :::"DecoratedTree-like"::: )     ($#v1_modal_1 :::"atomic"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_modal_1 :::"MP-WFF"::: )  ); 

cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set  ($#k8_mcart_1 :::"[:"::: ) (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k5_numbers :::"NAT"::: ) ) ($#k8_mcart_1 :::":]"::: ) )  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_finset_1 :::"finite"::: )     ($#v3_trees_2 :::"DecoratedTree-like"::: )     ($#v2_modal_1 :::"negative"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_modal_1 :::"MP-WFF"::: )  ); 

cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set  ($#k8_mcart_1 :::"[:"::: ) (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k5_numbers :::"NAT"::: ) ) ($#k8_mcart_1 :::":]"::: ) )  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_finset_1 :::"finite"::: )     ($#v3_trees_2 :::"DecoratedTree-like"::: )     ($#v3_modal_1 :::"necessitive"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_modal_1 :::"MP-WFF"::: )  ); 

cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set  ($#k8_mcart_1 :::"[:"::: ) (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k5_numbers :::"NAT"::: ) ) ($#k8_mcart_1 :::":]"::: ) )  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_finset_1 :::"finite"::: )     ($#v3_trees_2 :::"DecoratedTree-like"::: )     ($#v4_modal_1 :::"conjunctive"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_modal_1 :::"MP-WFF"::: )  ); 
end; scheme  :: MODAL_1:sch 1 MPInd{ P1[   ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_modal_1 :::"MP-WFF"::: )  )] } : 
(Bool  "for" (Set (Var "A")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_modal_1 :::"MP-WFF"::: )  ) "holds"  (Bool P1[(Set (Var "A"))]))
 provided
(Bool P1[(Set   ($#k17_modal_1 :::"VERUM"::: )  )])
 and  
(Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"MP-variable":::) "holds"  (Bool P1[(Set   ($#k16_modal_1 :::"@"::: )  (Set (Var "p")))]))
 and  
(Bool  "for" (Set (Var "A")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_modal_1 :::"MP-WFF"::: )  )  "st" (Bool (Bool P1[(Set (Var "A"))])) "holds"  (Bool P1[(Set   ($#k10_modal_1 :::"'not'"::: )  (Set (Var "A")))]))
 and  
(Bool  "for" (Set (Var "A")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_modal_1 :::"MP-WFF"::: )  )  "st" (Bool (Bool P1[(Set (Var "A"))])) "holds"  (Bool P1[(Set   ($#k11_modal_1 :::"(#)"::: )  (Set (Var "A")))]))
 and  
(Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_modal_1 :::"MP-WFF"::: )  )  "st" (Bool (Bool P1[(Set (Var "A"))]) & (Bool P1[(Set (Var "B"))])) "holds"  (Bool P1[(Set (Set (Var "A"))  ($#k12_modal_1 :::"'&'"::: )  (Set (Var "B")))]))
 proof 


end; 
theorem :: MODAL_1:41 (Bool  "for" (Set (Var "A")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_modal_1 :::"MP-WFF"::: )  )  "holds"  (Bool  "("  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k17_modal_1 :::"VERUM"::: )  )) "or" (Bool (Set (Var "A")) "is"   ($#v1_modal_1 :::"atomic"::: )    ($#m1_subset_1 :::"MP-wff":::)) "or" (Bool (Set (Var "A")) "is"   ($#v2_modal_1 :::"negative"::: )    ($#m1_subset_1 :::"MP-wff":::)) "or" (Bool (Set (Var "A")) "is"   ($#v3_modal_1 :::"necessitive"::: )    ($#m1_subset_1 :::"MP-wff":::)) "or" (Bool (Set (Var "A")) "is"   ($#v4_modal_1 :::"conjunctive"::: )    ($#m1_subset_1 :::"MP-wff":::))  ")" )) ; 
 
theorem :: MODAL_1:42 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"MP-wff":::)  "holds"  (Bool  "("  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k17_modal_1 :::"VERUM"::: )  )) "or" (Bool  "ex" (Set (Var "p")) "being"   ($#m1_subset_1 :::"MP-variable":::) "st" (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k16_modal_1 :::"@"::: )  (Set (Var "p"))))) "or" (Bool  "ex" (Set (Var "B")) "being"   ($#m1_subset_1 :::"MP-wff":::) "st" (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_modal_1 :::"'not'"::: )  (Set (Var "B"))))) "or" (Bool  "ex" (Set (Var "B")) "being"   ($#m1_subset_1 :::"MP-wff":::) "st" (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_modal_1 :::"(#)"::: )  (Set (Var "B"))))) "or" (Bool  "ex" (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_subset_1 :::"MP-wff":::) "st" (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "B"))  ($#k12_modal_1 :::"'&'"::: )  (Set (Var "C")))))  ")" )) ; 
 
theorem :: MODAL_1:43 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"MP-variable":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"MP-wff":::) "holds"   (Bool  "("  (Bool (Set   ($#k16_modal_1 :::"@"::: )  (Set (Var "p")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k10_modal_1 :::"'not'"::: )  (Set (Var "A")))) & (Bool (Set   ($#k16_modal_1 :::"@"::: )  (Set (Var "p")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k11_modal_1 :::"(#)"::: )  (Set (Var "A")))) & (Bool (Set   ($#k16_modal_1 :::"@"::: )  (Set (Var "p")))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "A"))  ($#k12_modal_1 :::"'&'"::: )  (Set (Var "B"))))  ")" ))) ; 
 
theorem :: MODAL_1:44 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_subset_1 :::"MP-wff":::) "holds"   (Bool  "("  (Bool (Set   ($#k10_modal_1 :::"'not'"::: )  (Set (Var "A")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k11_modal_1 :::"(#)"::: )  (Set (Var "B")))) & (Bool (Set   ($#k10_modal_1 :::"'not'"::: )  (Set (Var "A")))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "B"))  ($#k12_modal_1 :::"'&'"::: )  (Set (Var "C"))))  ")" )) ; 
 
theorem :: MODAL_1:45 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_subset_1 :::"MP-wff":::)  "holds" (Bool (Set   ($#k11_modal_1 :::"(#)"::: )  (Set (Var "A")))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "B"))  ($#k12_modal_1 :::"'&'"::: )  (Set (Var "C"))))) ; 
 
theorem :: MODAL_1:46 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"MP-variable":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"MP-wff":::) "holds"   (Bool  "("  (Bool (Set   ($#k17_modal_1 :::"VERUM"::: )  )  ($#r1_hidden :::"<>"::: )  (Set   ($#k16_modal_1 :::"@"::: )  (Set (Var "p")))) & (Bool (Set   ($#k17_modal_1 :::"VERUM"::: )  )  ($#r1_hidden :::"<>"::: )  (Set   ($#k10_modal_1 :::"'not'"::: )  (Set (Var "A")))) & (Bool (Set   ($#k17_modal_1 :::"VERUM"::: )  )  ($#r1_hidden :::"<>"::: )  (Set   ($#k11_modal_1 :::"(#)"::: )  (Set (Var "A")))) & (Bool (Set   ($#k17_modal_1 :::"VERUM"::: )  )  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "A"))  ($#k12_modal_1 :::"'&'"::: )  (Set (Var "B"))))  ")" ))) ; 
 scheme  :: MODAL_1:sch 2 MPFuncEx{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ), F3(   ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k3_modal_1 :::"MP-variables"::: )  )) ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ), F4(   ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )) ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ), F5(   ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )) ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ), F6(   ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) ","    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )) ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) } : 
(Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k6_modal_1 :::"MP-WFF"::: ) ) "," (Set F1 "("  ")" ) "st"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  ($#k17_modal_1 :::"VERUM"::: ) ))  ($#r1_hidden :::"="::: )  (Set F2 "("  ")" )) & (Bool  "("   "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"MP-variable":::) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k16_modal_1 :::"@"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "p")) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "A")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_modal_1 :::"MP-WFF"::: )  ) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k10_modal_1 :::"'not'"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "A")) ")" ) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "A")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_modal_1 :::"MP-WFF"::: )  ) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k11_modal_1 :::"(#)"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set F5 "(" (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "A")) ")" ) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_modal_1 :::"MP-WFF"::: )  ) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "A"))  ($#k12_modal_1 :::"'&'"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set F6 "(" (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "A")) ")" ) "," (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "B")) ")" ) ")" ))  ")" )  ")" ))
 proof 


end;