:: On same equivalents of well-foundedness
:: by Piotr Rudnicki and Andrzej Trybulec
::
:: Received February 25, 1997
:: Copyright (c) 1997 Association of Mizar Users
theorem :: WELLFND1:1
canceled;
theorem Th2: :: WELLFND1:2
theorem Th3: :: WELLFND1:3
theorem Th4: :: WELLFND1:4
:: deftheorem Def1 defines lower WELLFND1:def 1 :
theorem Th5: :: WELLFND1:5
theorem Th6: :: WELLFND1:6
:: deftheorem Def2 defines well_founded WELLFND1:def 2 :
:: deftheorem Def3 defines well_founded WELLFND1:def 3 :
:: deftheorem Def4 defines well_founded-Part WELLFND1:def 4 :
theorem Th7: :: WELLFND1:7
theorem Th8: :: WELLFND1:8
theorem Th9: :: WELLFND1:9
theorem Th10: :: WELLFND1:10
theorem Th11: :: WELLFND1:11
:: deftheorem Def5 defines is_recursively_expressed_by WELLFND1:def 5 :
theorem :: WELLFND1:12
theorem :: WELLFND1:13
theorem :: WELLFND1:14
:: deftheorem WELLFND1:def 6 :
canceled;
:: deftheorem Def7 defines descending WELLFND1:def 7 :
theorem :: WELLFND1:15