Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 955


Synopsis:        unprovable TCC generated?!
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Mon May  1 03:25:00 2006
Originator:      Hesselink
Organization:    rug.nl
Release:         PVS 3.2
Environment: 
 System:          
 Architecture: 

Description: 
  This is a multi-part message in MIME format.
  --------------000106010303050106070903
  Content-Type: text/plain; charset=ISO-8859-1; format=flowed
  Content-Transfer-Encoding: 7bit
  
  Dear PVS team,
  
  The attached dumpfile contains a lemma infty_gg_injective, where I try 
  to call a lemma that forms an inverse of a surjective function between 
  subtypes. When calling this lemma, PVS creates an unprovable TCC, while 
  --as far as I can see-- it should not do so.
  
  Best regards,
  Wim
  
  -- 
  Wim H. Hesselink  
  
  Dept. of Computing Science | phone +31 50 3633933
  University of Groningen    |    or +31 50 3633939
  P.O.Box 800                | fax   +31 50 3633800
  9700 AV Groningen          | email: w.h.hesselink@rug.nl
  The Netherlands            | http://www.cs.rug.nl/~wim
  
  
  --------------000106010303050106070903
  Content-Type: text/plain;
   name="dumplcard"
  Content-Transfer-Encoding: 7bit
  Content-Disposition: inline;
   filename="dumplcard"
  
  
  %% PVS Version 3.2
  %% 6.2 [Linux (x86)] (Nov 3, 2004 23:30)
  $$$PVSHOME/.pvs.lisp
  
  $$$PVSHOME/.pvs.lisp
  
  $$$moreLift.pvs
  % Wim H. Hesselink, April 2006
  
  moreLift[T: TYPE]: THEORY
  
  BEGIN
    x, x1: VAR T
    y: VAR lift[T]
  
    up_down: LEMMA
      up(x) = y IMPLIES x = down(y)
  
    down_up: LEMMA
      up?(y) AND x = down(y) IMPLIES up(x) = y
  
    up_injective: LEMMA
      up(x) = up(x1) IMPLIES x = x1
  
  END moreLift
  
  $$$moreLift.prf
  (moreLift
   (up_down_TCC1 0
    (up_down_TCC1-1 nil 3355454976 3355455077 ("" (grind) nil nil) proved
     nil 57 40 nil nil))
   (up_down 0
    (up_down-1 nil 3355454976 3355455125
     ("" (skosimp) (("" (replace -1 + rl) (("" (assert) nil nil)) nil))
      nil)
     proved nil 31247 330 t nil))
   (down_up 0
    (down_up-1 nil 3355454976 3355455078
     ("" (skosimp)
      (("" (replace -2) (("" (apply-extensionality :hide? t) nil nil))
        nil))
      nil)
     proved
     ((up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
      (boolean nonempty-type-decl nil booleans nil)
      (lift type-decl nil lift_adt nil)
      (T formal-type-decl nil moreLift nil)
      (lift_up_extensionality formula-decl nil lift_adt nil)
      (down adt-accessor-decl "[(up?) -> T]" lift_adt nil)
      (up adt-constructor-decl "[T -> (up?)]" lift_adt nil))
     21 20 nil nil))
   (up_injective 0
    (up_injective-1 nil 3355454976 3355455078
     ("" (skosimp) (("" (use "up_down") (("" (assert) nil nil)) nil))
      nil)
     proved
     ((up_down formula-decl nil moreLift nil)
      (up adt-constructor-decl "[T -> (up?)]" lift_adt nil)
      (up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
      (boolean nonempty-type-decl nil booleans nil)
      (lift type-decl nil lift_adt nil)
      (T formal-type-decl nil moreLift nil))
     43 20 nil nil)))
  
  
  $$$lcard_def.pvs
  % Wim H. Hesslink, October 2005
  % A theory that allows card(S) = infty for infinite sets.
  % We use -1: int as the alias for infty.
  % We therefore redefine plus, times and leq (less than or equal).
  
  lnat_th: THEORY
  
  BEGIN 
    IMPORTING moreLift
  
    lnat: TYPE = lift[nat]
    % bottom serves as infinity
  
    x, y, z: VAR lnat
  
    <= (x, y): bool =
      bottom?(y) OR up?(x) AND down(x) <= down(y)
  
    leq_transitive: LEMMA
      x <= y AND y <= z IMPLIES x <= z
  
    leq_connected: LEMMA
      x <= y OR y <= x
  
    leq_antisymmetric: LEMMA
      x <= y AND y <= x IMPLIES x = y ;
  
    + (x, y): lnat =
      IF bottom?(x) OR bottom?(y) THEN bottom ELSE up(down(x) + down(y)) ENDIF
  
    plus_associative: LEMMA
      (x + y) + z = x + (y + z)
  
    plus_commutative: LEMMA
      x + y = y + x
  
    plus_monotonic: LEMMA
      x <= y IMPLIES x + z <= y + z ;
  
    * (x, y): lnat =
      IF x = up(0) OR y = up(0) THEN up(0)
      ELSIF bottom?(x) OR bottom?(y) THEN bottom
      ELSE up(down(x) * down(y)) ENDIF
  
    no_zero_divisors: LEMMA
      x * y = up(0) IMPLIES x = up(0) OR y = up(0)
  
    no_zero_adding: LEMMA
      x + y = up(0) IMPLIES x = up(0) AND y = up(0)
  
    times_zero1: LEMMA
      x * up(0) = up(0)
  
    times_zero2: LEMMA
      up(0) * x = up(0)
  
    plus_zero1: LEMMA
      x + up(0) = x
  
    plus_zero2: LEMMA
      up(0) + x = x
  
    times_associative: LEMMA
      (x * y) * z = x * (y * z)
  
    times_commutative: LEMMA
      x * y = y * x
  
    plus_times_distribution: LEMMA
      (x * y) + (x * z) = x * (y + z)
  
    times_monotonic: LEMMA
      x <= y IMPLIES x * z <= y * z
  
    k, n: VAR nat 
  
    scanning_rectangle: LEMMA
      EXISTS (h: [below[k], below[n] -> below[k*n]]): bijective?(h)
  
    nat_not_finite: THEOREM
      NOT is_finite(fullset[nat])
  
  END lnat_th
  
  lcard_def[T: TYPE]: THEORY
  BEGIN
    IMPORTING lnat_th, finite_sets
  
    S, A, B: VAR pred[T]
    x: VAR T
    N: VAR nat
  
    lcard(S): lnat =
      IF is_finite(S) THEN up(card(S)) ELSE bottom ENDIF
  
    lcard_empty? : THEOREM 
      (lcard(S) = up(0)) = empty?(S)
  
    lcard_one: THEOREM 
      lcard(S) = up(1) IFF (EXISTS x : S = singleton(x))
  
    lcard_subset: THEOREM 
      subset?(A,B) IMPLIES lcard(A) <= lcard(B)
  
    lcard_disj_union: THEOREM 
      disjoint?(A,B) IMPLIES 
      lcard(union(A,B)) = lcard(A) + lcard(B)
  
    lcard_add: THEOREM 
      lcard(add(x, S)) = lcard(S) + up(IF S(x) THEN 0 ELSE 1 ENDIF)
  
    lcard_union: THEOREM 
      lcard(union(A,B)) + lcard(intersection(A,B)) = 
        lcard(A) + lcard(B)
  
    lcard_bij: LEMMA
      lcard(S) = up(N) IFF (EXISTS (f: [(S) -> below[N]]): bijective?(f))    
  
  END lcard_def
  
  lcard_th2[T, U: TYPE]: THEORY
  BEGIN
    IMPORTING lcard_def
  
    A: VAR pred[T]
    B: VAR pred[U]
  
    injective_lcard: THEOREM
      (EXISTS (f: [(A) -> (B)]): injective?(f))
      IMPLIES lcard(A) <= lcard(B)
  
    surjective_injective: THEOREM
      FORALL (f: [(A) -> (B)]): surjective?(f) 
        IMPLIES EXISTS (g: [(B) -> (A)]): f o g = id[(B)]
  
    lcard_Cartesian: THEOREM
      lcard({x: [T, U] | A(x`1) AND B(x`2)}) = lcard(A) * lcard(B)
  
  END lcard_th2
  
  lcard_th4[T, U: TYPE]: THEORY
  BEGIN
    IMPORTING lcard_th2
  
    A: VAR pred[T]
    B: VAR pred[U]
  
    surjective_lcard: THEOREM 
      (EXISTS (f: [(A) -> (B)]): surjective?(f))
      IMPLIES lcard(B) <= lcard(A)
  
    bijective_lcard: THEOREM
      (EXISTS (f: [(A) -> (B)]): bijective?(f))
      IMPLIES lcard(B) = lcard(A)
  END lcard_th4
  
  lcard_th3[T: TYPE]: THEORY
  BEGIN 
    IMPORTING lcard_th2
  
    S: VAR pred[T]
    x, undef: VAR T
    i, n: VAR nat
  
    gg(S, undef)(n): RECURSIVE T =
      epsilon({x| S(x) AND FORALL i: i < n IMPLIES x /= gg(S, undef)(i)})
      MEASURE LAMBDA (S, undef) (n): n
  
    inrange?(S, (f:[nat -> T])): bool =
      FORALL i: S(f(i))
  
    infty_gg_injective: LEMMA
      bottom?(lcard(S)) IMPLIES 
        injective?(gg(S, epsilon(S))) AND inrange?(S, gg(S, epsilon(S)))
  
    infty_lcard: THEOREM
      bottom?(lcard(S)) = EXISTS (f: [nat -> (S)]): injective?(f)
  
  END lcard_th3
  
  $$$lcard_def.prf
  (lnat_th
   (lesseqp_TCC1 0
    (lesseqp_TCC1-1 nil 3355454976 3355454987 ("" (subtype-tcc) nil nil)
     proved
     ((boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (number nonempty-type-decl nil numbers nil)
      (PRED type-eq-decl nil defined_types nil)
      (lift type-decl nil lift_adt nil)
      (every adt-def-decl "boolean" lift_adt nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields
       nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (>= const-decl "bool" reals nil)
      (lnat type-eq-decl nil lnat_th nil))
     191 130 nil nil))
   (leq_transitive 0
    (leq_transitive-1 nil 3355454976 3355454988 ("" (grind) nil nil)
     proved
     ((boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (number nonempty-type-decl nil numbers nil)
      (PRED type-eq-decl nil defined_types nil)
      (lift type-decl nil lift_adt nil)
      (every adt-def-decl "boolean" lift_adt nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields
       nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (>= const-decl "bool" reals nil)
      (lnat type-eq-decl nil lnat_th nil)
      (<= const-decl "bool" lnat_th nil))
     273 210 nil nil))
   (leq_connected 0
    (leq_connected-1 nil 3355454976 3355454988 ("" (grind) nil nil)
     proved
     ((boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (number nonempty-type-decl nil numbers nil)
      (PRED type-eq-decl nil defined_types nil)
      (lift type-decl nil lift_adt nil)
      (every adt-def-decl "boolean" lift_adt nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields
       nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (>= const-decl "bool" reals nil)
      (lnat type-eq-decl nil lnat_th nil)
      (<= const-decl "bool" lnat_th nil))
     115 80 nil nil))
   (leq_antisymmetric 0
    (leq_antisymmetric-1 nil 3355454976 3355454988
     ("" (skosimp)
      (("" (expand "<=")
        (("" (prop)
          (("1" (assert) nil nil) ("2" (assert) nil nil)
           ("3" (assert) nil nil)
           ("4" (case "down(x!1) = down(y!1)")
            (("1" (hide -3 -5)
              (("1" (case "x!1 = up(down(y!1))")
                (("1" (replace -1 +)
                  (("1" (apply-extensionality :hide? t) nil nil)) nil)
                 ("2" (replace -1 + rl)
                  (("2" (apply-extensionality :hide? t) nil nil)) nil))
                nil))
              nil)
             ("2" (assert) nil nil) ("3" (propax) nil nil)
             ("4" (propax) nil nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((<= const-decl "bool" lnat_th nil)
      (lnat type-eq-decl nil lnat_th nil)
      (down adt-accessor-decl "[(up?) -> T]" lift_adt nil)
      (up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (int nonempty-type-eq-decl nil integers nil)
      (>= const-decl "bool" reals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields
       nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (every adt-def-decl "boolean" lift_adt nil)
      (PRED type-eq-decl nil defined_types nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (lift type-decl nil lift_adt nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (boolean nonempty-type-decl nil booleans nil)
      (number nonempty-type-decl nil numbers nil)
      (up adt-constructor-decl "[T -> (up?)]" lift_adt nil)
      (lift_up_extensionality formula-decl nil lift_adt nil))
     159 110 nil nil))
   (plus_TCC1 0
    (plus_TCC1-1 nil 3355454976 3355454988 ("" (grind) nil nil) proved
     ((boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (number nonempty-type-decl nil numbers nil)
      (PRED type-eq-decl nil defined_types nil)
      (lift type-decl nil lift_adt nil)
      (every adt-def-decl "boolean" lift_adt nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields
       nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (>= const-decl "bool" reals nil)
      (lnat type-eq-decl nil lnat_th nil))
     84 70 nil nil))
   (plus_TCC2 0
    (plus_TCC2-1 nil 3355454976 3355454988 ("" (subtype-tcc) nil nil)
     proved
     ((boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (number nonempty-type-decl nil numbers nil)
      (PRED type-eq-decl nil defined_types nil)
      (lift type-decl nil lift_adt nil)
      (every adt-def-decl "boolean" lift_adt nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields
       nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (>= const-decl "bool" reals nil)
      (lnat type-eq-decl nil lnat_th nil))
     73 50 nil nil))
   (plus_TCC3 0
    (plus_TCC3-1 nil 3355454976 3355454988 ("" (grind) nil nil) proved
     ((boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (number nonempty-type-decl nil numbers nil)
      (PRED type-eq-decl nil defined_types nil)
      (lift type-decl nil lift_adt nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields
       nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (>= const-decl "bool" reals nil)
      (lnat type-eq-decl nil lnat_th nil)
      (every adt-def-decl "boolean" lift_adt nil))
     330 300 nil nil))
   (plus_associative 0
    (plus_associative-1 nil 3355454976 3355454989 ("" (grind) nil nil)
     proved
     ((boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (number nonempty-type-decl nil numbers nil)
      (PRED type-eq-decl nil defined_types nil)
      (lift type-decl nil lift_adt nil)
      (every adt-def-decl "boolean" lift_adt nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields
       nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (>= const-decl "bool" reals nil)
      (lnat type-eq-decl nil lnat_th nil)
      (+ const-decl "lnat" lnat_th nil))
     482 420 nil nil))
   (plus_commutative 0
    (plus_commutative-1 nil 3355454976 3355454989 ("" (grind) nil nil)
     proved
     ((boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (number nonempty-type-decl nil numbers nil)
      (PRED type-eq-decl nil defined_types nil)
      (lift type-decl nil lift_adt nil)
      (every adt-def-decl "boolean" lift_adt nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields
       nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (>= const-decl "bool" reals nil)
      (lnat type-eq-decl nil lnat_th nil)
      (+ const-decl "lnat" lnat_th nil))
     134 110 nil nil))
   (plus_monotonic 0
    (plus_monotonic-1 nil 3355454976 3355454989 ("" (grind) nil nil)
     proved
     ((boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (number nonempty-type-decl nil numbers nil)
      (PRED type-eq-decl nil defined_types nil)
      (lift type-decl nil lift_adt nil)
      (every adt-def-decl "boolean" lift_adt nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields
       nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (>= const-decl "bool" reals nil)
      (lnat type-eq-decl nil lnat_th nil)
      (<= const-decl "bool" lnat_th nil)
      (+ const-decl "lnat" lnat_th nil))
     466 410 nil nil))
   (times_TCC1 0
    (times_TCC1-1 nil 3355454976 3355454990
     ("" (skosimp)
      (("" (use "pos_times_le") (("" (assert) nil nil)) nil)) nil)
     proved
     ((pos_times_le formula-decl nil real_props nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields
       nil)
      (boolean nonempty-type-decl nil booleans nil)
      (number nonempty-type-decl nil numbers nil))
     372 340 nil nil))
   (times_TCC2 0
    (times_TCC2-1 nil 3355454976 3355454990 ("" (grind) nil nil) proved
     ((boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (number nonempty-type-decl nil numbers nil)
      (PRED type-eq-decl nil defined_types nil)
      (lift type-decl nil lift_adt nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields
       nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (>= const-decl "bool" reals nil)
      (lnat type-eq-decl nil lnat_th nil)
      (every adt-def-decl "boolean" lift_adt nil))
     420 380 nil nil))
   (no_zero_divisors 0
    (no_zero_divisors-1 nil 3355454976 3355454991
     ("" (skosimp)
      (("" (expand "*")
        (("" (assert)
          (("" (lift-if)
            (("" (ground)
              (("" (use "up_injective[nat]")
                (("" (assert)
                  (("" (hide -2)
                    (("" (use "zero_times3")
                      (("" (assert)
                        (("" (split)
                          (("1" (use "down_up[nat]")
                            (("1" (assert) nil nil)) nil)
                           ("2" (use "down_up[nat]")
                            (("2" (ground) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((* const-decl "lnat" lnat_th nil)
      (up_injective formula-decl nil moreLift nil)
      (number nonempty-type-decl nil numbers nil)
      (boolean nonempty-type-decl nil booleans nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields
       nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (int nonempty-type-eq-decl nil integers nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (>= const-decl "bool" reals nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (lnat type-eq-decl nil lnat_th nil)
      (down adt-accessor-decl "[(up?) -> T]" lift_adt nil)
      (up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (every adt-def-decl "boolean" lift_adt nil)
      (PRED type-eq-decl nil defined_types nil)
      (lift type-decl nil lift_adt nil)
      (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (numfield nonempty-type-eq-decl nil number_fields nil)
      (down_up formula-decl nil moreLift nil)
      (zero_times3 formula-decl nil real_props nil))
     533 450 nil nil))
   (no_zero_adding 0
    (no_zero_adding-1 nil 3355454976 3355454991
     ("" (skosimp)
      (("" (expand "+ ")
        (("" (lift-if)
          (("" (split -)
            (("1" (flatten) (("1" (assert) nil nil)) nil)
             ("2" (flatten)
              (("2" (use "up_injective[nat]")
                (("1" (assert)
                  (("1" (case "down(x!1) = 0 AND down(y!1) = 0")
                    (("1" (flatten)
                      (("1" (use "down_up" ("y" "y!1"))
                        (("1" (use "down_up" ("y" "x!1"))
                          (("1" (assert) nil nil)) nil))
                        nil))
                      nil)
                     ("2" (hide -2 4) (("2" (assert) nil nil)) nil))
                    nil))
                  nil)
                 ("2" (assert) nil nil) ("3" (assert) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((+ const-decl "lnat" lnat_th nil)
      (up_injective formula-decl nil moreLift nil)
      (number nonempty-type-decl nil numbers nil)
      (boolean nonempty-type-decl nil booleans nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields
       nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (int nonempty-type-eq-decl nil integers nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (>= const-decl "bool" reals nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (lnat type-eq-decl nil lnat_th nil)
      (down adt-accessor-decl "[(up?) -> T]" lift_adt nil)
      (up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (every adt-def-decl "boolean" lift_adt nil)
      (PRED type-eq-decl nil defined_types nil)
      (lift type-decl nil lift_adt nil)
      (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (numfield nonempty-type-eq-decl nil number_fields nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (down_up formula-decl nil moreLift nil))
     420 320 nil nil))
   (times_zero1_TCC1 0
    (times_zero1_TCC1-1 nil 3355454976 3355454991 ("" (grind) nil nil)
     proved ((every adt-def-decl "boolean" lift_adt nil)) 22 20 nil nil))
   (times_zero1 0
    (times_zero1-1 nil 3355454976 3355454991 ("" (grind) nil nil) proved
     ((* const-decl "lnat" lnat_th nil)) 12 20 nil nil))
   (times_zero2 0
    (times_zero2-1 nil 3355454976 3355454991 ("" (grind) nil nil) proved
     ((* const-decl "lnat" lnat_th nil)) 11 10 nil nil))
   (plus_zero1 0
    (plus_zero1-1 nil 3355454976 3355454991
     ("" (skosimp)
      (("" (expand "+ ")
        (("" (lift-if)
          (("" (prop)
            (("1" (apply-extensionality :hide? t) nil nil)
             ("2" (apply-extensionality :hide? t) nil nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((+ const-decl "lnat" lnat_th nil)
      (bottom? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (int nonempty-type-eq-decl nil integers nil)
      (>= const-decl "bool" reals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields
       nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (every adt-def-decl "boolean" lift_adt nil)
      (PRED type-eq-decl nil defined_types nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (lift type-decl nil lift_adt nil)
      (number nonempty-type-decl nil numbers nil)
      (lift_bottom_extensionality formula-decl nil lift_adt nil)
      (x!1 skolem-const-decl "lnat" lnat_th nil)
      (lnat type-eq-decl nil lnat_th nil)
      (bottom adt-constructor-decl "(bottom?)" lift_adt nil)
      (up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
      (numfield nonempty-type-eq-decl nil number_fields nil)
      (lift_up_extensionality formula-decl nil lift_adt nil)
      (down adt-accessor-decl "[(up?) -> T]" lift_adt nil)
      (up adt-constructor-decl "[T -> (up?)]" lift_adt nil))
     66 30 nil nil))
   (plus_zero2 0
    (plus_zero2-1 nil 3355454976 3355454991
     ("" (skolem!)
      (("" (expand "+ ")
        (("" (lift-if)
          (("" (prop)
            (("1" (apply-extensionality :hide? t) nil nil)
             ("2" (apply-extensionality :hide? t) nil nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((+ const-decl "lnat" lnat_th nil)
      (bottom? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (int nonempty-type-eq-decl nil integers nil)
      (>= const-decl "bool" reals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields
       nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (every adt-def-decl "boolean" lift_adt nil)
      (PRED type-eq-decl nil defined_types nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (lift type-decl nil lift_adt nil)
      (number nonempty-type-decl nil numbers nil)
      (lift_bottom_extensionality formula-decl nil lift_adt nil)
      (x!1 skolem-const-decl "lnat" lnat_th nil)
      (lnat type-eq-decl nil lnat_th nil)
      (bottom adt-constructor-decl "(bottom?)" lift_adt nil)
      (up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
      (numfield nonempty-type-eq-decl nil number_fields nil)
      (lift_up_extensionality formula-decl nil lift_adt nil)
      (down adt-accessor-decl "[(up?) -> T]" lift_adt nil)
      (up adt-constructor-decl "[T -> (up?)]" lift_adt nil))
     43 40 nil nil))
   (times_associative 0
    (times_associative-1 nil 3355454976 3355454992
     ("" (skosimp)
      (("" (case "x!1=up(0)")
        (("1" (grind) nil nil)
         ("2" (case "y!1=up(0)")
          (("1" (grind) nil nil)
           ("2" (case "z!1=up(0)")
            (("1" (grind) nil nil)
             ("2" (case "x!1*y!1=up(0)")
              (("1" (use "no_zero_divisors") (("1" (assert) nil nil))
                nil)
               ("2" (case "y!1 * z!1=up(0)")
                (("1" (use "no_zero_divisors") (("1" (assert) nil nil))
                  nil)
                 ("2" (grind) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((up adt-constructor-decl "[T -> (up?)]" lift_adt nil)
      (up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
      (lnat type-eq-decl nil lnat_th nil)
      (>= const-decl "bool" reals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields
       nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (every adt-def-decl "boolean" lift_adt nil)
      (PRED type-eq-decl nil defined_types nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (boolean nonempty-type-decl nil booleans nil)
      (lift type-decl nil lift_adt nil)
      (number nonempty-type-decl nil numbers nil)
      (* const-decl "lnat" lnat_th nil)
      (no_zero_divisors formula-decl nil lnat_th nil))
     957 830 nil nil))
   (times_commutative 0
    (times_commutative-1 nil 3355454976 3355454993 ("" (grind) nil nil)
     proved
     ((boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (number nonempty-type-decl nil numbers nil)
      (PRED type-eq-decl nil defined_types nil)
      (lift type-decl nil lift_adt nil)
      (every adt-def-decl "boolean" lift_adt nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields
       nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (>= const-decl "bool" reals nil)
      (lnat type-eq-decl nil lnat_th nil)
      (* const-decl "lnat" lnat_th nil))
     219 180 nil nil))
   (plus_times_distribution 0
    (plus_times_distribution-1 nil 3355454976 3355454994
     ("" (skosimp)
      (("" (case "x!1=up(0)")
        (("1" (grind) nil nil)
         ("2" (case "y!1=up(0)")
          (("1" (replace -1)
            (("1" (use "times_zero1")
              (("1" (replace -1)
                (("1" (use "plus_zero2")
                  (("1" (use "plus_zero2" ("x" "z!1"))
                    (("1" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (case "z!1 = up(0)")
            (("1" (replace -1)
              (("1" (use "times_zero1")
                (("1" (replace -1)
                  (("1" (use "plus_zero1")
                    (("1" (use "plus_zero1" ("x" "y!1"))
                      (("1" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (case "y!1 + z!1 = up(0)")
              (("1" (use "no_zero_adding") (("1" (assert) nil nil)) nil)
               ("2" (grind) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((up adt-constructor-decl "[T -> (up?)]" lift_adt nil)
      (up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
      (lnat type-eq-decl nil lnat_th nil)
      (>= const-decl "bool" reals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields
       nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (every adt-def-decl "boolean" lift_adt nil)
      (PRED type-eq-decl nil defined_types nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (boolean nonempty-type-decl nil booleans nil)
      (lift type-decl nil lift_adt nil)
      (number nonempty-type-decl nil numbers nil)
      (+ const-decl "lnat" lnat_th nil) (* const-decl "lnat" lnat_th nil)
      (plus_zero1 formula-decl nil lnat_th nil)
      (no_zero_adding formula-decl nil lnat_th nil)
      (plus_zero2 formula-decl nil lnat_th nil)
      (times_zero1 formula-decl nil lnat_th nil))
     998 850 nil nil))
   (times_monotonic 0
    (times_monotonic-1 nil 3355454976 3355454994
     ("" (skosimp)
      (("" (case "x!1 = up(0)")
        (("1" (grind) nil nil)
         ("2" (case "y!1=up(0)")
          (("1" (hide 2)
            (("1" (expand "<=")
              (("1" (assert)
                (("1" (flatten)
                  (("1" (replace -1)
                    (("1" (assert)
                      (("1" (case "down(x!1) = 0")
                        (("1" (apply-extensionality :hide? t) nil nil)
                         ("2" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (grind)
            (("2" (use "both_sides_times_pos_le1")
              (("2" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((up adt-constructor-decl "[T -> (up?)]" lift_adt nil)
      (up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
      (lnat type-eq-decl nil lnat_th nil)
      (>= const-decl "bool" reals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields
       nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (every adt-def-decl "boolean" lift_adt nil)
      (PRED type-eq-decl nil defined_types nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (boolean nonempty-type-decl nil booleans nil)
      (lift type-decl nil lift_adt nil)
      (number nonempty-type-decl nil numbers nil)
      (* const-decl "lnat" lnat_th nil)
      (<= const-decl "bool" lnat_th nil)
      (nonneg_real nonempty-type-eq-decl nil real_types nil)
      (> const-decl "bool" reals nil)
      (posreal nonempty-type-eq-decl nil real_types nil)
      (both_sides_times_pos_le1 formula-decl nil real_props nil)
      (down adt-accessor-decl "[(up?) -> T]" lift_adt nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (int nonempty-type-eq-decl nil integers nil)
      (lift_up_extensionality formula-decl nil lift_adt nil))
     916 790 nil nil))
   (scanning_rectangle 0
    (scanning_rectangle-1 nil 3355454976 3355454998
     ("" (skosimp)
      (("" (inst + "LAMBDA (x: below[k!1], y: below[n!1]): n!1 * x + y")
        (("1" (expand "bijective?")
          (("1" (split)
            (("1" (expand "injective?")
              (("1" (skosimp)
                (("1" (use "unique_quotient")
                  (("1" (assert)
                    (("1" (apply-extensionality :hide? t) nil nil)) nil)
                   ("2" (apply-extensionality :hide? t) nil nil))
                  nil))
                nil))
              nil)
             ("2" (expand "surjective?")
              (("2" (skolem!)
                (("2" (typepred "y!1")
                  (("2" (name "nd" "ndiv(y!1, n!1)")
                    (("2" (typepred "ndiv(y!1, n!1)")
                      (("2" (inst + "(nd, rem(n!1)(y!1))")
                        (("1" (assert) nil nil)
                         ("2" (replace -3 :hide? t)
                          (("2"
                            (use "both_sides_times_pos_le1"
                                 ("x" "k!1" "y" "nd"))
                            (("2" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (skolem!)
          (("2" (typepred "y!1")
            (("2" (typepred "x!1")
              (("2" (case "x!1<=k!1-1")
                (("1" (use "both_sides_times_pos_le2" ("pz" "n!1"))
                  (("1" (assert) nil nil)) nil)
                 ("2" (assert) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((* const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (numfield nonempty-type-eq-decl nil number_fields nil)
      (n!1 skolem-const-decl "nat" lnat_th nil)
      (below type-eq-decl nil nat_types nil)
      (k!1 skolem-const-decl "nat" lnat_th nil)
      (< const-decl "bool" reals nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (>= const-decl "bool" reals nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (int nonempty-type-eq-decl nil integers nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields
       nil)
      (boolean nonempty-type-decl nil booleans nil)
      (number nonempty-type-decl nil numbers nil)
      (> const-decl "bool" reals nil)
      (mod nonempty-type-eq-decl nil euclidean_division nil)
      (posnat nonempty-type-eq-decl nil integers nil)
      (nonneg_int nonempty-type-eq-decl nil integers nil)
      (unique_quotient formula-decl nil euclidean_division nil)
      (injective? const-decl "bool" functions nil)
      (ndiv const-decl "{q: int | x = b * q + rem(b)(x)}"
       modulo_arithmetic nil)
      (rem const-decl "{r: mod(b) | EXISTS q: x = b * q + r}"
           modulo_arithmetic nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (y!1 skolem-const-decl "below[k!1 * n!1]" lnat_th nil)
      (nd skolem-const-decl "{q: int | y!1 = rem(n!1)(y!1) + n!1 * q}"
       lnat_th nil)
      (both_sides_times_pos_le1 formula-decl nil real_props nil)
      (nonneg_real nonempty-type-eq-decl nil real_types nil)
      (posreal nonempty-type-eq-decl nil real_types nil)
      (<= const-decl "bool" reals nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (surjective? const-decl "bool" functions nil)
      (bijective? const-decl "bool" functions nil)
      (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (both_sides_times_pos_le2 formula-decl nil real_props nil))
     3156 2770 nil nil))
   (nat_not_finite 0
    (nat_not_finite-1 nil 3355454976 3355455347
     ("" (expand "is_finite")
      (("" (skolem!)
        (("" (name "ss" "{i: nat | i < N!1+1}")
          (("" (case "EXISTS (f: [(ss) -> below[N!1+1]]): bijective?(f)")
            (("1" (skolem!)
              (("1" (case "card(ss) = N!1 + 1")
                (("1" (use "Card_injection" ("S" "ss" "n" "N!1"))
                  (("1" (ground)
                    (("1" (inst + "LAMBDA (x: (ss)): f!1(x)")
                      (("1" (expand "injective?")
                        (("1" (skosimp)
                          (("1" (inst - "x1!1" "x2!1")
                            (("1" (assert) nil nil)) nil))
                          nil))
                        nil)
                       ("2" (skosimp)
                        (("2" (expand "fullset") (("2" (propax) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (use "card_bij[nat]")
                  (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)
                 ("3" (expand "is_finite")
                  (("3" (inst + "N!1+1" "f!2")
                    (("3" (expand "bijective?") (("3" (flatten) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (inst + "LAMBDA (x: (ss)): x")
              (("1" (expand "bijective?")
                (("1" (expand "injective?")
                  (("1" (expand "surjective?")
                    (("1" (expand "ss")
                      (("1" (split +)
                        (("1" (skosimp) nil nil)
                         ("2" (skosimp)
                          (("2" (inst + "y!1")
                            (("2" (expand "ss") (("2" (assert) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (skolem!)
                (("2" (typepred "x!1")
                  (("2" (expand "ss") (("2" (propax) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((is_finite const-decl "bool" finite_sets nil)
      (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (numfield nonempty-type-eq-decl nil number_fields nil)
      (< const-decl "bool" reals nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (>= const-decl "bool" reals nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (int nonempty-type-eq-decl nil integers nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields
       nil)
      (boolean nonempty-type-decl nil booleans nil)
      (number nonempty-type-decl nil numbers nil)
      (N!1 skolem-const-decl "nat" lnat_th nil)
      (y!1 skolem-const-decl "below[N!1 + 1]" lnat_th nil)
      (surjective? const-decl "bool" functions nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (card_bij formula-decl nil finite_sets nil)
      (Card_injection formula-decl nil finite_sets nil)
      (ss skolem-const-decl "[nat -> bool]" lnat_th nil)
      (fullset const-decl "set" sets nil)
      (injective? const-decl "bool" functions nil)
      (set type-eq-decl nil sets nil)
      (finite_set type-eq-decl nil finite_sets nil)
      (Card const-decl "nat" finite_sets nil)
      (card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
      (below type-eq-decl nil nat_types nil)
      (bijective? const-decl "bool" functions nil))
     176018 1790 t nil)))
  (lcard_def
   (lcard_empty? 0
    (lcard_empty?-1 nil 3355454976 3355455393
     ("" (skolem!)
      (("" (expand "lcard")
        (("" (lift-if)
          (("" (ground)
            (("1" (use "card_empty?[T]")
              (("1" (iff)
                (("1" (prop)
                  (("1" (assert) nil nil)
                   ("2" (use "up_injective[nat]")
                    (("2" (assert) nil nil)) nil))
                  nil))
                nil))
              nil)
             ("2" (expand "is_finite")
              (("2" (inst + "1" "LAMBDA (x:(S!1)): 0")
                (("2" (expand "injective?")
                  (("2" (expand "empty?")
                    (("2" (expand "member")
                      (("2" (skolem!)
                        (("2" (inst?) (("2" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((lcard const-decl "lnat" lcard_def nil)
      (up_injective formula-decl nil moreLift nil)
      (number nonempty-type-decl nil numbers nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields
       nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (int nonempty-type-eq-decl nil integers nil)
      (>= const-decl "bool" reals nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
      (Card const-decl "nat" finite_sets nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (set type-eq-decl nil sets nil)
      (is_finite const-decl "bool" finite_sets nil)
      (finite_set type-eq-decl nil finite_sets nil)
      (pred type-eq-decl nil defined_types nil)
      (T formal-type-decl nil lcard_def nil)
      (card_empty? formula-decl nil finite_sets nil)
      (< const-decl "bool" reals nil)
      (below type-eq-decl nil nat_types nil)
      (empty? const-decl "bool" sets nil)
      (member const-decl "bool" sets nil)
      (injective? const-decl "bool" functions nil))
     285 170 nil nil))
   (lcard_one 0
    (lcard_one-1 nil 3355454976 3355455394
     ("" (skolem!)
      (("" (expand "lcard")
        (("" (lift-if)
          (("" (split)
            (("1" (flatten)
              (("1" (use "card_one[T]")
                (("1" (prop)
                  (("1" (assert) nil nil)
                   ("2" (use "up_injective[nat]")
                    (("2" (assert) nil nil)) nil))
                  nil))
                nil))
              nil)
             ("2" (flatten)
              (("2" (expand "singleton")
                (("2" (expand "is_finite")
                  (("2" (inst 1 "1" "LAMBDA (x:T): 0")
                    (("1" (expand "restrict")
                      (("1" (expand "injective?")
                        (("1" (skolem!)
                          (("1" (skolem!)
                            (("1" (typepred "x1!1")
                              (("1" (typepred "x2!1")
                                (("1"
                                  (replace -3)
                                  (("1" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (grind) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((lcard const-decl "lnat" lcard_def nil)
      (card_one formula-decl nil finite_sets nil)
      (T formal-type-decl nil lcard_def nil)
      (pred type-eq-decl nil defined_types nil)
      (finite_set type-eq-decl nil finite_sets nil)
      (is_finite const-decl "bool" finite_sets nil)
      (set type-eq-decl nil sets nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (up_injective formula-decl nil moreLift nil)
      (number nonempty-type-decl nil numbers nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields
       nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (int nonempty-type-eq-decl nil integers nil)
      (>= const-decl "bool" reals nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
      (Card const-decl "nat" finite_sets nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (singleton const-decl "(singleton?)" sets nil)
      (< const-decl "bool" reals nil)
      (below type-eq-decl nil nat_types nil)
      (restrict const-decl "R" restrict nil)
      (injective? const-decl "bool" functions nil)
      (NOT const-decl "[bool -> bool]" booleans nil))
     291 170 nil nil))
   (lcard_subset 0
    (lcard_subset-1 nil 3355454976 3355455394
     ("" (skosimp)
      (("" (case "is_finite(B!1)")
        (("1" (use "finite_subset[T]")
          (("1" (assert)
            (("1" (use "card_subset[T]")
              (("1" (assert)
                (("1" (expand "lcard")
                  (("1" (assert)
                    (("1" (expand "<=") (("1" (propax) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (expand "lcard")
          (("2" (assert)
            (("2" (lift-if)
              (("2" (expand "<=") (("2" (propax) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((pred type-eq-decl nil defined_types nil)
      (is_finite const-decl "bool" finite_sets nil)
      (set type-eq-decl nil sets nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (T formal-type-decl nil lcard_def nil)
      (<= const-decl "bool" reals nil) (<= const-decl "bool" lnat_th nil)
      (lcard const-decl "lnat" lcard_def nil)
      (card_subset formula-decl nil finite_sets nil)
      (B!1 skolem-const-decl "pred[T]" lcard_def nil)
      (finite_set type-eq-decl nil finite_sets nil)
      (finite_subset formula-decl nil finite_sets nil))
     191 140 t nil))
   (lcard_disj_union 0
    (lcard_disj_union-1 nil 3355454976 3355455395
     ("" (skosimp)
      (("" (case "is_finite(A!1)")
        (("1" (case "is_finite(B!1)")
          (("1" (expand "lcard")
            (("1" (assert)
              (("1" (use "card_disj_union[T]")
                (("1" (assert)
                  (("1" (lift-if)
                    (("1" (assert)
                      (("1" (prop)
                        (("1" (use "finite_union[T]")
                          (("1" (expand "+ ") (("1" (assert) nil nil))
                            nil))
                          nil)
                         ("2" (use "finite_union[T]") nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (expand "lcard")
            (("2" (assert)
              (("2" (lift-if)
                (("2"
                  (use "finite_subset" ("s" "B!1" "A" "union(A!1, B!1)"))
                  (("1" (assert)
                    (("1" (hide-all-but 1) (("1" (grind) nil nil)) nil))
                    nil)
                   ("2" (assert)
                    (("2" (expand "+ ") (("2" (propax) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (expand "lcard")
          (("2" (assert)
            (("2" (lift-if)
              (("2" (prop)
                (("1"
                  (use "finite_subset" ("s" "A!1" "A" "union(A!1, B!1)"))
                  (("1" (assert)
                    (("1" (hide-all-but 1) (("1" (grind) nil nil)) nil))
                    nil))
                  nil)
                 ("2" (expand "+ ") (("2" (propax) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((pred type-eq-decl nil defined_types nil)
      (is_finite const-decl "bool" finite_sets nil)
      (set type-eq-decl nil sets nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (T formal-type-decl nil lcard_def nil)
      (member const-decl "bool" sets nil)
      (subset? const-decl "bool" sets nil)
      (union const-decl "set" sets nil)
      (finite_subset formula-decl nil finite_sets nil)
      (lcard const-decl "lnat" lcard_def nil)
      (card_disj_union formula-decl nil finite_sets nil)
      (finite_set type-eq-decl nil finite_sets nil)
      (+ const-decl "lnat" lnat_th nil)
      (finite_union judgement-tcc nil finite_sets nil))
     1041 730 nil nil))
   (lcard_add_TCC1 0
    (lcard_add_TCC1-1 nil 3355454976 3355455395 ("" (grind) nil nil)
     proved ((every adt-def-decl "boolean" lift_adt nil)) 34 30 nil nil))
   (lcard_add 0
    (lcard_add-1 nil 3355454976 3355455396
     ("" (skolem!)
      (("" (case "is_finite(S!1)")
        (("1" (expand "lcard")
          (("1" (assert)
            (("1" (lift-if)
              (("1" (prop)
                (("1" (lift-if)
                  (("1" (assert)
                    (("1" (use "card_add[T]")
                      (("1" (lift-if)
                        (("1" (prop)
                          (("1" (assert)
                            (("1" (replace -3)
                              (("1"
                                (use "plus_zero1" ("x" "up(card(S!1))"))
                                (("1" (assert) nil nil)) nil))
                              nil))
                            nil)
                           ("2" (assert)
                            (("2" (replace -1)
                              (("2" (expand "+ ")
                                (("2" (propax) nil nil)) nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (use "finite_add" ("A" "S!1")) nil nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (expand "lcard")
          (("2" (assert)
            (("2" (case "is_finite(add(x!1, S!1))")
              (("1" (assert)
                (("1"
                  (use "finite_subset" ("s" "S!1" "A" "add(x!1, S!1)"))
                  (("1" (assert)
                    (("1" (hide-all-but 1) (("1" (grind) nil nil)) nil))
                    nil))
                  nil))
                nil)
               ("2" (assert)
                (("2"
                  (name-replace "aa" "IF S!1(x!1) THEN 0 ELSE 1 ENDIF")
                  (("2" (hide 1 2)
                    (("2" (expand "+ ") (("2" (propax) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((pred type-eq-decl nil defined_types nil)
      (is_finite const-decl "bool" finite_sets nil)
      (set type-eq-decl nil sets nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (T formal-type-decl nil lcard_def nil)
      (+ const-decl "lnat" lnat_th nil)
      (plus_zero1 formula-decl nil lnat_th nil)
      (number nonempty-type-decl nil numbers nil)
      (lift type-decl nil lift_adt nil)
      (PRED type-eq-decl nil defined_types nil)
      (every adt-def-decl "boolean" lift_adt nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields
       nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (>= const-decl "bool" reals nil)
      (lnat type-eq-decl nil lnat_th nil)
      (int nonempty-type-eq-decl nil integers nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (Card const-decl "nat" finite_sets nil)
      (up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
      (up adt-constructor-decl "[T -> (up?)]" lift_adt nil)
      (card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
      (finite_set type-eq-decl nil finite_sets nil)
      (card_add formula-decl nil finite_sets nil)
      (finite_add formula-decl nil finite_sets nil)
      (lcard const-decl "lnat" lcard_def nil)
      (naturalnumber type-eq-decl nil naturalnumbers nil)
      (IF const-decl "[boolean, T, T -> T]" if_def nil)
      (member const-decl "bool" sets nil)
      (subset? const-decl "bool" sets nil)
      (finite_subset formula-decl nil finite_sets nil)
      (nonempty? const-decl "bool" sets nil)
      (add const-decl "(nonempty?)" sets nil))
     900 670 nil nil))
   (lcard_union 0
    (lcard_union-1 nil 3355454976 3355455398
     ("" (skolem!)
      (("" (expand "lcard")
        (("" (case "is_finite(A!1)")
          (("1" (case "is_finite(B!1)")
            (("1" (assert)
              (("1" (case "is_finite(union(A!1, B!1))")
                (("1" (case "is_finite(intersection(A!1, B!1))")
                  (("1" (assert)
                    (("1" (use "card_union[T]")
                      (("1" (assert)
                        (("1" (expand "+ ") (("1" (assert) nil nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (hide -1 -2 2)
                    (("2"
                      (use "finite_subset"
                           ("s" "intersection(A!1, B!1)" "A" "A!1"))
                      (("2" (assert)
                        (("2" (hide -1 2) (("2" (grind) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (hide 2) (("2" (use "finite_union[T]") nil nil))
                  nil))
                nil))
              nil)
             ("2" (assert)
              (("2" (case "is_finite(union(A!1, B!1))")
                (("1" (hide -2 2)
                  (("1"
                    (use "finite_subset"
                         ("s" "B!1" "A" "union(A!1, B!1)"))
                    (("1" (assert)
                      (("1" (hide -1 2) (("1" (grind) nil nil)) nil))
                      nil))
                    nil))
                  nil)
                 ("2" (assert)
                  (("2" (hide -1 1 2)
                    (("2"
                      (expand "+
  ")
                      (("2" (propax) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (assert)
            (("2" (case "is_finite(union(A!1, B!1))")
              (("1" (hide 2)
                (("1"
                  (use "finite_subset" ("s" "A!1" "A" "union(A!1, B!1)"))
                  (("1" (assert)
                    (("1" (hide -1 2) (("1" (grind) nil nil)) nil)) nil))
                  nil))
                nil)
               ("2" (assert)
                (("2"
                  (expand "+
  ")
                  (("2" (propax) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((lcard const-decl "lnat" lcard_def nil)
      (union const-decl "set" sets nil)
      (member const-decl "bool" sets nil)
      (subset? const-decl "bool" sets nil)
      (finite_subset formula-decl nil finite_sets nil)
      (+ const-decl "lnat" lnat_th nil)
      (finite_set type-eq-decl nil finite_sets nil)
      (card_union formula-decl nil finite_sets nil)
      (intersection const-decl "set" sets nil)
      (finite_union judgement-tcc nil finite_sets nil)
      (T formal-type-decl nil lcard_def nil)
      (boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (set type-eq-decl nil sets nil)
      (is_finite const-decl "bool" finite_sets nil)
      (pred type-eq-decl nil defined_types nil))
     1579 1330 nil nil))
   (lcard_bij 0
    (lcard_bij-1 nil 3355454976 3355455398
     ("" (skolem!)
      (("" (expand "lcard")
        (("" (lift-if)
          (("" (use "card_bij[T]")
            (("1" (prop)
              (("1" (expand "is_finite")
                (("1" (expand "bijective?")
                  (("1" (skosimp) (("1" (assert) nil nil)) nil)) nil))
                nil)
               ("2" (assert)
                (("2" (expand "is_finite")
                  (("2" (hide -2 -3 1)
                    (("2" (skolem!)
                      (("2" (expand "bijective?")
                        (("2" (flatten) (("2" (inst?) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("3" (use "up_injective[nat]") (("3" (assert) nil nil))
                nil)
               ("4" (assert) nil nil))
              nil)
             ("2" (assert)
              (("2" (expand "bijective?")
                (("2" (skosimp)
                  (("2" (expand "is_finite") (("2" (inst?) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((lcard const-decl "lnat" lcard_def nil)
      (card_bij formula-decl nil finite_sets nil)
      (T formal-type-decl nil lcard_def nil)
      (finite_set type-eq-decl nil finite_sets nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (>= const-decl "bool" reals nil)
      (int nonempty-type-eq-decl nil integers nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields
       nil)
      (number nonempty-type-decl nil numbers nil)
      (boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (set type-eq-decl nil sets nil)
      (is_finite const-decl "bool" finite_sets nil)
      (pred type-eq-decl nil defined_types nil)
      (S!1 skolem-const-decl "pred[T]" lcard_def nil)
      (up_injective formula-decl nil moreLift nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (Card const-decl "nat" finite_sets nil)
      (card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
      (< const-decl "bool" reals nil)
      (below type-eq-decl nil nat_types nil)
      (bijective? const-decl "bool" functions nil))
     266 170 nil nil)))
  (lcard_th2
   (injective_lcard 0
    (injective_lcard-1 nil 3355454976 3355464980
     ("" (skosimp)
      (("" (skolem!)
        (("" (expand "lcard")
          (("" (lift-if)
            (("" (lift-if)
              (("" (expand "<=")
                (("" (case "is_finite(B!1)")
                  (("1" (assert)
                    (("1" (name "N" "card(B!1)")
                      (("1" (use "card_bij" ("S" "B!1"))
                        (("1" (assert)
                          (("1" (skolem!)
                            (("1" (case "injective?(f!2 o f!1)")
                              (("1" (case "is_finite(A!1)")
                                (("1"
                                  (assert)
                                  (("1"
                                    (use "Card_injection" ("S" "A!1"))
                                    (("1"
                                      (assert)
                                      (("1"
                                        (inst? +)
                                        (("1"
                                          (hide-all-but (-2 1))
                                          (("1"
                                            (expand "injective?")
                                            (("1" (propax) nil nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (skosimp)
                                          (("2"
                                            (expand "o")
                                            (("2" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (expand "is_finite")
                                  (("2" (inst? +) nil nil))
                                  nil))
                                nil)
                               ("2" (hide 2 -2 -3)
                                (("2" (grind) nil nil)) nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((<= const-decl "bool" lnat_th nil)
      (card_bij formula-decl nil finite_sets nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bijective? const-decl "bool" functions nil)
      (surjective? const-decl "bool" functions nil)
      (Card_injection formula-decl nil finite_sets nil)
      (f!1 skolem-const-decl "[(A!1) -> (B!1)]" lcard_th2 nil)
      (f!2 skolem-const-decl "[(B!1) -> below[N]]" lcard_th2 nil)
      (N skolem-const-decl "{n: nat | n = Card[U](B!1)}" lcard_th2 nil)
      (B!1 skolem-const-decl "pred[U]" lcard_th2 nil)
      (A!1 skolem-const-decl "pred[T]" lcard_th2 nil)
      (T formal-type-decl nil lcard_th2 nil)
      (< const-decl "bool" reals nil)
      (below type-eq-decl nil nat_types nil)
      (injective? const-decl "bool" functions nil)
      (O const-decl "T3" function_props nil)
      (number nonempty-type-decl nil numbers nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (finite_set type-eq-decl nil finite_sets nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields
       nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (int nonempty-type-eq-decl nil integers nil)
      (>= const-decl "bool" reals nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (Card const-decl "nat" finite_sets nil)
      (card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
      (U formal-type-decl nil lcard_th2 nil)
      (boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (set type-eq-decl nil sets nil)
      (is_finite const-decl "bool" finite_sets nil)
      (pred type-eq-decl nil defined_types nil)
      (lcard const-decl "lnat" lcard_def nil))
     788 530 t nil))
   (surjective_injective 0
    (surjective_injective-1 nil 3355454976 3355464980
     ("" (skosimp)
      ((""
        (name "gg" "LAMBDA (b: (B!1)): epsilon({a: (A!1) | f!1(a) = b})")
        (("1" (inst + "gg")
          (("1" (apply-extensionality :hide? t)
            (("1" (expand "id")
              (("1" (expand "o ")
                (("1" (name "gx" "gg(x!1)")
                  (("1" (replace -1)
                    (("1" (expand "gg")
                      (("1" (hide -2)
                        (("1"
                          (use "epsilon_ax"
                               ("p" "{a: (A!1) | f!1(a) = x!1}"))
                          (("1" (split)
                            (("1" (assert) nil nil)
                             ("2" (hide -1 2) (("2" (grind) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (hide 2) (("2" (grind) nil nil)) nil))
        nil))
      nil)
     proved
     ((epsilon const-decl "T" epsilons nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (T formal-type-decl nil lcard_th2 nil)
      (pred type-eq-decl nil defined_types nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (U formal-type-decl nil lcard_th2 nil)
      (TRUE const-decl "bool" booleans nil)
      (id const-decl "(bijective?[T, T])" identity nil)
      (bijective? const-decl "bool" functions nil)
      (O const-decl "T3" function_props nil)
      (surjective? const-decl "bool" functions nil)
      (epsilon_ax formula-decl nil epsilons nil)
      (gg skolem-const-decl "[(B!1) -> (A!1)]" lcard_th2 nil)
      (NOT const-decl "[bool -> bool]" booleans nil))
     278 140 nil nil))
   (lcard_Cartesian 0
    (lcard_Cartesian-1 nil 3355454976 3355464983
     ("" (skosimp)
      (("" (use "lcard_empty?" ("S" "A!1"))
        (("" (use "lcard_empty?" ("S" "B!1"))
          ((""
            (use "lcard_empty?"
                 ("S" "{x: [T, U] | A!1(x`1) AND B!1(x`2)}"))
            (("" (case "empty?(A!1) OR empty?(B!1)")
              (("1" (case "empty?({x: [T, U] | A!1(x`1) AND B!1(x`2)})")
                (("1" (split)
                  (("1" (assert)
                    (("1" (replace* -3 -5)
                      (("1" (expand "*") (("1" (propax) nil nil)) nil))
                      nil))
                    nil)
                   ("2" (assert)
                    (("2" (replace* -3 -4)
                      (("2" (expand "*") (("2" (propax) nil nil)) nil))
                      nil))
                    nil))
                  nil)
                 ("2" (hide -2 -3 -4 2) (("2" (grind) nil nil)) nil))
                nil)
               ("2" (flatten)
                (("2" (assert)
                  (("2" (hide -)
                    (("2" (case "is_finite(A!1) AND is_finite(B!1)")
                      (("1" (flatten)
                        (("1" (name "nA" "card(A!1)")
                          (("1" (name "nB" "card(B!1)")
                            (("1" (use "card_bij" ("S" "A!1"))
                              (("1" (use "card_bij" ("S" "B!1"))
                                (("1"
                                  (assert)
                                  (("1"
                                    (skolem! -2)
                                    (("1"
                                      (skolem!)
                                      (("1"
                                        (name
                                         "AB"
                                         "{x: [T, U] | A!1(x`1) AND B!1(x`2)}")
                                        (("1"
                                          (name
                                           "ff"
                                           "LAMBDA (x: (AB)): (f!1(x`1), f!2(x`
 2))")
                                          (("1"
                                            (case
                                             "bijective?[(AB), [below(nA), belo
 w(nB)]](ff)")
                                            (("1"
                                              (use
                                               "scanning_rectangle"
                                               ("k" "nA" "n" "nB"))
                                              (("1"
                                                (skolem!)
                                                (("1"
                                                  (name
                                                   "hf"
                                                   "o[(AB), [below(nA), below(n
 B)], below[nA*nB]] (h!1, ff)")
                                                  (("1"
                                                    (use
                                                     "composition_bijective[(AB
 ), [below(nA), below(nB)], below[nA * nB]]")
                                                    (("1"
                                                      (replace -2)
                                                      (("1"
                                                        (case
                                                         "is_finite(AB)")
                                                        (("1"
                                                          (use
                                                           "card_bij"
                                                           ("S"
                                                            "AB"
                                                            "N"
                                                            "nA*nB"))
                                                          (("1"
                                                            (expand
                                                             "lcard")
                                                            (("1"
                                                              (assert)
                                                              (("1"
                                                                (replace*
                                                                 -11
                                                                 -12
                                                                 -8)
                                                                (("1"
                                                                  (expand
                                                                   "*")
                                                                  (("1"
                                                                    (prop)
                                                                    (("1"
                                                                      (assert)
                                                                      nil
                                                                      nil)
                                                                     ("2"
                                                                      (inst?)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (expand
                                                           "is_finite")
                                                          (("2"
                                                            (expand
                                                             "bijective?")
                                                            (("2"
                                                              (flatten)
                                                              (("2"
                                                                (inst?)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (hide
                                               -5
                                               -6
                                               -7
                                               -8
                                               2
                                               3
                                               4
                                               5
                                               6)
                                              (("2"
                                                (expand "bijective?")
                                                (("2"
                                                  (flatten)
                                                  (("2"
                                                    (split)
                                                    (("1"
                                                      (expand
                                                       "injective?")
                                                      (("1"
                                                        (skosimp)
                                                        (("1"
                                                          (expand "ff")
                                                          (("1"
                                                            (flatten)
                                                            (("1"
                                                              (typepred
                                                               "x1!1")
                                                              (("1"
                                                                (typepred
                                                                 "x2!1")
                                                                (("1"
                                                                  (expand
                                                                   "AB")
                                                                  (("1"
                                                                    (flatten)
                                                                    (("1"
                                                                      (inst?)
                                                                      (("1"
                                                                        (inst?)
                                                                        (("1"
                                                                          (asse
 rt)
                                                                          (("1"
                                                                            (ap
 ply-extensionality
                                                                             :h
 ide?
                                                                             t)
                                                                            nil
                                                                            nil
 ))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (expand
                                                       "surjective?")
                                                      (("2"
                                                        (skolem!)
                                                        (("2"
                                                          (inst
                                                           -4
                                                           "y!1`2")
                                                          (("2"
                                                            (inst
                                                             -6
                                                             "y!1`1")
                                                            (("2"
                                                              (skolem!)
                                                              (("2"
                                                                (skolem!)
                                                                (("2"
                                                                  (inst
                                                                   +
                                                                   "(x!2, x!1)"
 )
                                                                  (("1"
                                                                    (expand
                                                                     "ff")
                                                                    (("1"
                                                                      (apply-ex
 tensionality
                                                                       :hide?
                                                                       t)
                                                                      nil
                                                                      nil))
                                                                    nil)
                                                                   ("2"
                                                                    (expand
                                                                     "AB")
                                                                    (("2"
                                                                      (propax)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (skolem!)
                                            (("2"
                                              (typepred "x!1")
                                              (("2"
                                                (expand "AB")
                                                (("2" (flatten) nil nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("3"
                                            (skolem!)
                                            (("3"
                                              (typepred "x!1")
                                              (("3"
                                                (expand "AB")
                                                (("3" (flatten) nil nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (propax) nil nil))
                            nil)
                           ("2" (propax) nil nil))
                          nil))
                        nil)
                       ("2"
                        (name "AB" "{x: [T, U] | A!1(x`1) AND B!1(x`2)}")
                        (("2" (replace -1)
                          (("2" (case "is_finite(AB)")
                            (("1" (expand "is_finite" -)
                              (("1" (hide 4 5 6)
                                (("1"
                                  (expand "empty?")
                                  (("1"
                                    (expand "member")
                                    (("1"
                                      (skosimp)
                                      (("1"
                                        (skosimp)
                                        (("1"
                                          (skosimp)
                                          (("1"
                                            (expand "is_finite")
                                            (("1"
                                              (split)
                                              (("1"
                                                (inst
                                                 +
                                                 "N!1"
                                                 "LAMBDA (a: (A!1)): f!1(a, x!2
 )")
                                                (("1"
                                                  (expand "injective?")
                                                  (("1"
                                                    (skosimp)
                                                    (("1"
                                                      (inst
                                                       -
                                                       "(x1!1, x!2)"
                                                       "(x2!1, x!2)")
                                                      (("1"
                                                        (assert)
                                                        nil
                                                        nil)
                                                       ("2"
                                                        (expand "AB")
                                                        (("2"
                                                          (propax)
                                                          nil
                                                          nil))
                                                        nil)
                                                       ("3"
                                                        (expand "AB")
                                                        (("3"
                                                          (propax)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (expand "AB")
                                                  (("2"
                                                    (assert)
                                                    (("2"
                                                      (skolem!)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (inst
                                                 +
                                                 "N!1"
                                                 "LAMBDA (b: (B!1)): f!1(x!1, b
 )")
                                                (("1"
                                                  (expand "injective?")
                                                  (("1"
                                                    (skosimp)
                                                    (("1"
                                                      (inst
                                                       -
                                                       "(x!1, x1!1)"
                                                       "(x!1, x2!1)")
                                                      (("1"
                                                        (assert)
                                                        nil
                                                        nil)
                                                       ("2"
                                                        (expand "AB")
                                                        (("2"
                                                          (propax)
                                                          nil
                                                          nil))
                                                        nil)
                                                       ("3"
                                                        (expand "AB")
                                                        (("3"
                                                          (propax)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (skolem!)
                                                  (("2"
                                                    (expand "AB")
                                                    (("2"
                                                      (propax)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (expand "*")
                              (("2" (expand "lcard")
                                (("2" (ground) nil nil)) nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((lcard_empty? formula-decl nil lcard_def nil)
      (T formal-type-decl nil lcard_th2 nil)
      (boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (pred type-eq-decl nil defined_types nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (x!1 skolem-const-decl "T" lcard_th2 nil)
      (AB skolem-const-decl "[[T, U] -> boolean]" lcard_th2 nil)
      (x!2 skolem-const-decl "U" lcard_th2 nil)
      (below type-eq-decl nil naturalnumbers nil)
      (bijective? const-decl "bool" functions nil)
      (composition_bijective judgement-tcc nil function_props nil)
      (h!1 skolem-const-decl "[[below[nA], below[nB]] -> below[nA * nB]]"
       lcard_th2 nil)
      (ff skolem-const-decl "[(AB) -> [below[nA], below[nB]]]" lcard_th2
       nil)
      (nB skolem-const-decl "{n: nat | n = Card[U](B!1)}" lcard_th2 nil)
      (B!1 skolem-const-decl "pred[U]" lcard_th2 nil)
      (nA skolem-const-decl "{n: nat | n = Card[T](A!1)}" lcard_th2 nil)
      (A!1 skolem-const-decl "pred[T]" lcard_th2 nil)
      (AB skolem-const-decl "[[T, U] -> boolean]" lcard_th2 nil)
      (lcard const-decl "lnat" lcard_def nil)
      (O const-decl "T3" function_props nil)
      (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (numfield nonempty-type-eq-decl nil number_fields nil)
      (scanning_rectangle formula-decl nil lnat_th nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (injective? const-decl "bool" functions nil)
      (x!1 skolem-const-decl "(B!1)" lcard_th2 nil)
      (x!2 skolem-const-decl "(A!1)" lcard_th2 nil)
      (surjective? const-decl "bool" functions nil)
      (below type-eq-decl nil nat_types nil)
      (< const-decl "bool" reals nil)
      (card_bij formula-decl nil finite_sets nil)
      (number nonempty-type-decl nil numbers nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (finite_set type-eq-decl nil finite_sets nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields
       nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (int nonempty-type-eq-decl nil integers nil)
      (>= const-decl "bool" reals nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (Card const-decl "nat" finite_sets nil)
      (card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
      (is_finite const-decl "bool" finite_sets nil)
      (* const-decl "lnat" lnat_th nil)
      (member const-decl "bool" sets nil)
      (OR const-decl "[bool, bool -> bool]" booleans nil)
      (set type-eq-decl nil sets nil) (empty? const-decl "bool" sets nil)
      (U formal-type-decl nil lcard_th2 nil))
     2425 1700 nil nil)))
  (lcard_th4
   (surjective_lcard 0
    (surjective_lcard-3 nil 3355464542 3355465015
     ("" (skosimp)
      (("" (skolem!)
        (("" (use "surjective_injective[T, U]")
          (("" (assert)
            (("" (skolem!)
              (("" (case "injective? (g!1)")
                (("1" (use "injective_lcard[U,T]")
                  (("1" (assert) (("1" (inst?) nil nil)) nil)) nil)
                 ("2" (hide 2)
                  (("2" (expand "injective?")
                    (("2" (skosimp)
                      (("2"
                        (case "(f!1 o g!1)(x1!1) = (f!1 o g!1)(x2!1)")
                        (("1" (replace -3)
                          (("1" (expand "id") (("1" (propax) nil nil))
                            nil))
                          nil)
                         ("2" (expand "o ") (("2" (assert) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((injective? const-decl "bool" functions nil)
      (injective_lcard formula-decl nil lcard_th2 nil)
      (O const-decl "T3" function_props nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (id const-decl "(bijective?[T, T])" identity nil)
      (boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (pred type-eq-decl nil defined_types nil)
      (U formal-type-decl nil lcard_th4 nil)
      (T formal-type-decl nil lcard_th4 nil)
      (surjective_injective formula-decl nil lcard_th2 nil))
     184 110 t nil)
    (surjective_lcard-2 nil 3355464389 3355464444
     ("" (skosimp)
      (("" (skosimp)
        (("" (skolem!)
          (("" (use "surjective_injective")
            (("" (assert)
              (("" (skolem!)
                (("" (case "injective? (g!1)")
                  (("1" (postpone) nil)
                   ("2" (hide 2)
                    (("2" (expand "injective?")
                      (("2" (skosimp)
                        (("2"
                          (case "(f!1 o g!1)(x1!1) = (f!1 o g!1)(x2!1)")
                          (("1" (replace -3)
                            (("1" (expand "id") (("1" (propax) nil)))))
                           ("2" (expand "o ")
                            (("2" (assert) nil))))))))))))))))))))))))
      nil)
     unfinished nil 45532 380 t nil)
    (surjective_lcard-1 nil 3355464339 3355464351
     ("" (skosimp) (("" (postpone) nil nil)) nil) unfinished nil 11882
     160 t shostak))
   (bijective_lcard 0
    (bijective_lcard-2 nil 3355464861 3355465015
     ("" (skosimp)
      (("" (skolem!)
        (("" (expand "bijective?")
          (("" (flatten)
            (("" (use "injective_lcard[T, U]")
              (("" (use "surjective_lcard")
                (("" (prop)
                  (("1" (use "leq_antisymmetric") (("1" (assert) nil)))
                   ("2" (inst?) nil) ("3" (inst?) nil)
                   ("4" (inst?) nil))))))))))))))
      nil)
     proved
     ((surjective_lcard formula-decl nil lcard_th4 nil)
      (leq_antisymmetric formula-decl nil lnat_th nil)
      (lcard const-decl "lnat" lcard_def nil)
      (lnat type-eq-decl nil lnat_th nil)
      (>= const-decl "bool" reals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields
       nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (every adt-def-decl "boolean" lift_adt nil)
      (PRED type-eq-decl nil defined_types nil)
      (lift type-decl nil lift_adt nil)
      (number nonempty-type-decl nil numbers nil)
      (boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (pred type-eq-decl nil defined_types nil)
      (U formal-type-decl nil lcard_th4 nil)
      (T formal-type-decl nil lcard_th4 nil)
      (injective_lcard formula-decl nil lcard_th2 nil)
      (bijective? const-decl "bool" functions nil))
     139 90 nil nil)
    (bijective_lcard-1 nil 3355464666 3355464770
     ("" (skosimp)
      (("" (skolem!)
        (("" (expand "bijective?")
          (("" (flatten)
            (("" (use "injective_lcard")
              (("" (use "surjective_lcard")
                (("" (prop)
                  (("1" (use "leq_antisymmetric") (("1" (assert) nil)))
                   ("2" (inst?) nil) ("3" (inst?) nil)
                   ("4" (inst?) nil))))))))))))))
      nil)
     unfinished nil 65197 230 t nil)))
  (lcard_th3
   (gg_TCC1 0
    (gg_TCC1-1 nil 3355454976 3355465027 ("" (skosimp*) nil nil) proved
     nil 13 20 nil nil))
   (infty_gg_injective 0
    (infty_gg_injective-1 nil 3355454976 3355466762
     ("" (skosimp)
      (("" (case "empty?(S!1)")
        (("1" (use "lcard_empty?[T]")
          (("1" (assert) (("1" (assert) nil nil)) nil)) nil)
         ("2" (name "ud" "epsilon(S!1)")
          (("2" (replace -1)
            (("2" (expand "injective?")
              (("2" (expand "inrange?")
                (("2"
                  (case "FORALL (n: nat):
  (FORALL (x1: nat), (x2: nat): x1 < x2 AND x2 < n IMPLIES
           (gg(S!1, ud)(x1) = gg(S!1, ud)(x2) => (x1 = x2)))
         AND (FORALL i: i < n IMPLIES S!1(gg(S!1, ud)(i)))")
                  (("1" (hide-all-but (-1 2))
                    (("1" (split)
                      (("1" (skosimp)
                        (("1" (case "x1!1 < x2!1")
                          (("1" (inst - "x2!1+1")
                            (("1" (flatten)
                              (("1" (inst?) (("1" (assert) nil nil))
                                nil))
                              nil))
                            nil)
                           ("2" (inst - "x1!1+1")
                            (("2" (flatten)
                              (("2" (inst - "x2!1" "x1!1")
                                (("2" (assert) nil nil)) nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (skolem!)
                        (("2" (inst - "i!1+1")
                          (("2" (flatten)
                            (("2" (inst? -2) (("2" (assert) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (hide 3)
                    (("2" (induct "n")
                      (("1" (skosimp) (("1" (assert) nil nil)) nil)
                       ("2" (skosimp) (("2" (assert) nil nil)) nil)
                       ("3" (skosimp)
                        (("3"
                          (case "S!1(gg(S!1, ud)(j!1)) AND FORALL (x1: nat):
           x1 < j!1 IMPLIES
            (gg(S!1, ud)(x1) = gg(S!1, ud)(j!1) => (x1 = j!1))")
                          (("1" (flatten)
                            (("1" (split)
                              (("1" (skosimp)
                                (("1"
                                  (inst? -6)
                                  (("1"
                                    (assert)
                                    (("1"
                                      (inst?)
                                      (("1" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2" (skosimp)
                                (("2"
                                  (inst? -5)
                                  (("2" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (hide 2)
                            (("2" (name "choice" "gg(S!1, ud)(j!1)")
                              (("2" (replace -1)
                                (("2"
                                  (expand "gg" -1)
                                  (("2"
                                    (use
                                     "epsilon_ax"
                                     ("p"
                                      "{x |
                   S!1(x) AND
                    (FORALL i: i < j!1 IMPLIES x /= gg(S!1, ud)(i))}"))
                                    (("2"
                                      (replace -2)
                                      (("2"
                                        (split -1)
                                        (("1"
                                          (flatten)
                                          (("1"
                                            (assert)
                                            (("1"
                                              (skosimp)
                                              (("1"
                                                (inst? -2)
                                                (("1" (assert) nil nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (hide -1 -4 2)
                                          (("2"
                                            (case
                                             "EXISTS (f: [({i: nat | i < j!1}) 
 -> (S!1)]): bijective?(f)")
                                            (("1"
                                              (hide -2 -3 1 2)
                                              (("1"
                                                (expand "lcard")
                                                (("1"
                                                  (lift-if)
                                                  (("1"
                                                    (ground)
                                                    (("1"
                                                      (skolem!)
                                                      (("1"
                                                        (expand
                                                         "bijective?")
                                                        (("1"
                                                          (flatten)
                                                          (("1"
                                                            (use
                                                             "surjective_inject
 ive"
                                                             ("A"
                                                              "{i: nat | i < j!
 1}"
                                                              "B"
                                                              "S!1"
                                                              "f"
                                                              "f!1"))
                                                            (("1"
                                                              (assert)
                                                              (("1"
                                                                (skolem!)
                                                                (("1"
                                                                  (expand
                                                                   "is_finite")
                                                                  (("1"
                                                                    (inst?)
                                                                    (("1"
                                                                      (expand
                                                                       "injecti
 ve?")
                                                                      (("1"
                                                                        (skosim
 p)
                                                                        (("1"
                                                                          (case
                                                                           "(f!
 1 o g!1)(x1!1) = (f!1 o g!1)(x2!1)")
                                                                          (("1"
                                                                            (re
 place
  
                                                                             -2
 )
                                                                            (("
 1"
                                                                              (
 expand
                                                                               
 "id")
                                                                              (
 ("1"
                                                                               
  (propax)
                                                                               
  nil
                                                                               
  nil))
                                                                              n
 il))
                                                                            nil
 )
                                                                           ("2"
                                                                            (ex
 pand
                                                                             "o
  ")
                                                                            (("
 2"
                                                                              (
 assert)
                                                                              n
 il
                                                                              n
 il))
                                                                            nil
 ))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (postpone)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (inst
                                               +
                                               "LAMBDA (i: ({i: nat | i < j!1})
 ): gg(S!1, ud)(i)")
                                              (("1"
                                                (expand "bijective?")
                                                (("1"
                                                  (split)
                                                  (("1"
                                                    (expand "injective?")
                                                    (("1"
                                                      (skosimp)
                                                      (("1"
                                                        (case
                                                         "x1!1 <x2!1")
                                                        (("1"
                                                          (inst? -)
                                                          (("1"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (inst
                                                           -2
                                                           "x2!1"
                                                           "x1!1")
                                                          (("2"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (expand
                                                     "surjective?")
                                                    (("2"
                                                      (skolem!)
                                                      (("2"
                                                        (typepred "y!1")
                                                        (("2"
                                                          (inst? 2)
                                                          (("2"
                                                            (assert)
                                                            (("2"
                                                              (skosimp)
                                                              (("2"
                                                                (inst? +)
                                                                (("2"
                                                                  (assert)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (skolem!)
                                                (("2"
                                                  (inst? -2)
                                                  (("2"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     unfinished nil 1713903 6340 t nil))
   (infty_lcard 0
    (infty_lcard-1 nil 3355454976 3355465029
     ("" (skolem!)
      (("" (iff)
        (("" (prop)
          (("1" (use "infty_gg_injective")
            (("1" (prop)
              (("1" (inst?)
                (("1" (expand "injective?") (("1" (propax) nil nil)) nil)
                 ("2" (expand "inrange?") (("2" (propax) nil nil)) nil))
                nil))
              nil))
            nil)
           ("2" (use "injective_lcard" ("A" "fullset[nat]" "B" "S!1"))
            (("2" (prop)
              (("1" (hide -2)
                (("1" (use "nat_not_finite")
                  (("1" (expand "lcard")
                    (("1" (assert)
                      (("1" (lift-if)
                        (("1" (assert)
                          (("1" (expand "<=") (("1" (propax) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (hide 2)
                (("2" (skolem!)
                  (("2" (inst?)
                    (("1" (expand "injective?")
                      (("1" (skosimp)
                        (("1" (inst?) (("1" (assert) nil nil)) nil))
                        nil))
                      nil)
                     ("2" (skosimp)
                      (("2" (expand "fullset") (("2" (propax) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((injective_lcard formula-decl nil lcard_th2 nil)
      (set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil)
      (lcard const-decl "lnat" lcard_def nil)
      (<= const-decl "bool" lnat_th nil)
      (nat_not_finite formula-decl nil lnat_th nil)
      (infty_gg_injective formula-decl nil lcard_th3 nil)
      (pred type-eq-decl nil defined_types nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (T formal-type-decl nil lcard_th3 nil)
      (epsilon const-decl "T" epsilons nil)
      (gg def-decl "T" lcard_th3 nil)
      (S!1 skolem-const-decl "pred[T]" lcard_th3 nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (>= const-decl "bool" reals nil)
      (int nonempty-type-eq-decl nil integers nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields
       nil)
      (number nonempty-type-decl nil numbers nil)
      (injective? const-decl "bool" functions nil)
      (inrange? const-decl "bool" lcard_th3 nil))
     395 270 nil nil)))
  
  
  --------------000106010303050106070903--

How-To-Repeat: 

Fix: 
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools