:: WELLFND1  semantic presentation begin  
theorem :: WELLFND1:1 (Bool  "for" (Set (Var "X")) "being"   ($#v4_funct_1 :::"functional"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "g"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "f"))  ($#r1_partfun1 :::"tolerates"::: )  (Set (Var "g")))  ")" )) "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set (Var "X"))) "is"   ($#m1_hidden :::"Function":::))) ; 
 scheme  :: WELLFND1:sch 1 PFSeparation{ F1() ->    ($#m1_hidden :::"set"::: )  , F2() ->    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "PFS")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_rfunct_3 :::"PFuncs"::: )   "(" (Set F1 "("  ")" ) "," (Set F2 "("  ")" ) ")"  ")" ) "st"  (Bool  "for" (Set (Var "pfs")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set F1 "("  ")" ) "," (Set F2 "("  ")" ) "holds"   (Bool  "("  (Bool (Set (Var "pfs"))  ($#r2_hidden :::"in"::: )  (Set (Var "PFS"))) "iff" (Bool P1[(Set (Var "pfs"))])  ")" )))
 proof 


end; registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k2_card_1 :::"nextcard"::: )  "X") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_ordinal1 :::"epsilon-transitive"::: )     ($#v2_ordinal1 :::"epsilon-connected"::: )     ($#v3_ordinal1 :::"ordinal"::: )    ($#~v1_finset_1  "non"   ($#v1_finset_1 :::"finite"::: )   )    ($#v1_card_1 :::"cardinal"::: )     ($#v1_card_5 :::"regular"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: WELLFND1:2 (Bool  "for" (Set (Var "M")) "being"   ($#v1_card_5 :::"regular"::: )    ($#m1_hidden :::"Aleph":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "M"))) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) "holds"  (Bool (Set   ($#k3_ordinal2 :::"sup"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))))) ; 
 
theorem :: WELLFND1:3 (Bool  "for" (Set (Var "R")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "R")))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "x")))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))))) ; 
 definitionlet "R" be    ($#l1_orders_2 :::"RelStr"::: )  ; let "X" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "R")); redefine attr "X" is  :::"lower":::  means :: WELLFND1:def 1 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "X") & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "R"))) "holds"  (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  "X")); end; 





:: deftheorem    defines :::"lower"::: WELLFND1:def 1 :  (Bool  "for" (Set (Var "R")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v12_waybel_0 :::"lower"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "R"))))) "holds"  (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))))  ")" ))); 
 
theorem :: WELLFND1:4 (Bool  "for" (Set (Var "R")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X")) "is"   ($#v12_waybel_0 :::"lower"::: )  ) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "R")))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "x")))  ($#r1_tarski :::"c="::: )  (Set (Var "X")))))) ; 
 
theorem :: WELLFND1:5 (Bool  "for" (Set (Var "R")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#v12_waybel_0 :::"lower"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "Y"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) & (Bool (Set (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "R")))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "x")))  ($#r1_tarski :::"c="::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "Y")) "is"   ($#v12_waybel_0 :::"lower"::: )  ))))) ; 
 begin  definitionlet "R" be    ($#l1_orders_2 :::"RelStr"::: )  ; attr "R" is  :::"well_founded":::  means :: WELLFND1:def 2 (Bool (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "R")  ($#r1_wellord1 :::"is_well_founded_in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "R")); end; 




:: deftheorem    defines :::"well_founded"::: WELLFND1:def 2 :  (Bool  "for" (Set (Var "R")) "being"    ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v1_wellfnd1 :::"well_founded"::: )  ) "iff" (Bool (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "R")))  ($#r1_wellord1 :::"is_well_founded_in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))))  ")" )); 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_wellfnd1 :::"well_founded"::: )    for    ($#l1_orders_2 :::"RelStr"::: )  ; 
end; definitionlet "R" be    ($#l1_orders_2 :::"RelStr"::: )  ; let "X" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "R")); attr "X" is  :::"well_founded":::  means :: WELLFND1:def 3 (Bool (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "R")  ($#r1_wellord1 :::"is_well_founded_in"::: )  "X"); end; 





:: deftheorem    defines :::"well_founded"::: WELLFND1:def 3 :  (Bool  "for" (Set (Var "R")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v2_wellfnd1 :::"well_founded"::: )  ) "iff" (Bool (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "R")))  ($#r1_wellord1 :::"is_well_founded_in"::: )  (Set (Var "X")))  ")" ))); 
 registrationlet "R" be    ($#l1_orders_2 :::"RelStr"::: )  ; 
cluster   ($#v2_wellfnd1 :::"well_founded"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "R")); 
end; definitionlet "R" be    ($#l1_orders_2 :::"RelStr"::: )  ; func  :::"well_founded-Part"::: "R" ->   ($#m1_subset_1 :::"Subset":::) "of" "R" means :: WELLFND1:def 4 (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )   "{"  (Set (Var "S")) where S "is"   ($#m1_subset_1 :::"Subset":::) "of" "R" : (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v2_wellfnd1 :::"well_founded"::: )  ) & (Bool (Set (Var "S")) "is"   ($#v12_waybel_0 :::"lower"::: )  )  ")" )  "}"  )); end; 





:: deftheorem    defines :::"well_founded-Part"::: WELLFND1:def 4 :  (Bool  "for" (Set (Var "R")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_wellfnd1 :::"well_founded-Part"::: )  (Set (Var "R")))) "iff" (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )   "{"  (Set (Var "S")) where S "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) : (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v2_wellfnd1 :::"well_founded"::: )  ) & (Bool (Set (Var "S")) "is"   ($#v12_waybel_0 :::"lower"::: )  )  ")" )  "}"  ))  ")" ))); 
 registrationlet "R" be    ($#l1_orders_2 :::"RelStr"::: )  ; 
cluster (Set   ($#k1_wellfnd1 :::"well_founded-Part"::: )  "R") ->   ($#v12_waybel_0 :::"lower"::: )     ($#v2_wellfnd1 :::"well_founded"::: )   ; 
end; 
theorem :: WELLFND1:6 (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds"  (Bool (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) "is"   ($#v2_wellfnd1 :::"well_founded"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R"))))) ; 
 
theorem :: WELLFND1:7 (Bool  "for" (Set (Var "R")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#v2_wellfnd1 :::"well_founded"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R"))  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v12_waybel_0 :::"lower"::: )  )) "holds"  (Bool (Set (Set (Var "X"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "Y"))) "is"   ($#v2_wellfnd1 :::"well_founded"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R"))))) ; 
 
theorem :: WELLFND1:8 (Bool  "for" (Set (Var "R")) "being"    ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v1_wellfnd1 :::"well_founded"::: )  ) "iff" (Bool (Set   ($#k1_wellfnd1 :::"well_founded-Part"::: )  (Set (Var "R")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))))  ")" )) ; 
 
theorem :: WELLFND1:9 (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R"))  "st" (Bool (Bool (Set (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "R")))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "x")))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_wellfnd1 :::"well_founded-Part"::: )  (Set (Var "R"))))) "holds"  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_wellfnd1 :::"well_founded-Part"::: )  (Set (Var "R")))))) ; 
 scheme  :: WELLFND1:sch 2 WFMin{ F1() ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  , F2() ->   ($#m1_subset_1 :::"Element":::) "of" (Set F1 "("  ")" ), P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set F1 "("  ")" ) "st"  (Bool  "("  (Bool P1[(Set (Var "x"))]) & (Bool  "("   "for" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set F1 "("  ")" )  "holds"  (Bool  "("   "not" (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y"))) "or"  "not" (Bool P1[(Set (Var "y"))]) "or"  "not" (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k1_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set F1 "("  ")" )))  ")" )  ")" )  ")" ))
 provided
(Bool P1[(Set F2 "("  ")" )])
 and  
(Bool (Set F1 "("  ")" ) "is"   ($#v1_wellfnd1 :::"well_founded"::: )  )
 proof 


end; 
theorem :: WELLFND1:10 (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v1_wellfnd1 :::"well_founded"::: )  ) "iff" (Bool  "for" (Set (Var "S")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R"))  "st" (Bool (Bool (Set (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "R")))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "x")))  ($#r1_tarski :::"c="::: )  (Set (Var "S")))) "holds"  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "S")))  ")" )) "holds"  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))  ($#r1_tarski :::"c="::: )  (Set (Var "S"))))  ")" )) ; 
 scheme  :: WELLFND1:sch 3 WFInduction{ F1() ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  , P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set F1 "("  ")" ) "holds"  (Bool P1[(Set (Var "x"))]))
 provided
(Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set F1 "("  ")" )  "st" (Bool (Bool  "("   "for" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set F1 "("  ")" )  "st" (Bool (Bool (Set (Var "y"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x"))) & (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k1_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set F1 "("  ")" )))) "holds"  (Bool P1[(Set (Var "y"))])  ")" )) "holds"  (Bool P1[(Set (Var "x"))]))
 and  
(Bool (Set F1 "("  ")" ) "is"   ($#v1_wellfnd1 :::"well_founded"::: )  )
 proof 


end; definitionlet "R" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; let "V" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "H" be   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Const "R"))) "," (Set  "("  ($#k3_rfunct_3 :::"PFuncs"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Const "R"))) "," (Set (Const "V")) ")"  ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "V")); let "F" be   ($#m1_hidden :::"Function":::); pred "F" :::"is_recursively_expressed_by"::: "H" means :: WELLFND1:def 5 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" "R" "holds"  (Bool (Set "F"  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set "H"  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set  "(" "F"  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "R")  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "x")) ")" ) ")" ) ")" ))); end; 







:: deftheorem    defines :::"is_recursively_expressed_by"::: WELLFND1:def 5 :  (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "V")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "H")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))) "," (Set  "("  ($#k3_rfunct_3 :::"PFuncs"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))) "," (Set (Var "V")) ")"  ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "V"))  (Bool  "for" (Set (Var "F")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "F"))  ($#r1_wellfnd1 :::"is_recursively_expressed_by"::: )  (Set (Var "H"))) "iff" (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds"  (Bool (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "H"))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set  "(" (Set (Var "F"))  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "R")))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "x")) ")" ) ")" ) ")" )))  ")" ))))); 
 
theorem :: WELLFND1:11 (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v1_wellfnd1 :::"well_founded"::: )  ) "iff" (Bool  "for" (Set (Var "V")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "H")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))) "," (Set  "("  ($#k3_rfunct_3 :::"PFuncs"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))) "," (Set (Var "V")) ")"  ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "V")) (Bool  "ex" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))) "," (Set (Var "V")) "st" (Bool (Set (Var "F"))  ($#r1_wellfnd1 :::"is_recursively_expressed_by"::: )  (Set (Var "H"))))))  ")" )) ; 
 
theorem :: WELLFND1:12 (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "V")) "being"  ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"trivial"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "H")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))) "," (Set  "("  ($#k3_rfunct_3 :::"PFuncs"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))) "," (Set (Var "V")) ")"  ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "V"))  (Bool  "for" (Set (Var "F1")) "," (Set (Var "F2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))) "," (Set (Var "V"))  "st" (Bool (Bool (Set (Var "F1"))  ($#r1_wellfnd1 :::"is_recursively_expressed_by"::: )  (Set (Var "H"))) & (Bool (Set (Var "F2"))  ($#r1_wellfnd1 :::"is_recursively_expressed_by"::: )  (Set (Var "H")))) "holds"  (Bool (Set (Var "F1"))  ($#r2_funct_2 :::"="::: )  (Set (Var "F2"))))  ")" )) "holds"  (Bool (Set (Var "R")) "is"   ($#v1_wellfnd1 :::"well_founded"::: )  ))) ; 
 
theorem :: WELLFND1:13 (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_wellfnd1 :::"well_founded"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "V")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "H")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))) "," (Set  "("  ($#k3_rfunct_3 :::"PFuncs"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))) "," (Set (Var "V")) ")"  ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "V"))  (Bool  "for" (Set (Var "F1")) "," (Set (Var "F2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))) "," (Set (Var "V"))  "st" (Bool (Bool (Set (Var "F1"))  ($#r1_wellfnd1 :::"is_recursively_expressed_by"::: )  (Set (Var "H"))) & (Bool (Set (Var "F2"))  ($#r1_wellfnd1 :::"is_recursively_expressed_by"::: )  (Set (Var "H")))) "holds"  (Bool (Set (Var "F1"))  ($#r2_funct_2 :::"="::: )  (Set (Var "F2"))))))) ; 
 definitionlet "R" be    ($#l1_orders_2 :::"RelStr"::: )  ; let "f" be   ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "R")); attr "f" is  :::"descending":::  means :: WELLFND1:def 6 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set "f"  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"<>"::: )  (Set "f"  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set  "(" "f"  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) "," (Set  "(" "f"  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "R"))  ")" )); end; 





:: deftheorem    defines :::"descending"::: WELLFND1:def 6 :  (Bool  "for" (Set (Var "R")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "R")) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v3_wellfnd1 :::"descending"::: )  ) "iff" (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "f"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) "," (Set  "(" (Set (Var "f"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "R"))))  ")" ))  ")" ))); 
 
theorem :: WELLFND1:14 (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v1_wellfnd1 :::"well_founded"::: )  ) "iff" (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "R"))  "holds" (Bool (Bool  "not" (Set (Var "f")) "is"   ($#v3_wellfnd1 :::"descending"::: )  )))  ")" )) ;