2015-07-08 01:01:57 +00:00
|
|
|
|
693.lean:10:2: proof state
|
|
|
|
|
|
c : ℕ,
|
|
|
|
|
|
h : c = 1
|
2015-10-13 23:28:11 +00:00
|
|
|
|
⊢ foo 1 c 0 = foo 1 1 0
|
2015-07-08 01:01:57 +00:00
|
|
|
|
693.lean:18:2: proof state
|
|
|
|
|
|
b c : ℕ,
|
|
|
|
|
|
h : c = 1
|
|
|
|
|
|
⊢ foo 1 c b = foo 1 1 b
|
|
|
|
|
|
693.lean:26:2: proof state
|
|
|
|
|
|
b c : ℕ,
|
|
|
|
|
|
h : c = 1
|
|
|
|
|
|
⊢ foo b c 0 = foo b 1 0
|
|
|
|
|
|
693.lean:34:2: proof state
|
|
|
|
|
|
b c : ℕ,
|
|
|
|
|
|
h : c = 1
|
2015-10-13 23:28:11 +00:00
|
|
|
|
⊢ foo 1 c 1 = foo c 1 1
|
