begin
theorem Th1:
for
n1,
n,
n2 being
Nat st (
n1 > n or
n2 > n ) holds
n1 + n2 > n
theorem Th2:
for
n1,
n,
n2 being
Nat st
n1 + n <= n2 + 1 &
n > 0 holds
n1 <= n2
theorem Th3:
for
n1,
n2 being
Nat holds
(
n1 + n2 = 1 iff ( (
n1 = 1 &
n2 = 0 ) or (
n1 = 0 &
n2 = 1 ) ) )
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem
theorem
canceled;
Th10:
for i, j being Nat
for p being XFinSequence st len p = i + j holds
ex q1, q2 being XFinSequence st
( len q1 = i & len q2 = j & p = q1 ^ q2 )
by AFINSQ_1:65;
theorem
theorem Th12:
begin
:: deftheorem Def1 defines ^^ FLANG_1:def 1 :
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem
begin
:: deftheorem Def2 defines |^ FLANG_1:def 2 :
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem
theorem Th31:
theorem
theorem Th33:
theorem Th34:
theorem
theorem Th36:
theorem
theorem Th38:
theorem
theorem
theorem Th41:
begin
:: deftheorem defines * FLANG_1:def 3 :
theorem Th42:
theorem Th43:
theorem Th44:
theorem
theorem Th46:
theorem Th47:
theorem
theorem Th49:
theorem
theorem Th51:
theorem
theorem Th53:
theorem
theorem Th55:
theorem
theorem Th57:
theorem Th58:
theorem
theorem Th60:
theorem Th61:
theorem Th62:
theorem Th63:
theorem
theorem
theorem Th66:
theorem
theorem Th68:
theorem Th69:
theorem
theorem
theorem
theorem Th73:
begin
:: deftheorem Def4 defines Lex FLANG_1:def 4 :
theorem Th74:
theorem
theorem