:: NAT_2  semantic presentation begin  








scheme  :: NAT_2:sch 1 NonUniqPiFinRecExD{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ), F3() ->   ($#m1_hidden :::"Nat":::), P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set F1 "("  ")" ) "st"  (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set F3 "("  ")" )) & (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set F2 "("  ")" )) "or" (Bool (Set F3 "("  ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set F3 "("  ")" ))) "holds"  (Bool P1[(Set (Var "n")) "," (Set (Set (Var "p"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n"))) "," (Set (Set (Var "p"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))])  ")" )  ")" ))
 provided
(Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set F3 "("  ")" ))) "holds"  (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) (Bool  "ex" (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) "st" (Bool P1[(Set (Var "n")) "," (Set (Var "x")) "," (Set (Var "y"))]))))
 proof 


end; 
theorem :: NAT_2:1 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "y"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "x"))  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set  ($#k1_int_1 :::"[\"::: ) (Set  "(" (Set (Var "x"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "y")) ")" ) ($#k1_int_1 :::"/]"::: ) )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "y")))) ; 
 begin  
theorem :: NAT_2:2 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  ($#k6_numbers :::"0"::: ) )  ($#k3_nat_d :::"div"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: NAT_2:3 (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "n"))  ($#k3_nat_d :::"div"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: NAT_2:4 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "n"))  ($#k3_nat_d :::"div"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) ; 
 
theorem :: NAT_2:5 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "," (Set (Var "l")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "j"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "k")) ")" )  ($#k2_nat_1 :::"+"::: )  (Set (Var "l"))))) "holds"  (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "j"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "i")) ")" )  ($#k2_nat_1 :::"+"::: )  (Set (Var "l"))))) ; 
 
theorem :: NAT_2:6 (Bool  "for" (Set (Var "i")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "i")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) ; 
 
theorem :: NAT_2:7 (Bool  "for" (Set (Var "j")) "," (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i")))) "holds"  (Bool (Set (Set  "(" (Set (Var "i"))  ($#k7_nat_d :::"-'"::: )  (Set  "(" (Set (Var "j"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "j"))))) ; 
 
theorem :: NAT_2:8 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "j")))) "holds"  (Bool (Set (Set (Var "j"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: NAT_2:9 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::)  "holds" (Bool (Set (Set (Var "i"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "j")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i")))) ; 
 
theorem :: NAT_2:10 (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Num 2)  ($#k3_power :::"to_power"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k3_power :::"to_power"::: )  (Set (Var "k")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Num 2)  ($#k3_power :::"to_power"::: )  (Set  "(" (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "k")) ")" ) ")" )))) ; 
 
theorem :: NAT_2:11 (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Num 2)  ($#k3_power :::"to_power"::: )  (Set (Var "k")))  ($#r1_nat_d :::"divides"::: )  (Set (Num 2)  ($#k3_power :::"to_power"::: )  (Set (Var "n"))))) ; 
 
theorem :: NAT_2:12 (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "n"))  ($#k3_nat_d :::"div"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "k")))) ; 
 
theorem :: NAT_2:13 (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set (Var "n"))  ($#k3_nat_d :::"div"::: )  (Set (Var "k")))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) ; 
 
theorem :: NAT_2:14 (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k")) ")" )  ($#k3_nat_d :::"div"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "n"))  ($#k3_nat_d :::"div"::: )  (Set (Var "k")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1)))) ; 
 
theorem :: NAT_2:15 (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "," (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "n"))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k")))) "holds"  (Bool (Set (Set  "(" (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "i")) ")" )  ($#k3_nat_d :::"div"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "n"))  ($#k3_nat_d :::"div"::: )  (Set (Var "k")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Num 1)))) ; 
 
theorem :: NAT_2:16 (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set  "(" (Num 2)  ($#k3_power :::"to_power"::: )  (Set (Var "n")) ")" )  ($#k3_nat_d :::"div"::: )  (Set  "(" (Num 2)  ($#k3_power :::"to_power"::: )  (Set (Var "k")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k3_power :::"to_power"::: )  (Set  "(" (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "k")) ")" )))) ; 
 
theorem :: NAT_2:17 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Num 2)  ($#k3_power :::"to_power"::: )  (Set (Var "n")) ")" )  ($#k4_nat_d :::"mod"::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: NAT_2:18 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Set (Var "n"))  ($#k4_nat_d :::"mod"::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool (Set (Set  "(" (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" )  ($#k4_nat_d :::"mod"::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )) ; 
 
theorem :: NAT_2:19 (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Num 1))) "holds"  (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Num 1))) ; 
 
theorem :: NAT_2:20 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "n"))))) "holds"  (Bool (Set (Set (Var "k"))  ($#k3_nat_d :::"div"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: NAT_2:21 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "n")) "is"   ($#v1_abian :::"even"::: )  ) "iff" (Bool (Set (Set (Var "n"))  ($#k4_nat_d :::"mod"::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) ; 
 
theorem :: NAT_2:22 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "n")) "is"   ($#v1_abian :::"odd"::: )  ) "iff" (Bool (Set (Set (Var "n"))  ($#k4_nat_d :::"mod"::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )) ; 
 
theorem :: NAT_2:23 (Bool  "for" (Set (Var "t")) "," (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "t"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "t")))  ($#r1_nat_d :::"divides"::: )  (Set (Var "k")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "n"))  ($#k3_nat_d :::"div"::: )  (Set (Var "t"))) "is"   ($#v1_abian :::"even"::: )  ) "iff" (Bool (Set (Set  "(" (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "k")) ")" )  ($#k3_nat_d :::"div"::: )  (Set (Var "t"))) "is"   ($#v1_abian :::"even"::: )  )  ")" )) ; 
 
theorem :: NAT_2:24 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))) "holds"  (Bool (Set (Set (Var "n"))  ($#k3_nat_d :::"div"::: )  (Set (Var "k")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "m"))  ($#k3_nat_d :::"div"::: )  (Set (Var "k"))))) ; 
 
theorem :: NAT_2:25 (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "k"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" )  ($#k3_nat_d :::"div"::: )  (Num 2))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) ; 
 
theorem :: NAT_2:26 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n")) "is"   ($#v1_abian :::"even"::: )  )) "holds"  (Bool (Set (Set (Var "n"))  ($#k3_nat_d :::"div"::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" )  ($#k3_nat_d :::"div"::: )  (Num 2)))) ; 
 
theorem :: NAT_2:27 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "," (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "n"))  ($#k3_nat_d :::"div"::: )  (Set (Var "k")) ")" )  ($#k3_nat_d :::"div"::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k3_nat_d :::"div"::: )  (Set  "(" (Set (Var "k"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "i")) ")" )))) ; 
 definitionlet "n" be   ($#m1_hidden :::"Nat":::); redefine attr "n" is  :::"trivial":::  means :: NAT_2:def 1 (Bool  "("  (Bool "n"  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool "n"  ($#r1_hidden :::"="::: )  (Num 1))  ")" ); end; 




:: deftheorem    defines :::"trivial"::: NAT_2:def 1 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "n")) "is"   ($#v1_zfmisc_1 :::"trivial"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )  ")" )); 
 registration
cluster   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )   ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"trivial"::: )   )    ($#v3_ordinal1 :::"ordinal"::: )     ($#v7_ordinal1 :::"natural"::: )   bbbadV1_XCMPLX_0()   ($#v1_xreal_0 :::"real"::: )     ($#v1_int_1 :::"integer"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: NAT_2:28 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Bool  "not" (Set (Var "k")) "is"   ($#v1_zfmisc_1 :::"trivial"::: )  )) "iff" (Bool  "("  (Bool (Bool  "not" (Set (Var "k")) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  (Num 1))  ")" )  ")" )) ; 
 
theorem :: NAT_2:29 (Bool  "for" (Set (Var "k")) "being"  ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"trivial"::: )   )   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) ; 
 scheme  :: NAT_2:sch 2 Indfrom2{ P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "for" (Set (Var "k")) "being"  ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"trivial"::: )   )   ($#m1_hidden :::"Nat":::) "holds"  (Bool P1[(Set (Var "k"))]))
 provided
(Bool P1[(Num 2)])
 and  
(Bool  "for" (Set (Var "k")) "being"  ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"trivial"::: )   )   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool P1[(Set (Var "k"))])) "holds"  (Bool P1[(Set (Set (Var "k"))  ($#k1_nat_1 :::"+"::: )  (Num 1))]))
 proof 


end; begin  
theorem :: NAT_2:30 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "i"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "j")) ")" )  ($#k7_nat_d :::"-'"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k7_nat_d :::"-'"::: )  (Set  "(" (Set (Var "j"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k")) ")" )))) ;