Gedichte Musik Bilder Quellcodebibliothek Diashow Normaldarstellung
Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/output/   (Beweissystem des Inria Version 9.1.0©)  Datei vom 15.8.2025 mit Größe 2 kB image not shown  

SSL Naming.out   Interaktion und
Portierbarkeitunbekannt

 
rahmenlose Ansicht.out DruckansichtUnknown {[0] [0] [0]}Entwicklung

1 goal
  
  x3 : nat
  ============================
  forall x x1 x4 x0 : nat,
  (forall x2 x5 : nat, x2 + x1 = x4 + x5) -> x + x1 = x4 + x0
1 goal
  
  x3, x, x1, x4, x0 : nat
  H : forall x x3 : nat, x + x1 = x4 + x3
  ============================
  x + x1 = x4 + x0
1 goal
  
  x3 : nat
  ============================
  forall x x1 x4 x0 : nat,
  (forall x2 x5 : nat, x2 + x1 = x4 + x5 -> foo (S x2 + x1)) ->
  x + x1 = x4 + x0 -> foo (S x)
1 goal
  
  x3 : nat
  ============================
  forall x x1 x4 x0 : nat,
  (forall x2 x5 : nat,
   x2 + x1 = x4 + x5 ->
   forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) ->
  x + x1 = x4 + x0 ->
  forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
1 goal
  
  x3, x, x1, x4, x0 : nat
  ============================
  (forall x2 x5 : nat,
   x2 + x1 = x4 + x5 ->
   forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) ->
  x + x1 = x4 + x0 ->
  forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
1 goal
  
  x3, x, x1, x4, x0 : nat
  H :
    forall x x3 : nat,
    x + x1 = x4 + x3 ->
    forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (S x + x1)
  H0 : x + x1 = x4 + x0
  ============================
  forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
1 goal
  
  x3, x, x1, x4, x0 : nat
  H :
    forall x x3 : nat,
    x + x1 = x4 + x3 ->
    forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (Datatypes.S x + x1)
  H0 : x + x1 = x4 + x0
  x5, x6, x7, S : nat
  ============================
  x5 + S = x6 + x7 + Datatypes.S x
1 goal
  
  x3, a : nat
  H : a = 0 -> forall a : nat, a = 0
  ============================
  a = 0
File "./output/Naming.v", line 101, characters 47-48:
Warning: Ignoring implicit binder declaration in unexpected position.
[unexpected-implicit-declaration,syntax,default]
File "./output/Naming.v", line 105, characters 36-37:
Warning: Ignoring implicit binder declaration in unexpected position.
[unexpected-implicit-declaration,syntax,default]
File "./output/Naming.v", line 106, characters 34-35:
Warning: Ignoring implicit binder declaration in unexpected position.
[unexpected-implicit-declaration,syntax,default]
File "./output/Naming.v", line 112, characters 22-23:
Warning: Ignoring implicit binder declaration in unexpected position.
[unexpected-implicit-declaration,syntax,default]
File "./output/Naming.v", line 112, characters 30-31:
Warning: Ignoring implicit binder declaration in unexpected position.
[unexpected-implicit-declaration,syntax,default]

[ Verzeichnis aufwärts0.70unsichere Verbindung  ]